Step | Hyp | Ref
| Expression |
1 | | iccpartgtprec.p |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) |
2 | | iccpartgtprec.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | | iccpart 44868 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ*
↑m (0...𝑀))
∧ ∀𝑖 ∈
(0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1))))) |
4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ*
↑m (0...𝑀))
∧ ∀𝑖 ∈
(0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1))))) |
5 | | elmapfn 8653 |
. . . . . . 7
⊢ (𝑃 ∈ (ℝ*
↑m (0...𝑀))
→ 𝑃 Fn (0...𝑀)) |
6 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝑃 ∈ (ℝ*
↑m (0...𝑀))
∧ ∀𝑖 ∈
(0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1))) → 𝑃 Fn (0...𝑀)) |
7 | 4, 6 | syl6bi 252 |
. . . . 5
⊢ (𝜑 → (𝑃 ∈ (RePart‘𝑀) → 𝑃 Fn (0...𝑀))) |
8 | 1, 7 | mpd 15 |
. . . 4
⊢ (𝜑 → 𝑃 Fn (0...𝑀)) |
9 | | fvelrnb 6830 |
. . . 4
⊢ (𝑃 Fn (0...𝑀) → (𝑝 ∈ ran 𝑃 ↔ ∃𝑖 ∈ (0...𝑀)(𝑃‘𝑖) = 𝑝)) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝑝 ∈ ran 𝑃 ↔ ∃𝑖 ∈ (0...𝑀)(𝑃‘𝑖) = 𝑝)) |
11 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ ℕ) |
12 | 1 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑃 ∈ (RePart‘𝑀)) |
13 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀)) |
14 | 11, 12, 13 | iccpartxr 44871 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑃‘𝑖) ∈
ℝ*) |
15 | 2, 1 | iccpartgel 44881 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑘)) |
16 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑃‘𝑘) = (𝑃‘𝑖)) |
17 | 16 | breq2d 5086 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((𝑃‘0) ≤ (𝑃‘𝑘) ↔ (𝑃‘0) ≤ (𝑃‘𝑖))) |
18 | 17 | rspcva 3559 |
. . . . . . . . 9
⊢ ((𝑖 ∈ (0...𝑀) ∧ ∀𝑘 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑘)) → (𝑃‘0) ≤ (𝑃‘𝑖)) |
19 | 18 | expcom 414 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑘) → (𝑖 ∈ (0...𝑀) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
20 | 15, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
21 | 20 | imp 407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖)) |
22 | 2, 1 | iccpartleu 44880 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ (0...𝑀)(𝑃‘𝑘) ≤ (𝑃‘𝑀)) |
23 | 16 | breq1d 5084 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → ((𝑃‘𝑘) ≤ (𝑃‘𝑀) ↔ (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
24 | 23 | rspcva 3559 |
. . . . . . . . 9
⊢ ((𝑖 ∈ (0...𝑀) ∧ ∀𝑘 ∈ (0...𝑀)(𝑃‘𝑘) ≤ (𝑃‘𝑀)) → (𝑃‘𝑖) ≤ (𝑃‘𝑀)) |
25 | 24 | expcom 414 |
. . . . . . . 8
⊢
(∀𝑘 ∈
(0...𝑀)(𝑃‘𝑘) ≤ (𝑃‘𝑀) → (𝑖 ∈ (0...𝑀) → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
26 | 22, 25 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (0...𝑀) → (𝑃‘𝑖) ≤ (𝑃‘𝑀))) |
27 | 26 | imp 407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑃‘𝑖) ≤ (𝑃‘𝑀)) |
28 | | nnnn0 12240 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
29 | | 0elfz 13353 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ 0 ∈ (0...𝑀)) |
30 | 2, 28, 29 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
31 | 2, 1, 30 | iccpartxr 44871 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃‘0) ∈
ℝ*) |
32 | | nn0fz0 13354 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈ (0...𝑀)) |
33 | 28, 32 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈ (0...𝑀)) |
34 | 2, 33 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
35 | 2, 1, 34 | iccpartxr 44871 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃‘𝑀) ∈
ℝ*) |
36 | 31, 35 | jca 512 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃‘0) ∈ ℝ* ∧
(𝑃‘𝑀) ∈
ℝ*)) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑃‘0) ∈ ℝ* ∧
(𝑃‘𝑀) ∈
ℝ*)) |
38 | | elicc1 13123 |
. . . . . . 7
⊢ (((𝑃‘0) ∈
ℝ* ∧ (𝑃‘𝑀) ∈ ℝ*) → ((𝑃‘𝑖) ∈ ((𝑃‘0)[,](𝑃‘𝑀)) ↔ ((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘0) ≤ (𝑃‘𝑖) ∧ (𝑃‘𝑖) ≤ (𝑃‘𝑀)))) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑃‘𝑖) ∈ ((𝑃‘0)[,](𝑃‘𝑀)) ↔ ((𝑃‘𝑖) ∈ ℝ* ∧ (𝑃‘0) ≤ (𝑃‘𝑖) ∧ (𝑃‘𝑖) ≤ (𝑃‘𝑀)))) |
40 | 14, 21, 27, 39 | mpbir3and 1341 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑃‘𝑖) ∈ ((𝑃‘0)[,](𝑃‘𝑀))) |
41 | | eleq1 2826 |
. . . . 5
⊢ ((𝑃‘𝑖) = 𝑝 → ((𝑃‘𝑖) ∈ ((𝑃‘0)[,](𝑃‘𝑀)) ↔ 𝑝 ∈ ((𝑃‘0)[,](𝑃‘𝑀)))) |
42 | 40, 41 | syl5ibcom 244 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑃‘𝑖) = 𝑝 → 𝑝 ∈ ((𝑃‘0)[,](𝑃‘𝑀)))) |
43 | 42 | rexlimdva 3213 |
. . 3
⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑃‘𝑖) = 𝑝 → 𝑝 ∈ ((𝑃‘0)[,](𝑃‘𝑀)))) |
44 | 10, 43 | sylbid 239 |
. 2
⊢ (𝜑 → (𝑝 ∈ ran 𝑃 → 𝑝 ∈ ((𝑃‘0)[,](𝑃‘𝑀)))) |
45 | 44 | ssrdv 3927 |
1
⊢ (𝜑 → ran 𝑃 ⊆ ((𝑃‘0)[,](𝑃‘𝑀))) |