axlowdimlem6

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

	Ref	Expression
Hypotheses	axlowdimlem6.1	$⊢ A = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
	axlowdimlem6.2	$⊢ B = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
	axlowdimlem6.3	$⊢ C = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})$
Assertion	axlowdimlem6	$⊢ N \in ℤ_{\geq 2} \to \neg (A Btwn ⟨B, C⟩ \lor B Btwn ⟨C, A⟩ \lor C Btwn ⟨A, B⟩)$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem6.1	$⊢ A = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
2		axlowdimlem6.2	$⊢ B = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
3		axlowdimlem6.3	$⊢ C = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})$
4		1zzd	$⊢ N \in ℤ_{\geq 2} \to 1 \in ℤ$
5		eluzelz	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ$
6		2nn	$⊢ 2 \in ℕ$
7		uznnssnn	$⊢ 2 \in ℕ \to ℤ_{\geq 2} \subseteq ℕ$
8	6 7	ax-mp	$⊢ ℤ_{\geq 2} \subseteq ℕ$
9		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
10	8 9	sseqtri	$⊢ ℤ_{\geq 2} \subseteq ℤ_{\geq 1}$
11	10	sseli	$⊢ N \in ℤ_{\geq 2} \to N \in ℤ_{\geq 1}$
12		eluzle	$⊢ N \in ℤ_{\geq 1} \to 1 \leq N$
13	11 12	syl	$⊢ N \in ℤ_{\geq 2} \to 1 \leq N$
14		1re	$⊢ 1 \in ℝ$
15	14	leidi	$⊢ 1 \leq 1$
16	13 15	jctil	$⊢ N \in ℤ_{\geq 2} \to (1 \leq 1 \land 1 \leq N)$
17		elfz4	$⊢ ((1 \in ℤ \land N \in ℤ \land 1 \in ℤ) \land (1 \leq 1 \land 1 \leq N)) \to 1 \in (1 \dots N)$
18	4 5 4 16 17	syl31anc	$⊢ N \in ℤ_{\geq 2} \to 1 \in (1 \dots N)$
19		eluzel2	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℤ$
20		eluzle	$⊢ N \in ℤ_{\geq 2} \to 2 \leq N$
21		1le2	$⊢ 1 \leq 2$
22	20 21	jctil	$⊢ N \in ℤ_{\geq 2} \to (1 \leq 2 \land 2 \leq N)$
23		elfz4	$⊢ ((1 \in ℤ \land N \in ℤ \land 2 \in ℤ) \land (1 \leq 2 \land 2 \leq N)) \to 2 \in (1 \dots N)$
24	4 5 19 22 23	syl31anc	$⊢ N \in ℤ_{\geq 2} \to 2 \in (1 \dots N)$
25		ax-1ne0	$⊢ 1 \neq 0$
26		1t1e1	$⊢ 1 \cdot 1 = 1$
27		0cn	$⊢ 0 \in ℂ$
28	27	mul01i	$⊢ 0 \cdot 0 = 0$
29	26 28	neeq12i	$⊢ 1 \cdot 1 \neq 0 \cdot 0 \leftrightarrow 1 \neq 0$
30	25 29	mpbir	$⊢ 1 \cdot 1 \neq 0 \cdot 0$
31		fveq2	$⊢ i = 1 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (1)$
32		0re	$⊢ 0 \in ℝ$
33	14 32	axlowdimlem4	$⊢ \{⟨1, 1⟩, ⟨2, 0⟩\} : (1 \dots 2) ⟶ ℝ$
34		ffn	$⊢ \{⟨1, 1⟩, ⟨2, 0⟩\} : (1 \dots 2) ⟶ ℝ \to \{⟨1, 1⟩, ⟨2, 0⟩\} Fn (1 \dots 2)$
35	33 34	ax-mp	$⊢ \{⟨1, 1⟩, ⟨2, 0⟩\} Fn (1 \dots 2)$
36		axlowdimlem1	$⊢ ((3 \dots N) \times \{0\}) : (3 \dots N) ⟶ ℝ$
37		ffn	$⊢ ((3 \dots N) \times \{0\}) : (3 \dots N) ⟶ ℝ \to ((3 \dots N) \times \{0\}) Fn (3 \dots N)$
38	36 37	ax-mp	$⊢ ((3 \dots N) \times \{0\}) Fn (3 \dots N)$
39		axlowdimlem2	$⊢ (1 \dots 2) \cap (3 \dots N) = \emptyset$
40		1z	$⊢ 1 \in ℤ$
41		2z	$⊢ 2 \in ℤ$
42	40 41 40	3pm3.2i	$⊢ (1 \in ℤ \land 2 \in ℤ \land 1 \in ℤ)$
43	15 21	pm3.2i	$⊢ (1 \leq 1 \land 1 \leq 2)$
44		elfz4	$⊢ ((1 \in ℤ \land 2 \in ℤ \land 1 \in ℤ) \land (1 \leq 1 \land 1 \leq 2)) \to 1 \in (1 \dots 2)$
45	42 43 44	mp2an	$⊢ 1 \in (1 \dots 2)$
46	39 45	pm3.2i	$⊢ ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 1 \in (1 \dots 2))$
47		fvun1	$⊢ (\{⟨1, 1⟩, ⟨2, 0⟩\} Fn (1 \dots 2) \land ((3 \dots N) \times \{0\}) Fn (3 \dots N) \land ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 1 \in (1 \dots 2))) \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (1) = \{⟨1, 1⟩, ⟨2, 0⟩\} (1)$
48	35 38 46 47	mp3an	$⊢ (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (1) = \{⟨1, 1⟩, ⟨2, 0⟩\} (1)$
49		1ne2	$⊢ 1 \neq 2$
50		1ex	$⊢ 1 \in V$
51	50 50	fvpr1	$⊢ 1 \neq 2 \to \{⟨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⟩\} \cup ((3 \dots N) \times \{0\})) (1) = 1$
54	31 53	eqtrdi	$⊢ i = 1 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = 1$
55		fveq2	$⊢ i = 1 \to (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (1)$
56	32 32	axlowdimlem4	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} : (1 \dots 2) ⟶ ℝ$
57		ffn	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} : (1 \dots 2) ⟶ ℝ \to \{⟨1, 0⟩, ⟨2, 0⟩\} Fn (1 \dots 2)$
58	56 57	ax-mp	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} Fn (1 \dots 2)$
59		fvun1	$⊢ (\{⟨1, 0⟩, ⟨2, 0⟩\} Fn (1 \dots 2) \land ((3 \dots N) \times \{0\}) Fn (3 \dots N) \land ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 1 \in (1 \dots 2))) \to (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (1) = \{⟨1, 0⟩, ⟨2, 0⟩\} (1)$
60	58 38 46 59	mp3an	$⊢ (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (1) = \{⟨1, 0⟩, ⟨2, 0⟩\} (1)$
61	32	elexi	$⊢ 0 \in V$
62	50 61	fvpr1	$⊢ 1 \neq 2 \to \{⟨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⟩\} \cup ((3 \dots N) \times \{0\})) (1) = 0$
65	55 64	eqtrdi	$⊢ i = 1 \to (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = 0$
66	54 65	oveq12d	$⊢ i = 1 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = 1 - 0$
67		1m0e1	$⊢ 1 - 0 = 1$
68	66 67	eqtrdi	$⊢ i = 1 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = 1$
69	68	oveq1d	$⊢ i = 1 \to ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = 1 ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j))$
70		fveq2	$⊢ i = 1 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) = (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (1)$
71	32 14	axlowdimlem4	$⊢ \{⟨1, 0⟩, ⟨2, 1⟩\} : (1 \dots 2) ⟶ ℝ$
72		ffn	$⊢ \{⟨1, 0⟩, ⟨2, 1⟩\} : (1 \dots 2) ⟶ ℝ \to \{⟨1, 0⟩, ⟨2, 1⟩\} Fn (1 \dots 2)$
73	71 72	ax-mp	$⊢ \{⟨1, 0⟩, ⟨2, 1⟩\} Fn (1 \dots 2)$
74		fvun1	$⊢ (\{⟨1, 0⟩, ⟨2, 1⟩\} Fn (1 \dots 2) \land ((3 \dots N) \times \{0\}) Fn (3 \dots N) \land ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 1 \in (1 \dots 2))) \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (1) = \{⟨1, 0⟩, ⟨2, 1⟩\} (1)$
75	73 38 46 74	mp3an	$⊢ (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (1) = \{⟨1, 0⟩, ⟨2, 1⟩\} (1)$
76	50 61	fvpr1	$⊢ 1 \neq 2 \to \{⟨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⟩\} \cup ((3 \dots N) \times \{0\})) (1) = 0$
79	70 78	eqtrdi	$⊢ i = 1 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) = 0$
80	79 65	oveq12d	$⊢ i = 1 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = 0 - 0$
81		0m0e0	$⊢ 0 - 0 = 0$
82	80 81	eqtrdi	$⊢ i = 1 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) = 0$
83	82	oveq2d	$⊢ i = 1 \to ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \cdot 0$
84	69 83	neeq12d	$⊢ i = 1 \to (((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow 1 ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \cdot 0)$
85		fveq2	$⊢ j = 2 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) = (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (2)$
86	40 41 41	3pm3.2i	$⊢ (1 \in ℤ \land 2 \in ℤ \land 2 \in ℤ)$
87		2re	$⊢ 2 \in ℝ$
88	87	leidi	$⊢ 2 \leq 2$
89	21 88	pm3.2i	$⊢ (1 \leq 2 \land 2 \leq 2)$
90		elfz4	$⊢ ((1 \in ℤ \land 2 \in ℤ \land 2 \in ℤ) \land (1 \leq 2 \land 2 \leq 2)) \to 2 \in (1 \dots 2)$
91	86 89 90	mp2an	$⊢ 2 \in (1 \dots 2)$
92	39 91	pm3.2i	$⊢ ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 2 \in (1 \dots 2))$
93		fvun1	$⊢ (\{⟨1, 0⟩, ⟨2, 1⟩\} Fn (1 \dots 2) \land ((3 \dots N) \times \{0\}) Fn (3 \dots N) \land ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 2 \in (1 \dots 2))) \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (2) = \{⟨1, 0⟩, ⟨2, 1⟩\} (2)$
94	73 38 92 93	mp3an	$⊢ (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (2) = \{⟨1, 0⟩, ⟨2, 1⟩\} (2)$
95	41	elexi	$⊢ 2 \in V$
96	95 50	fvpr2	$⊢ 1 \neq 2 \to \{⟨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⟩\} \cup ((3 \dots N) \times \{0\})) (2) = 1$
99	85 98	eqtrdi	$⊢ j = 2 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) = 1$
100		fveq2	$⊢ j = 2 \to (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (2)$
101		fvun1	$⊢ (\{⟨1, 0⟩, ⟨2, 0⟩\} Fn (1 \dots 2) \land ((3 \dots N) \times \{0\}) Fn (3 \dots N) \land ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 2 \in (1 \dots 2))) \to (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (2) = \{⟨1, 0⟩, ⟨2, 0⟩\} (2)$
102	58 38 92 101	mp3an	$⊢ (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (2) = \{⟨1, 0⟩, ⟨2, 0⟩\} (2)$
103	95 61	fvpr2	$⊢ 1 \neq 2 \to \{⟨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⟩\} \cup ((3 \dots N) \times \{0\})) (2) = 0$
106	100 105	eqtrdi	$⊢ j = 2 \to (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = 0$
107	99 106	oveq12d	$⊢ j = 2 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = 1 - 0$
108	107 67	eqtrdi	$⊢ j = 2 \to (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = 1$
109	108	oveq2d	$⊢ j = 2 \to 1 ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = 1 \cdot 1$
110		fveq2	$⊢ j = 2 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (2)$
111		fvun1	$⊢ (\{⟨1, 1⟩, ⟨2, 0⟩\} Fn (1 \dots 2) \land ((3 \dots N) \times \{0\}) Fn (3 \dots N) \land ((1 \dots 2) \cap (3 \dots N) = \emptyset \land 2 \in (1 \dots 2))) \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (2) = \{⟨1, 1⟩, ⟨2, 0⟩\} (2)$
112	35 38 92 111	mp3an	$⊢ (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (2) = \{⟨1, 1⟩, ⟨2, 0⟩\} (2)$
113	95 61	fvpr2	$⊢ 1 \neq 2 \to \{⟨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⟩\} \cup ((3 \dots N) \times \{0\})) (2) = 0$
116	110 115	eqtrdi	$⊢ j = 2 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = 0$
117	116 106	oveq12d	$⊢ j = 2 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = 0 - 0$
118	117 81	eqtrdi	$⊢ j = 2 \to (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) = 0$
119	118	oveq1d	$⊢ j = 2 \to ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \cdot 0 = 0 \cdot 0$
120	109 119	neeq12d	$⊢ j = 2 \to (1 ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \cdot 0 \leftrightarrow 1 \cdot 1 \neq 0 \cdot 0)$
121	84 120	rspc2ev	$⊢ (1 \in (1 \dots N) \land 2 \in (1 \dots N) \land 1 \cdot 1 \neq 0 \cdot 0) \to \exists i \in (1 \dots N) \exists j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
122	30 121	mp3an3	$⊢ (1 \in (1 \dots N) \land 2 \in (1 \dots N)) \to \exists i \in (1 \dots N) \exists j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
123	18 24 122	syl2anc	$⊢ N \in ℤ_{\geq 2} \to \exists i \in (1 \dots N) \exists j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
124		df-ne	$⊢ ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow \neg ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
125	124	rexbii	$⊢ \exists j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow \exists j \in (1 \dots N) \neg ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
126		rexnal	$⊢ \exists j \in (1 \dots N) \neg ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow \neg \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
127	125 126	bitri	$⊢ \exists j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow \neg \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
128	127	rexbii	$⊢ \exists i \in (1 \dots N) \exists j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow \exists i \in (1 \dots N) \neg \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
129		rexnal	$⊢ \exists i \in (1 \dots N) \neg \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow \neg \forall i \in (1 \dots N) \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
130	128 129	bitri	$⊢ \exists i \in (1 \dots N) \exists j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) \neq ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) \leftrightarrow \neg \forall i \in (1 \dots N) \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
131	123 130	sylib	$⊢ N \in ℤ_{\geq 2} \to \neg \forall i \in (1 \dots N) \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i))$
132	32 32	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
133	14 32	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
134	32 14	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
135		colinearalg	$⊢ (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N) \land \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N) \land \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)) \to (((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩) \leftrightarrow \forall i \in (1 \dots N) \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)))$
136	132 133 134 135	syl3anc	$⊢ N \in ℤ_{\geq 2} \to (((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩) \leftrightarrow \forall i \in (1 \dots N) \forall j \in (1 \dots N) ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) = ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (j)) ((\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) (i) - (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) (i)))$
137	131 136	mtbird	$⊢ N \in ℤ_{\geq 2} \to \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
138	2 3	opeq12i	$⊢ ⟨B, C⟩ = ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
139	1 138	breq12i	$⊢ A Btwn ⟨B, C⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
140	3 1	opeq12i	$⊢ ⟨C, A⟩ = ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
141	2 140	breq12i	$⊢ B Btwn ⟨C, A⟩ \leftrightarrow (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
142	1 2	opeq12i	$⊢ ⟨A, B⟩ = ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
143	3 142	breq12i	$⊢ C Btwn ⟨A, B⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
144	139 141 143	3orbi123i	$⊢ (A Btwn ⟨B, C⟩ \lor B Btwn ⟨C, A⟩ \lor C Btwn ⟨A, B⟩) \leftrightarrow ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
145	137 144	sylnibr	$⊢ N \in ℤ_{\geq 2} \to \neg (A Btwn ⟨B, C⟩ \lor B Btwn ⟨C, A⟩ \lor C Btwn ⟨A, B⟩)$

Metamath Proof Explorer

Theorem axlowdimlem6

Proof