Step | Hyp | Ref
| Expression |
1 | | rphalfcl 11734 |
. . 3
⊢ (𝑌 ∈ ℝ+
→ (𝑌 / 2) ∈
ℝ+) |
2 | | ftc1anc.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹‘𝑡) d𝑡) |
3 | | ftc1anc.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℝ) |
4 | | ftc1anc.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) |
5 | | ftc1anc.le |
. . . 4
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
6 | | ftc1anc.s |
. . . 4
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
7 | | ftc1anc.d |
. . . 4
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
8 | | ftc1anc.i |
. . . 4
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
9 | | ftc1anc.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
10 | 2, 3, 4, 5, 6, 7, 8, 9 | ftc1anclem5 32659 |
. . 3
⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) →
∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2)) |
11 | 1, 10 | sylan2 490 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2)) |
12 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡) |
13 | | ax-icn 9874 |
. . . . . . . 8
⊢ i ∈
ℂ |
14 | | ine0 10344 |
. . . . . . . 8
⊢ i ≠
0 |
15 | 13, 14 | reccli 10634 |
. . . . . . 7
⊢ (1 / i)
∈ ℂ |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 / i) ∈
ℂ) |
17 | 9 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℂ) |
18 | 9 | feqmptd 6159 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦))) |
19 | 18, 8 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈
𝐿1) |
20 | | divrec2 10581 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦))) |
21 | 13, 14, 20 | mp3an23 1408 |
. . . . . . . . 9
⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦))) |
22 | 17, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦))) |
23 | 22 | mpteq2dva 4672 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))) |
24 | | iblmbf 23340 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn) |
25 | 19, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
27 | 26 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (ℜ‘(𝐹‘𝑦)) = (ℜ‘(𝐹‘𝑥))) |
28 | 27 | cbvmptv 4678 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) |
29 | 28 | eleq1i 2679 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
30 | 17 | recld 13782 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℝ) |
31 | 30 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ) |
32 | 31 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ) |
33 | 29 | biimpri 217 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
35 | 32, 34 | mbfneg 23223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
36 | 29, 35 | sylan2b 491 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
37 | 9 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℂ) |
38 | 37 | recld 13782 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ) |
39 | 38 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℂ) |
40 | 39 | negnegd 10262 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → --(ℜ‘(𝐹‘𝑥)) = (ℜ‘(𝐹‘𝑥))) |
41 | 40 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥)))) |
42 | 41, 28 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦)))) |
43 | 42 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦)))) |
44 | | negex 10158 |
. . . . . . . . . . . . . . . 16
⊢
-(ℜ‘(𝐹‘𝑥)) ∈ V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) ∧ 𝑥 ∈ 𝐷) → -(ℜ‘(𝐹‘𝑥)) ∈ V) |
46 | 27 | negeqd 10154 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → -(ℜ‘(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑥))) |
47 | 46 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) |
48 | 47 | eleq1i 2679 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
49 | 48 | biimpi 205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
51 | 45, 50 | mbfneg 23223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
52 | 43, 51 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
53 | 36, 52 | impbida 873 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)) |
54 | | divcl 10570 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → ((𝐹‘𝑦) / i) ∈ ℂ) |
55 | | imre 13696 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑦) / i) ∈ ℂ →
(ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i)))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i)))) |
57 | 13, 14, 56 | mp3an23 1408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ ℂ →
(ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i)))) |
58 | 13, 14, 54 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) ∈ ℂ) |
59 | | mulneg1 10345 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ ((𝐹‘𝑦) / i) ∈ ℂ) → (-i ·
((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i))) |
60 | 13, 58, 59 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i))) |
61 | | divcan2 10572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦)) |
62 | 13, 14, 61 | mp3an23 1408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) ∈ ℂ → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦)) |
63 | 62 | negeqd 10154 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ ℂ → -(i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦)) |
64 | 60, 63 | eqtrd 2644 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦)) |
65 | 64 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘(-i
· ((𝐹‘𝑦) / i))) = (ℜ‘-(𝐹‘𝑦))) |
66 | | reneg 13713 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘-(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑦))) |
67 | 57, 65, 66 | 3eqtrd 2648 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑦) ∈ ℂ →
(ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦))) |
68 | 17, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦))) |
69 | 68 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) = (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦)))) |
70 | 69 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)) |
71 | 53, 70 | bitr4d 270 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)) |
72 | | imval 13695 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i))) |
73 | 17, 72 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i))) |
74 | 73 | mpteq2dva 4672 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i)))) |
75 | 74 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn)) |
76 | 71, 75 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn))) |
77 | | ancom 465 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)) |
78 | 76, 77 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))) |
79 | 17 | ismbfcn2 23212 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn))) |
80 | 17, 58 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) ∈ ℂ) |
81 | 80 | ismbfcn2 23212 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))) |
82 | 78, 79, 81 | 3bitr4d 299 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn)) |
83 | 25, 82 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn) |
84 | 23, 83 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ MblFn) |
85 | 16, 17, 19, 84 | iblmulc2nc 32645 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈
𝐿1) |
86 | | mulcl 9899 |
. . . . . . 7
⊢ (((1 / i)
∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → ((1 / i) ·
(𝐹‘𝑦)) ∈ ℂ) |
87 | 15, 17, 86 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ) |
88 | | eqid 2610 |
. . . . . 6
⊢ (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) |
89 | 87, 88 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))):𝐷⟶ℂ) |
90 | 12, 3, 4, 5, 6, 7, 85, 89 | ftc1anclem5 32659 |
. . . 4
⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) |
91 | 1, 90 | sylan2 490 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) |
92 | 9 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
93 | | 0cnd 9912 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
94 | 92, 93 | ifclda 4070 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
95 | | imval 13695 |
. . . . . . . . . . . 12
⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ →
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))) |
97 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑡 → (𝐹‘𝑦) = (𝐹‘𝑡)) |
98 | 97 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑡 → ((1 / i) · (𝐹‘𝑦)) = ((1 / i) · (𝐹‘𝑡))) |
99 | | ovex 6577 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 / i)
· (𝐹‘𝑡)) ∈ V |
100 | 98, 88, 99 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡))) |
101 | 100 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡))) |
102 | | divrec2 10581 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑡) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡))) |
103 | 13, 14, 102 | mp3an23 1408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑡) ∈ ℂ → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡))) |
104 | 92, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡))) |
105 | 101, 104 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((𝐹‘𝑡) / i)) |
106 | 105 | ifeq1da 4066 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)) |
107 | | ovif 6635 |
. . . . . . . . . . . . . 14
⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i)) |
108 | 13, 14 | div0i 10638 |
. . . . . . . . . . . . . . 15
⊢ (0 / i) =
0 |
109 | | ifeq2 4041 |
. . . . . . . . . . . . . . 15
⊢ ((0 / i)
= 0 → if(𝑡 ∈
𝐷, ((𝐹‘𝑡) / i), (0 / i)) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)) |
110 | 108, 109 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i)) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0) |
111 | 107, 110 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0) |
112 | 106, 111 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)) |
113 | 112 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))) |
114 | 96, 113 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0))) |
115 | 114 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))) |
116 | 115 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡)))) |
117 | 116 | mpteq2dv 4673 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) |
118 | 117 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡)))))) |
119 | 118 | breq1d 4593 |
. . . . 5
⊢ (𝜑 →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))) |
120 | 119 | rexbidv 3034 |
. . . 4
⊢ (𝜑 → (∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))) |
121 | 120 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))) |
122 | 91, 121 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) |
123 | | reeanv 3086 |
. . 3
⊢
(∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) ↔ (∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))) |
124 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷)) |
125 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡)) |
126 | 124, 125 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
127 | 126 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
128 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) |
129 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V |
130 | 127, 128,
129 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
131 | 130 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
132 | 131 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ℝ →
(abs‘(((𝑥 ∈
ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
133 | 132 | mpteq2ia 4668 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ ↦
(abs‘(((𝑥 ∈
ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
134 | 133 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
135 | | rembl 23115 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ
∈ dom vol |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ℝ ∈ dom
vol) |
137 | | 0cnd 9912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐷) → 0 ∈ ℂ) |
138 | 37, 137 | ifclda 4070 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ) |
139 | 138 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ) |
140 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (ℝ ∖ 𝐷) → ¬ 𝑥 ∈ 𝐷) |
141 | 140 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑥 ∈ 𝐷) |
142 | 141 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0) |
143 | 9 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥))) |
144 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ 𝐷 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
145 | 144 | mpteq2ia 4668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) |
146 | 143, 145 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) |
147 | 146, 8 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈
𝐿1) |
148 | 7, 136, 139, 142, 147 | iblss2 23378 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈
𝐿1) |
149 | 138 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ) |
150 | 149 | iblcn 23371 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1 ↔
((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1))) |
151 | 148, 150 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1)) |
152 | 151 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1) |
153 | 149 | recld 13782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ∈ ℝ) |
154 | 153, 128 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ) |
155 | 152, 154 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
156 | | ftc1anclem4 32658 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ dom ∫1
∧ (𝑥 ∈ ℝ
↦ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
157 | 156 | 3expb 1258 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ dom ∫1
∧ ((𝑥 ∈ ℝ
↦ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
158 | 155, 157 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ 𝜑) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
159 | 158 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
160 | 134, 159 | syl5eqelr 2693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ) |
161 | 126 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
162 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) |
163 | | fvex 6113 |
. . . . . . . . . . . . . . . . 17
⊢
(ℑ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V |
164 | 161, 162,
163 | fvmpt 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
165 | 164 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡)) = ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) |
166 | 165 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ℝ →
(abs‘(((𝑥 ∈
ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
167 | 166 | mpteq2ia 4668 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ ↦
(abs‘(((𝑥 ∈
ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
168 | 167 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
169 | 151 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1) |
170 | 138 | imcld 13783 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ) |
171 | 170 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ∈ ℝ) |
172 | 171, 162 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ) |
173 | 169, 172 | jca 553 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
174 | | ftc1anclem4 32658 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ dom ∫1
∧ (𝑥 ∈ ℝ
↦ (ℑ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
175 | 174 | 3expb 1258 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ dom ∫1
∧ ((𝑥 ∈ ℝ
↦ (ℑ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
176 | 173, 175 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ dom ∫1
∧ 𝜑) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
177 | 176 | ancoms 468 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
178 | 168, 177 | syl5eqelr 2693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) |
179 | 160, 178 | anim12dan 878 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)) |
180 | 1 | rpred 11748 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ℝ+
→ (𝑌 / 2) ∈
ℝ) |
181 | 180, 180 | jca 553 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) ∈
ℝ ∧ (𝑌 / 2)
∈ ℝ)) |
182 | | lt2add 10392 |
. . . . . . . . . 10
⊢
((((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) ∧ ((𝑌 / 2) ∈ ℝ ∧
(𝑌 / 2) ∈ ℝ))
→ (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
183 | 179, 181,
182 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑌 ∈
ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
184 | 183 | an32s 842 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
185 | 94 | recld 13782 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
186 | 185 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
187 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
188 | 187 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℝ) |
189 | 188 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℂ) |
190 | | subcl 10159 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑓‘𝑡) ∈ ℂ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
191 | 186, 189,
190 | syl2an 493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
192 | 191 | anassrs 678 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
193 | 192 | adantlrr 753 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
194 | 94 | imcld 13783 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
195 | 194 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
196 | | i1ff 23249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
197 | 196 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
198 | 197 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℂ) |
199 | | subcl 10159 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) →
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) |
200 | 195, 198,
199 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) |
201 | 200 | anassrs 678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) |
202 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
203 | 13, 201, 202 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
204 | 203 | adantlrl 752 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
205 | 193, 204 | addcld 9938 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ ℂ) |
206 | 205 | abscld 14023 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) |
207 | 206 | rexrd 9968 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈
ℝ*) |
208 | 205 | absge0d 14031 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
209 | | elxrge0 12152 |
. . . . . . . . . . . . . 14
⊢
((abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ (0[,]+∞) ↔
((abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ* ∧ 0 ≤
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
210 | 207, 208,
209 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ (0[,]+∞)) |
211 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
212 | 210, 211 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞)) |
213 | | icossicc 12131 |
. . . . . . . . . . . . . . 15
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
214 | | ge0addcl 12155 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,)+∞)) |
215 | 213, 214 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,]+∞)) |
216 | 215 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑥 ∈
(0[,)+∞) ∧ 𝑦
∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,]+∞)) |
217 | 192 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ) |
218 | 192 | absge0d 14031 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
219 | | elrege0 12149 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞) ↔
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ ∧ 0 ≤
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
220 | 217, 218,
219 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞)) |
221 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
222 | 220, 221 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞)) |
223 | 222 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞)) |
224 | 201 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ) |
225 | 201 | absge0d 14031 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
226 | | elrege0 12149 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞) ↔
((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ ∧ 0 ≤
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
227 | 224, 225,
226 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞)) |
228 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
229 | 227, 228 | fmptd 6292 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞)) |
230 | 229 | adantrl 748 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞)) |
231 | | reex 9906 |
. . . . . . . . . . . . . 14
⊢ ℝ
∈ V |
232 | 231 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ℝ ∈ V) |
233 | | inidm 3784 |
. . . . . . . . . . . . 13
⊢ (ℝ
∩ ℝ) = ℝ |
234 | 216, 223,
230, 232, 232, 233 | off 6810 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))):ℝ⟶(0[,]+∞)) |
235 | 193, 204 | abstrid 14043 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
236 | 235 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ∀𝑡 ∈
ℝ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
237 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ V |
238 | 237 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ V) |
239 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
240 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ V |
241 | 240 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ V) |
242 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ V |
243 | 242 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ V) |
244 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
245 | | absmul 13882 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (abs‘(i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) ·
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
246 | 13, 201, 245 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) ·
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
247 | | absi 13874 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(abs‘i) = 1 |
248 | 247 | oveq1i 6559 |
. . . . . . . . . . . . . . . . . . 19
⊢
((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (1 ·
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
249 | 224 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
250 | 249 | mulid2d 9937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (1
· (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
251 | 248, 250 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
252 | 246, 251 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
253 | 252 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
254 | 253 | adantrl 748 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
255 | 232, 241,
243, 244, 254 | offval2 6812 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (𝑡 ∈ ℝ ↦
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
256 | 232, 206,
238, 239, 255 | ofrfval2 6813 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ↔ ∀𝑡 ∈ ℝ
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
257 | 236, 256 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
258 | | itg2le 23312 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞) ∧
((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))):ℝ⟶(0[,]+∞) ∧
(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
259 | 212, 234,
257, 258 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
260 | | eqidd 2611 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
261 | | absf 13925 |
. . . . . . . . . . . . . . . . 17
⊢
abs:ℂ⟶ℝ |
262 | 261 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
abs:ℂ⟶ℝ) |
263 | 262 | feqmptd 6159 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → abs =
(𝑥 ∈ ℂ ↦
(abs‘𝑥))) |
264 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) → (abs‘𝑥) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
265 | 192, 260,
263, 264 | fmptco 6303 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs
∘ (𝑡 ∈ ℝ
↦ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
266 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑓‘𝑡) ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ) |
267 | 185, 188,
266 | syl2an 493 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ) |
268 | 267 | anassrs 678 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ) |
269 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
270 | 268, 269 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ) |
271 | 135 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ
∈ dom vol) |
272 | | iunin2 4520 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) |
273 | | imaiun 6407 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡𝑓 “ ∪
𝑦 ∈ ran 𝑓{𝑦}) = ∪
𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}) |
274 | | iunid 4511 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ 𝑦 ∈ ran 𝑓{𝑦} = ran 𝑓 |
275 | 274 | imaeq2i 5383 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡𝑓 “ ∪
𝑦 ∈ ran 𝑓{𝑦}) = (◡𝑓 “ ran 𝑓) |
276 | 273, 275 | eqtr3i 2634 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}) = (◡𝑓 “ ran 𝑓) |
277 | 276 | ineq2i 3773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) |
278 | 272, 277 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) |
279 | | cnvimass 5404 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ dom (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
280 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ V |
281 | 280, 269 | dmmpti 5936 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom
(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = ℝ |
282 | 279, 281 | sseqtri 3600 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆
ℝ |
283 | | cnvimarndm 5405 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡𝑓 “ ran 𝑓) = dom 𝑓 |
284 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓:ℝ⟶ℝ →
dom 𝑓 =
ℝ) |
285 | 187, 284 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ dom ∫1
→ dom 𝑓 =
ℝ) |
286 | 283, 285 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ (◡𝑓 “ ran 𝑓) = ℝ) |
287 | 282, 286 | syl5sseqr 3617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓)) |
288 | | df-ss 3554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
289 | 287, 288 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
290 | 278, 289 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
291 | 290 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
292 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:ℝ⟶ℝ →
ran 𝑓 ⊆
ℝ) |
293 | 187, 292 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ⊆
ℝ) |
294 | 293 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ran
𝑓 ⊆
ℝ) |
295 | 294 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → 𝑦 ∈ ℝ) |
296 | 185 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
297 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ) |
298 | 185, 297 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ) |
299 | 298 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ) |
300 | 296, 299 | 2thd 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ↔
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)) |
301 | | ltaddsub 10381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
302 | 185, 301 | syl3an3 1353 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
303 | 302 | 3comr 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
304 | 303 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
305 | 300, 304 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))) |
306 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
307 | 306 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈
ℝ*) |
308 | 307 | adantll 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈
ℝ*) |
309 | | elioopnf 12138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 + 𝑦) ∈ ℝ* →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
310 | 308, 309 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
311 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
312 | 311 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ*) |
313 | | elioopnf 12138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ ℝ*
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))) |
314 | 312, 313 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))) |
315 | 305, 310,
314 | 3bitr4rd 300 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))) |
316 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓‘𝑡) = 𝑦 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)) |
317 | 316 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞))) |
318 | 317 | bibi1d 332 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)) ↔
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))) |
319 | 315, 318 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))) |
320 | 319 | pm5.32rd 670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦))) |
321 | 320 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦))) |
322 | 295, 321 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦))) |
323 | 322 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
324 | 187 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡))) |
325 | 324 | cnveqd 5220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 ∈ dom ∫1
→ ◡𝑓 = ◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡))) |
326 | 325 | imaeq1d 5384 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ dom ∫1
→ (◡𝑓 “ {𝑦}) = (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) |
327 | 326 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
328 | 269 | mptpreima 5545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} |
329 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑦 ∈ V |
330 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) |
331 | 330 | mptiniseg 5546 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ V → (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
332 | 329, 331 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦} |
333 | 328, 332 | ineq12i 3774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
334 | | inrab 3858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
335 | 333, 334 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
336 | 327, 335 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
337 | 336 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
338 | 326 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
339 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) |
340 | 339 | mptpreima 5545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) = {𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} |
341 | 340, 332 | ineq12i 3774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
342 | | inrab 3858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
343 | 341, 342 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
344 | 338, 343 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
345 | 344 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
346 | 323, 337,
345 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦}))) |
347 | 346 | iuneq2dv 4478 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ∪
𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦}))) |
348 | 291, 347 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦}))) |
349 | | i1frn 23250 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ∈
Fin) |
350 | 349 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ran
𝑓 ∈
Fin) |
351 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
352 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷) |
353 | 352 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷) |
354 | 353 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0) |
355 | 9 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
356 | | iftrue 4042 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡)) |
357 | 356 | mpteq2ia 4668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) |
358 | 355, 357 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
359 | | iblmbf 23340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 ∈ 𝐿1
→ 𝐹 ∈
MblFn) |
360 | 8, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹 ∈ MblFn) |
361 | 358, 360 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn) |
362 | 7, 136, 351, 354, 361 | mbfss 23219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn) |
363 | 94 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
364 | 363 | ismbfcn2 23212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn ↔ ((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn))) |
365 | 362, 364 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)) |
366 | 365 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) |
367 | 185 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
368 | 367, 339 | fmptd 6292 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡),
0))):ℝ⟶ℝ) |
369 | | mbfima 23205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom
vol) |
370 | 366, 368,
369 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom
vol) |
371 | | i1fima 23251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ (◡𝑓 “ {𝑦}) ∈ dom vol) |
372 | | inmbl 23117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
373 | 370, 371,
372 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
374 | 373 | ralrimivw 2950 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
375 | | finiunmbl 23119 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ran
𝑓 ∈ Fin ∧
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
376 | 350, 374,
375 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
377 | 376 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
378 | 348, 377 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∈ dom
vol) |
379 | | iunin2 4520 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪
𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) |
380 | 276 | ineq2i 3773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪
𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) |
381 | 379, 380 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) |
382 | | cnvimass 5404 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ dom (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
383 | 382, 281 | sseqtri 3600 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ ℝ |
384 | 383, 286 | syl5sseqr 3617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓)) |
385 | | df-ss 3554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
386 | 384, 385 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
387 | 381, 386 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
388 | 387 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
389 | 299, 296 | 2thd 254 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ↔
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)) |
390 | | ltsubadd 10377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
391 | 185, 390 | syl3an1 1351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
392 | 391 | 3expa 1257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
393 | 392 | an32s 842 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
394 | 389, 393 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))) |
395 | | elioomnf 12139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ ℝ*
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥))) |
396 | 312, 395 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥))) |
397 | | elioomnf 12139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 + 𝑦) ∈ ℝ* →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))) |
398 | 308, 397 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))) |
399 | 394, 396,
398 | 3bitr4d 299 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))) |
400 | 316 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥))) |
401 | 400 | bibi1d 332 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))) |
402 | 399, 401 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))) |
403 | 402 | pm5.32rd 670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦))) |
404 | 403 | adantllr 751 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦))) |
405 | 295, 404 | syldan 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦))) |
406 | 405 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}) |
407 | 326 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
408 | 269 | mptpreima 5545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} |
409 | 408, 332 | ineq12i 3774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
410 | | inrab 3858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} |
411 | 409, 410 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} |
412 | 407, 411 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}) |
413 | 412 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}) |
414 | 326 | ineq2d 3776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
415 | 339 | mptpreima 5545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) = {𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} |
416 | 415, 332 | ineq12i 3774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
417 | | inrab 3858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)} |
418 | 416, 417 | eqtri 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)} |
419 | 414, 418 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}) |
420 | 419 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}) |
421 | 406, 413,
420 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦}))) |
422 | 421 | iuneq2dv 4478 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ∪
𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦}))) |
423 | 388, 422 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = ∪
𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦}))) |
424 | | mbfima 23205 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol) |
425 | 366, 368,
424 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol) |
426 | | inmbl 23117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
427 | 425, 371,
426 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
428 | 427 | ralrimivw 2950 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
429 | | finiunmbl 23119 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ran
𝑓 ∈ Fin ∧
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
430 | 350, 428,
429 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
431 | 430 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
432 | 423, 431 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∈ dom vol) |
433 | 270, 271,
378, 432 | ismbf2d 23214 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn) |
434 | | ftc1anclem1 32655 |
. . . . . . . . . . . . . . 15
⊢ (((𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
435 | 270, 433,
434 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs
∘ (𝑡 ∈ ℝ
↦ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
436 | 265, 435 | eqeltrrd 2689 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
437 | 436 | adantrr 749 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
438 | 160 | adantrr 749 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ) |
439 | 178 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) |
440 | 437, 223,
438, 230, 439 | itg2addnc 32634 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
441 | 259, 440 | breqtrd 4609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
442 | 441 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
443 | | itg2cl 23305 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈
ℝ*) |
444 | 212, 443 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈
ℝ*) |
445 | 444 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈
ℝ*) |
446 | | readdcl 9898 |
. . . . . . . . . . . . . 14
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ) |
447 | 160, 178,
446 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ (𝜑 ∧ 𝑔 ∈ dom ∫1)) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ) |
448 | 447 | anandis 869 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ) |
449 | 448 | rexrd 9968 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈
ℝ*) |
450 | 449 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈
ℝ*) |
451 | 1, 1 | rpaddcld 11763 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) + (𝑌 / 2)) ∈
ℝ+) |
452 | 451 | rpxrd 11749 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) + (𝑌 / 2)) ∈
ℝ*) |
453 | 452 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((𝑌 / 2) + (𝑌 / 2)) ∈
ℝ*) |
454 | | xrlelttr 11863 |
. . . . . . . . . 10
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈ ℝ* ∧
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ* ∧
((𝑌 / 2) + (𝑌 / 2)) ∈
ℝ*) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∧ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2))) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
455 | 445, 450,
453, 454 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∧ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2))) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
456 | 442, 455 | mpand 707 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
457 | 184, 456 | syld 46 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
458 | | mulcl 9899 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) → (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) |
459 | 13, 195, 458 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) |
460 | 186, 459 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)) |
461 | | mulcl 9899 |
. . . . . . . . . . . . . . . . . 18
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ) |
462 | 13, 198, 461 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (i · (𝑔‘𝑡)) ∈ ℂ) |
463 | 189, 462 | anim12i 588 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) |
464 | 463 | anandirs 870 |
. . . . . . . . . . . . . . 15
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) |
465 | | addsub4 10203 |
. . . . . . . . . . . . . . 15
⊢
((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) ∧ ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
466 | 460, 464,
465 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ 𝑡 ∈ ℝ))
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
467 | 466 | anassrs 678 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
468 | 94 | replimd 13785 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
469 | 468 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
470 | 469 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
471 | 198 | adantll 746 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (𝑔‘𝑡) ∈ ℂ) |
472 | | subdi 10342 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))) |
473 | 13, 472 | mp3an1 1403 |
. . . . . . . . . . . . . . . 16
⊢
(((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))) |
474 | 195, 471,
473 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ 𝑡 ∈ ℝ))
→ (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))) |
475 | 474 | anassrs 678 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))) |
476 | 475 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
477 | 467, 470,
476 | 3eqtr4rd 2655 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
478 | 477 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
479 | 478 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
480 | 479 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))) |
481 | 480 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))) |
482 | | rpcn 11717 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℝ+
→ 𝑌 ∈
ℂ) |
483 | 482 | 2halvesd 11155 |
. . . . . . . . 9
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) + (𝑌 / 2)) = 𝑌) |
484 | 483 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌) |
485 | 481, 484 | breq12d 4596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
486 | 457, 485 | sylibd 228 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
487 | 486 | anassrs 678 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑓 ∈ dom ∫1)
∧ 𝑔 ∈ dom
∫1) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
488 | 487 | reximdva 3000 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑓 ∈ dom ∫1)
→ (∃𝑔 ∈ dom
∫1((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
489 | 488 | reximdva 3000 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
490 | 123, 489 | syl5bir 232 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
491 | 11, 122, 490 | mp2and 711 |
1
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌) |