Proof of Theorem fvmptnn04ifb
Step | Hyp | Ref
| Expression |
1 | | fvmptnn04if.g |
. 2
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) |
2 | | fvmptnn04if.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ ℕ) |
3 | 2 | 3ad2ant1 1075 |
. 2
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → 𝑆 ∈ ℕ) |
4 | | fvmptnn04if.n |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | 4 | 3ad2ant1 1075 |
. 2
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → 𝑁 ∈
ℕ0) |
6 | | simp3 1056 |
. 2
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) |
7 | | nn0re 11178 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
8 | | nn0ge0 11195 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
9 | 7, 8 | jca 553 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℝ
∧ 0 ≤ 𝑁)) |
10 | | ne0gt0 10021 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 0 ≤
𝑁) → (𝑁 ≠ 0 ↔ 0 < 𝑁)) |
11 | 4, 9, 10 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ≠ 0 ↔ 0 < 𝑁)) |
12 | 11 | biimprcd 239 |
. . . . . . 7
⊢ (0 <
𝑁 → (𝜑 → 𝑁 ≠ 0)) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ ((0 <
𝑁 ∧ 𝑁 < 𝑆) → (𝜑 → 𝑁 ≠ 0)) |
14 | 13 | impcom 445 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆)) → 𝑁 ≠ 0) |
15 | 14 | 3adant3 1074 |
. . . 4
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → 𝑁 ≠ 0) |
16 | | df-ne 2782 |
. . . . . 6
⊢ (𝑁 ≠ 0 ↔ ¬ 𝑁 = 0) |
17 | 16 | biimpi 205 |
. . . . 5
⊢ (𝑁 ≠ 0 → ¬ 𝑁 = 0) |
18 | 17 | pm2.21d 117 |
. . . 4
⊢ (𝑁 ≠ 0 → (𝑁 = 0 → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐴)) |
19 | 15, 18 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → (𝑁 = 0 → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐴)) |
20 | 19 | imp 444 |
. 2
⊢ (((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) ∧ 𝑁 = 0) → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐴) |
21 | | eqidd 2611 |
. 2
⊢ (((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆) → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐵) |
22 | 4, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
23 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 < 𝑆) → 𝑁 ∈ ℝ) |
24 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 < 𝑆) → 𝑁 < 𝑆) |
25 | 23, 24 | ltned 10052 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 < 𝑆) → 𝑁 ≠ 𝑆) |
26 | 25 | neneqd 2787 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 < 𝑆) → ¬ 𝑁 = 𝑆) |
27 | 26 | adantrl 748 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆)) → ¬ 𝑁 = 𝑆) |
28 | 27 | 3adant3 1074 |
. . . 4
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → ¬ 𝑁 = 𝑆) |
29 | 28 | pm2.21d 117 |
. . 3
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → (𝑁 = 𝑆 → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐶)) |
30 | 29 | imp 444 |
. 2
⊢ (((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) ∧ 𝑁 = 𝑆) → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐶) |
31 | 2 | nnred 10912 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℝ) |
32 | | ltnsym 10014 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑁 < 𝑆 → ¬ 𝑆 < 𝑁)) |
33 | 22, 31, 32 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 < 𝑆 → ¬ 𝑆 < 𝑁)) |
34 | 33 | com12 32 |
. . . . . . 7
⊢ (𝑁 < 𝑆 → (𝜑 → ¬ 𝑆 < 𝑁)) |
35 | 34 | adantl 481 |
. . . . . 6
⊢ ((0 <
𝑁 ∧ 𝑁 < 𝑆) → (𝜑 → ¬ 𝑆 < 𝑁)) |
36 | 35 | impcom 445 |
. . . . 5
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆)) → ¬ 𝑆 < 𝑁) |
37 | 36 | 3adant3 1074 |
. . . 4
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → ¬ 𝑆 < 𝑁) |
38 | 37 | pm2.21d 117 |
. . 3
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → (𝑆 < 𝑁 → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐷)) |
39 | 38 | imp 444 |
. 2
⊢ (((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) ∧ 𝑆 < 𝑁) → ⦋𝑁 / 𝑛⦌𝐵 = ⦋𝑁 / 𝑛⦌𝐷) |
40 | 1, 3, 5, 6, 20, 21, 30, 39 | fvmptnn04if 20473 |
1
⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐵) |