Theorem trkgstr

Description: Functionality of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017)

	Ref	Expression
Hypothesis	trkgstr.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩,⟨\mathrm{Itv}\left(\mathrm{ndx}\right),I⟩\right\}$$
Assertion	trkgstr	$$⊢W\mathrm{Struct}⟨1,16⟩$$

Proof

Step	Hyp	Ref	Expression
1		trkgstr.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩,⟨\mathrm{Itv}\left(\mathrm{ndx}\right),I⟩\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		6nn	$$⊢6\in \mathbb{N}$$
12		2lt6	$$⊢2<6$$
13	5 4 11 12	declt	$$⊢12<16$$
14	5 11	decnncl	$$⊢16\in \mathbb{N}$$
15		itvndx	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)=16$$
16	2 3 7 9 10 13 14 15	strle3	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},U⟩,⟨\mathrm{dist}\left(\mathrm{ndx}\right),D⟩,⟨\mathrm{Itv}\left(\mathrm{ndx}\right),I⟩\right\}\mathrm{Struct}⟨1,16⟩$$
17	1 16	eqbrtri	$$⊢W\mathrm{Struct}⟨1,16⟩$$