Proof of Theorem ftc1anclem8
Step | Hyp | Ref
| Expression |
1 | | ftc1anc.g |
. . 3
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
2 | | ftc1anc.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | | ftc1anc.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
4 | | ftc1anc.le |
. . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
5 | | ftc1anc.s |
. . 3
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
6 | | ftc1anc.d |
. . 3
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
7 | | ftc1anc.i |
. . 3
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
8 | | ftc1anc.f |
. . 3
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | ftc1anclem7 32661 |
. 2
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2))) |
10 | | simplll 794 |
. . . 4
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom
∫1))) |
11 | | 3simpa 1051 |
. . . 4
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤) → (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) |
12 | | ioossre 12106 |
. . . . . . . . 9
⊢ (𝑢(,)𝑤) ⊆ ℝ |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑢(,)𝑤) ⊆
ℝ) |
14 | | rembl 23115 |
. . . . . . . . 9
⊢ ℝ
∈ dom vol |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ℝ ∈ dom vol) |
16 | | fvex 6113 |
. . . . . . . . . 10
⊢
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ V |
17 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
18 | 16, 17 | ifex 4106 |
. . . . . . . . 9
⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V) |
20 | | eldifn 3695 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (ℝ ∖ (𝑢(,)𝑤)) → ¬ 𝑡 ∈ (𝑢(,)𝑤)) |
21 | 20 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (ℝ
∖ (𝑢(,)𝑤))) → ¬ 𝑡 ∈ (𝑢(,)𝑤)) |
22 | 21 | iffalsed 4047 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (ℝ
∖ (𝑢(,)𝑤))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0) |
23 | | iftrue 4042 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
24 | 23 | mpteq2ia 4668 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
25 | | resmpt 5369 |
. . . . . . . . . . . 12
⊢ ((𝑢(,)𝑤) ⊆ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
26 | 12, 25 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ↦
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) = (𝑡 ∈ (𝑢(,)𝑤) ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
27 | 24, 26 | eqtr4i 2635 |
. . . . . . . . . 10
⊢ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) |
28 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
29 | 28 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℝ) |
30 | 29 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℂ) |
31 | | ax-icn 9874 |
. . . . . . . . . . . . . . . . 17
⊢ i ∈
ℂ |
32 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
33 | 32 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
34 | 33 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℂ) |
35 | | mulcl 9899 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ) |
36 | 31, 34, 35 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (i · (𝑔‘𝑡)) ∈ ℂ) |
37 | | addcl 9897 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
38 | 30, 36, 37 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
39 | 38 | anandirs 870 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
40 | | reex 9906 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
∈ V |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ℝ ∈ V) |
42 | 29 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (𝑓‘𝑡) ∈ ℝ) |
43 | 36 | adantll 746 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (i · (𝑔‘𝑡)) ∈ ℂ) |
44 | 28 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡))) |
45 | 44 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑓
= (𝑡 ∈ ℝ ↦
(𝑓‘𝑡))) |
46 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ∈ dom ∫1
→ ℝ ∈ V) |
47 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ i ∈ ℂ) |
48 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℝ
× {i}) = (𝑡 ∈
ℝ ↦ i) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ∈ dom ∫1
→ (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i)) |
50 | 32 | feqmptd 6159 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡))) |
51 | 46, 47, 33, 49, 50 | offval2 6812 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 ∈ dom ∫1
→ ((ℝ × {i}) ∘𝑓 · 𝑔) = (𝑡 ∈ ℝ ↦ (i · (𝑔‘𝑡)))) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((ℝ × {i}) ∘𝑓
· 𝑔) = (𝑡 ∈ ℝ ↦ (i
· (𝑔‘𝑡)))) |
53 | 41, 42, 43, 45, 52 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
54 | | absf 13925 |
. . . . . . . . . . . . . . . 16
⊢
abs:ℂ⟶ℝ |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → abs:ℂ⟶ℝ) |
56 | 55 | feqmptd 6159 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥))) |
57 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) → (abs‘𝑥) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
58 | 39, 53, 56, 57 | fmptco 6303 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
59 | | ftc1anclem3 32657 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔))) ∈ dom
∫1) |
60 | 58, 59 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom
∫1) |
61 | | i1fmbf 23248 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ↦
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ dom ∫1 →
(𝑡 ∈ ℝ ↦
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn) |
63 | | ioombl 23140 |
. . . . . . . . . . 11
⊢ (𝑢(,)𝑤) ∈ dom vol |
64 | | mbfres 23217 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ ℝ ↦
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ MblFn ∧ (𝑢(,)𝑤) ∈ dom vol) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn) |
65 | 62, 63, 64 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ (𝑢(,)𝑤)) ∈ MblFn) |
66 | 27, 65 | syl5eqel 2692 |
. . . . . . . . 9
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn) |
67 | 66 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ (𝑢(,)𝑤) ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn) |
68 | 13, 15, 19, 22, 67 | mbfss 23219 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn) |
69 | 68 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn) |
70 | 39 | abscld 14023 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
71 | 39 | absge0d 14031 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
72 | | elrege0 12149 |
. . . . . . . . . 10
⊢
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ↔
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ≤
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
73 | 70, 71, 72 | sylanbrc 695 |
. . . . . . . . 9
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞)) |
74 | | 0e0icopnf 12153 |
. . . . . . . . 9
⊢ 0 ∈
(0[,)+∞) |
75 | | ifcl 4080 |
. . . . . . . . 9
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈
(0[,)+∞)) → if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,)+∞)) |
76 | 73, 74, 75 | sylancl 693 |
. . . . . . . 8
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,)+∞)) |
77 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
78 | 76, 77 | fmptd 6292 |
. . . . . . 7
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,)+∞)) |
79 | 78 | ad2antlr 759 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,)+∞)) |
80 | 70 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈
ℝ*) |
81 | | elxrge0 12152 |
. . . . . . . . . . 11
⊢
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ↔
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
82 | 80, 71, 81 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞)) |
83 | | 0e0iccpnf 12154 |
. . . . . . . . . 10
⊢ 0 ∈
(0[,]+∞) |
84 | | ifcl 4080 |
. . . . . . . . . 10
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈
(0[,]+∞)) → if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,]+∞)) |
85 | 82, 83, 84 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,]+∞)) |
86 | 85, 77 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,]+∞)) |
87 | 86 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,]+∞)) |
88 | | ifcl 4080 |
. . . . . . . . . . 11
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈
(0[,]+∞)) → if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,]+∞)) |
89 | 82, 83, 88 | sylancl 693 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,]+∞)) |
90 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
91 | 89, 90 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,]+∞)) |
92 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
93 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:ℝ⟶ℝ →
ran 𝑓 ⊆
ℝ) |
94 | | ax-resscn 9872 |
. . . . . . . . . . . . . . . 16
⊢ ℝ
⊆ ℂ |
95 | 93, 94 | syl6ss 3580 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:ℝ⟶ℝ →
ran 𝑓 ⊆
ℂ) |
96 | | ffn 5958 |
. . . . . . . . . . . . . . . . 17
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
97 | 54, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ abs Fn
ℂ |
98 | | fnco 5913 |
. . . . . . . . . . . . . . . 16
⊢ ((abs Fn
ℂ ∧ 𝑓 Fn ℝ
∧ ran 𝑓 ⊆
ℂ) → (abs ∘ 𝑓) Fn ℝ) |
99 | 97, 98 | mp3an1 1403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 Fn ℝ ∧ ran 𝑓 ⊆ ℂ) → (abs
∘ 𝑓) Fn
ℝ) |
100 | 92, 95, 99 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑓:ℝ⟶ℝ →
(abs ∘ 𝑓) Fn
ℝ) |
101 | 28, 100 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ dom ∫1
→ (abs ∘ 𝑓) Fn
ℝ) |
102 | 101 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ 𝑓) Fn ℝ) |
103 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℝ⟶ℝ →
𝑔 Fn
ℝ) |
104 | | frn 5966 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:ℝ⟶ℝ →
ran 𝑔 ⊆
ℝ) |
105 | 104, 94 | syl6ss 3580 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:ℝ⟶ℝ →
ran 𝑔 ⊆
ℂ) |
106 | | fnco 5913 |
. . . . . . . . . . . . . . . 16
⊢ ((abs Fn
ℂ ∧ 𝑔 Fn ℝ
∧ ran 𝑔 ⊆
ℂ) → (abs ∘ 𝑔) Fn ℝ) |
107 | 97, 106 | mp3an1 1403 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 Fn ℝ ∧ ran 𝑔 ⊆ ℂ) → (abs
∘ 𝑔) Fn
ℝ) |
108 | 103, 105,
107 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝑔:ℝ⟶ℝ →
(abs ∘ 𝑔) Fn
ℝ) |
109 | 32, 108 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ (abs ∘ 𝑔) Fn
ℝ) |
110 | 109 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ 𝑔) Fn ℝ) |
111 | | inidm 3784 |
. . . . . . . . . . . 12
⊢ (ℝ
∩ ℝ) = ℝ |
112 | 28 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑓:ℝ⟶ℝ) |
113 | | fvco3 6185 |
. . . . . . . . . . . . 13
⊢ ((𝑓:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡))) |
114 | 112, 113 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs ∘ 𝑓)‘𝑡) = (abs‘(𝑓‘𝑡))) |
115 | 32 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑔:ℝ⟶ℝ) |
116 | | fvco3 6185 |
. . . . . . . . . . . . 13
⊢ ((𝑔:ℝ⟶ℝ ∧
𝑡 ∈ ℝ) →
((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡))) |
117 | 115, 116 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs ∘ 𝑔)‘𝑡) = (abs‘(𝑔‘𝑡))) |
118 | 102, 110,
41, 41, 111, 114, 117 | offval 6802 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((abs ∘ 𝑓) ∘𝑓 + (abs ∘
𝑔)) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) |
119 | 30 | addid1d 10115 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ ((𝑓‘𝑡) + 0) = (𝑓‘𝑡)) |
120 | 119 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ ((𝑓‘𝑡) + 0)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡))) |
121 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ dom ∫1
→ ℝ ∈ V) |
122 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ∈ V) |
123 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ i ∈ ℂ) |
124 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ (ℝ × {i}) = (𝑡 ∈ ℝ ↦ i)) |
125 | | fconstmpt 5085 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℝ
× {0}) = (𝑡 ∈
ℝ ↦ 0) |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)) |
127 | 121, 123,
122, 124, 126 | offval2 6812 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ ((ℝ × {i}) ∘𝑓 · (ℝ
× {0})) = (𝑡 ∈
ℝ ↦ (i · 0))) |
128 | | it0e0 11131 |
. . . . . . . . . . . . . . . . . . 19
⊢ (i
· 0) = 0 |
129 | 128 | mpteq2i 4669 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ ↦ (i
· 0)) = (𝑡 ∈
ℝ ↦ 0) |
130 | 127, 129 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ dom ∫1
→ ((ℝ × {i}) ∘𝑓 · (ℝ
× {0})) = (𝑡 ∈
ℝ ↦ 0)) |
131 | 121, 29, 122, 44, 130 | offval2 6812 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈ dom ∫1
→ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · (ℝ × {0}))) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + 0))) |
132 | 120, 131,
44 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ dom ∫1
→ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · (ℝ × {0}))) = 𝑓) |
133 | 132 | coeq2d 5206 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ dom ∫1
→ (abs ∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · (ℝ × {0})))) = (abs ∘
𝑓)) |
134 | | i1f0 23260 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
× {0}) ∈ dom ∫1 |
135 | | ftc1anclem3 32657 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ (ℝ × {0}) ∈ dom ∫1) → (abs ∘
(𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · (ℝ × {0})))) ∈ dom
∫1) |
136 | 134, 135 | mpan2 703 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ dom ∫1
→ (abs ∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · (ℝ × {0})))) ∈ dom
∫1) |
137 | 133, 136 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ dom ∫1
→ (abs ∘ 𝑓)
∈ dom ∫1) |
138 | 137 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ 𝑓) ∈ dom
∫1) |
139 | | coeq2 5202 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑔 → (abs ∘ 𝑓) = (abs ∘ 𝑔)) |
140 | 139 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑔 → ((abs ∘ 𝑓) ∈ dom ∫1 ↔ (abs
∘ 𝑔) ∈ dom
∫1)) |
141 | 140, 137 | vtoclga 3245 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ (abs ∘ 𝑔)
∈ dom ∫1) |
142 | 141 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ 𝑔) ∈ dom
∫1) |
143 | 138, 142 | i1fadd 23268 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((abs ∘ 𝑓) ∘𝑓 + (abs ∘
𝑔)) ∈ dom
∫1) |
144 | 118, 143 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom
∫1) |
145 | 30 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑓‘𝑡)) ∈ ℝ) |
146 | 30 | absge0d 14031 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘(𝑓‘𝑡))) |
147 | | elrege0 12149 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ↔
((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ 0 ≤
(abs‘(𝑓‘𝑡)))) |
148 | 145, 146,
147 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑓‘𝑡)) ∈ (0[,)+∞)) |
149 | 34 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑔‘𝑡)) ∈ ℝ) |
150 | 34 | absge0d 14031 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘(𝑔‘𝑡))) |
151 | | elrege0 12149 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘(𝑔‘𝑡)) ∈ (0[,)+∞) ↔
((abs‘(𝑔‘𝑡)) ∈ ℝ ∧ 0 ≤
(abs‘(𝑔‘𝑡)))) |
152 | 149, 150,
151 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑔‘𝑡)) ∈ (0[,)+∞)) |
153 | | ge0addcl 12155 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝑓‘𝑡)) ∈ (0[,)+∞) ∧
(abs‘(𝑔‘𝑡)) ∈ (0[,)+∞)) →
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞)) |
154 | 148, 152,
153 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞)) |
155 | 154 | anandirs 870 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ (0[,)+∞)) |
156 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) |
157 | 155, 156 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞)) |
158 | | 0plef 23245 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ↔
((𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) |
159 | 157, 158 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶ℝ ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) |
160 | 159 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0𝑝 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) |
161 | | itg2itg1 23309 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) = (∫1‘(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) |
162 | | itg1cl 23258 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 →
(∫1‘(𝑡
∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ) |
163 | 162 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫1‘(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ) |
164 | 161, 163 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ) |
165 | 144, 160,
164 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∫2‘(𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ) |
166 | | icossicc 12131 |
. . . . . . . . . . 11
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
167 | | fss 5969 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,)+∞) ∧
(0[,)+∞) ⊆ (0[,]+∞)) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞)) |
168 | 157, 166,
167 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞)) |
169 | | 0re 9919 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
170 | | ifcl 4080 |
. . . . . . . . . . . . . 14
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ) |
171 | 70, 169, 170 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ) |
172 | | readdcl 9898 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ (abs‘(𝑔‘𝑡)) ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ) |
173 | 145, 149,
172 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ) |
174 | 173 | anandirs 870 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ) |
175 | 70 | leidd 10473 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
176 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
177 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (0 =
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
178 | 176, 177 | ifboth 4074 |
. . . . . . . . . . . . . 14
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∧ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
179 | 175, 71, 178 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
180 | | abstri 13918 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡))))) |
181 | 30, 36, 180 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡))))) |
182 | 181 | anandirs 870 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡))))) |
183 | | absmul 13882 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (abs‘(i
· (𝑔‘𝑡))) = ((abs‘i) ·
(abs‘(𝑔‘𝑡)))) |
184 | 31, 34, 183 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) ·
(abs‘(𝑔‘𝑡)))) |
185 | | absi 13874 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs‘i) = 1 |
186 | 185 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . 18
⊢
((abs‘i) · (abs‘(𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡))) |
187 | 184, 186 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · (𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡)))) |
188 | 149 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑔‘𝑡)) ∈ ℂ) |
189 | 188 | mulid2d 9937 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (1 · (abs‘(𝑔‘𝑡))) = (abs‘(𝑔‘𝑡))) |
190 | 187, 189 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡))) |
191 | 190 | adantll 746 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡))) |
192 | 191 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))) = ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) |
193 | 182, 192 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) |
194 | 171, 70, 174, 179, 193 | letrd 10073 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) |
195 | 194 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) |
196 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
197 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) |
198 | 41, 171, 174, 196, 197 | ofrfval2 6813 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) |
199 | 195, 198 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) |
200 | | itg2le 23312 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) |
201 | 91, 168, 199, 200 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) |
202 | | itg2lecl 23311 |
. . . . . . . . 9
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
203 | 91, 165, 201, 202 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
204 | 203 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
205 | 91 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,]+∞)) |
206 | | breq1 4586 |
. . . . . . . . . . 11
⊢
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
207 | | breq1 4586 |
. . . . . . . . . . 11
⊢ (0 =
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
208 | | elioore 12076 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ) |
209 | 208, 175 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
210 | 209 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
211 | 210 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
212 | 2 | rexrd 9968 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
213 | 3 | rexrd 9968 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
214 | 212, 213 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
215 | | df-icc 12053 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)}) |
216 | 215 | elixx3g 12059 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑢 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
217 | 216 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)) |
218 | 217 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢) |
219 | 215 | elixx3g 12059 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))) |
220 | 219 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)) |
221 | 220 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵) |
222 | 218, 221 | anim12i 588 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) |
223 | | ioossioo 12136 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
224 | 214, 222,
223 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
225 | 5 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷) |
226 | 224, 225 | sstrd 3578 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷) |
227 | 226 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷) |
228 | | iftrue 4042 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
229 | 227, 228 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
230 | 229 | adantllr 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
231 | 211, 230 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
232 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
233 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
234 | 6 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ) |
235 | 234 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ) |
236 | 71 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
237 | 235, 236 | syldan 486 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → 0 ≤
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
238 | | 0le0 10987 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
0 |
239 | 238 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ¬ 𝑡 ∈ 𝐷) → 0 ≤
0) |
240 | 232, 233,
237, 239 | ifbothda 4073 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ 0 ≤ if(𝑡 ∈
𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
241 | 240 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
242 | 206, 207,
231, 241 | ifbothda 4073 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
243 | 242 | ralrimivw 2950 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
244 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ℝ ∈
V) |
245 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V) |
246 | 16, 17 | ifex 4106 |
. . . . . . . . . . . 12
⊢ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V |
247 | 246 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V) |
248 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
249 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
250 | 244, 245,
247, 248, 249 | ofrfval2 6813 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
251 | 250 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
252 | 243, 251 | mpbird 246 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
253 | | itg2le 23312 |
. . . . . . . 8
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))) |
254 | 87, 205, 252, 253 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))) |
255 | | itg2lecl 23311 |
. . . . . . 7
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
256 | 87, 204, 254, 255 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
257 | 8 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
258 | 257 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
259 | 227, 258 | syldan 486 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
260 | 259 | adantllr 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
261 | 208, 39 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
262 | 261 | adantll 746 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
263 | 262 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
264 | 260, 263 | subcld 10271 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
265 | 264 | abscld 14023 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
266 | 264 | absge0d 14031 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
267 | | elrege0 12149 |
. . . . . . . . . 10
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞) ↔
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ ∧ 0 ≤
(abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
268 | 265, 266,
267 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,)+∞)) |
269 | 74 | a1i 11 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
(0[,)+∞)) |
270 | 268, 269 | ifclda 4070 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,)+∞)) |
271 | 270 | adantr 480 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,)+∞)) |
272 | | eqid 2610 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
273 | 271, 272 | fmptd 6292 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))),
0)):ℝ⟶(0[,)+∞)) |
274 | 265 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
275 | | elxrge0 12152 |
. . . . . . . . . . 11
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
276 | 274, 266,
275 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞)) |
277 | 83 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
(0[,]+∞)) |
278 | 276, 277 | ifclda 4070 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
279 | 278 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
280 | 279, 272 | fmptd 6292 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))),
0)):ℝ⟶(0[,]+∞)) |
281 | | recncf 22513 |
. . . . . . . . . . . . 13
⊢ ℜ
∈ (ℂ–cn→ℝ) |
282 | | prid1g 4239 |
. . . . . . . . . . . . 13
⊢ (ℜ
∈ (ℂ–cn→ℝ)
→ ℜ ∈ {ℜ, ℑ}) |
283 | 281, 282 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ℜ
∈ {ℜ, ℑ} |
284 | | ftc1anclem2 32656 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℜ
∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
285 | 283, 284 | mp3an3 1405 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
286 | 8, 7, 285 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
287 | | imcncf 22514 |
. . . . . . . . . . . . 13
⊢ ℑ
∈ (ℂ–cn→ℝ) |
288 | | prid2g 4240 |
. . . . . . . . . . . . 13
⊢ (ℑ
∈ (ℂ–cn→ℝ)
→ ℑ ∈ {ℜ, ℑ}) |
289 | 287, 288 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ℑ
∈ {ℜ, ℑ} |
290 | | ftc1anclem2 32656 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1 ∧ ℑ
∈ {ℜ, ℑ}) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
291 | 289, 290 | mp3an3 1405 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐷⟶ℂ ∧ 𝐹 ∈ 𝐿1) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
292 | 8, 7, 291 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ 𝐷,
(abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
293 | 286, 292 | readdcld 9948 |
. . . . . . . . 9
⊢ (𝜑 →
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ) |
294 | 293 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ) |
295 | 204, 294 | readdcld 9948 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) ∈ ℝ) |
296 | | ge0addcl 12155 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,)+∞)) |
297 | 296 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑥 ∈
(0[,)+∞) ∧ 𝑦
∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,)+∞)) |
298 | | ifcl 4080 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,)+∞) ∧ 0 ∈
(0[,)+∞)) → if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,)+∞)) |
299 | 73, 74, 298 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ 𝐷,
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,)+∞)) |
300 | 299, 90 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,)+∞)) |
301 | 300 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,)+∞)) |
302 | 296 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,)+∞) ∧ 𝑦 ∈ (0[,)+∞))) →
(𝑥 + 𝑦) ∈ (0[,)+∞)) |
303 | 257 | recld 13782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℝ) |
304 | 303 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘(𝐹‘𝑡)) ∈ ℂ) |
305 | 304 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ) |
306 | 304 | absge0d 14031 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤
(abs‘(ℜ‘(𝐹‘𝑡)))) |
307 | | elrege0 12149 |
. . . . . . . . . . . . . . . . . 18
⊢
((abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔
((abs‘(ℜ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤
(abs‘(ℜ‘(𝐹‘𝑡))))) |
308 | 305, 306,
307 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℜ‘(𝐹‘𝑡))) ∈ (0[,)+∞)) |
309 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈
(0[,)+∞)) |
310 | 308, 309 | ifclda 4070 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈
(0[,)+∞)) |
311 | 310 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈
(0[,)+∞)) |
312 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) |
313 | 311, 312 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))),
0)):ℝ⟶(0[,)+∞)) |
314 | 257 | imcld 13783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℝ) |
315 | 314 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℑ‘(𝐹‘𝑡)) ∈ ℂ) |
316 | 315 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ) |
317 | 315 | absge0d 14031 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 0 ≤
(abs‘(ℑ‘(𝐹‘𝑡)))) |
318 | | elrege0 12149 |
. . . . . . . . . . . . . . . . . 18
⊢
((abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞) ↔
((abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℝ ∧ 0 ≤
(abs‘(ℑ‘(𝐹‘𝑡))))) |
319 | 316, 317,
318 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ (0[,)+∞)) |
320 | 319, 309 | ifclda 4070 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈
(0[,)+∞)) |
321 | 320 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈
(0[,)+∞)) |
322 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) |
323 | 321, 322 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))),
0)):ℝ⟶(0[,)+∞)) |
324 | 302, 313,
323, 244, 244, 111 | off 6810 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))),
0))):ℝ⟶(0[,)+∞)) |
325 | 324 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))),
0))):ℝ⟶(0[,)+∞)) |
326 | 40 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ℝ ∈ V) |
327 | 297, 301,
325, 326, 326, 111 | off 6810 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))),
0)))):ℝ⟶(0[,)+∞)) |
328 | | fss 5969 |
. . . . . . . . . . 11
⊢ ((((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,)+∞)
∧ (0[,)+∞) ⊆ (0[,]+∞)) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))),
0)))):ℝ⟶(0[,]+∞)) |
329 | 327, 166,
328 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))),
0)))):ℝ⟶(0[,]+∞)) |
330 | 329 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))),
0)))):ℝ⟶(0[,]+∞)) |
331 | | 0xr 9965 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
332 | 331 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
ℝ*) |
333 | 274, 332 | ifclda 4070 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
ℝ*) |
334 | 257 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
335 | 39 | adantll 746 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
336 | 235, 335 | syldan 486 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
337 | 334, 336 | subcld 10271 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
338 | 337 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
339 | 338 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
340 | 331 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈
ℝ*) |
341 | 339, 340 | ifclda 4070 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
ℝ*) |
342 | 341 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
ℝ*) |
343 | 336 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
344 | | 0red 9920 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈
ℝ) |
345 | 343, 344 | ifclda 4070 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ ℝ) |
346 | | 0red 9920 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℝ) |
347 | 305, 346 | ifclda 4070 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ) |
348 | 316, 346 | ifclda 4070 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ) |
349 | 347, 348 | readdcld 9948 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ) |
350 | 349 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ ℝ) |
351 | 345, 350 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ ℝ) |
352 | 351 | rexrd 9968 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈
ℝ*) |
353 | 352 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈
ℝ*) |
354 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
355 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
356 | 227 | adantllr 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷) |
357 | 338 | leidd 10473 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
358 | 357 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
359 | | iftrue 4042 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
360 | 359 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
361 | 358, 360 | breqtrrd 4611 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
362 | 356, 361 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
363 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↔ 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
364 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (0 =
if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ 0 ↔ 0 ≤
if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
365 | 337 | absge0d 14031 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → 0 ≤
(abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
366 | 363, 364,
365, 239 | ifbothda 4073 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ 0 ≤ if(𝑡 ∈
𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
367 | 366 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
368 | 354, 355,
362, 367 | ifbothda 4073 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
369 | 257 | negcld 10258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ) |
370 | 369 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → -(𝐹‘𝑡) ∈ ℂ) |
371 | 336, 370 | addcld 9938 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) ∈ ℂ) |
372 | 371 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ∈ ℝ) |
373 | 369 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ) |
374 | 373 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ∈ ℝ) |
375 | 343, 374 | readdcld 9948 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ∈ ℝ) |
376 | 305, 316 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ) |
377 | 376 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) →
((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) ∈ ℝ) |
378 | 343, 377 | readdcld 9948 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) ∈ ℝ) |
379 | 336, 370 | abstrid 14043 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡)))) |
380 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((i
∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (i ·
(ℑ‘(𝐹‘𝑡))) ∈ ℂ) |
381 | 31, 315, 380 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (i · (ℑ‘(𝐹‘𝑡))) ∈ ℂ) |
382 | 304, 381 | abstrid 14043 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i ·
(ℑ‘(𝐹‘𝑡)))))) |
383 | 257 | absnegd 14036 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘(𝐹‘𝑡))) |
384 | 257 | replimd 13785 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) = ((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡))))) |
385 | 384 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡)))))) |
386 | 383, 385 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) = (abs‘((ℜ‘(𝐹‘𝑡)) + (i · (ℑ‘(𝐹‘𝑡)))))) |
387 | | absmul 13882 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((i
∈ ℂ ∧ (ℑ‘(𝐹‘𝑡)) ∈ ℂ) → (abs‘(i
· (ℑ‘(𝐹‘𝑡)))) = ((abs‘i) ·
(abs‘(ℑ‘(𝐹‘𝑡))))) |
388 | 31, 315, 387 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i ·
(ℑ‘(𝐹‘𝑡)))) = ((abs‘i) ·
(abs‘(ℑ‘(𝐹‘𝑡))))) |
389 | 185 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((abs‘i) · (abs‘(ℑ‘(𝐹‘𝑡)))) = (1 ·
(abs‘(ℑ‘(𝐹‘𝑡)))) |
390 | 388, 389 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(i ·
(ℑ‘(𝐹‘𝑡)))) = (1 ·
(abs‘(ℑ‘(𝐹‘𝑡))))) |
391 | 316 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) ∈ ℂ) |
392 | 391 | mulid2d 9937 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (1 ·
(abs‘(ℑ‘(𝐹‘𝑡)))) = (abs‘(ℑ‘(𝐹‘𝑡)))) |
393 | 390, 392 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘(ℑ‘(𝐹‘𝑡))) = (abs‘(i ·
(ℑ‘(𝐹‘𝑡))))) |
394 | 393 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(i ·
(ℑ‘(𝐹‘𝑡)))))) |
395 | 382, 386,
394 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) |
396 | 395 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘-(𝐹‘𝑡)) ≤ ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) |
397 | 374, 377,
343, 396 | leadd2dd 10521 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘-(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))) |
398 | 372, 375,
378, 379, 397 | letrd 10073 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) ≤ ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))) |
399 | 334, 336 | abssubd 14040 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡)))) |
400 | 359 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
401 | 336, 334 | negsubd 10277 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)) = (((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡))) |
402 | 401 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡))) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) − (𝐹‘𝑡)))) |
403 | 399, 400,
402 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘(((𝑓‘𝑡) + (i · (𝑔‘𝑡))) + -(𝐹‘𝑡)))) |
404 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))) |
405 | 404 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))) |
406 | 398, 403,
405 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)) |
407 | 406 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0))) |
408 | 238 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑡 ∈ 𝐷 → 0 ≤ 0) |
409 | | iffalse 4045 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0) |
410 | | iffalse 4045 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) = 0) |
411 | 408, 409,
410 | 3brtr4d 4615 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)) |
412 | 407, 411 | pm2.61d1 170 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)) |
413 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = (abs‘(ℜ‘(𝐹‘𝑡)))) |
414 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = (abs‘(ℑ‘(𝐹‘𝑡)))) |
415 | 413, 414 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))) |
416 | 228, 415 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡)))))) |
417 | 416, 404 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)) |
418 | | 00id 10090 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 0) =
0 |
419 | 418 | oveq2i 6560 |
. . . . . . . . . . . . . . . . 17
⊢ (0 + (0 +
0)) = (0 + 0) |
420 | 419, 418 | eqtri 2632 |
. . . . . . . . . . . . . . . 16
⊢ (0 + (0 +
0)) = 0 |
421 | | iffalse 4045 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0) |
422 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) = 0) |
423 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) = 0) |
424 | 422, 423 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (0 + 0)) |
425 | 421, 424 | oveq12d 6567 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (0 + (0 + 0))) |
426 | 420, 425,
410 | 3eqtr4a 2670 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0)) |
427 | 417, 426 | pm2.61i 175 |
. . . . . . . . . . . . . 14
⊢ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = if(𝑡 ∈ 𝐷, ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + ((abs‘(ℜ‘(𝐹‘𝑡))) + (abs‘(ℑ‘(𝐹‘𝑡))))), 0) |
428 | 412, 427 | syl6breqr 4625 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
429 | 428 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ 𝐷, (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
430 | 333, 342,
353, 368, 429 | xrletrd 11869 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
431 | 430 | ralrimivw 2950 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
432 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V |
433 | 432, 17 | ifex 4106 |
. . . . . . . . . . . . 13
⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V |
434 | 433 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V) |
435 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ V |
436 | 435 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) ∈ V) |
437 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
438 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ V |
439 | 438 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) ∈ V) |
440 | 347 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) ∈ ℝ) |
441 | 348 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0) ∈ ℝ) |
442 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) |
443 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) |
444 | 244, 440,
441, 442, 443 | offval2 6812 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) |
445 | 244, 247,
439, 249, 444 | offval2 6812 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) |
446 | 244, 434,
436, 437, 445 | ofrfval2 6813 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) |
447 | 446 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + (if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) + if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) |
448 | 431, 447 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) |
449 | | itg2le 23312 |
. . . . . . . . 9
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞)
∧ ((𝑡 ∈ ℝ
↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))):ℝ⟶(0[,]+∞)
∧ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤
(∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) |
450 | 280, 330,
448, 449 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤
(∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) |
451 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ 𝐷 ⊆
ℝ) |
452 | 246 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V) |
453 | | eldifn 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷) |
454 | 453 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0) |
455 | 454 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (ℝ
∖ 𝐷)) → if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0) |
456 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (i
· (𝑔‘𝑡)) ∈ V |
457 | 456 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (i · (𝑔‘𝑡)) ∈ V) |
458 | 41, 42, 457, 45, 52 | offval2 6812 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔)) = (𝑡 ∈ ℝ ↦ ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
459 | 39, 458, 56, 57 | fmptco 6303 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔))) = (𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
460 | 459 | reseq1d 5316 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((abs ∘ (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔))) ↾ 𝐷) = ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷)) |
461 | 6 | resmptd 5371 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
462 | 460, 461 | sylan9eqr 2666 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((abs ∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
463 | 228 | mpteq2ia 4668 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ 𝐷 ↦ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
464 | 462, 463 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((abs ∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · 𝑔))) ↾ 𝐷) = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
465 | | i1fmbf 23248 |
. . . . . . . . . . . . . . 15
⊢ ((abs
∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · 𝑔))) ∈ dom ∫1 → (abs
∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · 𝑔))) ∈ MblFn) |
466 | 59, 465 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔))) ∈ MblFn) |
467 | | fdm 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:𝐷⟶ℂ → dom 𝐹 = 𝐷) |
468 | 8, 467 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐹 = 𝐷) |
469 | | iblmbf 23340 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ 𝐿1
→ 𝐹 ∈
MblFn) |
470 | | mbfdm 23201 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
471 | 7, 469, 470 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
472 | 468, 471 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ dom vol) |
473 | | mbfres 23217 |
. . . . . . . . . . . . . 14
⊢ (((abs
∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · 𝑔))) ∈ MblFn ∧ 𝐷 ∈ dom vol) → ((abs ∘ (𝑓 ∘𝑓 +
((ℝ × {i}) ∘𝑓 · 𝑔))) ↾ 𝐷) ∈ MblFn) |
474 | 466, 472,
473 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((abs ∘ (𝑓
∘𝑓 + ((ℝ × {i})
∘𝑓 · 𝑔))) ↾ 𝐷) ∈ MblFn) |
475 | 464, 474 | eqeltrrd 2689 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn) |
476 | 451, 15, 452, 455, 475 | mbfss 23219 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ MblFn) |
477 | 203 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
478 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
479 | 304, 478 | ifclda 4070 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ) |
480 | 479 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℂ) |
481 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) |
482 | 54 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
483 | 482 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥))) |
484 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = (abs‘if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) |
485 | | fvif 6114 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs‘if(𝑡
∈ 𝐷,
(ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0)) |
486 | | abs0 13873 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs‘0) = 0 |
487 | | ifeq2 4041 |
. . . . . . . . . . . . . . . . . . 19
⊢
((abs‘0) = 0 → if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) |
488 | 486, 487 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), (abs‘0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) |
489 | 485, 488 | eqtri 2632 |
. . . . . . . . . . . . . . . . 17
⊢
(abs‘if(𝑡
∈ 𝐷,
(ℜ‘(𝐹‘𝑡)), 0)) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0) |
490 | 484, 489 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) → (abs‘𝑥) = if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) |
491 | 480, 481,
483, 490 | fmptco 6303 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) |
492 | 303, 346 | ifclda 4070 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ) |
493 | 492 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ) |
494 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) |
495 | 493, 494 | fmptd 6292 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)),
0)):ℝ⟶ℝ) |
496 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ℝ ∈ dom
vol) |
497 | 492 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) ∈ ℝ) |
498 | 453 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷) |
499 | 498 | iffalsed 4047 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = 0) |
500 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0) = (ℜ‘(𝐹‘𝑡))) |
501 | 500 | mpteq2ia 4668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) |
502 | 8 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
503 | 7, 469 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐹 ∈ MblFn) |
504 | 502, 503 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn) |
505 | 257 | ismbfcn2 23212 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))) |
506 | 504, 505 | mpbid 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)) |
507 | 506 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn) |
508 | 501, 507 | syl5eqel 2692 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn) |
509 | 6, 496, 497, 499, 508 | mbfss 23219 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn) |
510 | | ftc1anclem1 32655 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0)) ∈ MblFn) → (abs ∘
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn) |
511 | 495, 509,
510 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (ℜ‘(𝐹‘𝑡)), 0))) ∈ MblFn) |
512 | 491, 511 | eqeltrrd 2689 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∈ MblFn) |
513 | 512, 313,
286, 323, 292 | itg2addnc 32634 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) |
514 | 513, 293 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ) |
515 | 514 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) ∈ ℝ) |
516 | 476, 301,
477, 325, 515 | itg2addnc 32634 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) =
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) |
517 | 513 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))) = ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) |
518 | 517 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) =
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) |
519 | 516, 518 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) =
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) |
520 | 519 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
((𝑡 ∈ ℝ ↦
if(𝑡 ∈ 𝐷,
(abs‘(ℜ‘(𝐹‘𝑡))), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) =
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) |
521 | 450, 520 | breqtrd 4609 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) |
522 | | itg2lecl 23311 |
. . . . . . 7
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞)
∧ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℜ‘(𝐹‘𝑡))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (abs‘(ℑ‘(𝐹‘𝑡))), 0)))))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ) |
523 | 280, 295,
521, 522 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ) |
524 | 69, 79, 256, 273, 523 | itg2addnc 32634 |
. . . . 5
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) =
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))))) |
525 | 244, 245,
434, 248, 437 | offval2 6812 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
526 | | eqeq2 2621 |
. . . . . . . . . . 11
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) → ((if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) ↔ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))) |
527 | | eqeq2 2621 |
. . . . . . . . . . 11
⊢ (0 =
if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) → ((if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0 ↔ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))) |
528 | | iftrue 4042 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
529 | 23, 528 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
530 | 529 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
531 | | iffalse 4045 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0) |
532 | | iffalse 4045 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) = 0) |
533 | 531, 532 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (0 + 0)) |
534 | 533, 418 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0) |
535 | 534 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = 0) |
536 | 526, 527,
530, 535 | ifbothda 4073 |
. . . . . . . . . 10
⊢ (𝜑 → (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)) |
537 | 536 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) + if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))) |
538 | 525, 537 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))) |
539 | 538 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0))) |
540 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom
∫1)) |
541 | 261 | abscld 14023 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
542 | 541 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
543 | 540, 542 | sylan 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
544 | 265 | recnd 9947 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℂ) |
545 | 543, 544 | addcomd 10117 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
546 | 545 | ifeq1da 4066 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
547 | 546 | mpteq2dv 4673 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) + (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
548 | 539, 547 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
549 | 548 | fveq2d 6107 |
. . . . 5
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑓 +
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) =
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
550 | 524, 549 | eqtr3d 2646 |
. . . 4
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) =
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
551 | 10, 11, 550 | syl2an 493 |
. . 3
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) =
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
552 | 551 | adantr 480 |
. 2
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) =
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) |
553 | | rpcn 11717 |
. . . 4
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
554 | 553 | 2halvesd 11155 |
. . 3
⊢ (𝑦 ∈ ℝ+
→ ((𝑦 / 2) + (𝑦 / 2)) = 𝑦) |
555 | 554 | ad3antlr 763 |
. 2
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
((𝑦 / 2) + (𝑦 / 2)) = 𝑦) |
556 | 9, 552, 555 | 3brtr3d 4614 |
1
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) + (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < 𝑦) |