Step | Hyp | Ref
| Expression |
1 | | itgulm.z |
. . . . 5
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | itgulm.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | 2 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑀 ∈
ℤ) |
4 | | itgulm.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝑍⟶𝐿1) |
5 | 4 | ffnd 6546 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝑍) |
6 | | itgulm.u |
. . . . . . 7
⊢ (𝜑 → 𝐹(⇝𝑢‘𝑆)𝐺) |
7 | | ulmf2 25276 |
. . . . . . 7
⊢ ((𝐹 Fn 𝑍 ∧ 𝐹(⇝𝑢‘𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) |
8 | 5, 6, 7 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) |
9 | 8 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑m 𝑆)) |
10 | | eqidd 2738 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) → ((𝐹‘𝑛)‘𝑧) = ((𝐹‘𝑛)‘𝑧)) |
11 | | eqidd 2738 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 ∈ 𝑆) → (𝐺‘𝑧) = (𝐺‘𝑧)) |
12 | 6 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐹(⇝𝑢‘𝑆)𝐺) |
13 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
14 | | itgulm.s |
. . . . . . . 8
⊢ (𝜑 → (vol‘𝑆) ∈
ℝ) |
15 | 14 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(vol‘𝑆) ∈
ℝ) |
16 | | ulmcl 25273 |
. . . . . . . . . . . 12
⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
17 | | fdm 6554 |
. . . . . . . . . . . 12
⊢ (𝐺:𝑆⟶ℂ → dom 𝐺 = 𝑆) |
18 | 6, 16, 17 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 = 𝑆) |
19 | 1, 2, 4, 6, 14 | iblulm 25299 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈
𝐿1) |
20 | | iblmbf 24665 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ 𝐿1
→ 𝐺 ∈
MblFn) |
21 | | mbfdm 24523 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 ∈ dom vol) |
23 | 18, 22 | eqeltrrd 2839 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ dom vol) |
24 | | mblss 24428 |
. . . . . . . . . 10
⊢ (𝑆 ∈ dom vol → 𝑆 ⊆
ℝ) |
25 | | ovolge0 24378 |
. . . . . . . . . 10
⊢ (𝑆 ⊆ ℝ → 0 ≤
(vol*‘𝑆)) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (vol*‘𝑆)) |
27 | | mblvol 24427 |
. . . . . . . . . 10
⊢ (𝑆 ∈ dom vol →
(vol‘𝑆) =
(vol*‘𝑆)) |
28 | 23, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (vol‘𝑆) = (vol*‘𝑆)) |
29 | 26, 28 | breqtrrd 5081 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (vol‘𝑆)) |
30 | 29 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 0 ≤
(vol‘𝑆)) |
31 | 15, 30 | ge0p1rpd 12658 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
((vol‘𝑆) + 1) ∈
ℝ+) |
32 | 13, 31 | rpdivcld 12645 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (𝑟 / ((vol‘𝑆) + 1)) ∈
ℝ+) |
33 | 1, 3, 9, 10, 11, 12, 32 | ulmi 25278 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1))) |
34 | 1 | uztrn2 12457 |
. . . . . . . 8
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
35 | 8 | ffvelrnda 6904 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈ (ℂ ↑m 𝑆)) |
36 | | elmapi 8530 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) ∈ (ℂ ↑m 𝑆) → (𝐹‘𝑛):𝑆⟶ℂ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):𝑆⟶ℂ) |
38 | 37 | ffvelrnda 6904 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ) |
39 | 38 | adantllr 719 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ) |
40 | 39 | adantlrr 721 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝑛)‘𝑥) ∈ ℂ) |
41 | 37 | feqmptd 6780 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) = (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑛)‘𝑥))) |
42 | 4 | ffvelrnda 6904 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛) ∈
𝐿1) |
43 | 41, 42 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑛)‘𝑥)) ∈
𝐿1) |
44 | 43 | ad2ant2r 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥 ∈ 𝑆 ↦ ((𝐹‘𝑛)‘𝑥)) ∈
𝐿1) |
45 | 6, 16 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑆⟶ℂ) |
46 | 45 | ffvelrnda 6904 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑥) ∈ ℂ) |
47 | 46 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥 ∈ 𝑆) → (𝐺‘𝑥) ∈ ℂ) |
48 | 45 | feqmptd 6780 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝑆 ↦ (𝐺‘𝑥))) |
49 | 48, 19 | eqeltrrd 2839 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↦ (𝐺‘𝑥)) ∈
𝐿1) |
50 | 49 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥 ∈ 𝑆 ↦ (𝐺‘𝑥)) ∈
𝐿1) |
51 | 40, 44, 47, 50 | itgsub 24723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)) d𝑥 = (∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) |
52 | 51 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)) d𝑥) = (abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥))) |
53 | 40, 47 | subcld 11189 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥 ∈ 𝑆) → (((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)) ∈ ℂ) |
54 | 40, 44, 47, 50 | iblsub 24719 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥 ∈ 𝑆 ↦ (((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) ∈
𝐿1) |
55 | 53, 54 | itgcl 24681 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)) d𝑥 ∈ ℂ) |
56 | 55 | abscld 15000 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)) d𝑥) ∈ ℝ) |
57 | 53 | abscld 15000 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥 ∈ 𝑆) → (abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) ∈ ℝ) |
58 | 53, 54 | iblabs 24726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥 ∈ 𝑆 ↦ (abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)))) ∈
𝐿1) |
59 | 57, 58 | itgrecl 24695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) d𝑥 ∈ ℝ) |
60 | | rpre 12594 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
61 | 60 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 𝑟 ∈ ℝ) |
62 | 53, 54 | itgabs 24732 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)) d𝑥) ≤ ∫𝑆(abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) d𝑥) |
63 | 32 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 / ((vol‘𝑆) + 1)) ∈
ℝ+) |
64 | 63 | rpred 12628 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℝ) |
65 | 14 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (vol‘𝑆) ∈
ℝ) |
66 | 64, 65 | remulcld 10863 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)) ∈
ℝ) |
67 | | fconstmpt 5611 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 × {(𝑟 / ((vol‘𝑆) + 1))}) = (𝑥 ∈ 𝑆 ↦ (𝑟 / ((vol‘𝑆) + 1))) |
68 | 23 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 𝑆 ∈ dom vol) |
69 | 63 | rpcnd 12630 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℂ) |
70 | | iblconst 24715 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ dom vol ∧
(vol‘𝑆) ∈
ℝ ∧ (𝑟 /
((vol‘𝑆) + 1)) ∈
ℂ) → (𝑆 ×
{(𝑟 / ((vol‘𝑆) + 1))}) ∈
𝐿1) |
71 | 68, 65, 69, 70 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑆 × {(𝑟 / ((vol‘𝑆) + 1))}) ∈
𝐿1) |
72 | 67, 71 | eqeltrrid 2843 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥 ∈ 𝑆 ↦ (𝑟 / ((vol‘𝑆) + 1))) ∈
𝐿1) |
73 | 64 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥 ∈ 𝑆) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℝ) |
74 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1))) |
75 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → ((𝐹‘𝑛)‘𝑧) = ((𝐹‘𝑛)‘𝑥)) |
76 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑥 → (𝐺‘𝑧) = (𝐺‘𝑥)) |
77 | 75, 76 | oveq12d 7231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 𝑥 → (((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧)) = (((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) |
78 | 77 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 𝑥 → (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) = (abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)))) |
79 | 78 | breq1d 5063 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑥 → ((abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) ↔ (abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) < (𝑟 / ((vol‘𝑆) + 1)))) |
80 | 79 | rspccva 3536 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑧 ∈
𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) ∧ 𝑥 ∈ 𝑆) → (abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) < (𝑟 / ((vol‘𝑆) + 1))) |
81 | 74, 80 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥 ∈ 𝑆) → (abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) < (𝑟 / ((vol‘𝑆) + 1))) |
82 | 57, 73, 81 | ltled 10980 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥 ∈ 𝑆) → (abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) ≤ (𝑟 / ((vol‘𝑆) + 1))) |
83 | 58, 72, 57, 73, 82 | itgle 24707 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) d𝑥 ≤ ∫𝑆(𝑟 / ((vol‘𝑆) + 1)) d𝑥) |
84 | | itgconst 24716 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ dom vol ∧
(vol‘𝑆) ∈
ℝ ∧ (𝑟 /
((vol‘𝑆) + 1)) ∈
ℂ) → ∫𝑆(𝑟 / ((vol‘𝑆) + 1)) d𝑥 = ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆))) |
85 | 68, 65, 69, 84 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(𝑟 / ((vol‘𝑆) + 1)) d𝑥 = ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆))) |
86 | 83, 85 | breqtrd 5079 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) d𝑥 ≤ ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆))) |
87 | 61 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 𝑟 ∈ ℂ) |
88 | 65 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (vol‘𝑆) ∈
ℂ) |
89 | 31 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ∈
ℝ+) |
90 | 89 | rpcnd 12630 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ∈
ℂ) |
91 | 89 | rpne0d 12633 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ≠ 0) |
92 | 87, 88, 90, 91 | div23d 11645 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 · (vol‘𝑆)) / ((vol‘𝑆) + 1)) = ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆))) |
93 | 65 | ltp1d 11762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (vol‘𝑆) < ((vol‘𝑆) + 1)) |
94 | | peano2re 11005 |
. . . . . . . . . . . . . . . . 17
⊢
((vol‘𝑆)
∈ ℝ → ((vol‘𝑆) + 1) ∈ ℝ) |
95 | 65, 94 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ∈
ℝ) |
96 | | rpgt0 12598 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 0 < 𝑟) |
97 | 96 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 0 < 𝑟) |
98 | | ltmul2 11683 |
. . . . . . . . . . . . . . . 16
⊢
(((vol‘𝑆)
∈ ℝ ∧ ((vol‘𝑆) + 1) ∈ ℝ ∧ (𝑟 ∈ ℝ ∧ 0 <
𝑟)) →
((vol‘𝑆) <
((vol‘𝑆) + 1) ↔
(𝑟 ·
(vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1)))) |
99 | 65, 95, 61, 97, 98 | syl112anc 1376 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) < ((vol‘𝑆) + 1) ↔ (𝑟 · (vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1)))) |
100 | 93, 99 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 · (vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1))) |
101 | 61, 65 | remulcld 10863 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 · (vol‘𝑆)) ∈ ℝ) |
102 | 101, 61, 89 | ltdivmul2d 12680 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (((𝑟 · (vol‘𝑆)) / ((vol‘𝑆) + 1)) < 𝑟 ↔ (𝑟 · (vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1)))) |
103 | 100, 102 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 · (vol‘𝑆)) / ((vol‘𝑆) + 1)) < 𝑟) |
104 | 92, 103 | eqbrtrrd 5077 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)) < 𝑟) |
105 | 59, 66, 61, 86, 104 | lelttrd 10990 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥))) d𝑥 < 𝑟) |
106 | 56, 59, 61, 62, 105 | lelttrd 10990 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹‘𝑛)‘𝑥) − (𝐺‘𝑥)) d𝑥) < 𝑟) |
107 | 52, 106 | eqbrtrrd 5077 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ ∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟) |
108 | 107 | expr 460 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑛 ∈ 𝑍) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → (abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟)) |
109 | 34, 108 | sylan2 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → (abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟)) |
110 | 109 | anassrs 471 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → (abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟)) |
111 | 110 | ralimdva 3100 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑛 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟)) |
112 | 111 | reximdva 3193 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑛)‘𝑧) − (𝐺‘𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟)) |
113 | 33, 112 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟) |
114 | 113 | ralrimiva 3105 |
. 2
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟) |
115 | 1 | fvexi 6731 |
. . . . 5
⊢ 𝑍 ∈ V |
116 | 115 | mptex 7039 |
. . . 4
⊢ (𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) ∈ V |
117 | 116 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) ∈ V) |
118 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛)) |
119 | 118 | fveq1d 6719 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → ((𝐹‘𝑘)‘𝑥) = ((𝐹‘𝑛)‘𝑥)) |
120 | 119 | adantr 484 |
. . . . . 6
⊢ ((𝑘 = 𝑛 ∧ 𝑥 ∈ 𝑆) → ((𝐹‘𝑘)‘𝑥) = ((𝐹‘𝑛)‘𝑥)) |
121 | 120 | itgeq2dv 24679 |
. . . . 5
⊢ (𝑘 = 𝑛 → ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥 = ∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥) |
122 | | eqid 2737 |
. . . . 5
⊢ (𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) = (𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) |
123 | | itgex 24668 |
. . . . 5
⊢
∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 ∈ V |
124 | 121, 122,
123 | fvmpt 6818 |
. . . 4
⊢ (𝑛 ∈ 𝑍 → ((𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥)‘𝑛) = ∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥) |
125 | 124 | adantl 485 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ((𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥)‘𝑛) = ∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥) |
126 | 46, 49 | itgcl 24681 |
. . 3
⊢ (𝜑 → ∫𝑆(𝐺‘𝑥) d𝑥 ∈ ℂ) |
127 | 38, 43 | itgcl 24681 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 ∈ ℂ) |
128 | 1, 2, 117, 125, 126, 127 | clim2c 15066 |
. 2
⊢ (𝜑 → ((𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) ⇝ ∫𝑆(𝐺‘𝑥) d𝑥 ↔ ∀𝑟 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(∫𝑆((𝐹‘𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺‘𝑥) d𝑥)) < 𝑟)) |
129 | 114, 128 | mpbird 260 |
1
⊢ (𝜑 → (𝑘 ∈ 𝑍 ↦ ∫𝑆((𝐹‘𝑘)‘𝑥) d𝑥) ⇝ ∫𝑆(𝐺‘𝑥) d𝑥) |