This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 < 10
6 2 3 4 5 declti ⊢ 5 < 12
7 1 6 gtneii ⊢ 12 ≠ 5
8 dsndx ⊢ dist ⁡ ndx = 12
9 scandx ⊢ Scalar ⁡ ndx = 5
10 8 9 neeq12i ⊢ dist ⁡ ndx ≠ Scalar ⁡ ndx ↔ 12 ≠ 5
11 7 10 mpbir ⊢ dist ⁡ ndx ≠ Scalar ⁡ ndx
12 6re ⊢ 6 ∈ ℝ
13 6nn0 ⊢ 6 ∈ ℕ 0
14 6lt10 ⊢ 6 < 10
15 2 3 13 14 declti ⊢ 6 < 12
16 12 15 gtneii ⊢ 12 ≠ 6
17 vscandx ⊢ ⋅ ndx = 6
18 8 17 neeq12i ⊢ dist ⁡ ndx ≠ ⋅ ndx ↔ 12 ≠ 6
19 16 18 mpbir ⊢ dist ⁡ ndx ≠ ⋅ ndx
20 8re ⊢ 8 ∈ ℝ
21 8nn0 ⊢ 8 ∈ ℕ 0
22 8lt10 ⊢ 8 < 10
23 2 3 21 22 declti ⊢ 8 < 12
24 20 23 gtneii ⊢ 12 ≠ 8
25 ipndx ⊢ ⋅ 𝑖 ⁡ ndx = 8
26 8 25 neeq12i ⊢ dist ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx ↔ 12 ≠ 8
27 24 26 mpbir ⊢ dist ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx
28 11 19 27 3pm3.2i ⊢ dist ⁡ ndx ≠ Scalar ⁡ ndx ∧ dist ⁡ ndx ≠ ⋅ ndx ∧ dist ⁡ ndx ≠ ⋅ 𝑖 ⁡ ndx