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	$$⊢A=\left\{⟨1,0⟩,⟨2,0⟩\right\}\cup \left(\left(3\dots N\right)\times \left\{0\right\}\right)$$
	axlowdimlem6.2	$$⊢B=\left\{⟨1,1⟩,⟨2,0⟩\right\}\cup \left(\left(3\dots N\right)\times \left\{0\right\}\right)$$
	axlowdimlem6.3	$$⊢C=\left\{⟨1,0⟩,⟨2,1⟩\right\}\cup \left(\left(3\dots N\right)\times \left\{0\right\}\right)$$
Assertion	axlowdimlem6	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \neg \left(A\mathrm{Btwn}⟨B,C⟩\vee B\mathrm{Btwn}⟨C,A⟩\vee C\mathrm{Btwn}⟨A,B⟩\right)$$

Proof

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