Theorem slotsdifunifndx

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

	Ref	Expression
Assertion	slotsdifunifndx	⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) ∧ ( ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) )

Proof

Step	Hyp	Ref	Expression
1		2re	⊢ 2 ∈ ℝ
2		1nn	⊢ 1 ∈ ℕ
3		3nn0	⊢ 3 ∈ ℕ0
4		2nn0	⊢ 2 ∈ ℕ0
5		2lt10	⊢ 2 < ; 1 0
6	2 3 4 5	declti	⊢ 2 < ; 1 3
7	1 6	ltneii	⊢ 2 ≠ ; 1 3
8		plusgndx	⊢ ( +g ‘ ndx ) = 2
9		unifndx	⊢ ( UnifSet ‘ ndx ) = ; 1 3
10	8 9	neeq12i	⊢ ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ↔ 2 ≠ ; 1 3 )
11	7 10	mpbir	⊢ ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx )
12		3re	⊢ 3 ∈ ℝ
13		3lt10	⊢ 3 < ; 1 0
14	2 3 3 13	declti	⊢ 3 < ; 1 3
15	12 14	ltneii	⊢ 3 ≠ ; 1 3
16		mulrndx	⊢ ( .r ‘ ndx ) = 3
17	16 9	neeq12i	⊢ ( ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ↔ 3 ≠ ; 1 3 )
18	15 17	mpbir	⊢ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx )
19		4re	⊢ 4 ∈ ℝ
20		4nn0	⊢ 4 ∈ ℕ0
21		4lt10	⊢ 4 < ; 1 0
22	2 3 20 21	declti	⊢ 4 < ; 1 3
23	19 22	ltneii	⊢ 4 ≠ ; 1 3
24		starvndx	⊢ ( *𝑟 ‘ ndx ) = 4
25	24 9	neeq12i	⊢ ( ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ↔ 4 ≠ ; 1 3 )
26	23 25	mpbir	⊢ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx )
27	11 18 26	3pm3.2i	⊢ ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) )
28		10re	⊢ ; 1 0 ∈ ℝ
29		1nn0	⊢ 1 ∈ ℕ0
30		0nn0	⊢ 0 ∈ ℕ0
31		3nn	⊢ 3 ∈ ℕ
32		3pos	⊢ 0 < 3
33	29 30 31 32	declt	⊢ ; 1 0 < ; 1 3
34	28 33	ltneii	⊢ ; 1 0 ≠ ; 1 3
35		plendx	⊢ ( le ‘ ndx ) = ; 1 0
36	35 9	neeq12i	⊢ ( ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ↔ ; 1 0 ≠ ; 1 3 )
37	34 36	mpbir	⊢ ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx )
38		2nn	⊢ 2 ∈ ℕ
39	29 38	decnncl	⊢ ; 1 2 ∈ ℕ
40	39	nnrei	⊢ ; 1 2 ∈ ℝ
41		2lt3	⊢ 2 < 3
42	29 4 31 41	declt	⊢ ; 1 2 < ; 1 3
43	40 42	ltneii	⊢ ; 1 2 ≠ ; 1 3
44		dsndx	⊢ ( dist ‘ ndx ) = ; 1 2
45	44 9	neeq12i	⊢ ( ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ↔ ; 1 2 ≠ ; 1 3 )
46	43 45	mpbir	⊢ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx )
47	37 46	pm3.2i	⊢ ( ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) )
48	27 47	pm3.2i	⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) ∧ ( ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) )