Metamath Proof Explorer

Theorem axlowdimlem6

Description: Lemma for axlowdim . Show that three points are non-colinear. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Hypotheses 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 axlowdimlem6 ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )

Proof

Step Hyp Ref Expression
1 axlowdimlem6.1 ⊢ 𝐴 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
2 axlowdimlem6.2 ⊢ 𝐵 = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
3 axlowdimlem6.3 ⊢ 𝐶 = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) )
4 1zzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℤ )
5 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℤ )
6 2nn ⊢ 2 ∈ ℕ
7 uznnssnn ⊢ ( 2 ∈ ℕ → ( ℤ≥ ‘ 2 ) ⊆ ℕ )
8 6 7 ax-mp ⊢ ( ℤ≥ ‘ 2 ) ⊆ ℕ
9 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
10 8 9 sseqtri ⊢ ( ℤ≥ ‘ 2 ) ⊆ ( ℤ≥ ‘ 1 )
11 10 sseli ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
12 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ≤ 𝑁 )
13 11 12 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ 𝑁 )
14 1re ⊢ 1 ∈ ℝ
15 14 leidi ⊢ 1 ≤ 1
16 13 15 jctil ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ≤ 1 ∧ 1 ≤ 𝑁 ) )
17 elfz4 ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 1 ≤ 1 ∧ 1 ≤ 𝑁 ) ) → 1 ∈ ( 1 ... 𝑁 ) )
18 4 5 4 16 17 syl31anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ( 1 ... 𝑁 ) )
19 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℤ )
20 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
21 1le2 ⊢ 1 ≤ 2
22 20 21 jctil ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) )
23 elfz4 ⊢ ( ( ( 1 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 1 ≤ 2 ∧ 2 ≤ 𝑁 ) ) → 2 ∈ ( 1 ... 𝑁 ) )
24 4 5 19 22 23 syl31anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ( 1 ... 𝑁 ) )
25 ax-1ne0 ⊢ 1 ≠ 0
26 1t1e1 ⊢ ( 1 · 1 ) = 1
27 0cn ⊢ 0 ∈ ℂ
28 27 mul01i ⊢ ( 0 · 0 ) = 0
29 26 28 neeq12i ⊢ ( ( 1 · 1 ) ≠ ( 0 · 0 ) ↔ 1 ≠ 0 )
30 25 29 mpbir ⊢ ( 1 · 1 ) ≠ ( 0 · 0 )
31 fveq2 ⊢ ( 𝑖 = 1 → ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) )
32 0re ⊢ 0 ∈ ℝ
33 14 32 axlowdimlem4 ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } : ( 1 ... 2 ) ⟶ ℝ
34 ffn ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } : ( 1 ... 2 ) ⟶ ℝ → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } Fn ( 1 ... 2 ) )
35 33 34 ax-mp ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } Fn ( 1 ... 2 )
36 axlowdimlem1 ⊢ ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ
37 ffn ⊢ ( ( ( 3 ... 𝑁 ) × { 0 } ) : ( 3 ... 𝑁 ) ⟶ ℝ → ( ( 3 ... 𝑁 ) × { 0 } ) Fn ( 3 ... 𝑁 ) )
38 36 37 ax-mp ⊢ ( ( 3 ... 𝑁 ) × { 0 } ) Fn ( 3 ... 𝑁 )
39 axlowdimlem2 ⊢ ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅
40 1z ⊢ 1 ∈ ℤ
41 2z ⊢ 2 ∈ ℤ
42 40 41 40 3pm3.2i ⊢ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ )
43 15 21 pm3.2i ⊢ ( 1 ≤ 1 ∧ 1 ≤ 2 )
44 elfz4 ⊢ ( ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ( 1 ≤ 1 ∧ 1 ≤ 2 ) ) → 1 ∈ ( 1 ... 2 ) )
45 42 43 44 mp2an ⊢ 1 ∈ ( 1 ... 2 )
46 39 45 pm3.2i ⊢ ( ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ ∧ 1 ∈ ( 1 ... 2 ) )
47 fvun1 ⊢ ( ( { ⟨ 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 ) )
48 35 38 46 47 mp3an ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 )
49 1ne2 ⊢ 1 ≠ 2
50 1ex ⊢ 1 ∈ V
51 50 50 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 1 )
52 49 51 ax-mp ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 1
53 48 52 eqtri ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) = 1
54 31 53 eqtrdi ⊢ ( 𝑖 = 1 → ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = 1 )
55 fveq2 ⊢ ( 𝑖 = 1 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) )
56 32 32 axlowdimlem4 ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } : ( 1 ... 2 ) ⟶ ℝ
57 ffn ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } : ( 1 ... 2 ) ⟶ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } Fn ( 1 ... 2 ) )
58 56 57 ax-mp ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } Fn ( 1 ... 2 )
59 fvun1 ⊢ ( ( { ⟨ 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 ) )
60 58 38 46 59 mp3an ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 )
61 32 elexi ⊢ 0 ∈ V
62 50 61 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 0 )
63 49 62 ax-mp ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 1 ) = 0
64 60 63 eqtri ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) = 0
65 55 64 eqtrdi ⊢ ( 𝑖 = 1 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = 0 )
66 54 65 oveq12d ⊢ ( 𝑖 = 1 → ( ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) ) = ( 1 − 0 ) )
67 1m0e1 ⊢ ( 1 − 0 ) = 1
68 66 67 eqtrdi ⊢ ( 𝑖 = 1 → ( ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) ) = 1 )
69 68 oveq1d ⊢ ( 𝑖 = 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 } ) ) ‘ 𝑗 ) ) ) )
70 fveq2 ⊢ ( 𝑖 = 1 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) )
71 32 14 axlowdimlem4 ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } : ( 1 ... 2 ) ⟶ ℝ
72 ffn ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } : ( 1 ... 2 ) ⟶ ℝ → { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } Fn ( 1 ... 2 ) )
73 71 72 ax-mp ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } Fn ( 1 ... 2 )
74 fvun1 ⊢ ( ( { ⟨ 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 ) )
75 73 38 46 74 mp3an ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 )
76 50 61 fvpr1 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 0 )
77 49 76 ax-mp ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 1 ) = 0
78 75 77 eqtri ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 1 ) = 0
79 70 78 eqtrdi ⊢ ( 𝑖 = 1 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) = 0 )
80 79 65 oveq12d ⊢ ( 𝑖 = 1 → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) ) = ( 0 − 0 ) )
81 0m0e0 ⊢ ( 0 − 0 ) = 0
82 80 81 eqtrdi ⊢ ( 𝑖 = 1 → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑖 ) ) = 0 )
83 82 oveq2d ⊢ ( 𝑖 = 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 ) )
84 69 83 neeq12d ⊢ ( 𝑖 = 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 ) ) )
85 fveq2 ⊢ ( 𝑗 = 2 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) = ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) )
86 40 41 41 3pm3.2i ⊢ ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ )
87 2re ⊢ 2 ∈ ℝ
88 87 leidi ⊢ 2 ≤ 2
89 21 88 pm3.2i ⊢ ( 1 ≤ 2 ∧ 2 ≤ 2 )
90 elfz4 ⊢ ( ( ( 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ ) ∧ ( 1 ≤ 2 ∧ 2 ≤ 2 ) ) → 2 ∈ ( 1 ... 2 ) )
91 86 89 90 mp2an ⊢ 2 ∈ ( 1 ... 2 )
92 39 91 pm3.2i ⊢ ( ( ( 1 ... 2 ) ∩ ( 3 ... 𝑁 ) ) = ∅ ∧ 2 ∈ ( 1 ... 2 ) )
93 fvun1 ⊢ ( ( { ⟨ 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 ) )
94 73 38 92 93 mp3an ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 )
95 41 elexi ⊢ 2 ∈ V
96 95 50 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1 )
97 49 96 ax-mp ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ‘ 2 ) = 1
98 94 97 eqtri ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) = 1
99 85 98 eqtrdi ⊢ ( 𝑗 = 2 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) = 1 )
100 fveq2 ⊢ ( 𝑗 = 2 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) = ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) )
101 fvun1 ⊢ ( ( { ⟨ 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 ) )
102 58 38 92 101 mp3an ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) = ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 )
103 95 61 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0 )
104 49 103 ax-mp ⊢ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0
105 102 104 eqtri ⊢ ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) = 0
106 100 105 eqtrdi ⊢ ( 𝑗 = 2 → ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) = 0 )
107 99 106 oveq12d ⊢ ( 𝑗 = 2 → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) ) = ( 1 − 0 ) )
108 107 67 eqtrdi ⊢ ( 𝑗 = 2 → ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) ) = 1 )
109 108 oveq2d ⊢ ( 𝑗 = 2 → ( 1 · ( ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) ) ) = ( 1 · 1 ) )
110 fveq2 ⊢ ( 𝑗 = 2 → ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) = ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) )
111 fvun1 ⊢ ( ( { ⟨ 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 ) )
112 35 38 92 111 mp3an ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) = ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 )
113 95 61 fvpr2 ⊢ ( 1 ≠ 2 → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0 )
114 49 113 ax-mp ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ‘ 2 ) = 0
115 112 114 eqtri ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 2 ) = 0
116 110 115 eqtrdi ⊢ ( 𝑗 = 2 → ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) = 0 )
117 116 106 oveq12d ⊢ ( 𝑗 = 2 → ( ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) ) = ( 0 − 0 ) )
118 117 81 eqtrdi ⊢ ( 𝑗 = 2 → ( ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) ) = 0 )
119 118 oveq1d ⊢ ( 𝑗 = 2 → ( ( ( ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) − ( ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ‘ 𝑗 ) ) · 0 ) = ( 0 · 0 ) )
120 109 119 neeq12d ⊢ ( 𝑗 = 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 ) ) )
121 84 120 rspc2ev ⊢ ( ( 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 } ) ) ‘ 𝑖 ) ) ) )
122 30 121 mp3an3 ⊢ ( ( 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 } ) ) ‘ 𝑖 ) ) ) )
123 18 24 122 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 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 } ) ) ‘ 𝑖 ) ) ) )
124 df-ne ⊢ ( ( ( ( ( { ⟨ 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 } ) ) ‘ 𝑖 ) ) ) )
125 124 rexbii ⊢ ( ∃ 𝑗 ∈ ( 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 } ) ) ‘ 𝑖 ) ) ) )
126 rexnal ⊢ ( ∃ 𝑗 ∈ ( 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 } ) ) ‘ 𝑖 ) ) ) )
127 125 126 bitri ⊢ ( ∃ 𝑗 ∈ ( 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 } ) ) ‘ 𝑖 ) ) ) )
128 127 rexbii ⊢ ( ∃ 𝑖 ∈ ( 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 } ) ) ‘ 𝑖 ) ) ) )
129 rexnal ⊢ ( ∃ 𝑖 ∈ ( 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 } ) ) ‘ 𝑖 ) ) ) )
130 128 129 bitri ⊢ ( ∃ 𝑖 ∈ ( 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 } ) ) ‘ 𝑖 ) ) ) )
131 123 130 sylib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 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 } ) ) ‘ 𝑖 ) ) ) )
132 32 32 axlowdimlem5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
133 14 32 axlowdimlem5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
134 32 14 axlowdimlem5 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
135 colinearalg ⊢ ( ( ( { ⟨ 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 } ) ) ‘ 𝑖 ) ) ) ) )
136 132 133 134 135 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 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 } ) ) ‘ 𝑖 ) ) ) ) )
137 131 136 mtbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 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 } ) ) ⟩ ) )
138 2 3 opeq12i ⊢ ⟨ 𝐵 , 𝐶 ⟩ = ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩
139 1 138 breq12i ⊢ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
140 3 1 opeq12i ⊢ ⟨ 𝐶 , 𝐴 ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩
141 2 140 breq12i ⊢ ( 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ↔ ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) Btwn ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 1 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩ )
142 1 2 opeq12i ⊢ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ ( { ⟨ 1 , 0 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) , ( { ⟨ 1 , 1 ⟩ , ⟨ 2 , 0 ⟩ } ∪ ( ( 3 ... 𝑁 ) × { 0 } ) ) ⟩
143 3 142 breq12i ⊢ ( 𝐶 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 ⊢ ( ( 𝐴 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 137 144 sylnibr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )