Metamath Proof Explorer

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 ) ) )