Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | 1 | nnnn0d 11351 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
3 | | elnn0uz 11725 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈
(ℤ≥‘0)) |
4 | 2, 3 | sylib 208 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
5 | | fzpred 12389 |
. . . . . 6
⊢ (𝑀 ∈
(ℤ≥‘0) → (0...𝑀) = ({0} ∪ ((0 + 1)...𝑀))) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → (0...𝑀) = ({0} ∪ ((0 + 1)...𝑀))) |
7 | 6 | eleq2d 2687 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) ↔ 𝑖 ∈ ({0} ∪ ((0 + 1)...𝑀)))) |
8 | | elun 3753 |
. . . . 5
⊢ (𝑖 ∈ ({0} ∪ ((0 +
1)...𝑀)) ↔ (𝑖 ∈ {0} ∨ 𝑖 ∈ ((0 + 1)...𝑀))) |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ ({0} ∪ ((0 + 1)...𝑀)) ↔ (𝑖 ∈ {0} ∨ 𝑖 ∈ ((0 + 1)...𝑀)))) |
10 | | velsn 4193 |
. . . . . 6
⊢ (𝑖 ∈ {0} ↔ 𝑖 = 0) |
11 | 10 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ {0} ↔ 𝑖 = 0)) |
12 | | 0p1e1 11132 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
13 | 12 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (0 + 1) =
1) |
14 | 13 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → ((0 + 1)...𝑀) = (1...𝑀)) |
15 | 14 | eleq2d 2687 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ ((0 + 1)...𝑀) ↔ 𝑖 ∈ (1...𝑀))) |
16 | 11, 15 | orbi12d 746 |
. . . 4
⊢ (𝜑 → ((𝑖 ∈ {0} ∨ 𝑖 ∈ ((0 + 1)...𝑀)) ↔ (𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)))) |
17 | 7, 9, 16 | 3bitrd 294 |
. . 3
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) ↔ (𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)))) |
18 | | iccpartgtprec.p |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) |
19 | | 0elfz 12436 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ 0 ∈ (0...𝑀)) |
20 | 2, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
21 | 1, 18, 20 | iccpartxr 41355 |
. . . . . . 7
⊢ (𝜑 → (𝑃‘0) ∈
ℝ*) |
22 | | xrleid 11983 |
. . . . . . 7
⊢ ((𝑃‘0) ∈
ℝ* → (𝑃‘0) ≤ (𝑃‘0)) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑃‘0) ≤ (𝑃‘0)) |
24 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑖 = 0 → (𝑃‘𝑖) = (𝑃‘0)) |
25 | 24 | breq2d 4665 |
. . . . . 6
⊢ (𝑖 = 0 → ((𝑃‘0) ≤ (𝑃‘𝑖) ↔ (𝑃‘0) ≤ (𝑃‘0))) |
26 | 23, 25 | syl5ibr 236 |
. . . . 5
⊢ (𝑖 = 0 → (𝜑 → (𝑃‘0) ≤ (𝑃‘𝑖))) |
27 | 1, 18 | iccpartgtl 41362 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑀)(𝑃‘0) < (𝑃‘𝑘)) |
28 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑃‘𝑘) = (𝑃‘𝑖)) |
29 | 28 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((𝑃‘0) < (𝑃‘𝑘) ↔ (𝑃‘0) < (𝑃‘𝑖))) |
30 | 29 | rspccv 3306 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(1...𝑀)(𝑃‘0) < (𝑃‘𝑘) → (𝑖 ∈ (1...𝑀) → (𝑃‘0) < (𝑃‘𝑖))) |
31 | 27, 30 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (1...𝑀) → (𝑃‘0) < (𝑃‘𝑖))) |
32 | 31 | imp 445 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) < (𝑃‘𝑖)) |
33 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) ∈
ℝ*) |
34 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑀 ∈ ℕ) |
35 | 18 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑃 ∈ (RePart‘𝑀)) |
36 | | 1nn0 11308 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℕ0 |
37 | 36 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℕ0) |
38 | | elnn0uz 11725 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℕ0 ↔ 1 ∈
(ℤ≥‘0)) |
39 | 37, 38 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
(ℤ≥‘0)) |
40 | | fzss1 12380 |
. . . . . . . . . . 11
⊢ (1 ∈
(ℤ≥‘0) → (1...𝑀) ⊆ (0...𝑀)) |
41 | 39, 40 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑀) ⊆ (0...𝑀)) |
42 | 41 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝑖 ∈ (0...𝑀)) |
43 | 34, 35, 42 | iccpartxr 41355 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘𝑖) ∈
ℝ*) |
44 | | xrltle 11982 |
. . . . . . . 8
⊢ (((𝑃‘0) ∈
ℝ* ∧ (𝑃‘𝑖) ∈ ℝ*) → ((𝑃‘0) < (𝑃‘𝑖) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
45 | 33, 43, 44 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝑃‘0) < (𝑃‘𝑖) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
46 | 32, 45 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖)) |
47 | 46 | expcom 451 |
. . . . 5
⊢ (𝑖 ∈ (1...𝑀) → (𝜑 → (𝑃‘0) ≤ (𝑃‘𝑖))) |
48 | 26, 47 | jaoi 394 |
. . . 4
⊢ ((𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)) → (𝜑 → (𝑃‘0) ≤ (𝑃‘𝑖))) |
49 | 48 | com12 32 |
. . 3
⊢ (𝜑 → ((𝑖 = 0 ∨ 𝑖 ∈ (1...𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
50 | 17, 49 | sylbid 230 |
. 2
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
51 | 50 | ralrimiv 2965 |
1
⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑖)) |