Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | itg2i1fseq.3 |
. . . . . 6
⊢ (𝜑 → 𝑃:ℕ⟶dom
∫1) |
4 | 3 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑃‘𝑚) ∈ dom
∫1) |
5 | | itg1cl 23258 |
. . . . 5
⊢ ((𝑃‘𝑚) ∈ dom ∫1 →
(∫1‘(𝑃‘𝑚)) ∈ ℝ) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(∫1‘(𝑃‘𝑚)) ∈ ℝ) |
7 | | itg2i1fseq.6 |
. . . 4
⊢ 𝑆 = (𝑚 ∈ ℕ ↦
(∫1‘(𝑃‘𝑚))) |
8 | 6, 7 | fmptd 6292 |
. . 3
⊢ (𝜑 → 𝑆:ℕ⟶ℝ) |
9 | 3 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘) ∈ dom
∫1) |
10 | | peano2nn 10909 |
. . . . . 6
⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈
ℕ) |
11 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝑃:ℕ⟶dom
∫1 ∧ (𝑘
+ 1) ∈ ℕ) → (𝑃‘(𝑘 + 1)) ∈ dom
∫1) |
12 | 3, 10, 11 | syl2an 493 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘(𝑘 + 1)) ∈ dom
∫1) |
13 | | itg2i1fseq.4 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ (0𝑝
∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1)))) |
14 | | simpr 476 |
. . . . . . . 8
⊢
((0𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) → (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) |
15 | 14 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ (0𝑝 ∘𝑟 ≤ (𝑃‘𝑛) ∧ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) → ∀𝑛 ∈ ℕ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) |
16 | 13, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1))) |
17 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑃‘𝑛) = (𝑃‘𝑘)) |
18 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝑛 + 1) = (𝑘 + 1)) |
19 | 18 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝑃‘(𝑛 + 1)) = (𝑃‘(𝑘 + 1))) |
20 | 17, 19 | breq12d 4596 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → ((𝑃‘𝑛) ∘𝑟 ≤ (𝑃‘(𝑛 + 1)) ↔ (𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1)))) |
21 | 20 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑛 ∈
ℕ (𝑃‘𝑛) ∘𝑟
≤ (𝑃‘(𝑛 + 1)) ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1))) |
22 | 16, 21 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1))) |
23 | | itg1le 23286 |
. . . . 5
⊢ (((𝑃‘𝑘) ∈ dom ∫1 ∧ (𝑃‘(𝑘 + 1)) ∈ dom ∫1 ∧
(𝑃‘𝑘) ∘𝑟 ≤ (𝑃‘(𝑘 + 1))) →
(∫1‘(𝑃‘𝑘)) ≤ (∫1‘(𝑃‘(𝑘 + 1)))) |
24 | 9, 12, 22, 23 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘(𝑃‘𝑘)) ≤ (∫1‘(𝑃‘(𝑘 + 1)))) |
25 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → (𝑃‘𝑚) = (𝑃‘𝑘)) |
26 | 25 | fveq2d 6107 |
. . . . . 6
⊢ (𝑚 = 𝑘 → (∫1‘(𝑃‘𝑚)) = (∫1‘(𝑃‘𝑘))) |
27 | | fvex 6113 |
. . . . . 6
⊢
(∫1‘(𝑃‘𝑘)) ∈ V |
28 | 26, 7, 27 | fvmpt 6191 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (𝑆‘𝑘) = (∫1‘(𝑃‘𝑘))) |
29 | 28 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) = (∫1‘(𝑃‘𝑘))) |
30 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = (𝑘 + 1) → (𝑃‘𝑚) = (𝑃‘(𝑘 + 1))) |
31 | 30 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑚 = (𝑘 + 1) → (∫1‘(𝑃‘𝑚)) = (∫1‘(𝑃‘(𝑘 + 1)))) |
32 | | fvex 6113 |
. . . . . . 7
⊢
(∫1‘(𝑃‘(𝑘 + 1))) ∈ V |
33 | 31, 7, 32 | fvmpt 6191 |
. . . . . 6
⊢ ((𝑘 + 1) ∈ ℕ →
(𝑆‘(𝑘 + 1)) =
(∫1‘(𝑃‘(𝑘 + 1)))) |
34 | 10, 33 | syl 17 |
. . . . 5
⊢ (𝑘 ∈ ℕ → (𝑆‘(𝑘 + 1)) = (∫1‘(𝑃‘(𝑘 + 1)))) |
35 | 34 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘(𝑘 + 1)) = (∫1‘(𝑃‘(𝑘 + 1)))) |
36 | 24, 29, 35 | 3brtr4d 4615 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ (𝑆‘(𝑘 + 1))) |
37 | | itg2i1fseq2.7 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
38 | | itg2i1fseq2.8 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) →
(∫1‘(𝑃‘𝑘)) ≤ 𝑀) |
39 | 29, 38 | eqbrtrd 4605 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑆‘𝑘) ≤ 𝑀) |
40 | 39 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑀) |
41 | | breq2 4587 |
. . . . . 6
⊢ (𝑧 = 𝑀 → ((𝑆‘𝑘) ≤ 𝑧 ↔ (𝑆‘𝑘) ≤ 𝑀)) |
42 | 41 | ralbidv 2969 |
. . . . 5
⊢ (𝑧 = 𝑀 → (∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑧 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑀)) |
43 | 42 | rspcev 3282 |
. . . 4
⊢ ((𝑀 ∈ ℝ ∧
∀𝑘 ∈ ℕ
(𝑆‘𝑘) ≤ 𝑀) → ∃𝑧 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑧) |
44 | 37, 40, 43 | syl2anc 691 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑧) |
45 | 1, 2, 8, 36, 44 | climsup 14248 |
. 2
⊢ (𝜑 → 𝑆 ⇝ sup(ran 𝑆, ℝ, < )) |
46 | | itg2i1fseq.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ MblFn) |
47 | | itg2i1fseq.2 |
. . . 4
⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞)) |
48 | | itg2i1fseq.5 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑃‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)) |
49 | 46, 47, 3, 13, 48, 7 | itg2i1fseq 23328 |
. . 3
⊢ (𝜑 →
(∫2‘𝐹)
= sup(ran 𝑆,
ℝ*, < )) |
50 | | frn 5966 |
. . . . 5
⊢ (𝑆:ℕ⟶ℝ →
ran 𝑆 ⊆
ℝ) |
51 | 8, 50 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝑆 ⊆ ℝ) |
52 | 7, 6 | dmmptd 5937 |
. . . . . 6
⊢ (𝜑 → dom 𝑆 = ℕ) |
53 | | 1nn 10908 |
. . . . . . 7
⊢ 1 ∈
ℕ |
54 | | ne0i 3880 |
. . . . . . 7
⊢ (1 ∈
ℕ → ℕ ≠ ∅) |
55 | 53, 54 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ℕ ≠
∅) |
56 | 52, 55 | eqnetrd 2849 |
. . . . 5
⊢ (𝜑 → dom 𝑆 ≠ ∅) |
57 | | dm0rn0 5263 |
. . . . . 6
⊢ (dom
𝑆 = ∅ ↔ ran
𝑆 =
∅) |
58 | 57 | necon3bii 2834 |
. . . . 5
⊢ (dom
𝑆 ≠ ∅ ↔ ran
𝑆 ≠
∅) |
59 | 56, 58 | sylib 207 |
. . . 4
⊢ (𝜑 → ran 𝑆 ≠ ∅) |
60 | | ffn 5958 |
. . . . . . 7
⊢ (𝑆:ℕ⟶ℝ →
𝑆 Fn
ℕ) |
61 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑦 = (𝑆‘𝑘) → (𝑦 ≤ 𝑧 ↔ (𝑆‘𝑘) ≤ 𝑧)) |
62 | 61 | ralrn 6270 |
. . . . . . 7
⊢ (𝑆 Fn ℕ →
(∀𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑧)) |
63 | 8, 60, 62 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 ↔ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑧)) |
64 | 63 | rexbidv 3034 |
. . . . 5
⊢ (𝜑 → (∃𝑧 ∈ ℝ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧 ↔ ∃𝑧 ∈ ℝ ∀𝑘 ∈ ℕ (𝑆‘𝑘) ≤ 𝑧)) |
65 | 44, 64 | mpbird 246 |
. . . 4
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧) |
66 | | supxrre 12029 |
. . . 4
⊢ ((ran
𝑆 ⊆ ℝ ∧ ran
𝑆 ≠ ∅ ∧
∃𝑧 ∈ ℝ
∀𝑦 ∈ ran 𝑆 𝑦 ≤ 𝑧) → sup(ran 𝑆, ℝ*, < ) = sup(ran
𝑆, ℝ, <
)) |
67 | 51, 59, 65, 66 | syl3anc 1318 |
. . 3
⊢ (𝜑 → sup(ran 𝑆, ℝ*, < ) = sup(ran
𝑆, ℝ, <
)) |
68 | 49, 67 | eqtrd 2644 |
. 2
⊢ (𝜑 →
(∫2‘𝐹)
= sup(ran 𝑆, ℝ, <
)) |
69 | 45, 68 | breqtrrd 4611 |
1
⊢ (𝜑 → 𝑆 ⇝ (∫2‘𝐹)) |