Theorem slotsdifdsndx

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

	Ref	Expression
Assertion	slotsdifdsndx	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		4re	$$⊢4\in ℝ$$
2		1nn	$$⊢1\in \mathbb{N}$$
3		2nn0	$$⊢2\in {\mathbb{N}}_0$$
4		4nn0	$$⊢4\in {\mathbb{N}}_0$$
5		4lt10	$$⊢4<10$$
6	2 3 4 5	declti	$$⊢4<12$$
7	1 6	ltneii	$$⊢4\ne 12$$
8		starvndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}=4$$
9		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
10	8 9	neeq12i	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\leftrightarrow 4\ne 12$$
11	7 10	mpbir	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
12		10re	$$⊢10\in ℝ$$
13		1nn0	$$⊢1\in {\mathbb{N}}_0$$
14		0nn0	$$⊢0\in {\mathbb{N}}_0$$
15		2nn	$$⊢2\in \mathbb{N}$$
16		2pos	$$⊢0<2$$
17	13 14 15 16	declt	$$⊢10<12$$
18	12 17	ltneii	$$⊢10\ne 12$$
19		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
20	19 9	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 12$$
21	18 20	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
22	11 21	pm3.2i	$$⊢\left({\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\wedge {\le }_{\mathrm{ndx}}\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$