Proof of Theorem fz0to4untppr
Step | Hyp | Ref
| Expression |
1 | | df-3 11894 |
. . . . 5
⊢ 3 = (2 +
1) |
2 | | 2cn 11905 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
3 | 2 | addid2i 11020 |
. . . . . . 7
⊢ (0 + 2) =
2 |
4 | 3 | eqcomi 2746 |
. . . . . 6
⊢ 2 = (0 +
2) |
5 | 4 | oveq1i 7223 |
. . . . 5
⊢ (2 + 1) =
((0 + 2) + 1) |
6 | 1, 5 | eqtri 2765 |
. . . 4
⊢ 3 = ((0 +
2) + 1) |
7 | | 3z 12210 |
. . . . 5
⊢ 3 ∈
ℤ |
8 | | 0re 10835 |
. . . . . 6
⊢ 0 ∈
ℝ |
9 | | 3re 11910 |
. . . . . 6
⊢ 3 ∈
ℝ |
10 | | 3pos 11935 |
. . . . . 6
⊢ 0 <
3 |
11 | 8, 9, 10 | ltleii 10955 |
. . . . 5
⊢ 0 ≤
3 |
12 | | 0z 12187 |
. . . . . 6
⊢ 0 ∈
ℤ |
13 | 12 | eluz1i 12446 |
. . . . 5
⊢ (3 ∈
(ℤ≥‘0) ↔ (3 ∈ ℤ ∧ 0 ≤
3)) |
14 | 7, 11, 13 | mpbir2an 711 |
. . . 4
⊢ 3 ∈
(ℤ≥‘0) |
15 | 6, 14 | eqeltrri 2835 |
. . 3
⊢ ((0 + 2)
+ 1) ∈ (ℤ≥‘0) |
16 | | 4z 12211 |
. . . . 5
⊢ 4 ∈
ℤ |
17 | | 2re 11904 |
. . . . . 6
⊢ 2 ∈
ℝ |
18 | | 4re 11914 |
. . . . . 6
⊢ 4 ∈
ℝ |
19 | | 2lt4 12005 |
. . . . . 6
⊢ 2 <
4 |
20 | 17, 18, 19 | ltleii 10955 |
. . . . 5
⊢ 2 ≤
4 |
21 | | 2z 12209 |
. . . . . 6
⊢ 2 ∈
ℤ |
22 | 21 | eluz1i 12446 |
. . . . 5
⊢ (4 ∈
(ℤ≥‘2) ↔ (4 ∈ ℤ ∧ 2 ≤
4)) |
23 | 16, 20, 22 | mpbir2an 711 |
. . . 4
⊢ 4 ∈
(ℤ≥‘2) |
24 | 4 | fveq2i 6720 |
. . . 4
⊢
(ℤ≥‘2) = (ℤ≥‘(0 +
2)) |
25 | 23, 24 | eleqtri 2836 |
. . 3
⊢ 4 ∈
(ℤ≥‘(0 + 2)) |
26 | | fzsplit2 13137 |
. . 3
⊢ ((((0 +
2) + 1) ∈ (ℤ≥‘0) ∧ 4 ∈
(ℤ≥‘(0 + 2))) → (0...4) = ((0...(0 + 2)) ∪
(((0 + 2) + 1)...4))) |
27 | 15, 25, 26 | mp2an 692 |
. 2
⊢ (0...4) =
((0...(0 + 2)) ∪ (((0 + 2) + 1)...4)) |
28 | | fztp 13168 |
. . . . 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 10787 |
. . . . 5
⊢ 1 ∈
ℂ |
31 | | eqidd 2738 |
. . . . . 6
⊢ (1 ∈
ℂ → 0 = 0) |
32 | | addid2 11015 |
. . . . . 6
⊢ (1 ∈
ℂ → (0 + 1) = 1) |
33 | 3 | a1i 11 |
. . . . . 6
⊢ (1 ∈
ℂ → (0 + 2) = 2) |
34 | 31, 32, 33 | tpeq123d 4664 |
. . . . 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 2765 |
. . 3
⊢ (0...(0 +
2)) = {0, 1, 2} |
37 | 3 | a1i 11 |
. . . . . . . 8
⊢ (3 ∈
ℤ → (0 + 2) = 2) |
38 | 37 | oveq1d 7228 |
. . . . . . 7
⊢ (3 ∈
ℤ → ((0 + 2) + 1) = (2 + 1)) |
39 | 38, 1 | eqtr4di 2796 |
. . . . . 6
⊢ (3 ∈
ℤ → ((0 + 2) + 1) = 3) |
40 | 39 | oveq1d 7228 |
. . . . 5
⊢ (3 ∈
ℤ → (((0 + 2) + 1)...4) = (3...4)) |
41 | | eqid 2737 |
. . . . . . . . . 10
⊢ 3 =
3 |
42 | | df-4 11895 |
. . . . . . . . . 10
⊢ 4 = (3 +
1) |
43 | 41, 42 | pm3.2i 474 |
. . . . . . . . 9
⊢ (3 = 3
∧ 4 = (3 + 1)) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ (3 ∈
ℤ → (3 = 3 ∧ 4 = (3 + 1))) |
45 | | 3lt4 12004 |
. . . . . . . . . . 11
⊢ 3 <
4 |
46 | 9, 18, 45 | ltleii 10955 |
. . . . . . . . . 10
⊢ 3 ≤
4 |
47 | 7 | eluz1i 12446 |
. . . . . . . . . 10
⊢ (4 ∈
(ℤ≥‘3) ↔ (4 ∈ ℤ ∧ 3 ≤
4)) |
48 | 16, 46, 47 | mpbir2an 711 |
. . . . . . . . 9
⊢ 4 ∈
(ℤ≥‘3) |
49 | | fzopth 13149 |
. . . . . . . . 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 237 |
. . . . . . 7
⊢ (3 ∈
ℤ → (3...4) = (3...(3 + 1))) |
52 | | fzpr 13167 |
. . . . . . 7
⊢ (3 ∈
ℤ → (3...(3 + 1)) = {3, (3 + 1)}) |
53 | 51, 52 | eqtrd 2777 |
. . . . . 6
⊢ (3 ∈
ℤ → (3...4) = {3, (3 + 1)}) |
54 | 42 | eqcomi 2746 |
. . . . . . 7
⊢ (3 + 1) =
4 |
55 | 54 | preq2i 4653 |
. . . . . 6
⊢ {3, (3 +
1)} = {3, 4} |
56 | 53, 55 | eqtrdi 2794 |
. . . . 5
⊢ (3 ∈
ℤ → (3...4) = {3, 4}) |
57 | 40, 56 | eqtrd 2777 |
. . . 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 4075 |
. 2
⊢ ((0...(0
+ 2)) ∪ (((0 + 2) + 1)...4)) = ({0, 1, 2} ∪ {3, 4}) |
60 | 27, 59 | eqtri 2765 |
1
⊢ (0...4) =
({0, 1, 2} ∪ {3, 4}) |