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	|- ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) )

Proof

Step	Hyp	Ref	Expression
1		lngndx	|- ( LineG ` ndx ) = ; 1 7
2		1re	|- 1 e. RR
3		1nn	|- 1 e. NN
4		7nn0	|- 7 e. NN0
5		1nn0	|- 1 e. NN0
6		1lt10	|- 1 < ; 1 0
7	3 4 5 6	declti	|- 1 < ; 1 7
8	2 7	gtneii	|- ; 1 7 =/= 1
9		basendx	|- ( Base ` ndx ) = 1
10	8 9	neeqtrri	|- ; 1 7 =/= ( Base ` ndx )
11	1 10	eqnetri	|- ( LineG ` ndx ) =/= ( Base ` ndx )
12		2re	|- 2 e. RR
13		2nn0	|- 2 e. NN0
14		2lt10	|- 2 < ; 1 0
15	3 4 13 14	declti	|- 2 < ; 1 7
16	12 15	gtneii	|- ; 1 7 =/= 2
17		plusgndx	|- ( +g ` ndx ) = 2
18	16 17	neeqtrri	|- ; 1 7 =/= ( +g ` ndx )
19	1 18	eqnetri	|- ( LineG ` ndx ) =/= ( +g ` ndx )
20	11 19	pm3.2i	|- ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) )
21		6re	|- 6 e. RR
22		6nn0	|- 6 e. NN0
23		6lt10	|- 6 < ; 1 0
24	3 4 22 23	declti	|- 6 < ; 1 7
25	21 24	gtneii	|- ; 1 7 =/= 6
26		vscandx	|- ( .s ` ndx ) = 6
27	25 26	neeqtrri	|- ; 1 7 =/= ( .s ` ndx )
28	1 27	eqnetri	|- ( LineG ` ndx ) =/= ( .s ` ndx )
29		2nn	|- 2 e. NN
30	5 29	decnncl	|- ; 1 2 e. NN
31	30	nnrei	|- ; 1 2 e. RR
32		7nn	|- 7 e. NN
33		2lt7	|- 2 < 7
34	5 13 32 33	declt	|- ; 1 2 < ; 1 7
35	31 34	gtneii	|- ; 1 7 =/= ; 1 2
36		dsndx	|- ( dist ` ndx ) = ; 1 2
37	35 36	neeqtrri	|- ; 1 7 =/= ( dist ` ndx )
38	1 37	eqnetri	|- ( LineG ` ndx ) =/= ( dist ` ndx )
39	28 38	pm3.2i	|- ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) )
40	20 39	pm3.2i	|- ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) )