Theorem slotsdifdsndx

Description: The index of the slot for the distance is not the index of other slots. Formerly part of proof for cnfldfun . (Contributed by AV, 11-Nov-2024)

	Ref	Expression
Assertion	slotsdifdsndx	⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) )

Proof

Step	Hyp	Ref	Expression
1		4re	⊢ 4 ∈ ℝ
2		1nn	⊢ 1 ∈ ℕ
3		2nn0	⊢ 2 ∈ ℕ0
4		4nn0	⊢ 4 ∈ ℕ0
5		4lt10	⊢ 4 < ; 1 0
6	2 3 4 5	declti	⊢ 4 < ; 1 2
7	1 6	ltneii	⊢ 4 ≠ ; 1 2
8		starvndx	⊢ ( *𝑟 ‘ ndx ) = 4
9		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
10	8 9	neeq12i	⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ↔ 4 ≠ ; 1 2 )
11	7 10	mpbir	⊢ ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx )
12		10re	⊢ ; 1 0 ∈ ℝ
13		1nn0	⊢ 1 ∈ ℕ0
14		0nn0	⊢ 0 ∈ ℕ0
15		2nn	⊢ 2 ∈ ℕ
16		2pos	⊢ 0 < 2
17	13 14 15 16	declt	⊢ ; 1 0 < ; 1 2
18	12 17	ltneii	⊢ ; 1 0 ≠ ; 1 2
19		plendx	⊢ ( le ‘ ndx ) = ; 1 0
20	19 9	neeq12i	⊢ ( ( le ‘ ndx ) ≠ ( dist ‘ ndx ) ↔ ; 1 0 ≠ ; 1 2 )
21	18 20	mpbir	⊢ ( le ‘ ndx ) ≠ ( dist ‘ ndx )
22	11 21	pm3.2i	⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) )