| Step | Hyp | Ref
| Expression |
| 1 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(𝐺‘𝑡) ∈ ℝ) |
| 2 | 1 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(𝐺‘𝑡) ∈ ℂ) |
| 3 | | i1ff 25711 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ 𝐹:ℝ⟶ℝ) |
| 4 | 3 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝐹‘𝑡) ∈
ℝ) |
| 5 | 4 | recnd 11289 |
. . . . . . . . 9
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝐹‘𝑡) ∈
ℂ) |
| 6 | | subcl 11507 |
. . . . . . . . 9
⊢ (((𝐺‘𝑡) ∈ ℂ ∧ (𝐹‘𝑡) ∈ ℂ) → ((𝐺‘𝑡) − (𝐹‘𝑡)) ∈ ℂ) |
| 7 | 2, 5, 6 | syl2anr 597 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝐺:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ)) → ((𝐺‘𝑡) − (𝐹‘𝑡)) ∈ ℂ) |
| 8 | 7 | anandirs 679 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → ((𝐺‘𝑡) − (𝐹‘𝑡)) ∈ ℂ) |
| 9 | 8 | abscld 15475 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ ℝ) |
| 10 | 9 | rexrd 11311 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈
ℝ*) |
| 11 | 8 | absge0d 15483 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) |
| 12 | | elxrge0 13497 |
. . . . 5
⊢
((abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ (0[,]+∞) ↔
((abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) |
| 13 | 10, 11, 12 | sylanbrc 583 |
. . . 4
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ∈ (0[,]+∞)) |
| 14 | 13 | fmpttd 7135 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
| 15 | 14 | 3adant2 1132 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
| 16 | | reex 11246 |
. . . . . . 7
⊢ ℝ
∈ V |
| 17 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → ℝ
∈ V) |
| 18 | | fvexd 6921 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈ V) |
| 19 | | fvexd 6921 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐹‘𝑡)) ∈ V) |
| 20 | | eqidd 2738 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) = (𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) |
| 21 | | eqidd 2738 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))) = (𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡)))) |
| 22 | 17, 18, 19, 20, 21 | offval2 7717 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∘f + (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
| 23 | 22 | fveq2d 6910 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘((𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) |
| 24 | | id 22 |
. . . . . . . . . 10
⊢ (𝐺:ℝ⟶ℝ →
𝐺:ℝ⟶ℝ) |
| 25 | 24 | feqmptd 6977 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ℝ →
𝐺 = (𝑡 ∈ ℝ ↦ (𝐺‘𝑡))) |
| 26 | | absf 15376 |
. . . . . . . . . . 11
⊢
abs:ℂ⟶ℝ |
| 27 | 26 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐺:ℝ⟶ℝ →
abs:ℂ⟶ℝ) |
| 28 | 27 | feqmptd 6977 |
. . . . . . . . 9
⊢ (𝐺:ℝ⟶ℝ →
abs = (𝑥 ∈ ℂ
↦ (abs‘𝑥))) |
| 29 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = (𝐺‘𝑡) → (abs‘𝑥) = (abs‘(𝐺‘𝑡))) |
| 30 | 2, 25, 28, 29 | fmptco 7149 |
. . . . . . . 8
⊢ (𝐺:ℝ⟶ℝ →
(abs ∘ 𝐺) = (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡)))) |
| 31 | 30 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (abs ∘
𝐺) = (𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) |
| 32 | | iblmbf 25802 |
. . . . . . . . 9
⊢ (𝐺 ∈ 𝐿1
→ 𝐺 ∈
MblFn) |
| 33 | | ftc1anclem1 37700 |
. . . . . . . . 9
⊢ ((𝐺:ℝ⟶ℝ ∧
𝐺 ∈ MblFn) → (abs
∘ 𝐺) ∈
MblFn) |
| 34 | 32, 33 | sylan2 593 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶ℝ ∧
𝐺 ∈
𝐿1) → (abs ∘ 𝐺) ∈ MblFn) |
| 35 | 34 | ancoms 458 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (abs ∘
𝐺) ∈
MblFn) |
| 36 | 31, 35 | eqeltrrd 2842 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈
MblFn) |
| 37 | 36 | 3adant1 1131 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈
MblFn) |
| 38 | 2 | abscld 15475 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
ℝ) |
| 39 | 2 | absge0d 15483 |
. . . . . . . 8
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) → 0
≤ (abs‘(𝐺‘𝑡))) |
| 40 | | elrege0 13494 |
. . . . . . . 8
⊢
((abs‘(𝐺‘𝑡)) ∈ (0[,)+∞) ↔
((abs‘(𝐺‘𝑡)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐺‘𝑡)))) |
| 41 | 38, 39, 40 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝐺:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
(0[,)+∞)) |
| 42 | 41 | fmpttd 7135 |
. . . . . 6
⊢ (𝐺:ℝ⟶ℝ →
(𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))):ℝ⟶(0[,)+∞)) |
| 43 | 42 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))):ℝ⟶(0[,)+∞)) |
| 44 | | iftrue 4531 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ,
(abs‘(𝐺‘𝑡)), 0) = (abs‘(𝐺‘𝑡))) |
| 45 | 44 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(𝐺‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡))) |
| 46 | 45 | fveq2i 6909 |
. . . . . . 7
⊢
(∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡)))) |
| 47 | 1 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → (𝐺‘𝑡) ∈ ℝ) |
| 48 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → 𝐺:ℝ⟶ℝ) |
| 49 | 48 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → 𝐺 = (𝑡 ∈ ℝ ↦ (𝐺‘𝑡))) |
| 50 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → 𝐺 ∈
𝐿1) |
| 51 | 49, 50 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦ (𝐺‘𝑡)) ∈
𝐿1) |
| 52 | 47, 51, 36 | iblabsnc 37691 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈
𝐿1) |
| 53 | 38 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
ℝ) |
| 54 | 39 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(𝐺‘𝑡))) |
| 55 | 53, 54 | iblpos 25828 |
. . . . . . . . 9
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈ 𝐿1
↔ ((𝑡 ∈ ℝ
↦ (abs‘(𝐺‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) ∈ ℝ))) |
| 56 | 52, 55 | mpbid 232 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) ∈ ℝ)) |
| 57 | 56 | simprd 495 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐺‘𝑡)), 0))) ∈ ℝ) |
| 58 | 46, 57 | eqeltrrid 2846 |
. . . . . 6
⊢ ((𝐺 ∈ 𝐿1
∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) ∈ ℝ) |
| 59 | 58 | 3adant1 1131 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) ∈ ℝ) |
| 60 | 5 | abscld 15475 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝐹‘𝑡)) ∈ ℝ) |
| 61 | 5 | absge0d 15483 |
. . . . . . . 8
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘(𝐹‘𝑡))) |
| 62 | | elrege0 13494 |
. . . . . . . 8
⊢
((abs‘(𝐹‘𝑡)) ∈ (0[,)+∞) ↔
((abs‘(𝐹‘𝑡)) ∈ ℝ ∧ 0 ≤
(abs‘(𝐹‘𝑡)))) |
| 63 | 60, 61, 62 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝐹‘𝑡)) ∈ (0[,)+∞)) |
| 64 | 63 | fmpttd 7135 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))):ℝ⟶(0[,)+∞)) |
| 65 | 64 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))):ℝ⟶(0[,)+∞)) |
| 66 | | iftrue 4531 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ,
(abs‘(𝐹‘𝑡)), 0) = (abs‘(𝐹‘𝑡))) |
| 67 | 66 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡))) |
| 68 | 67 | fveq2i 6909 |
. . . . . . 7
⊢
(∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡)))) |
| 69 | 3 | feqmptd 6977 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 = (𝑡 ∈ ℝ ↦ (𝐹‘𝑡))) |
| 70 | | i1fibl 25843 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
𝐿1) |
| 71 | 69, 70 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (𝐹‘𝑡)) ∈
𝐿1) |
| 72 | 26 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ dom ∫1
→ abs:ℂ⟶ℝ) |
| 73 | 72 | feqmptd 6977 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ dom ∫1
→ abs = (𝑥 ∈
ℂ ↦ (abs‘𝑥))) |
| 74 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝐹‘𝑡) → (abs‘𝑥) = (abs‘(𝐹‘𝑡))) |
| 75 | 5, 69, 73, 74 | fmptco 7149 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (abs ∘ 𝐹) =
(𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡)))) |
| 76 | | i1fmbf 25710 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ dom ∫1
→ 𝐹 ∈
MblFn) |
| 77 | | ftc1anclem1 37700 |
. . . . . . . . . . . 12
⊢ ((𝐹:ℝ⟶ℝ ∧
𝐹 ∈ MblFn) → (abs
∘ 𝐹) ∈
MblFn) |
| 78 | 3, 76, 77 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ dom ∫1
→ (abs ∘ 𝐹)
∈ MblFn) |
| 79 | 75, 78 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈ MblFn) |
| 80 | 4, 71, 79 | iblabsnc 37691 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈
𝐿1) |
| 81 | 60, 61 | iblpos 25828 |
. . . . . . . . 9
⊢ (𝐹 ∈ dom ∫1
→ ((𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈ 𝐿1 ↔
((𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ))) |
| 82 | 80, 81 | mpbid 232 |
. . . . . . . 8
⊢ (𝐹 ∈ dom ∫1
→ ((𝑡 ∈ ℝ
↦ (abs‘(𝐹‘𝑡))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ)) |
| 83 | 82 | simprd 495 |
. . . . . . 7
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(𝐹‘𝑡)), 0))) ∈ ℝ) |
| 84 | 68, 83 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝐹 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡)))) ∈ ℝ) |
| 85 | 84 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐹‘𝑡)))) ∈ ℝ) |
| 86 | 37, 43, 59, 65, 85 | itg2addnc 37681 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘((𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡))) ∘f + (𝑡 ∈ ℝ ↦ (abs‘(𝐹‘𝑡))))) = ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡)))) +
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐹‘𝑡)))))) |
| 87 | 23, 86 | eqtr3d 2779 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) = ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐺‘𝑡)))) +
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(𝐹‘𝑡)))))) |
| 88 | 59, 85 | readdcld 11290 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(𝐺‘𝑡)))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(𝐹‘𝑡))))) ∈
ℝ) |
| 89 | 87, 88 | eqeltrd 2841 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) ∈ ℝ) |
| 90 | | readdcl 11238 |
. . . . . . . . 9
⊢
(((abs‘(𝐺‘𝑡)) ∈ ℝ ∧ (abs‘(𝐹‘𝑡)) ∈ ℝ) → ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ) |
| 91 | 38, 60, 90 | syl2anr 597 |
. . . . . . . 8
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝐺:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ)) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ) |
| 92 | 91 | anandirs 679 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ) |
| 93 | 92 | rexrd 11311 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈
ℝ*) |
| 94 | 38 | adantll 714 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐺‘𝑡)) ∈
ℝ) |
| 95 | 60 | adantlr 715 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘(𝐹‘𝑡)) ∈
ℝ) |
| 96 | 39 | adantll 714 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(𝐺‘𝑡))) |
| 97 | 61 | adantlr 715 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(𝐹‘𝑡))) |
| 98 | 94, 95, 96, 97 | addge0d 11839 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) → 0 ≤
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
| 99 | | elxrge0 13497 |
. . . . . 6
⊢
(((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ (0[,]+∞) ↔
(((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ ℝ* ∧ 0 ≤
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
| 100 | 93, 98, 99 | sylanbrc 583 |
. . . . 5
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))) ∈ (0[,]+∞)) |
| 101 | 100 | fmpttd 7135 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
| 102 | 101 | 3adant2 1132 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))):ℝ⟶(0[,]+∞)) |
| 103 | | abs2dif2 15372 |
. . . . . . . 8
⊢ (((𝐺‘𝑡) ∈ ℂ ∧ (𝐹‘𝑡) ∈ ℂ) → (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
| 104 | 2, 5, 103 | syl2anr 597 |
. . . . . . 7
⊢ (((𝐹 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝐺:ℝ⟶ℝ ∧ 𝑡 ∈ ℝ)) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
| 105 | 104 | anandirs 679 |
. . . . . 6
⊢ (((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) ∧ 𝑡 ∈ ℝ) →
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
| 106 | 105 | ralrimiva 3146 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) →
∀𝑡 ∈ ℝ
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) |
| 107 | 16 | a1i 11 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → ℝ
∈ V) |
| 108 | | eqidd 2738 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) |
| 109 | | eqidd 2738 |
. . . . . 6
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
| 110 | 107, 9, 92, 108, 109 | ofrfval2 7718 |
. . . . 5
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → ((𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘r ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))) ↔ ∀𝑡 ∈ ℝ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))) ≤ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
| 111 | 106, 110 | mpbird 257 |
. . . 4
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘r ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
| 112 | 111 | 3adant2 1132 |
. . 3
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) → (𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘r ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) |
| 113 | | itg2le 25774 |
. . 3
⊢ (((𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))) ∘r ≤ (𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ≤ (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) |
| 114 | 15, 102, 112, 113 | syl3anc 1373 |
. 2
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ≤ (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) |
| 115 | | itg2lecl 25773 |
. 2
⊢ (((𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡)))):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ≤ (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝐺‘𝑡)) + (abs‘(𝐹‘𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ) |
| 116 | 15, 89, 114, 115 | syl3anc 1373 |
1
⊢ ((𝐹 ∈ dom ∫1
∧ 𝐺 ∈
𝐿1 ∧ 𝐺:ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((𝐺‘𝑡) − (𝐹‘𝑡))))) ∈ ℝ) |