| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1zzd 12650 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ ℤ) | 
| 2 |  | eluzelz 12889 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℤ) | 
| 3 |  | 2nn 12340 | . . . . . . . . . . 11
⊢ 2 ∈
ℕ | 
| 4 |  | uznnssnn 12938 | . . . . . . . . . . 11
⊢ (2 ∈
ℕ → (ℤ≥‘2) ⊆
ℕ) | 
| 5 | 3, 4 | ax-mp 5 | . . . . . . . . . 10
⊢
(ℤ≥‘2) ⊆ ℕ | 
| 6 |  | nnuz 12922 | . . . . . . . . . 10
⊢ ℕ =
(ℤ≥‘1) | 
| 7 | 5, 6 | sseqtri 4031 | . . . . . . . . 9
⊢
(ℤ≥‘2) ⊆
(ℤ≥‘1) | 
| 8 | 7 | sseli 3978 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈
(ℤ≥‘1)) | 
| 9 |  | eluzle 12892 | . . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘1) → 1 ≤ 𝑁) | 
| 10 | 8, 9 | syl 17 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ≤ 𝑁) | 
| 11 |  | 1re 11262 | . . . . . . . 8
⊢ 1 ∈
ℝ | 
| 12 | 11 | leidi 11798 | . . . . . . 7
⊢ 1 ≤
1 | 
| 13 | 10, 12 | jctil 519 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 ≤ 1 ∧ 1 ≤ 𝑁)) | 
| 14 |  | elfz4 13558 | . . . . . 6
⊢ (((1
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ≤ 1 ∧ 1 ≤ 𝑁)) → 1 ∈ (1...𝑁)) | 
| 15 | 1, 2, 1, 13, 14 | syl31anc 1374 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 1 ∈ (1...𝑁)) | 
| 16 |  | eluzel2 12884 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ ℤ) | 
| 17 |  | eluzle 12892 | . . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ≤ 𝑁) | 
| 18 |  | 1le2 12476 | . . . . . . 7
⊢ 1 ≤
2 | 
| 19 | 17, 18 | jctil 519 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘2) → (1 ≤ 2 ∧ 2 ≤ 𝑁)) | 
| 20 |  | elfz4 13558 | . . . . . 6
⊢ (((1
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 2 ∈ ℤ) ∧ (1 ≤ 2 ∧ 2 ≤ 𝑁)) → 2 ∈ (1...𝑁)) | 
| 21 | 1, 2, 16, 19, 20 | syl31anc 1374 | . . . . 5
⊢ (𝑁 ∈
(ℤ≥‘2) → 2 ∈ (1...𝑁)) | 
| 22 |  | ax-1ne0 11225 | . . . . . . 7
⊢ 1 ≠
0 | 
| 23 |  | 1t1e1 12429 | . . . . . . . 8
⊢ (1
· 1) = 1 | 
| 24 |  | 0cn 11254 | . . . . . . . . 9
⊢ 0 ∈
ℂ | 
| 25 | 24 | mul01i 11452 | . . . . . . . 8
⊢ (0
· 0) = 0 | 
| 26 | 23, 25 | neeq12i 3006 | . . . . . . 7
⊢ ((1
· 1) ≠ (0 · 0) ↔ 1 ≠ 0) | 
| 27 | 22, 26 | mpbir 231 | . . . . . 6
⊢ (1
· 1) ≠ (0 · 0) | 
| 28 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑖 = 1 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘1)) | 
| 29 |  | 0re 11264 | . . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ | 
| 30 | 11, 29 | axlowdimlem4 28961 | . . . . . . . . . . . . . . 15
⊢ {〈1,
1〉, 〈2, 0〉}:(1...2)⟶ℝ | 
| 31 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢
({〈1, 1〉, 〈2, 0〉}:(1...2)⟶ℝ →
{〈1, 1〉, 〈2, 0〉} Fn (1...2)) | 
| 32 | 30, 31 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ {〈1,
1〉, 〈2, 0〉} Fn (1...2) | 
| 33 |  | axlowdimlem1 28958 | . . . . . . . . . . . . . . 15
⊢
((3...𝑁) ×
{0}):(3...𝑁)⟶ℝ | 
| 34 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢
(((3...𝑁) ×
{0}):(3...𝑁)⟶ℝ
→ ((3...𝑁) ×
{0}) Fn (3...𝑁)) | 
| 35 | 33, 34 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
((3...𝑁) ×
{0}) Fn (3...𝑁) | 
| 36 |  | axlowdimlem2 28959 | . . . . . . . . . . . . . . 15
⊢ ((1...2)
∩ (3...𝑁)) =
∅ | 
| 37 |  | 1z 12649 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ | 
| 38 |  | 2z 12651 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ | 
| 39 | 37, 38, 37 | 3pm3.2i 1339 | . . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ) | 
| 40 | 12, 18 | pm3.2i 470 | . . . . . . . . . . . . . . . 16
⊢ (1 ≤ 1
∧ 1 ≤ 2) | 
| 41 |  | elfz4 13558 | . . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ≤ 1
∧ 1 ≤ 2)) → 1 ∈ (1...2)) | 
| 42 | 39, 40, 41 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
(1...2) | 
| 43 | 36, 42 | pm3.2i 470 | . . . . . . . . . . . . . 14
⊢ (((1...2)
∩ (3...𝑁)) = ∅
∧ 1 ∈ (1...2)) | 
| 44 |  | fvun1 6999 | . . . . . . . . . . . . . 14
⊢
(({〈1, 1〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 1
∈ (1...2))) → (({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘1) = ({〈1, 1〉, 〈2,
0〉}‘1)) | 
| 45 | 32, 35, 43, 44 | mp3an 1462 | . . . . . . . . . . . . 13
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) = ({〈1,
1〉, 〈2, 0〉}‘1) | 
| 46 |  | 1ne2 12475 | . . . . . . . . . . . . . 14
⊢ 1 ≠
2 | 
| 47 |  | 1ex 11258 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
V | 
| 48 | 47, 47 | fvpr1 7213 | . . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 1〉, 〈2, 0〉}‘1) = 1) | 
| 49 | 46, 48 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
({〈1, 1〉, 〈2, 0〉}‘1) = 1 | 
| 50 | 45, 49 | eqtri 2764 | . . . . . . . . . . . 12
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) =
1 | 
| 51 | 28, 50 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑖 = 1 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = 1) | 
| 52 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘1)) | 
| 53 | 29, 29 | axlowdimlem4 28961 | . . . . . . . . . . . . . . 15
⊢ {〈1,
0〉, 〈2, 0〉}:(1...2)⟶ℝ | 
| 54 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢
({〈1, 0〉, 〈2, 0〉}:(1...2)⟶ℝ →
{〈1, 0〉, 〈2, 0〉} Fn (1...2)) | 
| 55 | 53, 54 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ {〈1,
0〉, 〈2, 0〉} Fn (1...2) | 
| 56 |  | fvun1 6999 | . . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 1
∈ (1...2))) → (({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘1) = ({〈1, 0〉, 〈2,
0〉}‘1)) | 
| 57 | 55, 35, 43, 56 | mp3an 1462 | . . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) = ({〈1,
0〉, 〈2, 0〉}‘1) | 
| 58 | 29 | elexi 3502 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
V | 
| 59 | 47, 58 | fvpr1 7213 | . . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 0〉}‘1) = 0) | 
| 60 | 46, 59 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 0〉}‘1) = 0 | 
| 61 | 57, 60 | eqtri 2764 | . . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘1) =
0 | 
| 62 | 52, 61 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) = 0) | 
| 63 | 51, 62 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑖 = 1 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
(1 − 0)) | 
| 64 |  | 1m0e1 12388 | . . . . . . . . . 10
⊢ (1
− 0) = 1 | 
| 65 | 63, 64 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑖 = 1 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
1) | 
| 66 | 65 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑖 = 1 → (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(1 · ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)))) | 
| 67 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) = (({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0}))‘1)) | 
| 68 | 29, 11 | axlowdimlem4 28961 | . . . . . . . . . . . . . . 15
⊢ {〈1,
0〉, 〈2, 1〉}:(1...2)⟶ℝ | 
| 69 |  | ffn 6735 | . . . . . . . . . . . . . . 15
⊢
({〈1, 0〉, 〈2, 1〉}:(1...2)⟶ℝ →
{〈1, 0〉, 〈2, 1〉} Fn (1...2)) | 
| 70 | 68, 69 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢ {〈1,
0〉, 〈2, 1〉} Fn (1...2) | 
| 71 |  | fvun1 6999 | . . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 1〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 1
∈ (1...2))) → (({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) ×
{0}))‘1) = ({〈1, 0〉, 〈2,
1〉}‘1)) | 
| 72 | 70, 35, 43, 71 | mp3an 1462 | . . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘1) = ({〈1,
0〉, 〈2, 1〉}‘1) | 
| 73 | 47, 58 | fvpr1 7213 | . . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 1〉}‘1) = 0) | 
| 74 | 46, 73 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 1〉}‘1) = 0 | 
| 75 | 72, 74 | eqtri 2764 | . . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘1) =
0 | 
| 76 | 67, 75 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑖 = 1 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) = 0) | 
| 77 | 76, 62 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑖 = 1 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
(0 − 0)) | 
| 78 |  | 0m0e0 12387 | . . . . . . . . . 10
⊢ (0
− 0) = 0 | 
| 79 | 77, 78 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑖 = 1 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)) =
0) | 
| 80 | 79 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑖 = 1 → (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· 0)) | 
| 81 | 66, 80 | neeq12d 3001 | . . . . . . 7
⊢ (𝑖 = 1 → ((((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ (1 · ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · 0))) | 
| 82 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) = (({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0}))‘2)) | 
| 83 | 37, 38, 38 | 3pm3.2i 1339 | . . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ) | 
| 84 |  | 2re 12341 | . . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ | 
| 85 | 84 | leidi 11798 | . . . . . . . . . . . . . . . . 17
⊢ 2 ≤
2 | 
| 86 | 18, 85 | pm3.2i 470 | . . . . . . . . . . . . . . . 16
⊢ (1 ≤ 2
∧ 2 ≤ 2) | 
| 87 |  | elfz4 13558 | . . . . . . . . . . . . . . . 16
⊢ (((1
∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ) ∧ (1 ≤ 2
∧ 2 ≤ 2)) → 2 ∈ (1...2)) | 
| 88 | 83, 86, 87 | mp2an 692 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
(1...2) | 
| 89 | 36, 88 | pm3.2i 470 | . . . . . . . . . . . . . 14
⊢ (((1...2)
∩ (3...𝑁)) = ∅
∧ 2 ∈ (1...2)) | 
| 90 |  | fvun1 6999 | . . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 1〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 2
∈ (1...2))) → (({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) ×
{0}))‘2) = ({〈1, 0〉, 〈2,
1〉}‘2)) | 
| 91 | 70, 35, 89, 90 | mp3an 1462 | . . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘2) = ({〈1,
0〉, 〈2, 1〉}‘2) | 
| 92 | 38 | elexi 3502 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
V | 
| 93 | 92, 47 | fvpr2 7214 | . . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 1〉}‘2) = 1) | 
| 94 | 46, 93 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 1〉}‘2) = 1 | 
| 95 | 91, 94 | eqtri 2764 | . . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘2) =
1 | 
| 96 | 82, 95 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) = 1) | 
| 97 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = (({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘2)) | 
| 98 |  | fvun1 6999 | . . . . . . . . . . . . . 14
⊢
(({〈1, 0〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 2
∈ (1...2))) → (({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘2) = ({〈1, 0〉, 〈2,
0〉}‘2)) | 
| 99 | 55, 35, 89, 98 | mp3an 1462 | . . . . . . . . . . . . 13
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) = ({〈1,
0〉, 〈2, 0〉}‘2) | 
| 100 | 92, 58 | fvpr2 7214 | . . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 0〉, 〈2, 0〉}‘2) = 0) | 
| 101 | 46, 100 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
({〈1, 0〉, 〈2, 0〉}‘2) = 0 | 
| 102 | 99, 101 | eqtri 2764 | . . . . . . . . . . . 12
⊢
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) =
0 | 
| 103 | 97, 102 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑗 = 2 → (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = 0) | 
| 104 | 96, 103 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑗 = 2 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
(1 − 0)) | 
| 105 | 104, 64 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑗 = 2 → ((({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
1) | 
| 106 | 105 | oveq2d 7448 | . . . . . . . 8
⊢ (𝑗 = 2 → (1 ·
((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(1 · 1)) | 
| 107 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑗 = 2 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = (({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘2)) | 
| 108 |  | fvun1 6999 | . . . . . . . . . . . . . 14
⊢
(({〈1, 1〉, 〈2, 0〉} Fn (1...2) ∧ ((3...𝑁) × {0}) Fn (3...𝑁) ∧ (((1...2) ∩
(3...𝑁)) = ∅ ∧ 2
∈ (1...2))) → (({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))‘2) = ({〈1, 1〉, 〈2,
0〉}‘2)) | 
| 109 | 32, 35, 89, 108 | mp3an 1462 | . . . . . . . . . . . . 13
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) = ({〈1,
1〉, 〈2, 0〉}‘2) | 
| 110 | 92, 58 | fvpr2 7214 | . . . . . . . . . . . . . 14
⊢ (1 ≠ 2
→ ({〈1, 1〉, 〈2, 0〉}‘2) = 0) | 
| 111 | 46, 110 | ax-mp 5 | . . . . . . . . . . . . 13
⊢
({〈1, 1〉, 〈2, 0〉}‘2) = 0 | 
| 112 | 109, 111 | eqtri 2764 | . . . . . . . . . . . 12
⊢
(({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘2) =
0 | 
| 113 | 107, 112 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑗 = 2 → (({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) = 0) | 
| 114 | 113, 103 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑗 = 2 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
(0 − 0)) | 
| 115 | 114, 78 | eqtrdi 2792 | . . . . . . . . 9
⊢ (𝑗 = 2 → ((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)) =
0) | 
| 116 | 115 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑗 = 2 → (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· 0) = (0 · 0)) | 
| 117 | 106, 116 | neeq12d 3001 | . . . . . . 7
⊢ (𝑗 = 2 → ((1 ·
((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· 0) ↔ (1 · 1) ≠ (0 · 0))) | 
| 118 | 81, 117 | rspc2ev 3634 | . . . . . 6
⊢ ((1
∈ (1...𝑁) ∧ 2
∈ (1...𝑁) ∧ (1
· 1) ≠ (0 · 0)) → ∃𝑖 ∈ (1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 119 | 27, 118 | mp3an3 1451 | . . . . 5
⊢ ((1
∈ (1...𝑁) ∧ 2
∈ (1...𝑁)) →
∃𝑖 ∈ (1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 120 | 15, 21, 119 | syl2anc 584 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ∃𝑖 ∈ (1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 121 |  | df-ne 2940 | . . . . . . . 8
⊢
((((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ¬ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 122 | 121 | rexbii 3093 | . . . . . . 7
⊢
(∃𝑗 ∈
(1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ∃𝑗 ∈
(1...𝑁) ¬ (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))) | 
| 123 |  | rexnal 3099 | . . . . . . 7
⊢
(∃𝑗 ∈
(1...𝑁) ¬ (((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ¬ ∀𝑗
∈ (1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))) | 
| 124 | 122, 123 | bitri 275 | . . . . . 6
⊢
(∃𝑗 ∈
(1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)))
≠ (((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))
↔ ¬ ∀𝑗
∈ (1...𝑁)(((({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))) =
(((({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗))
· ((({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))‘𝑖) − (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑖)))) | 
| 125 | 124 | rexbii 3093 | . . . . 5
⊢
(∃𝑖 ∈
(1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))) ↔ ∃𝑖 ∈ (1...𝑁) ¬ ∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 126 |  | rexnal 3099 | . . . . 5
⊢
(∃𝑖 ∈
(1...𝑁) ¬ ∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))) ↔ ¬ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 127 | 125, 126 | bitri 275 | . . . 4
⊢
(∃𝑖 ∈
(1...𝑁)∃𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) ≠ (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))) ↔ ¬ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 128 | 120, 127 | sylib 218 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)))) | 
| 129 | 29, 29 | axlowdimlem5 28962 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) | 
| 130 | 11, 29 | axlowdimlem5 28962 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) | 
| 131 | 29, 11 | axlowdimlem5 28962 | . . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) | 
| 132 |  | colinearalg 28926 | . . . 4
⊢
((({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁)) → ((({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))))) | 
| 133 | 129, 130,
131, 132 | syl3anc 1372 | . . 3
⊢ (𝑁 ∈
(ℤ≥‘2) → ((({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) ↔ ∀𝑖 ∈ (1...𝑁)∀𝑗 ∈ (1...𝑁)(((({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0}))‘𝑖) −
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗))) = (((({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))‘𝑗)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑗)) · ((({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0}))‘𝑖)
− (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))‘𝑖))))) | 
| 134 | 128, 133 | mtbird 325 | . 2
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) | 
| 135 |  | axlowdimlem6.1 | . . . 4
⊢ 𝐴 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) | 
| 136 |  | axlowdimlem6.2 | . . . . 5
⊢ 𝐵 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) | 
| 137 |  | axlowdimlem6.3 | . . . . 5
⊢ 𝐶 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) | 
| 138 | 136, 137 | opeq12i 4877 | . . . 4
⊢
〈𝐵, 𝐶〉 = 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 | 
| 139 | 135, 138 | breq12i 5151 | . . 3
⊢ (𝐴 Btwn 〈𝐵, 𝐶〉 ↔ ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) | 
| 140 | 137, 135 | opeq12i 4877 | . . . 4
⊢
〈𝐶, 𝐴〉 = 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 | 
| 141 | 136, 140 | breq12i 5151 | . . 3
⊢ (𝐵 Btwn 〈𝐶, 𝐴〉 ↔ ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) | 
| 142 | 135, 136 | opeq12i 4877 | . . . 4
⊢
〈𝐴, 𝐵〉 = 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 | 
| 143 | 137, 142 | breq12i 5151 | . . 3
⊢ (𝐶 Btwn 〈𝐴, 𝐵〉 ↔ ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) | 
| 144 | 139, 141,
143 | 3orbi123i 1156 | . 2
⊢ ((𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉) ↔ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) | 
| 145 | 134, 144 | sylnibr 329 | 1
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ (𝐴 Btwn 〈𝐵, 𝐶〉 ∨ 𝐵 Btwn 〈𝐶, 𝐴〉 ∨ 𝐶 Btwn 〈𝐴, 𝐵〉)) |