Theorem slotsinbpsd

Description: The slots Base , +g , .s and dist are different from the slot Itv . Formerly part of ttglem and proofs using it. (Contributed by AV, 29-Oct-2024)

	Ref	Expression
Assertion	slotsinbpsd	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		itvndx	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)=16$$
2		1re	$$⊢1\in ℝ$$
3		1nn	$$⊢1\in \mathbb{N}$$
4		6nn0	$$⊢6\in {\mathbb{N}}_0$$
5		1nn0	$$⊢1\in {\mathbb{N}}_0$$
6		1lt10	$$⊢1<10$$
7	3 4 5 6	declti	$$⊢1<16$$
8	2 7	gtneii	$$⊢16\ne 1$$
9		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
10	8 9	neeqtrri	$$⊢16\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
11	1 10	eqnetri	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
12		2re	$$⊢2\in ℝ$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14		2lt10	$$⊢2<10$$
15	3 4 13 14	declti	$$⊢2<16$$
16	12 15	gtneii	$$⊢16\ne 2$$
17		plusgndx	$$⊢{+}_{\mathrm{ndx}}=2$$
18	16 17	neeqtrri	$$⊢16\ne {+}_{\mathrm{ndx}}$$
19	1 18	eqnetri	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
20	11 19	pm3.2i	$$⊢\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)$$
21		6re	$$⊢6\in ℝ$$
22		6lt10	$$⊢6<10$$
23	3 4 4 22	declti	$$⊢6<16$$
24	21 23	gtneii	$$⊢16\ne 6$$
25		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
26	24 25	neeqtrri	$$⊢16\ne {\cdot }_{\mathrm{ndx}}$$
27	1 26	eqnetri	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
28		2nn	$$⊢2\in \mathbb{N}$$
29	5 28	decnncl	$$⊢12\in \mathbb{N}$$
30	29	nnrei	$$⊢12\in ℝ$$
31		6nn	$$⊢6\in \mathbb{N}$$
32		2lt6	$$⊢2<6$$
33	5 13 31 32	declt	$$⊢12<16$$
34	30 33	gtneii	$$⊢16\ne 12$$
35		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
36	34 35	neeqtrri	$$⊢16\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
37	1 36	eqnetri	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
38	27 37	pm3.2i	$$⊢\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)$$
39	20 38	pm3.2i	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$