Description: The slot for the line is not the slot for the Interval (segment) in an extensible structure. Formerly part of proof for ttgval . (Contributed by AV, 9-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lngndxnitvndx | |- ( LineG ` ndx ) =/= ( Itv ` ndx ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1nn0 | |- 1 e. NN0 |
|
| 2 | 6nn | |- 6 e. NN |
|
| 3 | 1 2 | decnncl | |- ; 1 6 e. NN |
| 4 | 3 | nnrei | |- ; 1 6 e. RR |
| 5 | 6nn0 | |- 6 e. NN0 |
|
| 6 | 7nn | |- 7 e. NN |
|
| 7 | 6lt7 | |- 6 < 7 |
|
| 8 | 1 5 6 7 | declt | |- ; 1 6 < ; 1 7 |
| 9 | 4 8 | gtneii | |- ; 1 7 =/= ; 1 6 |
| 10 | lngndx | |- ( LineG ` ndx ) = ; 1 7 |
|
| 11 | itvndx | |- ( Itv ` ndx ) = ; 1 6 |
|
| 12 | 10 11 | neeq12i | |- ( ( LineG ` ndx ) =/= ( Itv ` ndx ) <-> ; 1 7 =/= ; 1 6 ) |
| 13 | 9 12 | mpbir | |- ( LineG ` ndx ) =/= ( Itv ` ndx ) |