Proof of Theorem ftc1anclem7
Step | Hyp | Ref
| Expression |
1 | | i1ff 23249 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
2 | 1 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑓‘𝑥) ∈
ℝ) |
3 | 2 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑓‘𝑥) ∈
ℂ) |
4 | | ax-icn 9874 |
. . . . . . . . . 10
⊢ i ∈
ℂ |
5 | | i1ff 23249 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
6 | 5 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑔‘𝑥) ∈
ℝ) |
7 | 6 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑔‘𝑥) ∈
ℂ) |
8 | | mulcl 9899 |
. . . . . . . . . 10
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑥) ∈ ℂ) → (i · (𝑔‘𝑥)) ∈ ℂ) |
9 | 4, 7, 8 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (i · (𝑔‘𝑥)) ∈ ℂ) |
10 | | addcl 9897 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) ∈ ℂ ∧ (i · (𝑔‘𝑥)) ∈ ℂ) → ((𝑓‘𝑥) + (i · (𝑔‘𝑥))) ∈ ℂ) |
11 | 3, 9, 10 | syl2an 493 |
. . . . . . . 8
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑥
∈ ℝ)) → ((𝑓‘𝑥) + (i · (𝑔‘𝑥))) ∈ ℂ) |
12 | 11 | anandirs 870 |
. . . . . . 7
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → ((𝑓‘𝑥) + (i · (𝑔‘𝑥))) ∈ ℂ) |
13 | | reex 9906 |
. . . . . . . . 9
⊢ ℝ
∈ V |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ℝ ∈ V) |
15 | 2 | adantlr 747 |
. . . . . . . 8
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (𝑓‘𝑥) ∈ ℝ) |
16 | | ovex 6577 |
. . . . . . . . 9
⊢ (i
· (𝑔‘𝑥)) ∈ V |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑥
∈ ℝ) → (i · (𝑔‘𝑥)) ∈ V) |
18 | 1 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 = (𝑥 ∈ ℝ ↦ (𝑓‘𝑥))) |
19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 𝑓
= (𝑥 ∈ ℝ ↦
(𝑓‘𝑥))) |
20 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ ℝ ∈ V) |
21 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ i ∈ ℂ) |
22 | | fconstmpt 5085 |
. . . . . . . . . . 11
⊢ (ℝ
× {i}) = (𝑥 ∈
ℝ ↦ i) |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ (ℝ × {i}) = (𝑥 ∈ ℝ ↦ i)) |
24 | 5 | feqmptd 6159 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 = (𝑥 ∈ ℝ ↦ (𝑔‘𝑥))) |
25 | 20, 21, 6, 23, 24 | offval2 6812 |
. . . . . . . . 9
⊢ (𝑔 ∈ dom ∫1
→ ((ℝ × {i}) ∘𝑓 · 𝑔) = (𝑥 ∈ ℝ ↦ (i · (𝑔‘𝑥)))) |
26 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((ℝ × {i}) ∘𝑓
· 𝑔) = (𝑥 ∈ ℝ ↦ (i
· (𝑔‘𝑥)))) |
27 | 14, 15, 17, 19, 26 | offval2 6812 |
. . . . . . 7
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔)) = (𝑥 ∈ ℝ ↦ ((𝑓‘𝑥) + (i · (𝑔‘𝑥))))) |
28 | | absf 13925 |
. . . . . . . . 9
⊢
abs:ℂ⟶ℝ |
29 | 28 | a1i 11 |
. . . . . . . 8
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → abs:ℂ⟶ℝ) |
30 | 29 | feqmptd 6159 |
. . . . . . 7
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → abs = (𝑡 ∈ ℂ ↦ (abs‘𝑡))) |
31 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑡 = ((𝑓‘𝑥) + (i · (𝑔‘𝑥))) → (abs‘𝑡) = (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥))))) |
32 | 12, 27, 30, 31 | fmptco 6303 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔))) = (𝑥 ∈ ℝ ↦ (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥)))))) |
33 | | ftc1anclem3 32657 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs ∘ (𝑓 ∘𝑓 + ((ℝ
× {i}) ∘𝑓 · 𝑔))) ∈ dom
∫1) |
34 | 32, 33 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑥 ∈ ℝ ↦ (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥))))) ∈ dom
∫1) |
35 | | ioombl 23140 |
. . . . 5
⊢ (𝑢(,)𝑤) ∈ dom vol |
36 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → (𝑓‘𝑥) = (𝑓‘𝑡)) |
37 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡)) |
38 | 37 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → (i · (𝑔‘𝑥)) = (i · (𝑔‘𝑡))) |
39 | 36, 38 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → ((𝑓‘𝑥) + (i · (𝑔‘𝑥))) = ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥)))) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
41 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ ↦
(abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥))))) = (𝑥 ∈ ℝ ↦ (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥))))) |
42 | | fvex 6113 |
. . . . . . . . . 10
⊢
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ V |
43 | 40, 41, 42 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥)))))‘𝑡) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
44 | 43 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ →
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = ((𝑥 ∈ ℝ ↦ (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥)))))‘𝑡)) |
45 | 44 | ifeq1d 4054 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = if(𝑡 ∈ (𝑢(,)𝑤), ((𝑥 ∈ ℝ ↦ (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥)))))‘𝑡), 0)) |
46 | 45 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), ((𝑥 ∈ ℝ ↦ (abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥)))))‘𝑡), 0)) |
47 | 46 | i1fres 23278 |
. . . . 5
⊢ (((𝑥 ∈ ℝ ↦
(abs‘((𝑓‘𝑥) + (i · (𝑔‘𝑥))))) ∈ dom ∫1 ∧
(𝑢(,)𝑤) ∈ dom vol) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ dom
∫1) |
48 | 34, 35, 47 | sylancl 693 |
. . . 4
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ dom
∫1) |
49 | | breq2 4587 |
. . . . . . 7
⊢
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ↔ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
50 | | breq2 4587 |
. . . . . . 7
⊢ (0 =
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) → (0 ≤ 0 ↔ 0 ≤
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
51 | | elioore 12076 |
. . . . . . . 8
⊢ (𝑡 ∈ (𝑢(,)𝑤) → 𝑡 ∈ ℝ) |
52 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑡 → (𝑥 ∈ ℝ ↔ 𝑡 ∈ ℝ)) |
53 | 52 | anbi2d 736 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ 𝑥 ∈ ℝ)
↔ ((𝑓 ∈ dom
∫1 ∧ 𝑔
∈ dom ∫1) ∧ 𝑡 ∈ ℝ))) |
54 | 39 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑡 → (((𝑓‘𝑥) + (i · (𝑔‘𝑥))) ∈ ℂ ↔ ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ)) |
55 | 53, 54 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑡 → ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ 𝑥 ∈ ℝ)
→ ((𝑓‘𝑥) + (i · (𝑔‘𝑥))) ∈ ℂ) ↔ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ))) |
56 | 55, 12 | chvarv 2251 |
. . . . . . . . 9
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
57 | 56 | absge0d 14031 |
. . . . . . . 8
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → 0 ≤ (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
58 | 51, 57 | sylan2 490 |
. . . . . . 7
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → 0 ≤
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
59 | | 0le0 10987 |
. . . . . . . 8
⊢ 0 ≤
0 |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ 0) |
61 | 49, 50, 58, 60 | ifbothda 4073 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
62 | 61 | ralrimivw 2950 |
. . . . 5
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
63 | | ax-resscn 9872 |
. . . . . . . 8
⊢ ℝ
⊆ ℂ |
64 | 63 | a1i 11 |
. . . . . . 7
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ℝ ⊆ ℂ) |
65 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
66 | 42, 65 | ifex 4106 |
. . . . . . . . 9
⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V |
67 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) |
68 | 66, 67 | fnmpti 5935 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) Fn ℝ |
69 | 68 | a1i 11 |
. . . . . . 7
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) Fn ℝ) |
70 | 64, 69 | 0pledm 23246 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (0𝑝 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ (ℝ × {0})
∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))) |
71 | 65 | a1i 11 |
. . . . . . 7
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → 0 ∈ V) |
72 | 66 | a1i 11 |
. . . . . . 7
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈ V) |
73 | | fconstmpt 5085 |
. . . . . . . 8
⊢ (ℝ
× {0}) = (𝑡 ∈
ℝ ↦ 0) |
74 | 73 | a1i 11 |
. . . . . . 7
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)) |
75 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
76 | 14, 71, 72, 74, 75 | ofrfval2 6813 |
. . . . . 6
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((ℝ × {0}) ∘𝑟
≤ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
77 | 70, 76 | bitrd 267 |
. . . . 5
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (0𝑝 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
78 | 62, 77 | mpbird 246 |
. . . 4
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0𝑝 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) |
79 | | itg2itg1 23309 |
. . . . 5
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)))) |
80 | | itg1cl 23258 |
. . . . . 6
⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ dom ∫1 →
(∫1‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
81 | 80 | adantr 480 |
. . . . 5
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) →
(∫1‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
82 | 79, 81 | eqeltrd 2688 |
. . . 4
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
83 | 48, 78, 82 | syl2anc 691 |
. . 3
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
84 | 83 | ad6antlr 769 |
. 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))) ∈ ℝ) |
85 | | simplll 794 |
. . . . 5
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom
∫1))) |
86 | | ftc1anc.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ∈ ℝ) |
87 | 86 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
88 | | ftc1anc.b |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐵 ∈ ℝ) |
89 | 88 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
90 | 87, 89 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴 ∈ ℝ* ∧ 𝐵 ∈
ℝ*)) |
91 | | df-icc 12053 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑡 ∈ ℝ* ∣ (𝑥 ≤ 𝑡 ∧ 𝑡 ≤ 𝑦)}) |
92 | 91 | elixx3g 12059 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑢 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵))) |
93 | 92 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑢 ∧ 𝑢 ≤ 𝐵)) |
94 | 93 | simpld 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑢) |
95 | 91 | elixx3g 12059 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ (𝐴[,]𝐵) ↔ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) ∧ (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵))) |
96 | 95 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝐴[,]𝐵) → (𝐴 ≤ 𝑤 ∧ 𝑤 ≤ 𝐵)) |
97 | 96 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ≤ 𝐵) |
98 | 94, 97 | anim12i 588 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵)) → (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) |
99 | | ioossioo 12136 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (𝐴 ≤ 𝑢 ∧ 𝑤 ≤ 𝐵)) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
100 | 90, 98, 99 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ (𝐴(,)𝐵)) |
101 | | ftc1anc.s |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
102 | 101 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝐴(,)𝐵) ⊆ 𝐷) |
103 | 100, 102 | sstrd 3578 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑢(,)𝑤) ⊆ 𝐷) |
104 | 103 | 3adantr3 1215 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑢(,)𝑤) ⊆ 𝐷) |
105 | 104 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷) |
106 | | ftc1anc.f |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
107 | 106 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
108 | 107 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
109 | 105, 108 | syldan 486 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
110 | 109 | adantllr 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (𝐹‘𝑡) ∈ ℂ) |
111 | 56 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
112 | 51, 111 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
113 | 112 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
114 | 110, 113 | subcld 10271 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
115 | 114 | abscld 14023 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
116 | 115 | rexrd 9968 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
117 | 114 | absge0d 14031 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
118 | | elxrge0 12152 |
. . . . . . . . 9
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
119 | 116, 117,
118 | sylanbrc 695 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞)) |
120 | | 0e0iccpnf 12154 |
. . . . . . . . 9
⊢ 0 ∈
(0[,]+∞) |
121 | 120 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
(0[,]+∞)) |
122 | 119, 121 | ifclda 4070 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
123 | 122 | adantr 480 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
124 | | eqid 2610 |
. . . . . 6
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) |
125 | 123, 124 | fmptd 6292 |
. . . . 5
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))),
0)):ℝ⟶(0[,]+∞)) |
126 | 85, 125 | sylan 487 |
. . . 4
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))),
0)):ℝ⟶(0[,]+∞)) |
127 | | rpre 11715 |
. . . . . 6
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
128 | 127 | rehalfcld 11156 |
. . . . 5
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ) |
129 | 128 | ad2antlr 759 |
. . . 4
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑦 / 2) ∈ ℝ) |
130 | | simpll 786 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) → (𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom
∫1))) |
131 | 103 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷) |
132 | 131 | adantllr 751 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 𝑡 ∈ 𝐷) |
133 | 107 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
134 | | ftc1anc.d |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
135 | 134 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ) |
136 | 135 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ ℝ) |
137 | 136, 111 | syldan 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) |
138 | 133, 137 | subcld 10271 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
139 | 138 | abscld 14023 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
140 | 139 | rexrd 9968 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
141 | 140 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
142 | 132, 141 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
143 | 138 | absge0d 14031 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → 0 ≤
(abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
144 | 143 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
145 | 132, 144 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
146 | 142, 145,
118 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞)) |
147 | 120 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ∈
(0[,]+∞)) |
148 | 146, 147 | ifclda 4070 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
149 | 148 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈
(0[,]+∞)) |
150 | 149, 124 | fmptd 6292 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))),
0)):ℝ⟶(0[,]+∞)) |
151 | | itg2cl 23305 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞)
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
152 | 150, 151 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
153 | 130, 152 | sylan 487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈
ℝ*) |
154 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
155 | 107, 154 | ifclda 4070 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
156 | | subcl 10159 |
. . . . . . . . . . . . . . . 16
⊢
((if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ ∧ ((𝑓‘𝑡) + (i · (𝑔‘𝑡))) ∈ ℂ) → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
157 | 155, 56, 156 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ 𝑡 ∈ ℝ))
→ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
158 | 157 | anassrs 678 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℂ) |
159 | 158 | abscld 14023 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ) |
160 | 159 | rexrd 9968 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈
ℝ*) |
161 | 158 | absge0d 14031 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
162 | | elxrge0 12152 |
. . . . . . . . . . . 12
⊢
((abs‘(if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔
((abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
163 | 160, 161,
162 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ (0[,]+∞)) |
164 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
165 | 163, 164 | fmptd 6292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞)) |
166 | | itg2cl 23305 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) ∈
ℝ*) |
167 | 165, 166 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) ∈
ℝ*) |
168 | 167 | ad3antrrr 762 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) ∈
ℝ*) |
169 | | rphalfcl 11734 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ+) |
170 | 169 | rpxrd 11749 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ (𝑦 / 2) ∈
ℝ*) |
171 | 170 | ad2antlr 759 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑦 / 2) ∈
ℝ*) |
172 | 165 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞)) |
173 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢
((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → ((abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
174 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) → (0 ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ↔ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
175 | 139 | leidd 10473 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
176 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡)) |
177 | 176 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ 𝐷 → (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = ((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
178 | 177 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ 𝐷 → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
179 | 178 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) = (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
180 | 175, 179 | breqtrrd 4611 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
181 | 180 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ 𝐷) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
182 | 132, 181 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
183 | 182 | adantlr 747 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) ∧ 𝑡 ∈ (𝑢(,)𝑤)) → (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
184 | 161 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
185 | 184 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) ∧ ¬ 𝑡 ∈ (𝑢(,)𝑤)) → 0 ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
186 | 173, 174,
183, 185 | ifbothda 4073 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
187 | 186 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
188 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℝ ∈
V) |
189 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢
(abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V |
190 | 189, 65 | ifex 4106 |
. . . . . . . . . . . . . 14
⊢ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V |
191 | 190 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ∈ V) |
192 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(abs‘(if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V |
193 | 192 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) ∈ V) |
194 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) |
195 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
196 | 188, 191,
193, 194, 195 | ofrfval2 6813 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
197 | 196 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) ↔ ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0) ≤ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
198 | 187, 197 | mpbird 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
199 | | itg2le 23312 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞)
∧ (𝑡 ∈ ℝ
↦ (abs‘(if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))) |
200 | 150, 172,
198, 199 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))) |
201 | 130, 200 | sylan 487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))) |
202 | | simpllr 795 |
. . . . . . . 8
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) |
203 | 153, 168,
171, 201, 202 | xrlelttrd 11867 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < (𝑦 / 2)) |
204 | | xrltle 11858 |
. . . . . . . 8
⊢
(((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ* ∧
(𝑦 / 2) ∈
ℝ*) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (𝑦 / 2))) |
205 | 153, 171,
204 | syl2anc 691 |
. . . . . . 7
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < (𝑦 / 2) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (𝑦 / 2))) |
206 | 203, 205 | mpd 15 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (𝑦 / 2)) |
207 | 206 | adantllr 751 |
. . . . 5
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (𝑦 / 2)) |
208 | 207 | 3adantr3 1215 |
. . . 4
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (𝑦 / 2)) |
209 | | itg2lecl 23311 |
. . . 4
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)):ℝ⟶(0[,]+∞)
∧ (𝑦 / 2) ∈
ℝ ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ≤ (𝑦 / 2)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ) |
210 | 126, 129,
208, 209 | syl3anc 1318 |
. . 3
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) ∈ ℝ) |
211 | 210 | 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))) ∈ ℝ) |
212 | 128 | ad3antlr 763 |
. 2
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(𝑦 / 2) ∈
ℝ) |
213 | 83 | adantr 480 |
. . . . . . . 8
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
214 | | 2rp 11713 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
215 | | imassrn 5396 |
. . . . . . . . . . . . . . . 16
⊢ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ran
abs |
216 | | frn 5966 |
. . . . . . . . . . . . . . . . 17
⊢
(abs:ℂ⟶ℝ → ran abs ⊆
ℝ) |
217 | 28, 216 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ ran abs
⊆ ℝ |
218 | 215, 217 | sstri 3577 |
. . . . . . . . . . . . . . 15
⊢ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆
ℝ |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ) |
220 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:ℝ⟶ℝ →
ran 𝑓 ⊆
ℝ) |
221 | 1, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ⊆
ℝ) |
222 | 221 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ran 𝑓 ⊆ ℝ) |
223 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔:ℝ⟶ℝ →
ran 𝑔 ⊆
ℝ) |
224 | 5, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 ∈ dom ∫1
→ ran 𝑔 ⊆
ℝ) |
225 | 224 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ran 𝑔 ⊆ ℝ) |
226 | 222, 225 | unssd 3751 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℝ) |
227 | 226, 63 | syl6ss 3580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ) |
228 | | i1f0rn 23255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ 0 ∈ ran 𝑓) |
229 | | elun1 3742 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ran 𝑓 → 0 ∈ (ran
𝑓 ∪ ran 𝑔)) |
230 | 228, 229 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ dom ∫1
→ 0 ∈ (ran 𝑓
∪ ran 𝑔)) |
231 | 230 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0 ∈ (ran 𝑓 ∪ ran 𝑔)) |
232 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
233 | 28, 232 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ abs Fn
ℂ |
234 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ 0 ∈ (ran 𝑓 ∪
ran 𝑔)) →
(abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
235 | 233, 234 | mp3an1 1403 |
. . . . . . . . . . . . . . . 16
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 0 ∈
(ran 𝑓 ∪ ran 𝑔)) → (abs‘0) ∈
(abs “ (ran 𝑓 ∪
ran 𝑔))) |
236 | 227, 231,
235 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
237 | | ne0i 3880 |
. . . . . . . . . . . . . . 15
⊢
((abs‘0) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔)) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅) |
238 | 236, 237 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ≠ ∅) |
239 | | ffun 5961 |
. . . . . . . . . . . . . . . . 17
⊢
(abs:ℂ⟶ℝ → Fun abs) |
240 | 28, 239 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ Fun
abs |
241 | | i1frn 23250 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ∈
Fin) |
242 | | i1frn 23250 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ∈ dom ∫1
→ ran 𝑔 ∈
Fin) |
243 | | unfi 8112 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝑓 ∈ Fin ∧ ran
𝑔 ∈ Fin) → (ran
𝑓 ∪ ran 𝑔) ∈ Fin) |
244 | 241, 242,
243 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (ran 𝑓 ∪ ran 𝑔) ∈ Fin) |
245 | | imafi 8142 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun abs
∧ (ran 𝑓 ∪ ran
𝑔) ∈ Fin) → (abs
“ (ran 𝑓 ∪ ran
𝑔)) ∈
Fin) |
246 | 240, 244,
245 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (abs “ (ran 𝑓 ∪ ran 𝑔)) ∈ Fin) |
247 | | fimaxre2 10848 |
. . . . . . . . . . . . . . 15
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ∈ Fin) →
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) |
248 | 218, 246,
247 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))𝑦 ≤ 𝑥) |
249 | | suprcl 10862 |
. . . . . . . . . . . . . 14
⊢ (((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
250 | 219, 238,
248, 249 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
251 | 250 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
252 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 ∈
ℝ) |
253 | 227 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → 𝑟 ∈
ℂ) |
254 | 253 | abscld 14023 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ∈
ℝ) |
255 | 254 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ∈
ℝ) |
256 | | absgt0 13912 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ℂ → (𝑟 ≠ 0 ↔ 0 <
(abs‘𝑟))) |
257 | 253, 256 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (𝑟 ≠ 0 ↔ 0 <
(abs‘𝑟))) |
258 | 257 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) ∧ 𝑟 ≠ 0) → 0 <
(abs‘𝑟)) |
259 | 258 | anasss 677 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 < (abs‘𝑟)) |
260 | 219, 238,
248 | 3jca 1235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran
𝑓 ∪ ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥)) |
261 | 260 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → ((abs “
(ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs
“ (ran 𝑓 ∪ ran
𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥)) |
262 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
263 | 233, 262 | mp3an1 1403 |
. . . . . . . . . . . . . . . 16
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ 𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
264 | 227, 263 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
265 | | suprub 10863 |
. . . . . . . . . . . . . . 15
⊢ ((((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) ∧ (abs‘𝑟) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘𝑟) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
266 | 261, 264,
265 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑟
∈ (ran 𝑓 ∪ ran
𝑔)) → (abs‘𝑟) ≤ sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
267 | 266 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → (abs‘𝑟) ≤ sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
268 | 252, 255,
251, 259, 267 | ltletrd 10076 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → 0 < sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)) |
269 | 251, 268 | elrpd 11745 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑟
∈ (ran 𝑓 ∪ ran
𝑔) ∧ 𝑟 ≠ 0)) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+) |
270 | 269 | rexlimdvaa 3014 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0 → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+)) |
271 | 270 | imp 444 |
. . . . . . . . 9
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+) |
272 | | rpmulcl 11731 |
. . . . . . . . 9
⊢ ((2
∈ ℝ+ ∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ+) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
273 | 214, 271,
272 | sylancr 694 |
. . . . . . . 8
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
274 | 213, 273 | rerpdivcld 11779 |
. . . . . . 7
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) →
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ) |
275 | 274 | adantll 746 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) →
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ) |
276 | 275 | adantlr 747 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) →
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ) |
277 | 276 | ad3antrrr 762 |
. . . 4
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ) |
278 | | simp-4l 802 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → 𝜑) |
279 | | iccssre 12126 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
280 | 86, 88, 279 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
281 | 280, 63 | syl6ss 3580 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℂ) |
282 | 281 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵)) → 𝑤 ∈ ℂ) |
283 | 281 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) → 𝑢 ∈ ℂ) |
284 | | subcl 10159 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℂ ∧ 𝑢 ∈ ℂ) → (𝑤 − 𝑢) ∈ ℂ) |
285 | 282, 283,
284 | syl2anr 494 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴[,]𝐵)) ∧ (𝜑 ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑤 − 𝑢) ∈ ℂ) |
286 | 285 | anandis 869 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (𝑤 − 𝑢) ∈ ℂ) |
287 | 286 | abscld 14023 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (abs‘(𝑤 − 𝑢)) ∈ ℝ) |
288 | 287 | 3adantr3 1215 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘(𝑤 − 𝑢)) ∈ ℝ) |
289 | 278, 288 | sylan 487 |
. . . . 5
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (abs‘(𝑤 − 𝑢)) ∈ ℝ) |
290 | 289 | adantr 480 |
. . . 4
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(abs‘(𝑤 − 𝑢)) ∈
ℝ) |
291 | | rpdivcl 11732 |
. . . . . . . . 9
⊢ (((𝑦 / 2) ∈ ℝ+
∧ (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) → ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ))) ∈
ℝ+) |
292 | 169, 273,
291 | syl2anr 494 |
. . . . . . . 8
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < )))
∈ ℝ+) |
293 | 292 | rpred 11748 |
. . . . . . 7
⊢ ((((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < )))
∈ ℝ) |
294 | 293 | adantlll 750 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < )))
∈ ℝ) |
295 | 294 | adantllr 751 |
. . . . 5
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → ((𝑦 / 2) / (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < )))
∈ ℝ) |
296 | 295 | ad2antrr 758 |
. . . 4
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
((𝑦 / 2) / (2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< ))) ∈ ℝ) |
297 | 280 | sseld 3567 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ∈ (𝐴[,]𝐵) → 𝑢 ∈ ℝ)) |
298 | 280 | sseld 3567 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑤 ∈ (𝐴[,]𝐵) → 𝑤 ∈ ℝ)) |
299 | | idd 24 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑢 ≤ 𝑤 → 𝑢 ≤ 𝑤)) |
300 | 297, 298,
299 | 3anim123d 1398 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤))) |
301 | 300 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → ((𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤))) |
302 | 301 | imp 444 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) |
303 | 56 | abscld 14023 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ) |
304 | 303 | rexrd 9968 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈
ℝ*) |
305 | | elxrge0 12152 |
. . . . . . . . . . . . . . . . . 18
⊢
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ↔
((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ ℝ* ∧ 0 ≤
(abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
306 | 304, 57, 305 | sylanbrc 695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞)) |
307 | | ifcl 4080 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ∈ (0[,]+∞) ∧ 0 ∈
(0[,]+∞)) → if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,]+∞)) |
308 | 306, 120,
307 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ∈
(0[,]+∞)) |
309 | 308, 67 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))),
0)):ℝ⟶(0[,]+∞)) |
310 | 250 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℂ) |
311 | 310 | 2timesd 11152 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) = (sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, <
))) |
312 | 250, 250 | readdcld 9948 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ) |
313 | 312 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ*) |
314 | | abs0 13873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(abs‘0) = 0 |
315 | 314, 236 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
316 | | suprub 10863 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) ∧ 0 ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
317 | 260, 315,
316 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0 ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
318 | 250, 250,
317, 317 | addge0d 10482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → 0 ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))) |
319 | | elxrge0 12152 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
(0[,]+∞) ↔ ((sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ* ∧ 0 ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)))) |
320 | 313, 318,
319 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
(0[,]+∞)) |
321 | 311, 320 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
(0[,]+∞)) |
322 | | ifcl 4080 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞)
∧ 0 ∈ (0[,]+∞)) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈
(0[,]+∞)) |
323 | 321, 120,
322 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈
(0[,]+∞)) |
324 | 323 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ (𝑢(,)𝑤), (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈
(0[,]+∞)) |
325 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) |
326 | 324, 325 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )),
0)):ℝ⟶(0[,]+∞)) |
327 | 1 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℝ) |
328 | 327 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℂ) |
329 | 328 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑓‘𝑡)) ∈ ℝ) |
330 | 5 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
331 | 330 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℂ) |
332 | 331 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑔‘𝑡)) ∈ ℝ) |
333 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((abs‘(𝑓‘𝑡)) ∈ ℝ ∧ (abs‘(𝑔‘𝑡)) ∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ) |
334 | 329, 332,
333 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ) |
335 | 334 | anandirs 870 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ∈ ℝ) |
336 | 312 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ) |
337 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ) |
338 | 4, 331, 337 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (i · (𝑔‘𝑡)) ∈ ℂ) |
339 | | abstri 13918 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡))))) |
340 | 328, 338,
339 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡))))) |
341 | 340 | anandirs 870 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡))))) |
342 | | absmul 13882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (abs‘(i
· (𝑔‘𝑡))) = ((abs‘i) ·
(abs‘(𝑔‘𝑡)))) |
343 | 4, 331, 342 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · (𝑔‘𝑡))) = ((abs‘i) ·
(abs‘(𝑔‘𝑡)))) |
344 | | absi 13874 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(abs‘i) = 1 |
345 | 344 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((abs‘i) · (abs‘(𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡))) |
346 | 343, 345 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · (𝑔‘𝑡))) = (1 · (abs‘(𝑔‘𝑡)))) |
347 | 332 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(𝑔‘𝑡)) ∈ ℂ) |
348 | 347 | mulid2d 9937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (1 · (abs‘(𝑔‘𝑡))) = (abs‘(𝑔‘𝑡))) |
349 | 346, 348 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡))) |
350 | 349 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(i · (𝑔‘𝑡))) = (abs‘(𝑔‘𝑡))) |
351 | 350 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(i · (𝑔‘𝑡)))) = ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) |
352 | 341, 351 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡)))) |
353 | 329 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ ℝ) |
354 | 332 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ ℝ) |
355 | 250 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
ℝ) |
356 | 260 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs “ (ran 𝑓 ∪ ran 𝑔)) ⊆ ℝ ∧ (abs “ (ran
𝑓 ∪ ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥)) |
357 | 227 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (ran 𝑓 ∪ ran 𝑔) ⊆ ℂ) |
358 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑓:ℝ⟶ℝ →
𝑓 Fn
ℝ) |
359 | 1, 358 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 Fn
ℝ) |
360 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑓 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) ∈ ran 𝑓) |
361 | 359, 360 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈ ran 𝑓) |
362 | | elun1 3742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓‘𝑡) ∈ ran 𝑓 → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
363 | 361, 362 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
364 | 363 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
365 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑓‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
366 | 233, 365 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑓‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑓‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
367 | 357, 364,
366 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(𝑓‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
368 | | suprub 10863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) ∧ (abs‘(𝑓‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘(𝑓‘𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
369 | 356, 367,
368 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(𝑓‘𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
370 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑔:ℝ⟶ℝ →
𝑔 Fn
ℝ) |
371 | 5, 370 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 Fn
ℝ) |
372 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑔 Fn ℝ ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ∈ ran 𝑔) |
373 | 371, 372 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈ ran 𝑔) |
374 | | elun2 3743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔‘𝑡) ∈ ran 𝑔 → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
375 | 373, 374 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
376 | 375 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) |
377 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((abs Fn
ℂ ∧ (ran 𝑓 ∪
ran 𝑔) ⊆ ℂ
∧ (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑔‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
378 | 233, 377 | mp3an1 1403 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((ran
𝑓 ∪ ran 𝑔) ⊆ ℂ ∧ (𝑔‘𝑡) ∈ (ran 𝑓 ∪ ran 𝑔)) → (abs‘(𝑔‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
379 | 357, 376,
378 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(𝑔‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) |
380 | | suprub 10863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((abs
“ (ran 𝑓 ∪ ran
𝑔)) ⊆ ℝ ∧
(abs “ (ran 𝑓 ∪
ran 𝑔)) ≠ ∅ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ (abs
“ (ran 𝑓 ∪ ran
𝑔))𝑦 ≤ 𝑥) ∧ (abs‘(𝑔‘𝑡)) ∈ (abs “ (ran 𝑓 ∪ ran 𝑔))) → (abs‘(𝑔‘𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
381 | 356, 379,
380 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘(𝑔‘𝑡)) ≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) |
382 | 353, 354,
355, 355, 369, 381 | le2addd 10525 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((abs‘(𝑓‘𝑡)) + (abs‘(𝑔‘𝑡))) ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))) |
383 | 303, 335,
336, 352, 382 | letrd 10073 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))) |
384 | 311 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) = (sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, <
))) |
385 | 383, 384 | breqtrrd 4611 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))) |
386 | 51, 385 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) ≤ (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
))) |
387 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
388 | 387 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
389 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = (2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< ))) |
390 | 389 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) = (2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< ))) |
391 | 386, 388,
390 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ (𝑢(,)𝑤)) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) |
392 | 391 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) |
393 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → 0 ≤ 0) |
394 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) = 0) |
395 | | iffalse 4045 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) =
0) |
396 | 393, 394,
395 | 3brtr4d 4615 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑡 ∈ (𝑢(,)𝑤) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) |
397 | 392, 396 | pm2.61d1 170 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) |
398 | 397 | ralrimivw 2950 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ∀𝑡 ∈ ℝ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) |
399 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2
· sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
V |
400 | 399, 65 | ifex 4106 |
. . . . . . . . . . . . . . . . . 18
⊢ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈
V |
401 | 400 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → if(𝑡
∈ (𝑢(,)𝑤), (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0) ∈
V) |
402 | | eqidd 2611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) = (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) |
403 | 14, 72, 401, 75, 402 | ofrfval2 6813 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0)) ↔
∀𝑡 ∈ ℝ
if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0) ≤ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) |
404 | 398, 403 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) |
405 | | itg2le 23312 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )),
0)):ℝ⟶(0[,]+∞) ∧ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0)) ∘𝑟 ≤
(𝑡 ∈ ℝ ↦
if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )),
0)))) |
406 | 309, 326,
404, 405 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )),
0)))) |
407 | 406 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑢
∈ ℝ ∧ 𝑤
∈ ℝ ∧ 𝑢 ≤
𝑤)) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )),
0)))) |
408 | | mblvol 23105 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢(,)𝑤) ∈ dom vol → (vol‘(𝑢(,)𝑤)) = (vol*‘(𝑢(,)𝑤))) |
409 | 35, 408 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(vol‘(𝑢(,)𝑤)) = (vol*‘(𝑢(,)𝑤)) |
410 | | ovolioo 23143 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤) → (vol*‘(𝑢(,)𝑤)) = (𝑤 − 𝑢)) |
411 | 409, 410 | syl5eq 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤) → (vol‘(𝑢(,)𝑤)) = (𝑤 − 𝑢)) |
412 | | resubcl 10224 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑤 ∈ ℝ ∧ 𝑢 ∈ ℝ) → (𝑤 − 𝑢) ∈ ℝ) |
413 | 412 | ancoms 468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ) → (𝑤 − 𝑢) ∈ ℝ) |
414 | 413 | 3adant3 1074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤) → (𝑤 − 𝑢) ∈ ℝ) |
415 | 411, 414 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤) → (vol‘(𝑢(,)𝑤)) ∈ ℝ) |
416 | | elrege0 12149 |
. . . . . . . . . . . . . . . . 17
⊢ (sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < ) ∈
(0[,)+∞) ↔ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ ℝ ∧ 0
≤ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) |
417 | 250, 317,
416 | sylanbrc 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈
(0[,)+∞)) |
418 | | ge0addcl 12155 |
. . . . . . . . . . . . . . . 16
⊢
((sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞)
∧ sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞))
→ (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
(0[,)+∞)) |
419 | 417, 417,
418 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < ) + sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
(0[,)+∞)) |
420 | 311, 419 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) → (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
(0[,)+∞)) |
421 | | itg2const 23313 |
. . . . . . . . . . . . . . 15
⊢ (((𝑢(,)𝑤) ∈ dom vol ∧ (vol‘(𝑢(,)𝑤)) ∈ ℝ ∧ (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < ))
∈ (0[,)+∞)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< )) · (vol‘(𝑢(,)𝑤)))) |
422 | 35, 421 | mp3an1 1403 |
. . . . . . . . . . . . . 14
⊢
(((vol‘(𝑢(,)𝑤)) ∈ ℝ ∧ (2 · sup((abs
“ (ran 𝑓 ∪ ran
𝑔)), ℝ, < ))
∈ (0[,)+∞)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (2 · sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< )) · (vol‘(𝑢(,)𝑤)))) |
423 | 415, 420,
422 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑢
∈ ℝ ∧ 𝑤
∈ ℝ ∧ 𝑢 ≤
𝑤)) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )), 0))) = ((2
· sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ·
(vol‘(𝑢(,)𝑤)))) |
424 | 407, 423 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ (𝑢
∈ ℝ ∧ 𝑤
∈ ℝ ∧ 𝑢 ≤
𝑤)) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ ((2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ·
(vol‘(𝑢(,)𝑤)))) |
425 | 424 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑢 ∈ ℝ
∧ 𝑤 ∈ ℝ
∧ 𝑢 ≤ 𝑤)) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ ((2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ·
(vol‘(𝑢(,)𝑤)))) |
426 | 425 | adantlr 747 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ ((2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ·
(vol‘(𝑢(,)𝑤)))) |
427 | 83 | ad3antlr 763 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
428 | 415 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → (vol‘(𝑢(,)𝑤)) ∈ ℝ) |
429 | 273 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
430 | 429 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
431 | 427, 428,
430 | ledivmuld 11801 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → (((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤
(vol‘(𝑢(,)𝑤)) ↔
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ≤ ((2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ·
(vol‘(𝑢(,)𝑤))))) |
432 | 426, 431 | mpbird 246 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤
(vol‘(𝑢(,)𝑤))) |
433 | | abssubge0 13915 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤) → (abs‘(𝑤 − 𝑢)) = (𝑤 − 𝑢)) |
434 | 410, 433 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤) → (vol*‘(𝑢(,)𝑤)) = (abs‘(𝑤 − 𝑢))) |
435 | 409, 434 | syl5eq 2656 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤) → (vol‘(𝑢(,)𝑤)) = (abs‘(𝑤 − 𝑢))) |
436 | 435 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → (vol‘(𝑢(,)𝑤)) = (abs‘(𝑤 − 𝑢))) |
437 | 432, 436 | breqtrd 4609 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤
(abs‘(𝑤 − 𝑢))) |
438 | 302, 437 | syldan 486 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ ∃𝑟 ∈ (ran
𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤
(abs‘(𝑤 − 𝑢))) |
439 | 438 | adantllr 751 |
. . . . . 6
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤
(abs‘(𝑤 − 𝑢))) |
440 | 439 | adantlr 747 |
. . . . 5
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤
(abs‘(𝑤 − 𝑢))) |
441 | 440 | adantr 480 |
. . . 4
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) ≤
(abs‘(𝑤 − 𝑢))) |
442 | | simpr 476 |
. . . 4
⊢
(((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) ∧ (abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, < )))) →
(abs‘(𝑤 − 𝑢)) < ((𝑦 / 2) / (2 · sup((abs “ (ran
𝑓 ∪ ran 𝑔)), ℝ, <
)))) |
443 | 277, 290,
296, 441, 442 | lelttrd 10074 |
. . 3
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) <
((𝑦 / 2) / (2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< )))) |
444 | 83 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
445 | 444 | ad3antrrr 762 |
. . . . 5
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) ∈ ℝ) |
446 | 128 | adantl 481 |
. . . . 5
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (𝑦 / 2) ∈
ℝ) |
447 | 429 | adantlr 747 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) → (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
448 | 447 | adantr 480 |
. . . . 5
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) → (2
· sup((abs “ (ran 𝑓 ∪ ran 𝑔)), ℝ, < )) ∈
ℝ+) |
449 | 445, 446,
448 | ltdiv1d 11793 |
. . . 4
⊢
(((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) < (𝑦 / 2) ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) <
((𝑦 / 2) / (2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< ))))) |
450 | 449 | ad2antrr 758 |
. . 3
⊢
(((((((𝜑 ∧ (𝑓 ∈ 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) ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝑓‘𝑡) + (i · (𝑔‘𝑡)))), 0))) / (2 · sup((abs “
(ran 𝑓 ∪ ran 𝑔)), ℝ, < ))) <
((𝑦 / 2) / (2 ·
sup((abs “ (ran 𝑓
∪ ran 𝑔)), ℝ,
< ))))) |
451 | 443, 450 | mpbird 246 |
. 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)) |
452 | 203 | adantllr 751 |
. . . 4
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵))) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < (𝑦 / 2)) |
453 | 452 | 3adantr3 1215 |
. . 3
⊢
((((((𝜑 ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) ∧ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < (𝑦 / 2)) ∧ ∃𝑟 ∈ (ran 𝑓 ∪ ran 𝑔)𝑟 ≠ 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑢 ∈ (𝐴[,]𝐵) ∧ 𝑤 ∈ (𝐴[,]𝐵) ∧ 𝑢 ≤ 𝑤)) → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0))) < (𝑦 / 2)) |
454 | 453 | 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)) |
455 | 84, 211, 212, 212, 451, 454 | lt2addd 10529 |
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 · (𝑔‘𝑡)))), 0))) + (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ (𝑢(,)𝑤), (abs‘((𝐹‘𝑡) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2))) |