Step | Hyp | Ref
| Expression |
1 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(𝐺‘𝑡) ∈ ℝ) |
2 | 1 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(𝐺‘𝑡) ∈ ℂ) |
3 | | i1ff 23249 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
4 | 3 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝐹‘𝑡) ∈
ℝ) |
5 | 4 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝐹‘𝑡) ∈
ℂ) |
6 | | subcl 10159 |
. . . . . . . . 9
⊢ (((𝐺‘𝑡) ∈ ℂ ∧ (𝐹‘𝑡) ∈ ℂ) → ((𝐺‘𝑡) − (𝐹‘𝑡)) ∈ ℂ) |
7 | 2, 5, 6 | syl2anr 494 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝐺:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ)) → ((𝐺‘𝑡) − (𝐹‘𝑡)) ∈ ℂ) |
8 | 7 | anandirs 870 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → ((𝐺‘𝑡) − (𝐹‘𝑡)) ∈ ℂ) |
9 | 8 | abscld 14023 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ ℝ) |
10 | 9 | rexrd 9968 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈
ℝ*) |
11 | 8 | absge0d 14031 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) |
12 | | elxrge0 12152 |
. . . . 5
⊢
((abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ (0[,]+∞) ↔
((abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) |
13 | 10, 11, 12 | sylanbrc 695 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ (0[,]+∞)) |
14 | | eqid 2610 |
. . . 4
⊢ (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) |
15 | 13, 14 | fmptd 6292 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
16 | 15 | 3adant2 1073 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
17 | | reex 9906 |
. . . . . . 7
⊢ ℝ
∈ V |
18 | 17 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → ℝ
∈ V) |
19 | | fvex 6113 |
. . . . . . 7
⊢
(abs‘(𝐺‘𝑡)) ∈ V |
20 | 19 | a1i 11 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈ V) |
21 | | fvex 6113 |
. . . . . . 7
⊢
(abs‘(𝐹‘𝑡)) ∈ V |
22 | 21 | a1i 11 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐹‘𝑡)) ∈ V) |
23 | | eqidd 2611 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) = (𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) |
24 | | eqidd 2611 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))) = (𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡)))) |
25 | 18, 20, 22, 23, 24 | offval2 6812 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∘𝑓
+ (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
26 | 25 | fveq2d 6107 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘((𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))))) =
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) |
27 | | id 22 |
. . . . . . . . . 10
⊢ (𝐺:ℝ⟶ℝ →
𝐺:ℝ⟶ℝ) |
28 | 27 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ℝ →
𝐺 = (𝑡 ∈ ℝ ↦ (𝐺‘𝑡))) |
29 | | absf 13925 |
. . . . . . . . . . 11
⊢
abs:ℂ⟶ℝ |
30 | 29 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐺:ℝ⟶ℝ →
abs:ℂ⟶ℝ) |
31 | 30 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ℝ →
abs = (𝑥 ∈ ℂ
↦ (abs‘𝑥))) |
32 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑡) → (abs‘𝑥) = (abs‘(𝐺‘𝑡))) |
33 | 2, 28, 31, 32 | fmptco 6303 |
. . . . . . . 8
⊢ (𝐺:ℝ⟶ℝ →
(abs ∘ 𝐺) = (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡)))) |
34 | 33 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (abs ∘
𝐺) = (𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) |
35 | | iblmbf 23340 |
. . . . . . . . 9
⊢ (𝐺 ∈ 𝐿1
→ 𝐺 ∈
MblFn) |
36 | | ftc1anclem1 32655 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶ℝ ∧
𝐺 ∈ MblFn) → (abs
∘ 𝐺) ∈
MblFn) |
37 | 35, 36 | sylan2 490 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶ℝ ∧
𝐺 ∈
𝐿1) → (abs ∘ 𝐺) ∈ MblFn) |
38 | 37 | ancoms 468 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (abs ∘
𝐺) ∈
MblFn) |
39 | 34, 38 | eqeltrrd 2689 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈
MblFn) |
40 | 39 | 3adant1 1072 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈
MblFn) |
41 | 2 | abscld 14023 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
ℝ) |
42 | 2 | absge0d 14031 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) → 0
≤ (abs‘(𝐺‘𝑡))) |
43 | | elrege0 12149 |
. . . . . . . 8
⊢
((abs‘(𝐺‘𝑡)) ∈ (0[,)+∞) ↔
((abs‘(𝐺‘𝑡)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑡)))) |
44 | 41, 42, 43 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
(0[,)+∞)) |
45 | | eqid 2610 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) = (𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡))) |
46 | 44, 45 | fmptd 6292 |
. . . . . 6
⊢ (𝐺:ℝ⟶ℝ →
(𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))):ℝ⟶(0[,)+∞)) |
47 | 46 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))):ℝ⟶(0[,)+∞)) |
48 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ,
(abs‘(𝐺‘𝑡)), 0) = (abs‘(𝐺‘𝑡))) |
49 | 48 | mpteq2ia 4668 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(𝐺‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡))) |
50 | 49 | fveq2i 6106 |
. . . . . . 7
⊢
(∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡)))) |
51 | 1 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → (𝐺‘𝑡) ∈ ℝ) |
52 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → 𝐺:ℝ⟶ℝ) |
53 | 52 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → 𝐺 = (𝑡 ∈ ℝ ↦ (𝐺‘𝑡))) |
54 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → 𝐺 ∈
𝐿1) |
55 | 53, 54 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦ (𝐺‘𝑡)) ∈
𝐿1) |
56 | 51, 55, 39 | iblabsnc 32644 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈
𝐿1) |
57 | 41 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
ℝ) |
58 | 42 | adantll 746 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(𝐺‘𝑡))) |
59 | 57, 58 | iblpos 23365 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈ 𝐿1
↔ ((𝑡 ∈ ℝ
↦ (abs‘(𝐺‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) ∈ ℝ))) |
60 | 56, 59 | mpbid 221 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) ∈ ℝ)) |
61 | 60 | simprd 478 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) ∈ ℝ) |
62 | 50, 61 | syl5eqelr 2693 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) ∈ ℝ) |
63 | 62 | 3adant1 1072 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) ∈ ℝ) |
64 | 5 | abscld 14023 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝐹‘𝑡)) ∈ ℝ) |
65 | 5 | absge0d 14031 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘(𝐹‘𝑡))) |
66 | | elrege0 12149 |
. . . . . . . 8
⊢
((abs‘(𝐹‘𝑡)) ∈ (0[,)+∞) ↔
((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐹‘𝑡)))) |
67 | 64, 65, 66 | sylanbrc 695 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝐹‘𝑡)) ∈ (0[,)+∞)) |
68 | | eqid 2610 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))) = (𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡))) |
69 | 67, 68 | fmptd 6292 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))):ℝ⟶(0[,)+∞)) |
70 | 69 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))):ℝ⟶(0[,)+∞)) |
71 | | iftrue 4042 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ,
(abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡))) |
72 | 71 | mpteq2ia 4668 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡))) |
73 | 72 | fveq2i 6106 |
. . . . . . 7
⊢
(∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡)))) |
74 | 3 | feqmptd 6159 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 = (𝑡 ∈ ℝ ↦ (𝐹‘𝑡))) |
75 | | i1fibl 23380 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
𝐿1) |
76 | 74, 75 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (𝐹‘𝑡)) ∈
𝐿1) |
77 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ dom ∫1
→ abs:ℂ⟶ℝ) |
78 | 77 | feqmptd 6159 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ dom ∫1
→ abs = (𝑥 ∈
ℂ ↦ (abs‘𝑥))) |
79 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐹‘𝑡) → (abs‘𝑥) = (abs‘(𝐹‘𝑡))) |
80 | 5, 74, 78, 79 | fmptco 6303 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (abs ∘ 𝐹) =
(𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡)))) |
81 | | i1fmbf 23248 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
MblFn) |
82 | | ftc1anclem1 32655 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℝ⟶ℝ ∧
𝐹 ∈ MblFn) → (abs
∘ 𝐹) ∈
MblFn) |
83 | 3, 81, 82 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (abs ∘ 𝐹)
∈ MblFn) |
84 | 80, 83 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈ MblFn) |
85 | 4, 76, 84 | iblabsnc 32644 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈
𝐿1) |
86 | 64, 65 | iblpos 23365 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈ 𝐿1 ↔
((𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ))) |
87 | 85, 86 | mpbid 221 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ)) |
88 | 87 | simprd 478 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ) |
89 | 73, 88 | syl5eqelr 2693 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡)))) ∈ ℝ) |
90 | 89 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐹‘𝑡)))) ∈ ℝ) |
91 | 40, 47, 63, 70, 90 | itg2addnc 32634 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘((𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))))) =
((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡)))))) |
92 | 26, 91 | eqtr3d 2646 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) = ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡)))) +
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐹‘𝑡)))))) |
93 | 63, 90 | readdcld 9948 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))))) ∈
ℝ) |
94 | 92, 93 | eqeltrd 2688 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) ∈ ℝ) |
95 | | readdcl 9898 |
. . . . . . . . 9
⊢
(((abs‘(𝐺‘𝑡)) ∈ ℝ ∧ (abs‘(𝐹‘𝑡)) ∈ ℝ) → ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ) |
96 | 41, 64, 95 | syl2anr 494 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝐺:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ)) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ) |
97 | 96 | anandirs 870 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ) |
98 | 97 | rexrd 9968 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈
ℝ*) |
99 | 41 | adantll 746 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
ℝ) |
100 | 64 | adantlr 747 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐹‘𝑡)) ∈
ℝ) |
101 | 42 | adantll 746 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(𝐺‘𝑡))) |
102 | 65 | adantlr 747 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(𝐹‘𝑡))) |
103 | 99, 100, 101, 102 | addge0d 10482 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
104 | | elxrge0 12152 |
. . . . . 6
⊢
(((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ (0[,]+∞) ↔
(((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ* ∧ 0 ≤
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
105 | 98, 103, 104 | sylanbrc 695 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ (0[,]+∞)) |
106 | | eqid 2610 |
. . . . 5
⊢ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
107 | 105, 106 | fmptd 6292 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
108 | 107 | 3adant2 1073 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
109 | | abs2dif2 13921 |
. . . . . . . 8
⊢ (((𝐺‘𝑡) ∈ ℂ ∧ (𝐹‘𝑡) ∈ ℂ) → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
110 | 2, 5, 109 | syl2anr 494 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝐺:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ)) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
111 | 110 | anandirs 870 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
112 | 111 | ralrimiva 2949 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) →
∀𝑡 ∈ ℝ
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
113 | 17 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → ℝ
∈ V) |
114 | | eqidd 2611 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) |
115 | | eqidd 2611 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
116 | 113, 9, 97, 114, 115 | ofrfval2 6813 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) ↔ ∀𝑡 ∈ ℝ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
117 | 112, 116 | mpbird 246 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
118 | 117 | 3adant2 1073 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
119 | | itg2le 23312 |
. . 3
⊢ (((𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ≤ (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) |
120 | 16, 108, 118, 119 | syl3anc 1318 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ≤ (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) |
121 | | itg2lecl 23311 |
. 2
⊢ (((𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ≤ (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ) |
122 | 16, 94, 120, 121 | syl3anc 1318 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ) |