axlowdim2

Description: The lower two-dimensional axiom. In any space where the dimension is greater than one, there are three non-colinear points. Axiom A8 of Schwabhauser p. 12. (Contributed by Scott Fenton, 15-Apr-2013)

		Ref	Expression
	Assertion	axlowdim2	$⊢ N \in ℤ_{\geq 2} \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2	1 1	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
3		1re	$⊢ 1 \in ℝ$
4	3 1	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
5	1 3	axlowdimlem5	$⊢ N \in ℤ_{\geq 2} \to \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N)$
6		eqid	$⊢ \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
7		eqid	$⊢ \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})$
8		eqid	$⊢ \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})$
9	6 7 8	axlowdimlem6	$⊢ 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\})⟩)$
10		opeq2	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ = ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\})⟩$
11	10	breq2d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \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\})⟩)$
12		opeq1	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ = ⟨\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
13	12	breq2d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to ((\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \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\})⟩)$
14		breq1	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \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\})⟩)$
15	11 13 14	3orbi123d	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩) \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\})⟩))$
16	15	notbid	$⊢ z = \{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \to (\neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩) \leftrightarrow \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\})⟩))$
17	16	rspcev	$⊢ (\{⟨1, 0⟩, ⟨2, 1⟩\} \cup ((3 \dots N) \times \{0\}) \in 𝔼 (N) \land \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\})⟩)) \to \exists z \in 𝔼 (N) \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
18	5 9 17	syl2anc	$⊢ N \in ℤ_{\geq 2} \to \exists z \in 𝔼 (N) \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
19		breq1	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (x Btwn ⟨y, z⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩)$
20		opeq2	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨z, x⟩ = ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
21	20	breq2d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (y Btwn ⟨z, x⟩ \leftrightarrow y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
22		opeq1	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨x, y⟩ = ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩$
23	22	breq2d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (z Btwn ⟨x, y⟩ \leftrightarrow z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩)$
24	19 21 23	3orbi123d	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ((x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩) \leftrightarrow ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩))$
25	24	notbid	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩) \leftrightarrow \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩))$
26	25	rexbidv	$⊢ x = \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\exists z \in 𝔼 (N) \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩) \leftrightarrow \exists z \in 𝔼 (N) \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩))$
27		opeq1	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨y, z⟩ = ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩$
28	27	breq2d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \leftrightarrow (\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩)$
29		breq1	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \leftrightarrow (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
30		opeq2	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩ = ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩$
31	30	breq2d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩ \leftrightarrow z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)$
32	28 29 31	3orbi123d	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩) \leftrightarrow ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
33	32	notbid	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩) \leftrightarrow \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
34	33	rexbidv	$⊢ y = \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}) \to (\exists z \in 𝔼 (N) \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨y, z⟩ \lor y Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), y⟩) \leftrightarrow \exists z \in 𝔼 (N) \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩))$
35	26 34	rspc2ev	$⊢ (\{⟨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 \exists z \in 𝔼 (N) \neg ((\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), z⟩ \lor (\{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})) Btwn ⟨z, \{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩ \lor z Btwn ⟨\{⟨1, 0⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\}), \{⟨1, 1⟩, ⟨2, 0⟩\} \cup ((3 \dots N) \times \{0\})⟩)) \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)$
36	2 4 18 35	syl3anc	$⊢ N \in ℤ_{\geq 2} \to \exists x \in 𝔼 (N) \exists y \in 𝔼 (N) \exists z \in 𝔼 (N) \neg (x Btwn ⟨y, z⟩ \lor y Btwn ⟨z, x⟩ \lor z Btwn ⟨x, y⟩)$

Metamath Proof Explorer

Theorem axlowdim2

Proof