Description: The slot for the scalar is not the index of other slots. Formerly part of proof for srasca and sravsca . (Contributed by AV, 12-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | slotsdifipndx | |- ( ( .s ` ndx ) =/= ( .i ` ndx ) /\ ( Scalar ` ndx ) =/= ( .i ` ndx ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 6re | |- 6 e. RR |
|
| 2 | 6lt8 | |- 6 < 8 |
|
| 3 | 1 2 | ltneii | |- 6 =/= 8 |
| 4 | vscandx | |- ( .s ` ndx ) = 6 |
|
| 5 | ipndx | |- ( .i ` ndx ) = 8 |
|
| 6 | 4 5 | neeq12i | |- ( ( .s ` ndx ) =/= ( .i ` ndx ) <-> 6 =/= 8 ) |
| 7 | 3 6 | mpbir | |- ( .s ` ndx ) =/= ( .i ` ndx ) |
| 8 | 5re | |- 5 e. RR |
|
| 9 | 5lt8 | |- 5 < 8 |
|
| 10 | 8 9 | ltneii | |- 5 =/= 8 |
| 11 | scandx | |- ( Scalar ` ndx ) = 5 |
|
| 12 | 11 5 | neeq12i | |- ( ( Scalar ` ndx ) =/= ( .i ` ndx ) <-> 5 =/= 8 ) |
| 13 | 10 12 | mpbir | |- ( Scalar ` ndx ) =/= ( .i ` ndx ) |
| 14 | 7 13 | pm3.2i | |- ( ( .s ` ndx ) =/= ( .i ` ndx ) /\ ( Scalar ` ndx ) =/= ( .i ` ndx ) ) |