| Step | Hyp | Ref
| Expression |
| 1 | | iccpartiun.p |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) |
| 2 | | iccpartiun.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 3 | | iccelpart 47420 |
. . . . . 6
⊢ (𝑀 ∈ ℕ →
∀𝑝 ∈
(RePart‘𝑀)(𝑥 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 4 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑃 → (𝑝‘0) = (𝑃‘0)) |
| 5 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑃 → (𝑝‘𝑀) = (𝑃‘𝑀)) |
| 6 | 4, 5 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → ((𝑝‘0)[,)(𝑝‘𝑀)) = ((𝑃‘0)[,)(𝑃‘𝑀))) |
| 7 | 6 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → (𝑥 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) ↔ 𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)))) |
| 8 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑃 → (𝑝‘𝑖) = (𝑃‘𝑖)) |
| 9 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑝 = 𝑃 → (𝑝‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1))) |
| 10 | 8, 9 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑃 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
| 11 | 10 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑃 → (𝑥 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 12 | 11 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑝 = 𝑃 → (∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 13 | 7, 12 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑝 = 𝑃 → ((𝑥 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))))) |
| 14 | 13 | rspcva 3620 |
. . . . . . 7
⊢ ((𝑃 ∈ (RePart‘𝑀) ∧ ∀𝑝 ∈ (RePart‘𝑀)(𝑥 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 15 | 14 | expcom 413 |
. . . . . 6
⊢
(∀𝑝 ∈
(RePart‘𝑀)(𝑥 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑃 ∈ (RePart‘𝑀) → (𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))))) |
| 16 | 2, 3, 15 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑃 ∈ (RePart‘𝑀) → (𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))))) |
| 17 | 1, 16 | mpd 15 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 18 | | nnnn0 12533 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 19 | | 0elfz 13664 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ 0 ∈ (0...𝑀)) |
| 20 | 2, 18, 19 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
| 21 | 2, 1, 20 | iccpartxr 47406 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃‘0) ∈
ℝ*) |
| 22 | | nn0fz0 13665 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈ (0...𝑀)) |
| 23 | 22 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈ (0...𝑀)) |
| 24 | 2, 18, 23 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
| 25 | 2, 1, 24 | iccpartxr 47406 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃‘𝑀) ∈
ℝ*) |
| 26 | 21, 25 | jca 511 |
. . . . . . . 8
⊢ (𝜑 → ((𝑃‘0) ∈ ℝ* ∧
(𝑃‘𝑀) ∈
ℝ*)) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑃‘0) ∈ ℝ* ∧
(𝑃‘𝑀) ∈
ℝ*)) |
| 28 | | elfzofz 13715 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
| 29 | 2, 1 | iccpartgel 47416 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗)) |
| 30 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑖 → (𝑃‘𝑗) = (𝑃‘𝑖)) |
| 31 | 30 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → ((𝑃‘0) ≤ (𝑃‘𝑗) ↔ (𝑃‘0) ≤ (𝑃‘𝑖))) |
| 32 | 31 | rspcva 3620 |
. . . . . . . 8
⊢ ((𝑖 ∈ (0...𝑀) ∧ ∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗)) → (𝑃‘0) ≤ (𝑃‘𝑖)) |
| 33 | 28, 29, 32 | syl2anr 597 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖)) |
| 34 | | fzofzp1 13803 |
. . . . . . . 8
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
| 35 | 2, 1 | iccpartleu 47415 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ (0...𝑀)(𝑃‘𝑘) ≤ (𝑃‘𝑀)) |
| 36 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑖 + 1) → (𝑃‘𝑘) = (𝑃‘(𝑖 + 1))) |
| 37 | 36 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑘 = (𝑖 + 1) → ((𝑃‘𝑘) ≤ (𝑃‘𝑀) ↔ (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
| 38 | 37 | rspcva 3620 |
. . . . . . . 8
⊢ (((𝑖 + 1) ∈ (0...𝑀) ∧ ∀𝑘 ∈ (0...𝑀)(𝑃‘𝑘) ≤ (𝑃‘𝑀)) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀)) |
| 39 | 34, 35, 38 | syl2anr 597 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀)) |
| 40 | | icossico 13457 |
. . . . . . 7
⊢ ((((𝑃‘0) ∈
ℝ* ∧ (𝑃‘𝑀) ∈ ℝ*) ∧ ((𝑃‘0) ≤ (𝑃‘𝑖) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) → ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ⊆ ((𝑃‘0)[,)(𝑃‘𝑀))) |
| 41 | 27, 33, 39, 40 | syl12anc 837 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ⊆ ((𝑃‘0)[,)(𝑃‘𝑀))) |
| 42 | 41 | sseld 3982 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → 𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)))) |
| 43 | 42 | rexlimdva 3155 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → 𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)))) |
| 44 | 17, 43 | impbid 212 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 45 | | eliun 4995 |
. . 3
⊢ (𝑥 ∈ ∪ 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑥 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
| 46 | 44, 45 | bitr4di 289 |
. 2
⊢ (𝜑 → (𝑥 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)) ↔ 𝑥 ∈ ∪
𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 47 | 46 | eqrdv 2735 |
1
⊢ (𝜑 → ((𝑃‘0)[,)(𝑃‘𝑀)) = ∪
𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |