MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axlowdimlem6 Structured version   Visualization version   GIF version

Theorem axlowdimlem6 26024
Description: Lemma for axlowdim 26038. Show that three points are non-colinear. (Contributed by Scott Fenton, 29-Jun-2013.)
Hypotheses
Ref Expression
axlowdimlem6.1 𝐴 = ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
axlowdimlem6.2 𝐵 = ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))
axlowdimlem6.3 𝐶 = ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))
Assertion
Ref Expression
axlowdimlem6 (𝑁 ∈ (ℤ‘2) → ¬ (𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩))

Proof of Theorem axlowdimlem6
Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1zzd 11598 . . . . . 6 (𝑁 ∈ (ℤ‘2) → 1 ∈ ℤ)
2 eluzelz 11887 . . . . . 6 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ ℤ)
3 2nn 11375 . . . . . . . . . . 11 2 ∈ ℕ
4 uznnssnn 11926 . . . . . . . . . . 11 (2 ∈ ℕ → (ℤ‘2) ⊆ ℕ)
53, 4ax-mp 5 . . . . . . . . . 10 (ℤ‘2) ⊆ ℕ
6 nnuz 11914 . . . . . . . . . 10 ℕ = (ℤ‘1)
75, 6sseqtri 3776 . . . . . . . . 9 (ℤ‘2) ⊆ (ℤ‘1)
87sseli 3738 . . . . . . . 8 (𝑁 ∈ (ℤ‘2) → 𝑁 ∈ (ℤ‘1))
9 eluzle 11890 . . . . . . . 8 (𝑁 ∈ (ℤ‘1) → 1 ≤ 𝑁)
108, 9syl 17 . . . . . . 7 (𝑁 ∈ (ℤ‘2) → 1 ≤ 𝑁)
11 1re 10229 . . . . . . . 8 1 ∈ ℝ
1211leidi 10752 . . . . . . 7 1 ≤ 1
1310, 12jctil 561 . . . . . 6 (𝑁 ∈ (ℤ‘2) → (1 ≤ 1 ∧ 1 ≤ 𝑁))
14 elfz4 12526 . . . . . 6 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ≤ 1 ∧ 1 ≤ 𝑁)) → 1 ∈ (1...𝑁))
151, 2, 1, 13, 14syl31anc 1480 . . . . 5 (𝑁 ∈ (ℤ‘2) → 1 ∈ (1...𝑁))
16 eluzel2 11882 . . . . . 6 (𝑁 ∈ (ℤ‘2) → 2 ∈ ℤ)
17 eluzle 11890 . . . . . . 7 (𝑁 ∈ (ℤ‘2) → 2 ≤ 𝑁)
18 1le2 11431 . . . . . . 7 1 ≤ 2
1917, 18jctil 561 . . . . . 6 (𝑁 ∈ (ℤ‘2) → (1 ≤ 2 ∧ 2 ≤ 𝑁))
20 elfz4 12526 . . . . . 6 (((1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ∈ ℤ) ∧ (1 ≤ 2 ∧ 2 ≤ 𝑁)) → 2 ∈ (1...𝑁))
211, 2, 16, 19, 20syl31anc 1480 . . . . 5 (𝑁 ∈ (ℤ‘2) → 2 ∈ (1...𝑁))
22 ax-1ne0 10195 . . . . . . 7 1 ≠ 0
23 1t1e1 11365 . . . . . . . 8 (1 · 1) = 1
24 0cn 10222 . . . . . . . . 9 0 ∈ ℂ
2524mul01i 10416 . . . . . . . 8 (0 · 0) = 0
2623, 25neeq12i 2996 . . . . . . 7 ((1 · 1) ≠ (0 · 0) ↔ 1 ≠ 0)
2722, 26mpbir 221 . . . . . 6 (1 · 1) ≠ (0 · 0)
28 fveq2 6350 . . . . . . . . . . . 12 (𝑖 = 1 → (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘1))
29 0re 10230 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
3011, 29axlowdimlem4 26022 . . . . . . . . . . . . . . 15 {⟨1, 1⟩, ⟨2, 0⟩}:(1...2)⟶ℝ
31 ffn 6204 . . . . . . . . . . . . . . 15 ({⟨1, 1⟩, ⟨2, 0⟩}:(1...2)⟶ℝ → {⟨1, 1⟩, ⟨2, 0⟩} Fn (1...2))
3230, 31ax-mp 5 . . . . . . . . . . . . . 14 {⟨1, 1⟩, ⟨2, 0⟩} Fn (1...2)
33 axlowdimlem1 26019 . . . . . . . . . . . . . . 15 ((3...𝑁) × {0}):(3...𝑁)⟶ℝ
34 ffn 6204 . . . . . . . . . . . . . . 15 (((3...𝑁) × {0}):(3...𝑁)⟶ℝ → ((3...𝑁) × {0}) Fn (3...𝑁))
3533, 34ax-mp 5 . . . . . . . . . . . . . 14 ((3...𝑁) × {0}) Fn (3...𝑁)
36 axlowdimlem2 26020 . . . . . . . . . . . . . . 15 ((1...2) ∩ (3...𝑁)) = ∅
37 1z 11597 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
38 2z 11599 . . . . . . . . . . . . . . . . 17 2 ∈ ℤ
3937, 38, 373pm3.2i 1424 . . . . . . . . . . . . . . . 16 (1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ)
4012, 18pm3.2i 470 . . . . . . . . . . . . . . . 16 (1 ≤ 1 ∧ 1 ≤ 2)
41 elfz4 12526 . . . . . . . . . . . . . . . 16 (((1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ) ∧ (1 ≤ 1 ∧ 1 ≤ 2)) → 1 ∈ (1...2))
4239, 40, 41mp2an 710 . . . . . . . . . . . . . . 15 1 ∈ (1...2)
4336, 42pm3.2i 470 . . . . . . . . . . . . . 14 (((1...2) ∩ (3...𝑁)) = ∅ ∧ 1 ∈ (1...2))
44 fvun1 6429 . . . . . . . . . . . . . 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))
4532, 35, 43, 44mp3an 1571 . . . . . . . . . . . . 13 (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘1) = ({⟨1, 1⟩, ⟨2, 0⟩}‘1)
46 1ne2 11430 . . . . . . . . . . . . . 14 1 ≠ 2
47 1ex 10225 . . . . . . . . . . . . . . 15 1 ∈ V
4847, 47fvpr1 6618 . . . . . . . . . . . . . 14 (1 ≠ 2 → ({⟨1, 1⟩, ⟨2, 0⟩}‘1) = 1)
4946, 48ax-mp 5 . . . . . . . . . . . . 13 ({⟨1, 1⟩, ⟨2, 0⟩}‘1) = 1
5045, 49eqtri 2780 . . . . . . . . . . . 12 (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘1) = 1
5128, 50syl6eq 2808 . . . . . . . . . . 11 (𝑖 = 1 → (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = 1)
52 fveq2 6350 . . . . . . . . . . . 12 (𝑖 = 1 → (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘1))
5329, 29axlowdimlem4 26022 . . . . . . . . . . . . . . 15 {⟨1, 0⟩, ⟨2, 0⟩}:(1...2)⟶ℝ
54 ffn 6204 . . . . . . . . . . . . . . 15 ({⟨1, 0⟩, ⟨2, 0⟩}:(1...2)⟶ℝ → {⟨1, 0⟩, ⟨2, 0⟩} Fn (1...2))
5553, 54ax-mp 5 . . . . . . . . . . . . . 14 {⟨1, 0⟩, ⟨2, 0⟩} Fn (1...2)
56 fvun1 6429 . . . . . . . . . . . . . 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))
5755, 35, 43, 56mp3an 1571 . . . . . . . . . . . . 13 (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘1) = ({⟨1, 0⟩, ⟨2, 0⟩}‘1)
5829elexi 3351 . . . . . . . . . . . . . . 15 0 ∈ V
5947, 58fvpr1 6618 . . . . . . . . . . . . . 14 (1 ≠ 2 → ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0)
6046, 59ax-mp 5 . . . . . . . . . . . . 13 ({⟨1, 0⟩, ⟨2, 0⟩}‘1) = 0
6157, 60eqtri 2780 . . . . . . . . . . . 12 (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘1) = 0
6252, 61syl6eq 2808 . . . . . . . . . . 11 (𝑖 = 1 → (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = 0)
6351, 62oveq12d 6829 . . . . . . . . . 10 (𝑖 = 1 → ((({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖)) = (1 − 0))
64 1m0e1 11321 . . . . . . . . . 10 (1 − 0) = 1
6563, 64syl6eq 2808 . . . . . . . . 9 (𝑖 = 1 → ((({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖)) = 1)
6665oveq1d 6826 . . . . . . . 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 6350 . . . . . . . . . . . 12 (𝑖 = 1 → (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘1))
6829, 11axlowdimlem4 26022 . . . . . . . . . . . . . . 15 {⟨1, 0⟩, ⟨2, 1⟩}:(1...2)⟶ℝ
69 ffn 6204 . . . . . . . . . . . . . . 15 ({⟨1, 0⟩, ⟨2, 1⟩}:(1...2)⟶ℝ → {⟨1, 0⟩, ⟨2, 1⟩} Fn (1...2))
7068, 69ax-mp 5 . . . . . . . . . . . . . 14 {⟨1, 0⟩, ⟨2, 1⟩} Fn (1...2)
71 fvun1 6429 . . . . . . . . . . . . . 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))
7270, 35, 43, 71mp3an 1571 . . . . . . . . . . . . 13 (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘1) = ({⟨1, 0⟩, ⟨2, 1⟩}‘1)
7347, 58fvpr1 6618 . . . . . . . . . . . . . 14 (1 ≠ 2 → ({⟨1, 0⟩, ⟨2, 1⟩}‘1) = 0)
7446, 73ax-mp 5 . . . . . . . . . . . . 13 ({⟨1, 0⟩, ⟨2, 1⟩}‘1) = 0
7572, 74eqtri 2780 . . . . . . . . . . . 12 (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘1) = 0
7667, 75syl6eq 2808 . . . . . . . . . . 11 (𝑖 = 1 → (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑖) = 0)
7776, 62oveq12d 6829 . . . . . . . . . 10 (𝑖 = 1 → ((({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑖) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖)) = (0 − 0))
78 0m0e0 11320 . . . . . . . . . 10 (0 − 0) = 0
7977, 78syl6eq 2808 . . . . . . . . 9 (𝑖 = 1 → ((({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑖) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑖)) = 0)
8079oveq2d 6827 . . . . . . . 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))
8166, 80neeq12d 2991 . . . . . . 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 6350 . . . . . . . . . . . 12 (𝑗 = 2 → (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑗) = (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘2))
8337, 38, 383pm3.2i 1424 . . . . . . . . . . . . . . . 16 (1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ)
84 2re 11280 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
8584leidi 10752 . . . . . . . . . . . . . . . . 17 2 ≤ 2
8618, 85pm3.2i 470 . . . . . . . . . . . . . . . 16 (1 ≤ 2 ∧ 2 ≤ 2)
87 elfz4 12526 . . . . . . . . . . . . . . . 16 (((1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ) ∧ (1 ≤ 2 ∧ 2 ≤ 2)) → 2 ∈ (1...2))
8883, 86, 87mp2an 710 . . . . . . . . . . . . . . 15 2 ∈ (1...2)
8936, 88pm3.2i 470 . . . . . . . . . . . . . 14 (((1...2) ∩ (3...𝑁)) = ∅ ∧ 2 ∈ (1...2))
90 fvun1 6429 . . . . . . . . . . . . . 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))
9170, 35, 89, 90mp3an 1571 . . . . . . . . . . . . 13 (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘2) = ({⟨1, 0⟩, ⟨2, 1⟩}‘2)
9238elexi 3351 . . . . . . . . . . . . . . 15 2 ∈ V
9392, 47fvpr2 6619 . . . . . . . . . . . . . 14 (1 ≠ 2 → ({⟨1, 0⟩, ⟨2, 1⟩}‘2) = 1)
9446, 93ax-mp 5 . . . . . . . . . . . . 13 ({⟨1, 0⟩, ⟨2, 1⟩}‘2) = 1
9591, 94eqtri 2780 . . . . . . . . . . . 12 (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘2) = 1
9682, 95syl6eq 2808 . . . . . . . . . . 11 (𝑗 = 2 → (({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑗) = 1)
97 fveq2 6350 . . . . . . . . . . . 12 (𝑗 = 2 → (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗) = (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘2))
98 fvun1 6429 . . . . . . . . . . . . . 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))
9955, 35, 89, 98mp3an 1571 . . . . . . . . . . . . 13 (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘2) = ({⟨1, 0⟩, ⟨2, 0⟩}‘2)
10092, 58fvpr2 6619 . . . . . . . . . . . . . 14 (1 ≠ 2 → ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0)
10146, 100ax-mp 5 . . . . . . . . . . . . 13 ({⟨1, 0⟩, ⟨2, 0⟩}‘2) = 0
10299, 101eqtri 2780 . . . . . . . . . . . 12 (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘2) = 0
10397, 102syl6eq 2808 . . . . . . . . . . 11 (𝑗 = 2 → (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗) = 0)
10496, 103oveq12d 6829 . . . . . . . . . 10 (𝑗 = 2 → ((({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑗) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗)) = (1 − 0))
105104, 64syl6eq 2808 . . . . . . . . 9 (𝑗 = 2 → ((({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑗) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗)) = 1)
106105oveq2d 6827 . . . . . . . 8 (𝑗 = 2 → (1 · ((({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))‘𝑗) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗))) = (1 · 1))
107 fveq2 6350 . . . . . . . . . . . 12 (𝑗 = 2 → (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗) = (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘2))
108 fvun1 6429 . . . . . . . . . . . . . 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))
10932, 35, 89, 108mp3an 1571 . . . . . . . . . . . . 13 (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘2) = ({⟨1, 1⟩, ⟨2, 0⟩}‘2)
11092, 58fvpr2 6619 . . . . . . . . . . . . . 14 (1 ≠ 2 → ({⟨1, 1⟩, ⟨2, 0⟩}‘2) = 0)
11146, 110ax-mp 5 . . . . . . . . . . . . 13 ({⟨1, 1⟩, ⟨2, 0⟩}‘2) = 0
112109, 111eqtri 2780 . . . . . . . . . . . 12 (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘2) = 0
113107, 112syl6eq 2808 . . . . . . . . . . 11 (𝑗 = 2 → (({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗) = 0)
114113, 103oveq12d 6829 . . . . . . . . . 10 (𝑗 = 2 → ((({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗)) = (0 − 0))
115114, 78syl6eq 2808 . . . . . . . . 9 (𝑗 = 2 → ((({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗)) = 0)
116115oveq1d 6826 . . . . . . . 8 (𝑗 = 2 → (((({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗) − (({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))‘𝑗)) · 0) = (0 · 0))
117106, 116neeq12d 2991 . . . . . . 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)))
11881, 117rspc2ev 3461 . . . . . 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}))‘𝑖))))
11927, 118mp3an3 1560 . . . . 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}))‘𝑖))))
12015, 21, 119syl2anc 696 . . . 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 2931 . . . . . . . 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}))‘𝑖))))
122121rexbii 3177 . . . . . . 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 3131 . . . . . . 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}))‘𝑖))))
124122, 123bitri 264 . . . . . 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}))‘𝑖))))
125124rexbii 3177 . . . . 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 3131 . . . . 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}))‘𝑖))))
127125, 126bitri 264 . . . 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}))‘𝑖))))
128120, 127sylib 208 . . 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}))‘𝑖))))
12929, 29axlowdimlem5 26023 . . . 4 (𝑁 ∈ (ℤ‘2) → ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
13011, 29axlowdimlem5 26023 . . . 4 (𝑁 ∈ (ℤ‘2) → ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
13129, 11axlowdimlem5 26023 . . . 4 (𝑁 ∈ (ℤ‘2) → ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁))
132 colinearalg 25987 . . . 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}))‘𝑖)))))
133129, 130, 131, 132syl3anc 1477 . . 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}))‘𝑖)))))
134128, 133mtbird 314 . 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}))
138136, 137opeq12i 4556 . . . 4 𝐵, 𝐶⟩ = ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩
139135, 138breq12i 4811 . . 3 (𝐴 Btwn ⟨𝐵, 𝐶⟩ ↔ ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0}))⟩)
140137, 135opeq12i 4556 . . . 4 𝐶, 𝐴⟩ = ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩
141136, 140breq12i 4811 . . 3 (𝐵 Btwn ⟨𝐶, 𝐴⟩ ↔ ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
142135, 136opeq12i 4556 . . . 4 𝐴, 𝐵⟩ = ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩
143137, 142breq12i 4811 . . 3 (𝐶 Btwn ⟨𝐴, 𝐵⟩ ↔ ({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})), ({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0}))⟩)
144139, 141, 1433orbi123i 1160 . 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}))⟩))
145134, 144sylnibr 318 1 (𝑁 ∈ (ℤ‘2) → ¬ (𝐴 Btwn ⟨𝐵, 𝐶⟩ ∨ 𝐵 Btwn ⟨𝐶, 𝐴⟩ ∨ 𝐶 Btwn ⟨𝐴, 𝐵⟩))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3o 1071  w3a 1072   = wceq 1630  wcel 2137  wne 2930  wral 3048  wrex 3049  cun 3711  cin 3712  wss 3713  c0 4056  {csn 4319  {cpr 4321  cop 4325   class class class wbr 4802   × cxp 5262   Fn wfn 6042  wf 6043  cfv 6047  (class class class)co 6811  cr 10125  0cc0 10126  1c1 10127   · cmul 10131  cle 10265  cmin 10456  cn 11210  2c2 11260  3c3 11261  cz 11567  cuz 11877  ...cfz 12517  𝔼cee 25965   Btwn cbtwn 25966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-iun 4672  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-er 7909  df-map 8023  df-en 8120  df-dom 8121  df-sdom 8122  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-n0 11483  df-z 11568  df-uz 11878  df-icc 12373  df-fz 12518  df-seq 12994  df-exp 13053  df-ee 25968  df-btwn 25969
This theorem is referenced by:  axlowdim2  26037  axlowdim  26038
  Copyright terms: Public domain W3C validator