Theorem slotsinbpsd

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

	Ref	Expression
Assertion	slotsinbpsd	|- ( ( ( Itv ` ndx ) =/= ( Base ` ndx ) /\ ( Itv ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( Itv ` ndx ) =/= ( .s ` ndx ) /\ ( Itv ` ndx ) =/= ( dist ` ndx ) ) )

Proof

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