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

Metamath Proof Explorer

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 ) ) )