Theorem eengstr

Description: The Euclidean geometry as a structure. (Contributed by Thierry Arnoux, 15-Mar-2019)

	Ref	Expression
Assertion	eengstr	$$⊢N\in \mathbb{N}\to {𝔼}_{𝒢}\left(N\right)\mathrm{Struct}⟨1,17⟩$$

Proof

Step	Hyp	Ref	Expression
1		eengv	$$⊢N\in \mathbb{N}\to {𝔼}_{𝒢}\left(N\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}\cup \left\{⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\left\{z\in 𝔼\left(N\right)|z\mathrm{Btwn}⟨x,y⟩\right\}\right)⟩,⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in \left(𝔼\left(N\right)\setminus \left\{x\right\}\right)⟼\left\{z\in 𝔼\left(N\right)|\left(z\mathrm{Btwn}⟨x,y⟩\vee x\mathrm{Btwn}⟨z,y⟩\vee y\mathrm{Btwn}⟨x,z⟩\right)\right\}\right)⟩\right\}$$
2		1nn	$$⊢1\in \mathbb{N}$$
3		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		1lt10	$$⊢1<10$$
7	2 4 5 6	declti	$$⊢1<12$$
8		2nn	$$⊢2\in \mathbb{N}$$
9	5 8	decnncl	$$⊢12\in \mathbb{N}$$
10		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
11	2 3 7 9 10	strle2	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}\mathrm{Struct}⟨1,12⟩$$
12		6nn	$$⊢6\in \mathbb{N}$$
13	5 12	decnncl	$$⊢16\in \mathbb{N}$$
14		itvndx	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)=16$$
15		6nn0	$$⊢6\in {\mathbb{N}}_0$$
16		7nn	$$⊢7\in \mathbb{N}$$
17		6lt7	$$⊢6<7$$
18	5 15 16 17	declt	$$⊢16<17$$
19	5 16	decnncl	$$⊢17\in \mathbb{N}$$
20		lngndx	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)=17$$
21	13 14 18 19 20	strle2	$$⊢\left\{⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\left\{z\in 𝔼\left(N\right)|z\mathrm{Btwn}⟨x,y⟩\right\}\right)⟩,⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in \left(𝔼\left(N\right)\setminus \left\{x\right\}\right)⟼\left\{z\in 𝔼\left(N\right)|\left(z\mathrm{Btwn}⟨x,y⟩\vee x\mathrm{Btwn}⟨z,y⟩\vee y\mathrm{Btwn}⟨x,z⟩\right)\right\}\right)⟩\right\}\mathrm{Struct}⟨16,17⟩$$
22		2lt6	$$⊢2<6$$
23	5 4 12 22	declt	$$⊢12<16$$
24	11 21 23	strleun	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},𝔼\left(N\right)⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\sum _{i=1}^N{\left(x\left(i\right)-y\left(i\right)\right)}^2\right)⟩\right\}\cup \left\{⟨\mathrm{Itv}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in 𝔼\left(N\right)⟼\left\{z\in 𝔼\left(N\right)|z\mathrm{Btwn}⟨x,y⟩\right\}\right)⟩,⟨{Line}_{𝒢}\left(\mathrm{ndx}\right),\left(x\in 𝔼\left(N\right),y\in \left(𝔼\left(N\right)\setminus \left\{x\right\}\right)⟼\left\{z\in 𝔼\left(N\right)|\left(z\mathrm{Btwn}⟨x,y⟩\vee x\mathrm{Btwn}⟨z,y⟩\vee y\mathrm{Btwn}⟨x,z⟩\right)\right\}\right)⟩\right\}\right)\mathrm{Struct}⟨1,17⟩$$
25	1 24	eqbrtrdi	$$⊢N\in \mathbb{N}\to {𝔼}_{𝒢}\left(N\right)\mathrm{Struct}⟨1,17⟩$$