Proof of Theorem axlowdimlem13
Step | Hyp | Ref
| Expression |
1 | | 2ne0 11486 |
. . . . . . . . 9
⊢ 2 ≠
0 |
2 | 1 | neii 2971 |
. . . . . . . 8
⊢ ¬ 2
= 0 |
3 | | eqcom 2785 |
. . . . . . . . 9
⊢ (2 = 0
↔ 0 = 2) |
4 | | 1pneg1e0 11501 |
. . . . . . . . . . 11
⊢ (1 + -1)
= 0 |
5 | 4 | eqcomi 2787 |
. . . . . . . . . 10
⊢ 0 = (1 +
-1) |
6 | | df-2 11438 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
7 | 5, 6 | eqeq12i 2792 |
. . . . . . . . 9
⊢ (0 = 2
↔ (1 + -1) = (1 + 1)) |
8 | | ax-1cn 10330 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
9 | | neg1cn 11496 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
10 | 8, 9, 8 | addcani 10569 |
. . . . . . . . 9
⊢ ((1 + -1)
= (1 + 1) ↔ -1 = 1) |
11 | 3, 7, 10 | 3bitri 289 |
. . . . . . . 8
⊢ (2 = 0
↔ -1 = 1) |
12 | 2, 11 | mtbi 314 |
. . . . . . 7
⊢ ¬ -1
= 1 |
13 | 12 | intnanr 483 |
. . . . . 6
⊢ ¬
(-1 = 1 ∧ 0 = 0) |
14 | | ax-1ne0 10341 |
. . . . . . . . 9
⊢ 1 ≠
0 |
15 | 14 | neii 2971 |
. . . . . . . 8
⊢ ¬ 1
= 0 |
16 | | negeq0 10677 |
. . . . . . . . 9
⊢ (1 ∈
ℂ → (1 = 0 ↔ -1 = 0)) |
17 | 8, 16 | ax-mp 5 |
. . . . . . . 8
⊢ (1 = 0
↔ -1 = 0) |
18 | 15, 17 | mtbi 314 |
. . . . . . 7
⊢ ¬ -1
= 0 |
19 | 18 | intnanr 483 |
. . . . . 6
⊢ ¬
(-1 = 0 ∧ 0 = 1) |
20 | 13, 19 | pm3.2ni 867 |
. . . . 5
⊢ ¬
((-1 = 1 ∧ 0 = 0) ∨ (-1 = 0 ∧ 0 = 1)) |
21 | | negex 10620 |
. . . . . 6
⊢ -1 ∈
V |
22 | | c0ex 10370 |
. . . . . 6
⊢ 0 ∈
V |
23 | | 1ex 10372 |
. . . . . 6
⊢ 1 ∈
V |
24 | 21, 22, 23, 22 | preq12b 4610 |
. . . . 5
⊢ ({-1, 0}
= {1, 0} ↔ ((-1 = 1 ∧ 0 = 0) ∨ (-1 = 0 ∧ 0 =
1))) |
25 | 20, 24 | mtbir 315 |
. . . 4
⊢ ¬
{-1, 0} = {1, 0} |
26 | | 3ex 11458 |
. . . . . . . . 9
⊢ 3 ∈
V |
27 | 26 | rnsnop 5871 |
. . . . . . . 8
⊢ ran
{〈3, -1〉} = {-1} |
28 | 27 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ran {〈3, -1〉}
= {-1}) |
29 | | elnnuz 12030 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈
(ℤ≥‘1)) |
30 | | eluzfz1 12665 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑁)) |
31 | 29, 30 | sylbi 209 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 1 ∈
(1...𝑁)) |
32 | | df-3 11439 |
. . . . . . . . . . . . . . . 16
⊢ 3 = (2 +
1) |
33 | | 1e0p1 11888 |
. . . . . . . . . . . . . . . 16
⊢ 1 = (0 +
1) |
34 | 32, 33 | eqeq12i 2792 |
. . . . . . . . . . . . . . 15
⊢ (3 = 1
↔ (2 + 1) = (0 + 1)) |
35 | | 2cn 11450 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℂ |
36 | | 0cn 10368 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℂ |
37 | 35, 36, 8 | addcan2i 10570 |
. . . . . . . . . . . . . . 15
⊢ ((2 + 1)
= (0 + 1) ↔ 2 = 0) |
38 | 34, 37 | bitri 267 |
. . . . . . . . . . . . . 14
⊢ (3 = 1
↔ 2 = 0) |
39 | 38 | necon3bii 3021 |
. . . . . . . . . . . . 13
⊢ (3 ≠ 1
↔ 2 ≠ 0) |
40 | 1, 39 | mpbir 223 |
. . . . . . . . . . . 12
⊢ 3 ≠
1 |
41 | 40 | necomi 3023 |
. . . . . . . . . . 11
⊢ 1 ≠
3 |
42 | 31, 41 | jctir 516 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → (1 ∈
(1...𝑁) ∧ 1 ≠
3)) |
43 | | eldifsn 4550 |
. . . . . . . . . 10
⊢ (1 ∈
((1...𝑁) ∖ {3})
↔ (1 ∈ (1...𝑁)
∧ 1 ≠ 3)) |
44 | 42, 43 | sylibr 226 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
((1...𝑁) ∖
{3})) |
45 | 44 | adantr 474 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 1 ∈ ((1...𝑁) ∖ {3})) |
46 | | ne0i 4149 |
. . . . . . . 8
⊢ (1 ∈
((1...𝑁) ∖ {3})
→ ((1...𝑁) ∖
{3}) ≠ ∅) |
47 | | rnxp 5818 |
. . . . . . . 8
⊢
(((1...𝑁) ∖
{3}) ≠ ∅ → ran (((1...𝑁) ∖ {3}) × {0}) =
{0}) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ran (((1...𝑁) ∖ {3}) × {0}) =
{0}) |
49 | 28, 48 | uneq12d 3991 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (ran {〈3,
-1〉} ∪ ran (((1...𝑁) ∖ {3}) × {0})) = ({-1} ∪
{0})) |
50 | | rnun 5795 |
. . . . . 6
⊢ ran
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) = (ran
{〈3, -1〉} ∪ ran (((1...𝑁) ∖ {3}) ×
{0})) |
51 | | df-pr 4401 |
. . . . . 6
⊢ {-1, 0} =
({-1} ∪ {0}) |
52 | 49, 50, 51 | 3eqtr4g 2839 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ran ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) = {-1, 0}) |
53 | | ovex 6954 |
. . . . . . . . 9
⊢ (𝐼 + 1) ∈ V |
54 | 53 | rnsnop 5871 |
. . . . . . . 8
⊢ ran
{〈(𝐼 + 1), 1〉} =
{1} |
55 | 54 | a1i 11 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ran {〈(𝐼 + 1), 1〉} =
{1}) |
56 | | nnz 11751 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
57 | | fzssp1 12701 |
. . . . . . . . . . . 12
⊢
(1...(𝑁 − 1))
⊆ (1...((𝑁 − 1)
+ 1)) |
58 | | zcn 11733 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
59 | | npcan1 10800 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) |
60 | 59 | oveq2d 6938 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ →
(1...((𝑁 − 1) + 1)) =
(1...𝑁)) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ →
(1...((𝑁 − 1) + 1)) =
(1...𝑁)) |
62 | 57, 61 | syl5sseq 3872 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ →
(1...(𝑁 − 1)) ⊆
(1...𝑁)) |
63 | 56, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(1...(𝑁 − 1)) ⊆
(1...𝑁)) |
64 | 63 | sselda 3821 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝐼 ∈ (1...𝑁)) |
65 | | elfzelz 12659 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ (1...(𝑁 − 1)) → 𝐼 ∈ ℤ) |
66 | 65 | zred 11834 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (1...(𝑁 − 1)) → 𝐼 ∈ ℝ) |
67 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ ℝ → 𝐼 ∈
ℝ) |
68 | | ltp1 11215 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ ℝ → 𝐼 < (𝐼 + 1)) |
69 | 67, 68 | ltned 10512 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ ℝ → 𝐼 ≠ (𝐼 + 1)) |
70 | 66, 69 | syl 17 |
. . . . . . . . . 10
⊢ (𝐼 ∈ (1...(𝑁 − 1)) → 𝐼 ≠ (𝐼 + 1)) |
71 | 70 | adantl 475 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝐼 ≠ (𝐼 + 1)) |
72 | | eldifsn 4550 |
. . . . . . . . 9
⊢ (𝐼 ∈ ((1...𝑁) ∖ {(𝐼 + 1)}) ↔ (𝐼 ∈ (1...𝑁) ∧ 𝐼 ≠ (𝐼 + 1))) |
73 | 64, 71, 72 | sylanbrc 578 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝐼 ∈ ((1...𝑁) ∖ {(𝐼 + 1)})) |
74 | | ne0i 4149 |
. . . . . . . 8
⊢ (𝐼 ∈ ((1...𝑁) ∖ {(𝐼 + 1)}) → ((1...𝑁) ∖ {(𝐼 + 1)}) ≠ ∅) |
75 | | rnxp 5818 |
. . . . . . . 8
⊢
(((1...𝑁) ∖
{(𝐼 + 1)}) ≠ ∅
→ ran (((1...𝑁)
∖ {(𝐼 + 1)}) ×
{0}) = {0}) |
76 | 73, 74, 75 | 3syl 18 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ran (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}) = {0}) |
77 | 55, 76 | uneq12d 3991 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (ran {〈(𝐼 + 1), 1〉} ∪ ran
(((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) = ({1}
∪ {0})) |
78 | | rnun 5795 |
. . . . . 6
⊢ ran
({〈(𝐼 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝐼 + 1)}) × {0})) =
(ran {〈(𝐼 + 1),
1〉} ∪ ran (((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) |
79 | | df-pr 4401 |
. . . . . 6
⊢ {1, 0} =
({1} ∪ {0}) |
80 | 77, 78, 79 | 3eqtr4g 2839 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ran ({〈(𝐼 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) = {1,
0}) |
81 | 52, 80 | eqeq12d 2793 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → (ran ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) = ran ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) ↔ {-1, 0} = {1,
0})) |
82 | 25, 81 | mtbiri 319 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ¬ ran ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) = ran ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))) |
83 | | rneq 5596 |
. . 3
⊢
(({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) =
({〈(𝐼 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝐼 + 1)}) × {0}))
→ ran ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) = ran
({〈(𝐼 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝐼 + 1)}) ×
{0}))) |
84 | 82, 83 | nsyl 138 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → ¬ ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) = ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))) |
85 | | axlowdimlem13.1 |
. . . 4
⊢ 𝑃 = ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) |
86 | | axlowdimlem13.2 |
. . . 4
⊢ 𝑄 = ({〈(𝐼 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0})) |
87 | 85, 86 | eqeq12i 2792 |
. . 3
⊢ (𝑃 = 𝑄 ↔ ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) = ({〈(𝐼
+ 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))) |
88 | 87 | necon3abii 3015 |
. 2
⊢ (𝑃 ≠ 𝑄 ↔ ¬ ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) = ({〈(𝐼
+ 1), 1〉} ∪ (((1...𝑁) ∖ {(𝐼 + 1)}) × {0}))) |
89 | 84, 88 | sylibr 226 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (1...(𝑁 − 1))) → 𝑃 ≠ 𝑄) |