Theorem slotslnbpsd

Description: The slots Base , +g , .s and dist are different from the slot LineG . Formerly part of ttglem and proofs using it. (Contributed by AV, 29-Oct-2024)

	Ref	Expression
Assertion	slotslnbpsd	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lngndx	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)=17$$
2		1re	$$⊢1\in ℝ$$
3		1nn	$$⊢1\in \mathbb{N}$$
4		7nn0	$$⊢7\in {\mathbb{N}}_0$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		1lt10	$$⊢1<10$$
7	3 4 5 6	declti	$$⊢1<17$$
8	2 7	gtneii	$$⊢17\ne 1$$
9		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
10	8 9	neeqtrri	$$⊢17\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
11	1 10	eqnetri	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
12		2re	$$⊢2\in ℝ$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14		2lt10	$$⊢2<10$$
15	3 4 13 14	declti	$$⊢2<17$$
16	12 15	gtneii	$$⊢17\ne 2$$
17		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
18	16 17	neeqtrri	$$⊢17\ne {+}_{\mathrm{ndx}}$$
19	1 18	eqnetri	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
20	11 19	pm3.2i	$$⊢\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)$$
21		6re	$$⊢6\in ℝ$$
22		6nn0	$$⊢6\in {\mathbb{N}}_0$$
23		6lt10	$$⊢6<10$$
24	3 4 22 23	declti	$$⊢6<17$$
25	21 24	gtneii	$$⊢17\ne 6$$
26		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
27	25 26	neeqtrri	$$⊢17\ne {\cdot }_{\mathrm{ndx}}$$
28	1 27	eqnetri	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
29		2nn	$$⊢2\in \mathbb{N}$$
30	5 29	decnncl	$$⊢12\in \mathbb{N}$$
31	30	nnrei	$$⊢12\in ℝ$$
32		7nn	$$⊢7\in \mathbb{N}$$
33		2lt7	$$⊢2<7$$
34	5 13 32 33	declt	$$⊢12<17$$
35	31 34	gtneii	$$⊢17\ne 12$$
36		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
37	35 36	neeqtrri	$$⊢17\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
38	1 37	eqnetri	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
39	28 38	pm3.2i	$$⊢\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$
40	20 39	pm3.2i	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$