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 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
iccpartgtprec.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑀 ) )
Assertion iccpartgtprec ( 𝜑 → ( 𝑃 ‘ ( 𝐼 − 1 ) ) < ( 𝑃 ‘ 𝐼 ) )

Proof

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