Metamath Proof Explorer

Theorem iccpartgtprec

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

Ref Expression
Hypotheses iccpartgtprec.m ⊢ φ → M ∈ ℕ
iccpartgtprec.p ⊢ φ → P ∈ RePart ⁡ M
iccpartgtprec.i ⊢ φ → I ∈ 1 … M
Assertion iccpartgtprec ⊢ φ → P ⁡ I − 1 < P ⁡ I

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ φ → M ∈ ℕ
2 iccpartgtprec.p ⊢ φ → P ∈ RePart ⁡ M
3 iccpartgtprec.i ⊢ φ → I ∈ 1 … M
4 1 nnzd ⊢ φ → M ∈ ℤ
5 fzval3 ⊢ M ∈ ℤ → 1 … M = 1 ..^ M + 1
6 5 eleq2d ⊢ M ∈ ℤ → I ∈ 1 … M ↔ I ∈ 1 ..^ M + 1
7 4 6 syl ⊢ φ → I ∈ 1 … M ↔ I ∈ 1 ..^ M + 1
8 3 7 mpbid ⊢ φ → I ∈ 1 ..^ M + 1
9 1 nncnd ⊢ φ → M ∈ ℂ
10 pncan1 ⊢ M ∈ ℂ → M + 1 - 1 = M
11 9 10 syl ⊢ φ → M + 1 - 1 = M
12 11 eqcomd ⊢ φ → M = M + 1 - 1
13 12 oveq2d ⊢ φ → 0 ..^ M = 0 ..^ M + 1 - 1
14 13 eleq2d ⊢ φ → I − 1 ∈ 0 ..^ M ↔ I − 1 ∈ 0 ..^ M + 1 - 1
15 elfzelz ⊢ I ∈ 1 … M → I ∈ ℤ
16 3 15 syl ⊢ φ → I ∈ ℤ
17 4 peano2zd ⊢ φ → M + 1 ∈ ℤ
18 elfzom1b ⊢ I ∈ ℤ ∧ M + 1 ∈ ℤ → I ∈ 1 ..^ M + 1 ↔ I − 1 ∈ 0 ..^ M + 1 - 1
19 16 17 18 syl2anc ⊢ φ → I ∈ 1 ..^ M + 1 ↔ I − 1 ∈ 0 ..^ M + 1 - 1
20 14 19 bitr4d ⊢ φ → I − 1 ∈ 0 ..^ M ↔ I ∈ 1 ..^ M + 1
21 8 20 mpbird ⊢ φ → I − 1 ∈ 0 ..^ M
22 iccpartimp ⊢ M ∈ ℕ ∧ P ∈ RePart ⁡ M ∧ I − 1 ∈ 0 ..^ M → P ∈ ℝ * 0 … M ∧ P ⁡ I − 1 < P ⁡ I - 1 + 1
23 1 2 21 22 syl3anc ⊢ φ → P ∈ ℝ * 0 … M ∧ P ⁡ I − 1 < P ⁡ I - 1 + 1
24 23 simprd ⊢ φ → P ⁡ I − 1 < P ⁡ I - 1 + 1
25 16 zcnd ⊢ φ → I ∈ ℂ
26 npcan1 ⊢ I ∈ ℂ → I - 1 + 1 = I
27 25 26 syl ⊢ φ → I - 1 + 1 = I
28 27 eqcomd ⊢ φ → I = I - 1 + 1
29 28 fveq2d ⊢ φ → P ⁡ I = P ⁡ I - 1 + 1
30 24 29 breqtrrd ⊢ φ → P ⁡ I − 1 < P ⁡ I