Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | | nnnn0 11299 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
3 | | elnn0uz 11725 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈
(ℤ≥‘0)) |
4 | 2, 3 | sylib 208 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘0)) |
5 | 1, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
6 | | fzisfzounsn 12580 |
. . . . . 6
⊢ (𝑀 ∈
(ℤ≥‘0) → (0...𝑀) = ((0..^𝑀) ∪ {𝑀})) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → (0...𝑀) = ((0..^𝑀) ∪ {𝑀})) |
8 | 7 | eleq2d 2687 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) ↔ 𝑖 ∈ ((0..^𝑀) ∪ {𝑀}))) |
9 | | elun 3753 |
. . . . 5
⊢ (𝑖 ∈ ((0..^𝑀) ∪ {𝑀}) ↔ (𝑖 ∈ (0..^𝑀) ∨ 𝑖 ∈ {𝑀})) |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ ((0..^𝑀) ∪ {𝑀}) ↔ (𝑖 ∈ (0..^𝑀) ∨ 𝑖 ∈ {𝑀}))) |
11 | | velsn 4193 |
. . . . . 6
⊢ (𝑖 ∈ {𝑀} ↔ 𝑖 = 𝑀) |
12 | 11 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ {𝑀} ↔ 𝑖 = 𝑀)) |
13 | 12 | orbi2d 738 |
. . . 4
⊢ (𝜑 → ((𝑖 ∈ (0..^𝑀) ∨ 𝑖 ∈ {𝑀}) ↔ (𝑖 ∈ (0..^𝑀) ∨ 𝑖 = 𝑀))) |
14 | 8, 10, 13 | 3bitrd 294 |
. . 3
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) ↔ (𝑖 ∈ (0..^𝑀) ∨ 𝑖 = 𝑀))) |
15 | | iccpartgtprec.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) |
16 | 1, 15 | iccpartltu 41361 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑀)(𝑃‘𝑘) < (𝑃‘𝑀)) |
17 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑃‘𝑘) = (𝑃‘𝑖)) |
18 | 17 | breq1d 4663 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((𝑃‘𝑘) < (𝑃‘𝑀) ↔ (𝑃‘𝑖) < (𝑃‘𝑀))) |
19 | 18 | rspccv 3306 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
(0..^𝑀)(𝑃‘𝑘) < (𝑃‘𝑀) → (𝑖 ∈ (0..^𝑀) → (𝑃‘𝑖) < (𝑃‘𝑀))) |
20 | 16, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (𝑃‘𝑖) < (𝑃‘𝑀))) |
21 | 20 | imp 445 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘𝑖) < (𝑃‘𝑀)) |
22 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ ℕ) |
23 | 15 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑃 ∈ (RePart‘𝑀)) |
24 | | fzossfz 12488 |
. . . . . . . . . . 11
⊢
(0..^𝑀) ⊆
(0...𝑀) |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → (0..^𝑀) ⊆ (0...𝑀)) |
26 | 25 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
27 | 22, 23, 26 | iccpartxr 41355 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘𝑖) ∈
ℝ*) |
28 | | nn0fz0 12437 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈ (0...𝑀)) |
29 | 2, 28 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (0...𝑀)) |
30 | 1, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
31 | 1, 15, 30 | iccpartxr 41355 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃‘𝑀) ∈
ℝ*) |
32 | 31 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘𝑀) ∈
ℝ*) |
33 | | xrltle 11982 |
. . . . . . . 8
⊢ (((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘𝑀) ∈ ℝ*) → ((𝑃‘𝑖) < (𝑃‘𝑀) → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
34 | 27, 32, 33 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑃‘𝑖) < (𝑃‘𝑀) → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
35 | 21, 34 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘𝑖) ≤ (𝑃‘𝑀)) |
36 | 35 | expcom 451 |
. . . . 5
⊢ (𝑖 ∈ (0..^𝑀) → (𝜑 → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
37 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑖 = 𝑀 → (𝑃‘𝑖) = (𝑃‘𝑀)) |
38 | 37 | adantr 481 |
. . . . . . 7
⊢ ((𝑖 = 𝑀 ∧ 𝜑) → (𝑃‘𝑖) = (𝑃‘𝑀)) |
39 | | xrleid 11983 |
. . . . . . . . 9
⊢ ((𝑃‘𝑀) ∈ ℝ* → (𝑃‘𝑀) ≤ (𝑃‘𝑀)) |
40 | 31, 39 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑃‘𝑀) ≤ (𝑃‘𝑀)) |
41 | 40 | adantl 482 |
. . . . . . 7
⊢ ((𝑖 = 𝑀 ∧ 𝜑) → (𝑃‘𝑀) ≤ (𝑃‘𝑀)) |
42 | 38, 41 | eqbrtrd 4675 |
. . . . . 6
⊢ ((𝑖 = 𝑀 ∧ 𝜑) → (𝑃‘𝑖) ≤ (𝑃‘𝑀)) |
43 | 42 | ex 450 |
. . . . 5
⊢ (𝑖 = 𝑀 → (𝜑 → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
44 | 36, 43 | jaoi 394 |
. . . 4
⊢ ((𝑖 ∈ (0..^𝑀) ∨ 𝑖 = 𝑀) → (𝜑 → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
45 | 44 | com12 32 |
. . 3
⊢ (𝜑 → ((𝑖 ∈ (0..^𝑀) ∨ 𝑖 = 𝑀) → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
46 | 14, 45 | sylbid 230 |
. 2
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
47 | 46 | ralrimiv 2965 |
1
⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘𝑖) ≤ (𝑃‘𝑀)) |