Proof of Theorem fz0to4untppr
| Step | Hyp | Ref
 | Expression | 
| 1 |   | df-3 9050 | 
. . . . 5
⊢ 3 = (2 +
1) | 
| 2 |   | 2cn 9061 | 
. . . . . . . 8
⊢ 2 ∈
ℂ | 
| 3 | 2 | addlidi 8169 | 
. . . . . . 7
⊢ (0 + 2) =
2 | 
| 4 | 3 | eqcomi 2200 | 
. . . . . 6
⊢ 2 = (0 +
2) | 
| 5 | 4 | oveq1i 5932 | 
. . . . 5
⊢ (2 + 1) =
((0 + 2) + 1) | 
| 6 | 1, 5 | eqtri 2217 | 
. . . 4
⊢ 3 = ((0 +
2) + 1) | 
| 7 |   | 3z 9355 | 
. . . . 5
⊢ 3 ∈
ℤ | 
| 8 |   | 0re 8026 | 
. . . . . 6
⊢ 0 ∈
ℝ | 
| 9 |   | 3re 9064 | 
. . . . . 6
⊢ 3 ∈
ℝ | 
| 10 |   | 3pos 9084 | 
. . . . . 6
⊢ 0 <
3 | 
| 11 | 8, 9, 10 | ltleii 8129 | 
. . . . 5
⊢ 0 ≤
3 | 
| 12 |   | 0z 9337 | 
. . . . . 6
⊢ 0 ∈
ℤ | 
| 13 | 12 | eluz1i 9608 | 
. . . . 5
⊢ (3 ∈
(ℤ≥‘0) ↔ (3 ∈ ℤ ∧ 0 ≤
3)) | 
| 14 | 7, 11, 13 | mpbir2an 944 | 
. . . 4
⊢ 3 ∈
(ℤ≥‘0) | 
| 15 | 6, 14 | eqeltrri 2270 | 
. . 3
⊢ ((0 + 2)
+ 1) ∈ (ℤ≥‘0) | 
| 16 |   | 4z 9356 | 
. . . . 5
⊢ 4 ∈
ℤ | 
| 17 |   | 2re 9060 | 
. . . . . 6
⊢ 2 ∈
ℝ | 
| 18 |   | 4re 9067 | 
. . . . . 6
⊢ 4 ∈
ℝ | 
| 19 |   | 2lt4 9164 | 
. . . . . 6
⊢ 2 <
4 | 
| 20 | 17, 18, 19 | ltleii 8129 | 
. . . . 5
⊢ 2 ≤
4 | 
| 21 |   | 2z 9354 | 
. . . . . 6
⊢ 2 ∈
ℤ | 
| 22 | 21 | eluz1i 9608 | 
. . . . 5
⊢ (4 ∈
(ℤ≥‘2) ↔ (4 ∈ ℤ ∧ 2 ≤
4)) | 
| 23 | 16, 20, 22 | mpbir2an 944 | 
. . . 4
⊢ 4 ∈
(ℤ≥‘2) | 
| 24 | 4 | fveq2i 5561 | 
. . . 4
⊢
(ℤ≥‘2) = (ℤ≥‘(0 +
2)) | 
| 25 | 23, 24 | eleqtri 2271 | 
. . 3
⊢ 4 ∈
(ℤ≥‘(0 + 2)) | 
| 26 |   | fzsplit2 10125 | 
. . 3
⊢ ((((0 +
2) + 1) ∈ (ℤ≥‘0) ∧ 4 ∈
(ℤ≥‘(0 + 2))) → (0...4) = ((0...(0 + 2)) ∪
(((0 + 2) + 1)...4))) | 
| 27 | 15, 25, 26 | mp2an 426 | 
. 2
⊢ (0...4) =
((0...(0 + 2)) ∪ (((0 + 2) + 1)...4)) | 
| 28 |   | fztp 10153 | 
. . . . 5
⊢ (0 ∈
ℤ → (0...(0 + 2)) = {0, (0 + 1), (0 + 2)}) | 
| 29 | 12, 28 | ax-mp 5 | 
. . . 4
⊢ (0...(0 +
2)) = {0, (0 + 1), (0 + 2)} | 
| 30 |   | ax-1cn 7972 | 
. . . . 5
⊢ 1 ∈
ℂ | 
| 31 |   | eqidd 2197 | 
. . . . . 6
⊢ (1 ∈
ℂ → 0 = 0) | 
| 32 |   | addlid 8165 | 
. . . . . 6
⊢ (1 ∈
ℂ → (0 + 1) = 1) | 
| 33 | 3 | a1i 9 | 
. . . . . 6
⊢ (1 ∈
ℂ → (0 + 2) = 2) | 
| 34 | 31, 32, 33 | tpeq123d 3714 | 
. . . . 5
⊢ (1 ∈
ℂ → {0, (0 + 1), (0 + 2)} = {0, 1, 2}) | 
| 35 | 30, 34 | ax-mp 5 | 
. . . 4
⊢ {0, (0 +
1), (0 + 2)} = {0, 1, 2} | 
| 36 | 29, 35 | eqtri 2217 | 
. . 3
⊢ (0...(0 +
2)) = {0, 1, 2} | 
| 37 | 3 | a1i 9 | 
. . . . . . . 8
⊢ (3 ∈
ℤ → (0 + 2) = 2) | 
| 38 | 37 | oveq1d 5937 | 
. . . . . . 7
⊢ (3 ∈
ℤ → ((0 + 2) + 1) = (2 + 1)) | 
| 39 | 38, 1 | eqtr4di 2247 | 
. . . . . 6
⊢ (3 ∈
ℤ → ((0 + 2) + 1) = 3) | 
| 40 | 39 | oveq1d 5937 | 
. . . . 5
⊢ (3 ∈
ℤ → (((0 + 2) + 1)...4) = (3...4)) | 
| 41 |   | eqid 2196 | 
. . . . . . . . . 10
⊢ 3 =
3 | 
| 42 |   | df-4 9051 | 
. . . . . . . . . 10
⊢ 4 = (3 +
1) | 
| 43 | 41, 42 | pm3.2i 272 | 
. . . . . . . . 9
⊢ (3 = 3
∧ 4 = (3 + 1)) | 
| 44 | 43 | a1i 9 | 
. . . . . . . 8
⊢ (3 ∈
ℤ → (3 = 3 ∧ 4 = (3 + 1))) | 
| 45 |   | 3lt4 9163 | 
. . . . . . . . . . 11
⊢ 3 <
4 | 
| 46 | 9, 18, 45 | ltleii 8129 | 
. . . . . . . . . 10
⊢ 3 ≤
4 | 
| 47 | 7 | eluz1i 9608 | 
. . . . . . . . . 10
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) | 
| 48 | 16, 46, 47 | mpbir2an 944 | 
. . . . . . . . 9
⊢ 4 ∈
(ℤ≥‘3) | 
| 49 |   | fzopth 10136 | 
. . . . . . . . 9
⊢ (4 ∈
(ℤ≥‘3) → ((3...4) = (3...(3 + 1)) ↔ (3 = 3
∧ 4 = (3 + 1)))) | 
| 50 | 48, 49 | ax-mp 5 | 
. . . . . . . 8
⊢ ((3...4)
= (3...(3 + 1)) ↔ (3 = 3 ∧ 4 = (3 + 1))) | 
| 51 | 44, 50 | sylibr 134 | 
. . . . . . 7
⊢ (3 ∈
ℤ → (3...4) = (3...(3 + 1))) | 
| 52 |   | fzpr 10152 | 
. . . . . . 7
⊢ (3 ∈
ℤ → (3...(3 + 1)) = {3, (3 + 1)}) | 
| 53 | 51, 52 | eqtrd 2229 | 
. . . . . 6
⊢ (3 ∈
ℤ → (3...4) = {3, (3 + 1)}) | 
| 54 | 42 | eqcomi 2200 | 
. . . . . . 7
⊢ (3 + 1) =
4 | 
| 55 | 54 | preq2i 3703 | 
. . . . . 6
⊢ {3, (3 +
1)} = {3, 4} | 
| 56 | 53, 55 | eqtrdi 2245 | 
. . . . 5
⊢ (3 ∈
ℤ → (3...4) = {3, 4}) | 
| 57 | 40, 56 | eqtrd 2229 | 
. . . 4
⊢ (3 ∈
ℤ → (((0 + 2) + 1)...4) = {3, 4}) | 
| 58 | 7, 57 | ax-mp 5 | 
. . 3
⊢ (((0 + 2)
+ 1)...4) = {3, 4} | 
| 59 | 36, 58 | uneq12i 3315 | 
. 2
⊢ ((0...(0
+ 2)) ∪ (((0 + 2) + 1)...4)) = ({0, 1, 2} ∪ {3, 4}) | 
| 60 | 27, 59 | eqtri 2217 | 
1
⊢ (0...4) =
({0, 1, 2} ∪ {3, 4}) |