Metamath Proof Explorer

Theorem slotsdifdsndx

Description: The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfun . (Contributed by AV, 11-Nov-2024)

Ref Expression
Assertion slotsdifdsndx 
|- ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) )

Proof

Step Hyp Ref Expression
1 4re 
 |-  4 e. RR
2 1nn 
 |-  1 e. NN
3 2nn0 
 |-  2 e. NN0
4 4nn0 
 |-  4 e. NN0
5 4lt10 
 |-  4 < ; 1 0
6 2 3 4 5 declti 
 |-  4 < ; 1 2
7 1 6 ltneii 
 |-  4 =/= ; 1 2
8 starvndx 
 |-  ( *r ` ndx ) = 4
9 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
10 8 9 neeq12i 
 |-  ( ( *r ` ndx ) =/= ( dist ` ndx ) <-> 4 =/= ; 1 2 )
11 7 10 mpbir 
 |-  ( *r ` ndx ) =/= ( dist ` ndx )
12 10re 
 |-  ; 1 0 e. RR
13 1nn0 
 |-  1 e. NN0
14 0nn0 
 |-  0 e. NN0
15 2nn 
 |-  2 e. NN
16 2pos 
 |-  0 < 2
17 13 14 15 16 declt 
 |-  ; 1 0 < ; 1 2
18 12 17 ltneii 
 |-  ; 1 0 =/= ; 1 2
19 plendx 
 |-  ( le ` ndx ) = ; 1 0
20 19 9 neeq12i 
 |-  ( ( le ` ndx ) =/= ( dist ` ndx ) <-> ; 1 0 =/= ; 1 2 )
21 18 20 mpbir 
 |-  ( le ` ndx ) =/= ( dist ` ndx )
22 11 21 pm3.2i 
 |-  ( ( *r ` ndx ) =/= ( dist ` ndx ) /\ ( le ` ndx ) =/= ( dist ` ndx ) )