Theorem lngndxnitvndx

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	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{Itv}\left(\mathrm{ndx}\right)$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		6nn	$$⊢6\in \mathbb{N}$$
3	1 2	decnncl	$$⊢16\in \mathbb{N}$$
4	3	nnrei	$$⊢16\in ℝ$$
5		6nn0	$$⊢6\in {\mathbb{N}}_0$$
6		7nn	$$⊢7\in \mathbb{N}$$
7		6lt7	$$⊢6<7$$
8	1 5 6 7	declt	$$⊢16<17$$
9	4 8	gtneii	$$⊢17\ne 16$$
10		lngndx	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)=17$$
11		itvndx	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)=16$$
12	10 11	neeq12i	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{Itv}\left(\mathrm{ndx}\right)\leftrightarrow 17\ne 16$$
13	9 12	mpbir	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{Itv}\left(\mathrm{ndx}\right)$$