| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | iccpartgtprec.m | . . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 2 |  | iccpartgtprec.p | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) | 
| 3 |  | lbfzo0 13740 | . . . . . . . 8
⊢ (0 ∈
(0..^𝑀) ↔ 𝑀 ∈
ℕ) | 
| 4 | 1, 3 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → 0 ∈ (0..^𝑀)) | 
| 5 |  | iccpartimp 47409 | . . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘𝑀) ∧ 0 ∈ (0..^𝑀)) → (𝑃 ∈ (ℝ*
↑m (0...𝑀))
∧ (𝑃‘0) <
(𝑃‘(0 +
1)))) | 
| 6 | 1, 2, 4, 5 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → (𝑃 ∈ (ℝ*
↑m (0...𝑀))
∧ (𝑃‘0) <
(𝑃‘(0 +
1)))) | 
| 7 | 6 | simprd 495 | . . . . 5
⊢ (𝜑 → (𝑃‘0) < (𝑃‘(0 + 1))) | 
| 8 | 7 | adantl 481 | . . . 4
⊢ ((𝑀 = 1 ∧ 𝜑) → (𝑃‘0) < (𝑃‘(0 + 1))) | 
| 9 |  | fveq2 6905 | . . . . . 6
⊢ (𝑀 = 1 → (𝑃‘𝑀) = (𝑃‘1)) | 
| 10 |  | 1e0p1 12777 | . . . . . . 7
⊢ 1 = (0 +
1) | 
| 11 | 10 | fveq2i 6908 | . . . . . 6
⊢ (𝑃‘1) = (𝑃‘(0 + 1)) | 
| 12 | 9, 11 | eqtrdi 2792 | . . . . 5
⊢ (𝑀 = 1 → (𝑃‘𝑀) = (𝑃‘(0 + 1))) | 
| 13 | 12 | adantr 480 | . . . 4
⊢ ((𝑀 = 1 ∧ 𝜑) → (𝑃‘𝑀) = (𝑃‘(0 + 1))) | 
| 14 | 8, 13 | breqtrrd 5170 | . . 3
⊢ ((𝑀 = 1 ∧ 𝜑) → (𝑃‘0) < (𝑃‘𝑀)) | 
| 15 | 14 | ex 412 | . 2
⊢ (𝑀 = 1 → (𝜑 → (𝑃‘0) < (𝑃‘𝑀))) | 
| 16 | 1, 2 | iccpartiltu 47414 | . . . 4
⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀)) | 
| 17 | 1, 2 | iccpartigtl 47415 | . . . 4
⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖)) | 
| 18 |  | 1nn 12278 | . . . . . . . . . 10
⊢ 1 ∈
ℕ | 
| 19 | 18 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 1 ∈
ℕ) | 
| 20 | 1 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 𝑀 ∈ ℕ) | 
| 21 |  | df-ne 2940 | . . . . . . . . . . 11
⊢ (𝑀 ≠ 1 ↔ ¬ 𝑀 = 1) | 
| 22 | 1 | nnge1d 12315 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ 𝑀) | 
| 23 |  | 1red 11263 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) | 
| 24 | 1 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 25 | 23, 24 | ltlend 11407 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1 < 𝑀 ↔ (1 ≤ 𝑀 ∧ 𝑀 ≠ 1))) | 
| 26 | 25 | biimprd 248 | . . . . . . . . . . . 12
⊢ (𝜑 → ((1 ≤ 𝑀 ∧ 𝑀 ≠ 1) → 1 < 𝑀)) | 
| 27 | 22, 26 | mpand 695 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 ≠ 1 → 1 < 𝑀)) | 
| 28 | 21, 27 | biimtrrid 243 | . . . . . . . . . 10
⊢ (𝜑 → (¬ 𝑀 = 1 → 1 < 𝑀)) | 
| 29 | 28 | imp 406 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 1 < 𝑀) | 
| 30 |  | elfzo1 13753 | . . . . . . . . 9
⊢ (1 ∈
(1..^𝑀) ↔ (1 ∈
ℕ ∧ 𝑀 ∈
ℕ ∧ 1 < 𝑀)) | 
| 31 | 19, 20, 29, 30 | syl3anbrc 1343 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 1 ∈ (1..^𝑀)) | 
| 32 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑖 = 1 → (𝑃‘𝑖) = (𝑃‘1)) | 
| 33 | 32 | breq2d 5154 | . . . . . . . . 9
⊢ (𝑖 = 1 → ((𝑃‘0) < (𝑃‘𝑖) ↔ (𝑃‘0) < (𝑃‘1))) | 
| 34 | 33 | rspcv 3617 | . . . . . . . 8
⊢ (1 ∈
(1..^𝑀) →
(∀𝑖 ∈
(1..^𝑀)(𝑃‘0) < (𝑃‘𝑖) → (𝑃‘0) < (𝑃‘1))) | 
| 35 | 31, 34 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖) → (𝑃‘0) < (𝑃‘1))) | 
| 36 | 32 | breq1d 5152 | . . . . . . . . . . 11
⊢ (𝑖 = 1 → ((𝑃‘𝑖) < (𝑃‘𝑀) ↔ (𝑃‘1) < (𝑃‘𝑀))) | 
| 37 | 36 | rspcv 3617 | . . . . . . . . . 10
⊢ (1 ∈
(1..^𝑀) →
(∀𝑖 ∈
(1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀) → (𝑃‘1) < (𝑃‘𝑀))) | 
| 38 | 31, 37 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀) → (𝑃‘1) < (𝑃‘𝑀))) | 
| 39 |  | nnnn0 12535 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) | 
| 40 |  | 0elfz 13665 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ0
→ 0 ∈ (0...𝑀)) | 
| 41 | 1, 39, 40 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ (0...𝑀)) | 
| 42 | 1, 2, 41 | iccpartxr 47411 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘0) ∈
ℝ*) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (𝑃‘0) ∈
ℝ*) | 
| 44 | 2 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 𝑃 ∈ (RePart‘𝑀)) | 
| 45 |  | 1nn0 12544 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 | 
| 46 | 45 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 1 ∈
ℕ0) | 
| 47 | 1, 39 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 48 | 47 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 𝑀 ∈
ℕ0) | 
| 49 | 22 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 1 ≤ 𝑀) | 
| 50 |  | elfz2nn0 13659 | . . . . . . . . . . . . 13
⊢ (1 ∈
(0...𝑀) ↔ (1 ∈
ℕ0 ∧ 𝑀
∈ ℕ0 ∧ 1 ≤ 𝑀)) | 
| 51 | 46, 48, 49, 50 | syl3anbrc 1343 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → 1 ∈ (0...𝑀)) | 
| 52 | 20, 44, 51 | iccpartxr 47411 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (𝑃‘1) ∈
ℝ*) | 
| 53 |  | nn0fz0 13666 | . . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈ (0...𝑀)) | 
| 54 | 39, 53 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (0...𝑀)) | 
| 55 | 1, 54 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) | 
| 56 | 1, 2, 55 | iccpartxr 47411 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑃‘𝑀) ∈
ℝ*) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (𝑃‘𝑀) ∈
ℝ*) | 
| 58 |  | xrlttr 13183 | . . . . . . . . . . 11
⊢ (((𝑃‘0) ∈
ℝ* ∧ (𝑃‘1) ∈ ℝ* ∧
(𝑃‘𝑀) ∈ ℝ*) →
(((𝑃‘0) < (𝑃‘1) ∧ (𝑃‘1) < (𝑃‘𝑀)) → (𝑃‘0) < (𝑃‘𝑀))) | 
| 59 | 43, 52, 57, 58 | syl3anc 1372 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (((𝑃‘0) < (𝑃‘1) ∧ (𝑃‘1) < (𝑃‘𝑀)) → (𝑃‘0) < (𝑃‘𝑀))) | 
| 60 | 59 | expcomd 416 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → ((𝑃‘1) < (𝑃‘𝑀) → ((𝑃‘0) < (𝑃‘1) → (𝑃‘0) < (𝑃‘𝑀)))) | 
| 61 | 38, 60 | syld 47 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀) → ((𝑃‘0) < (𝑃‘1) → (𝑃‘0) < (𝑃‘𝑀)))) | 
| 62 | 61 | com23 86 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → ((𝑃‘0) < (𝑃‘1) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀) → (𝑃‘0) < (𝑃‘𝑀)))) | 
| 63 | 35, 62 | syld 47 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑀 = 1) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀) → (𝑃‘0) < (𝑃‘𝑀)))) | 
| 64 | 63 | ex 412 | . . . . 5
⊢ (𝜑 → (¬ 𝑀 = 1 → (∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀) → (𝑃‘0) < (𝑃‘𝑀))))) | 
| 65 | 64 | com24 95 | . . . 4
⊢ (𝜑 → (∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀) → (∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖) → (¬ 𝑀 = 1 → (𝑃‘0) < (𝑃‘𝑀))))) | 
| 66 | 16, 17, 65 | mp2d 49 | . . 3
⊢ (𝜑 → (¬ 𝑀 = 1 → (𝑃‘0) < (𝑃‘𝑀))) | 
| 67 | 66 | com12 32 | . 2
⊢ (¬
𝑀 = 1 → (𝜑 → (𝑃‘0) < (𝑃‘𝑀))) | 
| 68 | 15, 67 | pm2.61i 182 | 1
⊢ (𝜑 → (𝑃‘0) < (𝑃‘𝑀)) |