| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑖𝜑 |
| 2 | | nfreu1 3412 |
. . . . 5
⊢
Ⅎ𝑖∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) |
| 3 | | simpl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝜑) |
| 4 | | iccpartiun.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 5 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ ℕ) |
| 6 | | iccpartiun.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) |
| 7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑃 ∈ (RePart‘𝑀)) |
| 8 | | nnnn0 12533 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
| 9 | | 0elfz 13664 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 0 ∈ (0...𝑀)) |
| 10 | 4, 8, 9 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
| 11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 0 ∈ (0...𝑀)) |
| 12 | 5, 7, 11 | iccpartxr 47406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘0) ∈
ℝ*) |
| 13 | | nn0fz0 13665 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈ (0...𝑀)) |
| 14 | 13 | biimpi 216 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈ (0...𝑀)) |
| 15 | 4, 8, 14 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
| 16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ (0...𝑀)) |
| 17 | 5, 7, 16 | iccpartxr 47406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘𝑀) ∈
ℝ*) |
| 18 | 4, 6 | iccpartgel 47416 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗)) |
| 19 | | elfzofz 13715 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
| 20 | 19 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
| 21 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝑃‘𝑗) = (𝑃‘𝑖)) |
| 22 | 21 | breq2d 5155 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝑃‘0) ≤ (𝑃‘𝑗) ↔ (𝑃‘0) ≤ (𝑃‘𝑖))) |
| 23 | 22 | rspcv 3618 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0...𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
| 24 | 20, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
| 25 | 24 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗) → (𝑃‘0) ≤ (𝑃‘𝑖)))) |
| 26 | 18, 25 | mpid 44 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
| 27 | 26 | imp 406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖)) |
| 28 | 4, 6 | iccpartleu 47415 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀)) |
| 29 | | fzofzp1 13803 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
| 30 | 29 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
| 31 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑖 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑖 + 1))) |
| 32 | 31 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑖 + 1) → ((𝑃‘𝑗) ≤ (𝑃‘𝑀) ↔ (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
| 33 | 32 | rspcv 3618 |
. . . . . . . . . . . . 13
⊢ ((𝑖 + 1) ∈ (0...𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
| 34 | 30, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
| 35 | 34 | ex 412 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀)))) |
| 36 | 28, 35 | mpid 44 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
| 37 | 36 | imp 406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀)) |
| 38 | | icossico 13457 |
. . . . . . . . 9
⊢ ((((𝑃‘0) ∈
ℝ* ∧ (𝑃‘𝑀) ∈ ℝ*) ∧ ((𝑃‘0) ≤ (𝑃‘𝑖) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) → ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ⊆ ((𝑃‘0)[,)(𝑃‘𝑀))) |
| 39 | 12, 17, 27, 37, 38 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ⊆ ((𝑃‘0)[,)(𝑃‘𝑀))) |
| 40 | 39 | sseld 3982 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → 𝑝 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)))) |
| 41 | 4, 6 | icceuelpart 47423 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((𝑃‘0)[,)(𝑃‘𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
| 42 | 3, 40, 41 | syl6an 684 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 43 | 42 | ex 412 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))))) |
| 44 | 1, 2, 43 | rexlimd 3266 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 45 | | rmo5 3400 |
. . . 4
⊢
(∃*𝑖 ∈
(0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ (∃𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
| 46 | 44, 45 | sylibr 234 |
. . 3
⊢ (𝜑 → ∃*𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
| 47 | 46 | alrimiv 1927 |
. 2
⊢ (𝜑 → ∀𝑝∃*𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
| 48 | | df-disj 5111 |
. 2
⊢
(Disj 𝑖
∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ ∀𝑝∃*𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
| 49 | 47, 48 | sylibr 234 |
1
⊢ (𝜑 → Disj 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |