Theorem slotslnbpsd

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

	Ref	Expression
Assertion	slotslnbpsd	⊢ ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( dist ‘ ndx ) ) )

Proof

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