Theorem slotsdifunifndx

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

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

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2		1nn	$$⊢1\in \mathbb{N}$$
3		3nn0	$$⊢3\in {\mathbb{N}}_0$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		2lt10	$$⊢2<10$$
6	2 3 4 5	declti	$$⊢2<13$$
7	1 6	ltneii	$$⊢2\ne 13$$
8		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
9		unifndx	$$⊢\mathrm{UnifSet}\left(\mathrm{ndx}\right)=13$$
10	8 9	neeq12i	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\leftrightarrow 2\ne 13$$
11	7 10	mpbir	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
12		3re	$$⊢3\in ℝ$$
13		3lt10	$$⊢3<10$$
14	2 3 3 13	declti	$$⊢3<13$$
15	12 14	ltneii	$$⊢3\ne 13$$
16		mulrndx	$$⊢{\cdot }_{\mathrm{ndx}}=3$$
17	16 9	neeq12i	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\leftrightarrow 3\ne 13$$
18	15 17	mpbir	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
19		4re	$$⊢4\in ℝ$$
20		4nn0	$$⊢4\in {\mathbb{N}}_0$$
21		4lt10	$$⊢4<10$$
22	2 3 20 21	declti	$$⊢4<13$$
23	19 22	ltneii	$$⊢4\ne 13$$
24		starvndx	$$⊢{\mathrm{*}}_{\mathrm{ndx}}=4$$
25	24 9	neeq12i	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\leftrightarrow 4\ne 13$$
26	23 25	mpbir	$$⊢{\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
27	11 18 26	3pm3.2i	$$⊢\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
28		10re	$$⊢10\in ℝ$$
29		1nn0	$$⊢1\in {\mathbb{N}}_0$$
30		0nn0	$$⊢0\in {\mathbb{N}}_0$$
31		3nn	$$⊢3\in \mathbb{N}$$
32		3pos	$$⊢0<3$$
33	29 30 31 32	declt	$$⊢10<13$$
34	28 33	ltneii	$$⊢10\ne 13$$
35		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
36	35 9	neeq12i	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\leftrightarrow 10\ne 13$$
37	34 36	mpbir	$$⊢{\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
38		2nn	$$⊢2\in \mathbb{N}$$
39	29 38	decnncl	$$⊢12\in \mathbb{N}$$
40	39	nnrei	$$⊢12\in ℝ$$
41		2lt3	$$⊢2<3$$
42	29 4 31 41	declt	$$⊢12<13$$
43	40 42	ltneii	$$⊢12\ne 13$$
44		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
45	44 9	neeq12i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\leftrightarrow 12\ne 13$$
46	43 45	mpbir	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)$$
47	37 46	pm3.2i	$$⊢\left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)$$
48	27 47	pm3.2i	$$⊢\left(\left({+}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\cdot }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge {\mathrm{*}}_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\wedge \left({\le }_{\mathrm{ndx}}\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{UnifSet}\left(\mathrm{ndx}\right)\right)\right)$$