| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iccpartgtprec.m | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 2 | 1 | nnnn0d 12589 | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 3 |  | elnn0uz 12924 | . . . . . . 7
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈
(ℤ≥‘0)) | 
| 4 | 2, 3 | sylib 218 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) | 
| 5 |  | fzpred 13613 | . . . . . 6
⊢ (𝑀 ∈
(ℤ≥‘0) → (0...𝑀) = ({0} ∪ ((0 + 1)...𝑀))) | 
| 6 | 4, 5 | syl 17 | . . . . 5
⊢ (𝜑 → (0...𝑀) = ({0} ∪ ((0 + 1)...𝑀))) | 
| 7 | 6 | eleq2d 2826 | . . . 4
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) ↔ 𝑖 ∈ ({0} ∪ ((0 + 1)...𝑀)))) | 
| 8 |  | elun 4152 | . . . . 5
⊢ (𝑖 ∈ ({0} ∪ ((0 +
1)...𝑀)) ↔ (𝑖 ∈ {0} ∨ 𝑖 ∈ ((0 + 1)...𝑀))) | 
| 9 | 8 | a1i 11 | . . . 4
⊢ (𝜑 → (𝑖 ∈ ({0} ∪ ((0 + 1)...𝑀)) ↔ (𝑖 ∈ {0} ∨ 𝑖 ∈ ((0 + 1)...𝑀)))) | 
| 10 |  | velsn 4641 | . . . . . 6
⊢ (𝑖 ∈ {0} ↔ 𝑖 = 0) | 
| 11 | 10 | a1i 11 | . . . . 5
⊢ (𝜑 → (𝑖 ∈ {0} ↔ 𝑖 = 0)) | 
| 12 |  | 0p1e1 12389 | . . . . . . . 8
⊢ (0 + 1) =
1 | 
| 13 | 12 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (0 + 1) =
1) | 
| 14 | 13 | oveq1d 7447 | . . . . . 6
⊢ (𝜑 → ((0 + 1)...𝑀) = (1...𝑀)) | 
| 15 | 14 | eleq2d 2826 | . . . . 5
⊢ (𝜑 → (𝑖 ∈ ((0 + 1)...𝑀) ↔ 𝑖 ∈ (1...𝑀))) | 
| 16 | 11, 15 | orbi12d 918 | . . . 4
⊢ (𝜑 → ((𝑖 ∈ {0} ∨ 𝑖 ∈ ((0 + 1)...𝑀)) ↔ (𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)))) | 
| 17 | 7, 9, 16 | 3bitrd 305 | . . 3
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) ↔ (𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)))) | 
| 18 |  | iccpartgtprec.p | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) | 
| 19 |  | 0elfz 13665 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ 0 ∈ (0...𝑀)) | 
| 20 | 2, 19 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 0 ∈ (0...𝑀)) | 
| 21 | 1, 18, 20 | iccpartxr 47411 | . . . . . . 7
⊢ (𝜑 → (𝑃‘0) ∈
ℝ*) | 
| 22 | 21 | xrleidd 13195 | . . . . . 6
⊢ (𝜑 → (𝑃‘0) ≤ (𝑃‘0)) | 
| 23 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑖 = 0 → (𝑃‘𝑖) = (𝑃‘0)) | 
| 24 | 23 | breq2d 5154 | . . . . . 6
⊢ (𝑖 = 0 → ((𝑃‘0) ≤ (𝑃‘𝑖) ↔ (𝑃‘0) ≤ (𝑃‘0))) | 
| 25 | 22, 24 | imbitrrid 246 | . . . . 5
⊢ (𝑖 = 0 → (𝜑 → (𝑃‘0) ≤ (𝑃‘𝑖))) | 
| 26 | 21 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) ∈
ℝ*) | 
| 27 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑀 ∈ ℕ) | 
| 28 | 18 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑃 ∈ (RePart‘𝑀)) | 
| 29 |  | 1nn0 12544 | . . . . . . . . . . . 12
⊢ 1 ∈
ℕ0 | 
| 30 | 29 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 31 |  | elnn0uz 12924 | . . . . . . . . . . 11
⊢ (1 ∈
ℕ0 ↔ 1 ∈
(ℤ≥‘0)) | 
| 32 | 30, 31 | sylib 218 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
(ℤ≥‘0)) | 
| 33 |  | fzss1 13604 | . . . . . . . . . 10
⊢ (1 ∈
(ℤ≥‘0) → (1...𝑀) ⊆ (0...𝑀)) | 
| 34 | 32, 33 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (1...𝑀) ⊆ (0...𝑀)) | 
| 35 | 34 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀)) | 
| 36 | 27, 28, 35 | iccpartxr 47411 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) ∈
ℝ*) | 
| 37 | 1, 18 | iccpartgtl 47418 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑃‘0) < (𝑃‘𝑘)) | 
| 38 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑃‘𝑘) = (𝑃‘𝑖)) | 
| 39 | 38 | breq2d 5154 | . . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((𝑃‘0) < (𝑃‘𝑘) ↔ (𝑃‘0) < (𝑃‘𝑖))) | 
| 40 | 39 | rspccv 3618 | . . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑀)(𝑃‘0) < (𝑃‘𝑘) → (𝑖 ∈ (1...𝑀) → (𝑃‘0) < (𝑃‘𝑖))) | 
| 41 | 37, 40 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (1...𝑀) → (𝑃‘0) < (𝑃‘𝑖))) | 
| 42 | 41 | imp 406 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) < (𝑃‘𝑖)) | 
| 43 | 26, 36, 42 | xrltled 13193 | . . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖)) | 
| 44 | 43 | expcom 413 | . . . . 5
⊢ (𝑖 ∈ (1...𝑀) → (𝜑 → (𝑃‘0) ≤ (𝑃‘𝑖))) | 
| 45 | 25, 44 | jaoi 857 | . . . 4
⊢ ((𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)) → (𝜑 → (𝑃‘0) ≤ (𝑃‘𝑖))) | 
| 46 | 45 | com12 32 | . . 3
⊢ (𝜑 → ((𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖))) | 
| 47 | 17, 46 | sylbid 240 | . 2
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) → (𝑃‘0) ≤ (𝑃‘𝑖))) | 
| 48 | 47 | ralrimiv 3144 | 1
⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑖)) |