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	⊢ ( ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) ) )

Proof

Step	Hyp	Ref	Expression
1		itvndx	⊢ ( Itv ‘ ndx ) = ; 1 6
2		1re	⊢ 1 ∈ ℝ
3		1nn	⊢ 1 ∈ ℕ
4		6nn0	⊢ 6 ∈ ℕ0
5		1nn0	⊢ 1 ∈ ℕ0
6		1lt10	⊢ 1 < ; 1 0
7	3 4 5 6	declti	⊢ 1 < ; 1 6
8	2 7	gtneii	⊢ ; 1 6 ≠ 1
9		basendx	⊢ ( Base ‘ ndx ) = 1
10	8 9	neeqtrri	⊢ ; 1 6 ≠ ( Base ‘ ndx )
11	1 10	eqnetri	⊢ ( Itv ‘ ndx ) ≠ ( Base ‘ ndx )
12		2re	⊢ 2 ∈ ℝ
13		2nn0	⊢ 2 ∈ ℕ0
14		2lt10	⊢ 2 < ; 1 0
15	3 4 13 14	declti	⊢ 2 < ; 1 6
16	12 15	gtneii	⊢ ; 1 6 ≠ 2
17		plusgndx	⊢ ( +g ‘ ndx ) = 2
18	16 17	neeqtrri	⊢ ; 1 6 ≠ ( +g ‘ ndx )
19	1 18	eqnetri	⊢ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx )
20	11 19	pm3.2i	⊢ ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) )
21		6re	⊢ 6 ∈ ℝ
22		6lt10	⊢ 6 < ; 1 0
23	3 4 4 22	declti	⊢ 6 < ; 1 6
24	21 23	gtneii	⊢ ; 1 6 ≠ 6
25		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
26	24 25	neeqtrri	⊢ ; 1 6 ≠ ( ·𝑠 ‘ ndx )
27	1 26	eqnetri	⊢ ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
28		2nn	⊢ 2 ∈ ℕ
29	5 28	decnncl	⊢ ; 1 2 ∈ ℕ
30	29	nnrei	⊢ ; 1 2 ∈ ℝ
31		6nn	⊢ 6 ∈ ℕ
32		2lt6	⊢ 2 < 6
33	5 13 31 32	declt	⊢ ; 1 2 < ; 1 6
34	30 33	gtneii	⊢ ; 1 6 ≠ ; 1 2
35		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
36	34 35	neeqtrri	⊢ ; 1 6 ≠ ( dist ‘ ndx )
37	1 36	eqnetri	⊢ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx )
38	27 37	pm3.2i	⊢ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) )
39	20 38	pm3.2i	⊢ ( ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) ) )