Step | Hyp | Ref
| Expression |
1 | | nfv 1920 |
. . . . 5
⊢
Ⅎ𝑖𝜑 |
2 | | nfreu1 3272 |
. . . . 5
⊢
Ⅎ𝑖∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) |
3 | | simpl 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝜑) |
4 | | iccpartiun.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
5 | 4 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ ℕ) |
6 | | iccpartiun.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) |
7 | 6 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑃 ∈ (RePart‘𝑀)) |
8 | | nnnn0 11976 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
9 | | 0elfz 13088 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 0 ∈ (0...𝑀)) |
10 | 4, 8, 9 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
11 | 10 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 0 ∈ (0...𝑀)) |
12 | 5, 7, 11 | iccpartxr 44389 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘0) ∈
ℝ*) |
13 | | nn0fz0 13089 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℕ0
↔ 𝑀 ∈ (0...𝑀)) |
14 | 13 | biimpi 219 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈ (0...𝑀)) |
15 | 4, 8, 14 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
16 | 15 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ (0...𝑀)) |
17 | 5, 7, 16 | iccpartxr 44389 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘𝑀) ∈
ℝ*) |
18 | 4, 6 | iccpartgel 44399 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗)) |
19 | | elfzofz 13137 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
20 | 19 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀)) |
21 | | fveq2 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → (𝑃‘𝑗) = (𝑃‘𝑖)) |
22 | 21 | breq2d 5039 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → ((𝑃‘0) ≤ (𝑃‘𝑗) ↔ (𝑃‘0) ≤ (𝑃‘𝑖))) |
23 | 22 | rspcv 3519 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (0...𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
25 | 24 | ex 416 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑗) → (𝑃‘0) ≤ (𝑃‘𝑖)))) |
26 | 18, 25 | mpid 44 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (𝑃‘0) ≤ (𝑃‘𝑖))) |
27 | 26 | imp 410 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘0) ≤ (𝑃‘𝑖)) |
28 | 4, 6 | iccpartleu 44398 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀)) |
29 | | fzofzp1 13218 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
30 | 29 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
31 | | fveq2 6668 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑖 + 1) → (𝑃‘𝑗) = (𝑃‘(𝑖 + 1))) |
32 | 31 | breq1d 5037 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = (𝑖 + 1) → ((𝑃‘𝑗) ≤ (𝑃‘𝑀) ↔ (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
33 | 32 | rspcv 3519 |
. . . . . . . . . . . . 13
⊢ ((𝑖 + 1) ∈ (0...𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
35 | 34 | ex 416 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (∀𝑗 ∈ (0...𝑀)(𝑃‘𝑗) ≤ (𝑃‘𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀)))) |
36 | 28, 35 | mpid 44 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) |
37 | 36 | imp 410 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀)) |
38 | | icossico 12884 |
. . . . . . . . 9
⊢ ((((𝑃‘0) ∈
ℝ* ∧ (𝑃‘𝑀) ∈ ℝ*) ∧ ((𝑃‘0) ≤ (𝑃‘𝑖) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃‘𝑀))) → ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ⊆ ((𝑃‘0)[,)(𝑃‘𝑀))) |
39 | 12, 17, 27, 37, 38 | syl22anc 838 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ⊆ ((𝑃‘0)[,)(𝑃‘𝑀))) |
40 | 39 | sseld 3874 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → 𝑝 ∈ ((𝑃‘0)[,)(𝑃‘𝑀)))) |
41 | 4, 6 | icceuelpart 44406 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((𝑃‘0)[,)(𝑃‘𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
42 | 3, 40, 41 | syl6an 684 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
43 | 42 | ex 416 |
. . . . 5
⊢ (𝜑 → (𝑖 ∈ (0..^𝑀) → (𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))))) |
44 | 1, 2, 43 | rexlimd 3226 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
45 | | rmo5 3331 |
. . . 4
⊢
(∃*𝑖 ∈
(0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ (∃𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) → ∃!𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))) |
46 | 44, 45 | sylibr 237 |
. . 3
⊢ (𝜑 → ∃*𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
47 | 46 | alrimiv 1933 |
. 2
⊢ (𝜑 → ∀𝑝∃*𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
48 | | df-disj 4993 |
. 2
⊢
(Disj 𝑖
∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ ∀𝑝∃*𝑖 ∈ (0..^𝑀)𝑝 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |
49 | 47, 48 | sylibr 237 |
1
⊢ (𝜑 → Disj 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1)))) |