Metamath Proof Explorer

Theorem slotsdnscsi

Description: The slots Scalar , .s and .i are different from the slot dist . Formerly part of sralem and proofs using it. (Contributed by AV, 29-Oct-2024)

Ref Expression
Assertion slotsdnscsi 
|- ( ( dist ` ndx ) =/= ( Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )

Proof

Step Hyp Ref Expression
1 5re 
 |-  5 e. RR
2 1nn 
 |-  1 e. NN
3 2nn0 
 |-  2 e. NN0
4 5nn0 
 |-  5 e. NN0
5 5lt10 
 |-  5 < ; 1 0
6 2 3 4 5 declti 
 |-  5 < ; 1 2
7 1 6 gtneii 
 |-  ; 1 2 =/= 5
8 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
9 scandx 
 |-  ( Scalar ` ndx ) = 5
10 8 9 neeq12i 
 |-  ( ( dist ` ndx ) =/= ( Scalar ` ndx ) <-> ; 1 2 =/= 5 )
11 7 10 mpbir 
 |-  ( dist ` ndx ) =/= ( Scalar ` ndx )
12 6re 
 |-  6 e. RR
13 6nn0 
 |-  6 e. NN0
14 6lt10 
 |-  6 < ; 1 0
15 2 3 13 14 declti 
 |-  6 < ; 1 2
16 12 15 gtneii 
 |-  ; 1 2 =/= 6
17 vscandx 
 |-  ( .s ` ndx ) = 6
18 8 17 neeq12i 
 |-  ( ( dist ` ndx ) =/= ( .s ` ndx ) <-> ; 1 2 =/= 6 )
19 16 18 mpbir 
 |-  ( dist ` ndx ) =/= ( .s ` ndx )
20 8re 
 |-  8 e. RR
21 8nn0 
 |-  8 e. NN0
22 8lt10 
 |-  8 < ; 1 0
23 2 3 21 22 declti 
 |-  8 < ; 1 2
24 20 23 gtneii 
 |-  ; 1 2 =/= 8
25 ipndx 
 |-  ( .i ` ndx ) = 8
26 8 25 neeq12i 
 |-  ( ( dist ` ndx ) =/= ( .i ` ndx ) <-> ; 1 2 =/= 8 )
27 24 26 mpbir 
 |-  ( dist ` ndx ) =/= ( .i ` ndx )
28 11 19 27 3pm3.2i 
 |-  ( ( dist ` ndx ) =/= ( Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )