slotsdifdsndx

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

		Ref	Expression
	Assertion	slotsdifdsndx	$⊢ (*_{ndx} \neq dist (ndx) \land \leq_{ndx} \neq dist (ndx))$

Proof

Step	Hyp	Ref	Expression
1		4re	$⊢ 4 \in ℝ$
2		1nn	$⊢ 1 \in ℕ$
3		2nn0	$⊢ 2 \in ℕ_{0}$
4		4nn0	$⊢ 4 \in ℕ_{0}$
5		4lt10	$⊢ 4 < 10$
6	2 3 4 5	declti	$⊢ 4 < 12$
7	1 6	ltneii	$⊢ 4 \neq 12$
8		starvndx	$⊢ *_{ndx} = 4$
9		dsndx	$⊢ dist (ndx) = 12$
10	8 9	neeq12i	$⊢ *_{ndx} \neq dist (ndx) \leftrightarrow 4 \neq 12$
11	7 10	mpbir	$⊢ *_{ndx} \neq dist (ndx)$
12		10re	$⊢ 10 \in ℝ$
13		1nn0	$⊢ 1 \in ℕ_{0}$
14		0nn0	$⊢ 0 \in ℕ_{0}$
15		2nn	$⊢ 2 \in ℕ$
16		2pos	$⊢ 0 < 2$
17	13 14 15 16	declt	$⊢ 10 < 12$
18	12 17	ltneii	$⊢ 10 \neq 12$
19		plendx	$⊢ \leq_{ndx} = 10$
20	19 9	neeq12i	$⊢ \leq_{ndx} \neq dist (ndx) \leftrightarrow 10 \neq 12$
21	18 20	mpbir	$⊢ \leq_{ndx} \neq dist (ndx)$
22	11 21	pm3.2i	$⊢ (*_{ndx} \neq dist (ndx) \land \leq_{ndx} \neq dist (ndx))$

Metamath Proof Explorer

Theorem slotsdifdsndx

Proof