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 elfzelz ⊢ ( 𝐼 ∈ ( 1 ... 𝑀 ) → 𝐼 ∈ ℤ )
16 3 15 syl ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
17 4 peano2zd ⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℤ )
18 elfzom1b ⊢ ( ( 𝐼 ∈ ℤ ∧ ( 𝑀 + 1 ) ∈ ℤ ) → ( 𝐼 ∈ ( 1 ..^ ( 𝑀 + 1 ) ) ↔ ( 𝐼 − 1 ) ∈ ( 0 ..^ ( ( 𝑀 + 1 ) − 1 ) ) ) )
19 16 17 18 syl2anc ⊢ ( 𝜑 → ( 𝐼 ∈ ( 1 ..^ ( 𝑀 + 1 ) ) ↔ ( 𝐼 − 1 ) ∈ ( 0 ..^ ( ( 𝑀 + 1 ) − 1 ) ) ) )
20 14 19 bitr4d ⊢ ( 𝜑 → ( ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑀 ) ↔ 𝐼 ∈ ( 1 ..^ ( 𝑀 + 1 ) ) ) )
21 8 20 mpbird ⊢ ( 𝜑 → ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑀 ) )
22 iccpartimp ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ ( 𝐼 − 1 ) ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ ( 𝐼 − 1 ) ) < ( 𝑃 ‘ ( ( 𝐼 − 1 ) + 1 ) ) ) )
23 1 2 21 22 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ ( 𝐼 − 1 ) ) < ( 𝑃 ‘ ( ( 𝐼 − 1 ) + 1 ) ) ) )
24 23 simprd ⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝐼 − 1 ) ) < ( 𝑃 ‘ ( ( 𝐼 − 1 ) + 1 ) ) )
25 16 zcnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
26 npcan1 ⊢ ( 𝐼 ∈ ℂ → ( ( 𝐼 − 1 ) + 1 ) = 𝐼 )
27 25 26 syl ⊢ ( 𝜑 → ( ( 𝐼 − 1 ) + 1 ) = 𝐼 )
28 27 eqcomd ⊢ ( 𝜑 → 𝐼 = ( ( 𝐼 − 1 ) + 1 ) )
29 28 fveq2d ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) = ( 𝑃 ‘ ( ( 𝐼 − 1 ) + 1 ) ) )
30 24 29 breqtrrd ⊢ ( 𝜑 → ( 𝑃 ‘ ( 𝐼 − 1 ) ) < ( 𝑃 ‘ 𝐼 ) )