Theorem slotsdnscsi

Description: The slots Scalar , .s and .i are different from the slot dist . Formerly part of sralem and proofs using it. (Contributed by AV, 29-Oct-2024)

	Ref	Expression
Assertion	slotsdnscsi	⊢ ( ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )

Proof

Step	Hyp	Ref	Expression
1		5re	⊢ 5 ∈ ℝ
2		1nn	⊢ 1 ∈ ℕ
3		2nn0	⊢ 2 ∈ ℕ0
4		5nn0	⊢ 5 ∈ ℕ0
5		5lt10	⊢ 5 < ; 1 0
6	2 3 4 5	declti	⊢ 5 < ; 1 2
7	1 6	gtneii	⊢ ; 1 2 ≠ 5
8		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
9		scandx	⊢ ( Scalar ‘ ndx ) = 5
10	8 9	neeq12i	⊢ ( ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) ↔ ; 1 2 ≠ 5 )
11	7 10	mpbir	⊢ ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx )
12		6re	⊢ 6 ∈ ℝ
13		6nn0	⊢ 6 ∈ ℕ0
14		6lt10	⊢ 6 < ; 1 0
15	2 3 13 14	declti	⊢ 6 < ; 1 2
16	12 15	gtneii	⊢ ; 1 2 ≠ 6
17		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
18	8 17	neeq12i	⊢ ( ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ↔ ; 1 2 ≠ 6 )
19	16 18	mpbir	⊢ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
20		8re	⊢ 8 ∈ ℝ
21		8nn0	⊢ 8 ∈ ℕ0
22		8lt10	⊢ 8 < ; 1 0
23	2 3 21 22	declti	⊢ 8 < ; 1 2
24	20 23	gtneii	⊢ ; 1 2 ≠ 8
25		ipndx	⊢ ( ·𝑖 ‘ ndx ) = 8
26	8 25	neeq12i	⊢ ( ( dist ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) ↔ ; 1 2 ≠ 8 )
27	24 26	mpbir	⊢ ( dist ‘ ndx ) ≠ ( ·𝑖 ‘ ndx )
28	11 19 27	3pm3.2i	⊢ ( ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )