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 3 elfzelzd ⊢ φ → I ∈ ℤ
16 4 peano2zd ⊢ φ → M + 1 ∈ ℤ
17 elfzom1b ⊢ I ∈ ℤ ∧ M + 1 ∈ ℤ → I ∈ 1 ..^ M + 1 ↔ I − 1 ∈ 0 ..^ M + 1 - 1
18 15 16 17 syl2anc ⊢ φ → I ∈ 1 ..^ M + 1 ↔ I − 1 ∈ 0 ..^ M + 1 - 1
19 14 18 bitr4d ⊢ φ → I − 1 ∈ 0 ..^ M ↔ I ∈ 1 ..^ M + 1
20 8 19 mpbird ⊢ φ → I − 1 ∈ 0 ..^ M
21 iccpartimp ⊢ M ∈ ℕ ∧ P ∈ RePart ⁡ M ∧ I − 1 ∈ 0 ..^ M → P ∈ ℝ * 0 … M ∧ P ⁡ I − 1 < P ⁡ I - 1 + 1
22 1 2 20 21 syl3anc ⊢ φ → P ∈ ℝ * 0 … M ∧ P ⁡ I − 1 < P ⁡ I - 1 + 1
23 22 simprd ⊢ φ → P ⁡ I − 1 < P ⁡ I - 1 + 1
24 15 zcnd ⊢ φ → I ∈ ℂ
25 npcan1 ⊢ I ∈ ℂ → I - 1 + 1 = I
26 24 25 syl ⊢ φ → I - 1 + 1 = I
27 26 eqcomd ⊢ φ → I = I - 1 + 1
28 27 fveq2d ⊢ φ → P ⁡ I = P ⁡ I - 1 + 1
29 23 28 breqtrrd ⊢ φ → P ⁡ I − 1 < P ⁡ I