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 ∈ ℕ0 | |
| 2 | 6nn | ⊢ 6 ∈ ℕ | |
| 3 | 1 2 | decnncl | ⊢ ; 1 6 ∈ ℕ |
| 4 | 3 | nnrei | ⊢ ; 1 6 ∈ ℝ |
| 5 | 6nn0 | ⊢ 6 ∈ ℕ0 | |
| 6 | 7nn | ⊢ 7 ∈ ℕ | |
| 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 ) |