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

Metamath Proof Explorer

Theorem iccpartltu

Description: If there is a partition, then all intermediate points and the lower bound are strictly less than the upper bound. (Contributed by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartltu ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 0zd ⊢ ( 𝑀 ∈ ℕ → 0 ∈ ℤ )
4 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
5 nngt0 ⊢ ( 𝑀 ∈ ℕ → 0 < 𝑀 )
6 3 4 5 3jca ⊢ ( 𝑀 ∈ ℕ → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
7 1 6 syl ⊢ ( 𝜑 → ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) )
8 fzopred ⊢ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 < 𝑀 ) → ( 0 ..^ 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ..^ 𝑀 ) ) )
9 7 8 syl ⊢ ( 𝜑 → ( 0 ..^ 𝑀 ) = ( { 0 } ∪ ( ( 0 + 1 ) ..^ 𝑀 ) ) )
10 0p1e1 ⊢ ( 0 + 1 ) = 1
11 10 a1i ⊢ ( 𝜑 → ( 0 + 1 ) = 1 )
12 11 oveq1d ⊢ ( 𝜑 → ( ( 0 + 1 ) ..^ 𝑀 ) = ( 1 ..^ 𝑀 ) )
13 12 uneq2d ⊢ ( 𝜑 → ( { 0 } ∪ ( ( 0 + 1 ) ..^ 𝑀 ) ) = ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) )
14 9 13 eqtrd ⊢ ( 𝜑 → ( 0 ..^ 𝑀 ) = ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) )
15 14 eleq2d ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↔ 𝑖 ∈ ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) ) )
16 elun ⊢ ( 𝑖 ∈ ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) ↔ ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) )
17 elsni ⊢ ( 𝑖 ∈ { 0 } → 𝑖 = 0 )
18 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 0 ) )
19 18 adantr ⊢ ( ( 𝑖 = 0 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 0 ) )
20 1 2 iccpartlt ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
21 20 adantl ⊢ ( ( 𝑖 = 0 ∧ 𝜑 ) → ( 𝑃 ‘ 0 ) < ( 𝑃 ‘ 𝑀 ) )
22 19 21 eqbrtrd ⊢ ( ( 𝑖 = 0 ∧ 𝜑 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )
23 22 ex ⊢ ( 𝑖 = 0 → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
24 17 23 syl ⊢ ( 𝑖 ∈ { 0 } → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
25 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑖 ) )
26 25 breq1d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
27 26 rspccv ⊢ ( ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) → ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
28 1 2 iccpartiltu ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ..^ 𝑀 ) ( 𝑃 ‘ 𝑘 ) < ( 𝑃 ‘ 𝑀 ) )
29 27 28 syl11 ⊢ ( 𝑖 ∈ ( 1 ..^ 𝑀 ) → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
30 24 29 jaoi ⊢ ( ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝜑 → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
31 30 com12 ⊢ ( 𝜑 → ( ( 𝑖 ∈ { 0 } ∨ 𝑖 ∈ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
32 16 31 biimtrid ⊢ ( 𝜑 → ( 𝑖 ∈ ( { 0 } ∪ ( 1 ..^ 𝑀 ) ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
33 15 32 sylbid ⊢ ( 𝜑 → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) ) )
34 33 ralrimiv ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ 𝑀 ) )