Step | Hyp | Ref
| Expression |
1 | | rphalfcl 11858 |
. . 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 33489 |
. . 3
⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) →
∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2)) |
11 | 1, 10 | sylan2 491 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2)) |
12 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) d𝑡) |
13 | | ax-icn 9995 |
. . . . . . . 8
⊢ i ∈
ℂ |
14 | | ine0 10465 |
. . . . . . . 8
⊢ i ≠
0 |
15 | 13, 14 | reccli 10755 |
. . . . . . 7
⊢ (1 / i)
∈ ℂ |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (1 / i) ∈
ℂ) |
17 | 9 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (𝐹‘𝑦) ∈ ℂ) |
18 | 9 | feqmptd 6249 |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦))) |
19 | 18, 8 | eqeltrrd 2702 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈
𝐿1) |
20 | | divrec2 10702 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦))) |
21 | 13, 14, 20 | mp3an23 1416 |
. . . . . . . . 9
⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦))) |
22 | 17, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) = ((1 / i) · (𝐹‘𝑦))) |
23 | 22 | mpteq2dva 4744 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))) |
24 | | iblmbf 23534 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ 𝐿1 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn) |
25 | 19, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn) |
26 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
27 | 26 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (ℜ‘(𝐹‘𝑦)) = (ℜ‘(𝐹‘𝑥))) |
28 | 27 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) |
29 | 28 | eleq1i 2692 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
30 | 17 | recld 13934 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℝ) |
31 | 30 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ) |
32 | 31 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) ∧ 𝑦 ∈ 𝐷) → (ℜ‘(𝐹‘𝑦)) ∈ ℂ) |
33 | 29 | biimpri 218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
35 | 32, 34 | mbfneg 23417 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
36 | 29, 35 | sylan2b 492 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
37 | 9 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹‘𝑥) ∈ ℂ) |
38 | 37 | recld 13934 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ) |
39 | 38 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (ℜ‘(𝐹‘𝑥)) ∈ ℂ) |
40 | 39 | negnegd 10383 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → --(ℜ‘(𝐹‘𝑥)) = (ℜ‘(𝐹‘𝑥))) |
41 | 40 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑥)))) |
42 | 41, 28 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦)))) |
43 | 42 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦)))) |
44 | | negex 10279 |
. . . . . . . . . . . . . . . 16
⊢
-(ℜ‘(𝐹‘𝑥)) ∈ V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) ∧ 𝑥 ∈ 𝐷) → -(ℜ‘(𝐹‘𝑥)) ∈ V) |
46 | 27 | negeqd 10275 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑥 → -(ℜ‘(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑥))) |
47 | 46 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) = (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) |
48 | 47 | eleq1i 2692 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
49 | 48 | biimpi 206 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
51 | 45, 50 | mbfneg 23417 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑥 ∈ 𝐷 ↦ --(ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
52 | 43, 51 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn) → (𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn) |
53 | 36, 52 | impbida 877 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)) |
54 | | divcl 10691 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → ((𝐹‘𝑦) / i) ∈ ℂ) |
55 | | imre 13848 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹‘𝑦) / i) ∈ ℂ →
(ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i)))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → (ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i)))) |
57 | 13, 14, 56 | mp3an23 1416 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ ℂ →
(ℑ‘((𝐹‘𝑦) / i)) = (ℜ‘(-i · ((𝐹‘𝑦) / i)))) |
58 | 13, 14, 54 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) ∈ ℂ → ((𝐹‘𝑦) / i) ∈ ℂ) |
59 | | mulneg1 10466 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((i
∈ ℂ ∧ ((𝐹‘𝑦) / i) ∈ ℂ) → (-i ·
((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i))) |
60 | 13, 58, 59 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(i · ((𝐹‘𝑦) / i))) |
61 | | divcan2 10693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘𝑦) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦)) |
62 | 13, 14, 61 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) ∈ ℂ → (i · ((𝐹‘𝑦) / i)) = (𝐹‘𝑦)) |
63 | 62 | negeqd 10275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) ∈ ℂ → -(i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦)) |
64 | 60, 63 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘𝑦) ∈ ℂ → (-i · ((𝐹‘𝑦) / i)) = -(𝐹‘𝑦)) |
65 | 64 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘(-i
· ((𝐹‘𝑦) / i))) = (ℜ‘-(𝐹‘𝑦))) |
66 | | reneg 13865 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑦) ∈ ℂ → (ℜ‘-(𝐹‘𝑦)) = -(ℜ‘(𝐹‘𝑦))) |
67 | 57, 65, 66 | 3eqtrd 2660 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑦) ∈ ℂ →
(ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦))) |
68 | 17, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘((𝐹‘𝑦) / i)) = -(ℜ‘(𝐹‘𝑦))) |
69 | 68 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) = (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦)))) |
70 | 69 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ -(ℜ‘(𝐹‘𝑦))) ∈ MblFn)) |
71 | 53, 70 | bitr4d 271 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)) |
72 | | imval 13847 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑦) ∈ ℂ → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i))) |
73 | 17, 72 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → (ℑ‘(𝐹‘𝑦)) = (ℜ‘((𝐹‘𝑦) / i))) |
74 | 73 | mpteq2dva 4744 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i)))) |
75 | 74 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn)) |
76 | 71, 75 | anbi12d 747 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn))) |
77 | | ancom 466 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn)) |
78 | 76, 77 | syl6bb 276 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn) ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))) |
79 | 17 | ismbfcn2 23406 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑦))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑦))) ∈ MblFn))) |
80 | 17, 58 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((𝐹‘𝑦) / i) ∈ ℂ) |
81 | 80 | ismbfcn2 23406 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn ↔ ((𝑦 ∈ 𝐷 ↦ (ℜ‘((𝐹‘𝑦) / i))) ∈ MblFn ∧ (𝑦 ∈ 𝐷 ↦ (ℑ‘((𝐹‘𝑦) / i))) ∈ MblFn))) |
82 | 78, 79, 81 | 3bitr4d 300 |
. . . . . . . 8
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ (𝐹‘𝑦)) ∈ MblFn ↔ (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn)) |
83 | 25, 82 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((𝐹‘𝑦) / i)) ∈ MblFn) |
84 | 23, 83 | eqeltrrd 2702 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈ MblFn) |
85 | 16, 17, 19, 84 | iblmulc2nc 33475 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) ∈
𝐿1) |
86 | | mulcl 10020 |
. . . . . . 7
⊢ (((1 / i)
∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → ((1 / i) ·
(𝐹‘𝑦)) ∈ ℂ) |
87 | 15, 17, 86 | sylancr 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → ((1 / i) · (𝐹‘𝑦)) ∈ ℂ) |
88 | | eqid 2622 |
. . . . . 6
⊢ (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) = (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))) |
89 | 87, 88 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦))):𝐷⟶ℂ) |
90 | 12, 3, 4, 5, 6, 7, 85, 89 | ftc1anclem5 33489 |
. . . 4
⊢ ((𝜑 ∧ (𝑌 / 2) ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) |
91 | 1, 90 | sylan2 491 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) |
92 | 9 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
93 | | 0cnd 10033 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
94 | 92, 93 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
95 | | imval 13847 |
. . . . . . . . . . . 12
⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ →
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))) |
97 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑡 → (𝐹‘𝑦) = (𝐹‘𝑡)) |
98 | 97 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑡 → ((1 / i) · (𝐹‘𝑦)) = ((1 / i) · (𝐹‘𝑡))) |
99 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 / i)
· (𝐹‘𝑡)) ∈ V |
100 | 98, 88, 99 | fvmpt 6282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡))) |
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((1 / i) · (𝐹‘𝑡))) |
102 | | divrec2 10702 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐹‘𝑡) ∈ ℂ ∧ i ∈ ℂ ∧
i ≠ 0) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡))) |
103 | 13, 14, 102 | mp3an23 1416 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑡) ∈ ℂ → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡))) |
104 | 92, 103 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝐹‘𝑡) / i) = ((1 / i) · (𝐹‘𝑡))) |
105 | 101, 104 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡) = ((𝐹‘𝑡) / i)) |
106 | 105 | ifeq1da 4116 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0)) |
107 | | ovif 6737 |
. . . . . . . . . . . . . 14
⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), (0 / i)) |
108 | 13, 14 | div0i 10759 |
. . . . . . . . . . . . . . 15
⊢ (0 / i) =
0 |
109 | | ifeq2 4091 |
. . . . . . . . . . . . . . 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 2644 |
. . . . . . . . . . . . 13
⊢ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i) = if(𝑡 ∈ 𝐷, ((𝐹‘𝑡) / i), 0) |
112 | 106, 111 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i)) |
113 | 112 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) = (ℜ‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) / i))) |
114 | 96, 113 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0))) |
115 | 114 | oveq1d 6665 |
. . . . . . . . 9
⊢ (𝜑 → ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))) |
116 | 115 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡)))) |
117 | 116 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) |
118 | 117 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡)))))) |
119 | 118 | breq1d 4663 |
. . . . 5
⊢ (𝜑 →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))) |
120 | 119 | rexbidv 3052 |
. . . 4
⊢ (𝜑 → (∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))) |
121 | 120 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2) ↔ ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, ((𝑦 ∈ 𝐷 ↦ ((1 / i) · (𝐹‘𝑦)))‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2))) |
122 | 91, 121 | mpbird 247 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) |
123 | | reeanv 3107 |
. . 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 | | eleq1w 2684 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷)) |
125 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡)) |
126 | 124, 125 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
127 | 126 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
128 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) |
129 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢
(ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V |
130 | 127, 128,
129 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
131 | 130 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
132 | 131 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ →
(abs‘(((𝑥 ∈
ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
133 | 132 | mpteq2ia 4740 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℝ ↦
(abs‘(((𝑥 ∈
ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
134 | 133 | fveq2i 6194 |
. . . . . . . . . 10
⊢
(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
135 | | rembl 23308 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
∈ dom vol |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ℝ ∈ dom
vol) |
137 | | 0cnd 10033 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ¬ 𝑥 ∈ 𝐷) → 0 ∈ ℂ) |
138 | 37, 137 | ifclda 4120 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ) |
139 | 138 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ) |
140 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (ℝ ∖ 𝐷) → ¬ 𝑥 ∈ 𝐷) |
141 | 140 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑥 ∈ 𝐷) |
142 | 141 | iffalsed 4097 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (ℝ ∖ 𝐷)) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0) |
143 | 9 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥))) |
144 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐷 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥)) |
145 | 144 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (𝑥 ∈ 𝐷 ↦ (𝐹‘𝑥)) |
146 | 143, 145 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0))) |
147 | 146, 8 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈
𝐿1) |
148 | 7, 136, 139, 142, 147 | iblss2 23572 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈
𝐿1) |
149 | 138 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) ∈ ℂ) |
150 | 149 | iblcn 23565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ 𝐿1 ↔
((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1))) |
151 | 148, 150 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1)) |
152 | 151 | simpld 475 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1) |
153 | 149 | recld 13934 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ∈ ℝ) |
154 | 153, 128 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ) |
155 | 152, 154 | jca 554 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
156 | | ftc1anclem4 33488 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ dom ∫1
∧ (𝑥 ∈ ℝ
↦ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
157 | 156 | 3expb 1266 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ dom ∫1
∧ ((𝑥 ∈ ℝ
↦ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
158 | 155, 157 | sylan2 491 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ dom ∫1
∧ 𝜑) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
159 | 158 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑓‘𝑡))))) ∈ ℝ) |
160 | 134, 159 | syl5eqelr 2706 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ) |
161 | 126 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑡 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
162 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) |
163 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢
(ℑ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V |
164 | 161, 162,
163 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
165 | 164 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡)) = ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) |
166 | 165 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ →
(abs‘(((𝑥 ∈
ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
167 | 166 | mpteq2ia 4740 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℝ ↦
(abs‘(((𝑥 ∈
ℝ ↦ (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
168 | 167 | fveq2i 6194 |
. . . . . . . . . 10
⊢
(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
169 | 151 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1) |
170 | 138 | imcld 13935 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ℑ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ∈ ℝ) |
171 | 170 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) →
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ∈ ℝ) |
172 | 171, 162 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ) |
173 | 169, 172 | jca 554 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
174 | | ftc1anclem4 33488 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ dom ∫1
∧ (𝑥 ∈ ℝ
↦ (ℑ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
175 | 174 | 3expb 1266 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ dom ∫1
∧ ((𝑥 ∈ ℝ
↦ (ℑ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
176 | 173, 175 | sylan2 491 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ dom ∫1
∧ 𝜑) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
177 | 176 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℑ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − (𝑔‘𝑡))))) ∈ ℝ) |
178 | 168, 177 | syl5eqelr 2706 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) |
179 | 160, 178 | anim12dan 882 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ)) |
180 | 1 | rpred 11872 |
. . . . . . . . 9
⊢ (𝑌 ∈ ℝ+
→ (𝑌 / 2) ∈
ℝ) |
181 | 180, 180 | jca 554 |
. . . . . . . 8
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) ∈
ℝ ∧ (𝑌 / 2)
∈ ℝ)) |
182 | | lt2add 10513 |
. . . . . . . 8
⊢
((((∫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 494 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑓 ∈ 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 846 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ 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 13934 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
186 | 185 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
187 | | i1ff 23443 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ 𝑓:ℝ⟶ℝ) |
188 | 187 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℝ) |
189 | 188 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑓‘𝑡) ∈
ℂ) |
190 | | subcl 10280 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑓‘𝑡) ∈ ℂ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
191 | 186, 189,
190 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
192 | 191 | anassrs 680 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
193 | 192 | adantlrr 757 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℂ) |
194 | 94 | imcld 13935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
195 | 194 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
196 | | i1ff 23443 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
197 | 196 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
198 | 197 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℂ) |
199 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) →
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) |
200 | 195, 198,
199 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) |
201 | 200 | anassrs 680 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) |
202 | | mulcl 10020 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
203 | 13, 201, 202 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
204 | 203 | adantlrl 756 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
205 | 193, 204 | addcld 10059 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ ℂ) |
206 | 205 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) |
207 | 206 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈
ℝ*) |
208 | 205 | absge0d 14183 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ 0 ≤ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
209 | | elxrge0 12281 |
. . . . . . . . . . . 12
⊢
((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 698 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ (0[,]+∞)) |
211 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
212 | 210, 211 | fmptd 6385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞)) |
213 | | icossicc 12260 |
. . . . . . . . . . . . 13
⊢
(0[,)+∞) ⊆ (0[,]+∞) |
214 | | ge0addcl 12284 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,)+∞)) |
215 | 213, 214 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (0[,)+∞) ∧
𝑦 ∈ (0[,)+∞))
→ (𝑥 + 𝑦) ∈
(0[,]+∞)) |
216 | 215 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ (𝑥 ∈
(0[,)+∞) ∧ 𝑦
∈ (0[,)+∞))) → (𝑥 + 𝑦) ∈ (0[,]+∞)) |
217 | 192 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ) |
218 | 192 | absge0d 14183 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
219 | | elrege0 12278 |
. . . . . . . . . . . . . 14
⊢
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞) ↔
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ ℝ ∧ 0 ≤
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
220 | 217, 218,
219 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ (0[,)+∞)) |
221 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) |
222 | 220, 221 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞)) |
223 | 222 | adantrr 753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))):ℝ⟶(0[,)+∞)) |
224 | 201 | abscld 14175 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ) |
225 | 201 | absge0d 14183 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
226 | | elrege0 12278 |
. . . . . . . . . . . . . 14
⊢
((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞) ↔
((abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℝ ∧ 0 ≤
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
227 | 224, 225,
226 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ (0[,)+∞)) |
228 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
229 | 227, 228 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞)) |
230 | 229 | adantrl 752 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))):ℝ⟶(0[,)+∞)) |
231 | | reex 10027 |
. . . . . . . . . . . 12
⊢ ℝ
∈ V |
232 | 231 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ℝ ∈ V) |
233 | | inidm 3822 |
. . . . . . . . . . 11
⊢ (ℝ
∩ ℝ) = ℝ |
234 | 216, 223,
230, 232, 232, 233 | off 6912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))):ℝ⟶(0[,]+∞)) |
235 | 193, 204 | abstrid 14195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
236 | 235 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ∀𝑡 ∈
ℝ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ≤
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
237 | | ovexd 6680 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ ((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ V) |
238 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
239 | | fvexd 6203 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ V) |
240 | | fvexd 6203 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) ∈ V) |
241 | | eqidd 2623 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
242 | | absmul 14034 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)) ∈ ℂ) → (abs‘(i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) ·
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
243 | 13, 201, 242 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘(i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = ((abs‘i) ·
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
244 | | absi 14026 |
. . . . . . . . . . . . . . . . . 18
⊢
(abs‘i) = 1 |
245 | 244 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
⊢
((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (1 ·
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
246 | 224 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) ∈ ℂ) |
247 | 246 | mulid2d 10058 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (1
· (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
248 | 245, 247 | syl5eq 2668 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((abs‘i) · (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) |
249 | 243, 248 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) |
250 | 249 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
251 | 250 | adantrl 752 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (𝑡 ∈ ℝ ↦ (abs‘(i
· ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
252 | 232, 239,
240, 241, 251 | offval2 6914 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (𝑡 ∈ ℝ ↦
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) + (abs‘(i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
253 | 232, 206,
237, 238, 252 | ofrfval2 6915 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ 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)) − (𝑔‘𝑡))))))) |
254 | 236, 253 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∘𝑟 ≤
((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) |
255 | | itg2le 23506 |
. . . . . . . . . 10
⊢ (((𝑡 ∈ ℝ ↦
(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)) − (𝑔‘𝑡))))))) |
256 | 212, 234,
254, 255 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ (∫2‘((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
257 | | absf 14077 |
. . . . . . . . . . . . . 14
⊢
abs:ℂ⟶ℝ |
258 | 257 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
abs:ℂ⟶ℝ) |
259 | 258, 192 | cofmpt 6399 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs
∘ (𝑡 ∈ ℝ
↦ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) |
260 | | resubcl 10345 |
. . . . . . . . . . . . . . . 16
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑓‘𝑡) ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ) |
261 | 185, 188,
260 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ) |
262 | 261 | anassrs 680 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ ℝ) |
263 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
264 | 262, 263 | fmptd 6385 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ) |
265 | 135 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ℝ
∈ dom vol) |
266 | | iunin2 4584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) |
267 | | imaiun 6503 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝑓 “ ∪
𝑦 ∈ ran 𝑓{𝑦}) = ∪
𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}) |
268 | | iunid 4575 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑦 ∈ ran 𝑓{𝑦} = ran 𝑓 |
269 | 268 | imaeq2i 5464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝑓 “ ∪
𝑦 ∈ ran 𝑓{𝑦}) = (◡𝑓 “ ran 𝑓) |
270 | 267, 269 | eqtr3i 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦}) = (◡𝑓 “ ran 𝑓) |
271 | 270 | ineq2i 3811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ ∪ 𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) |
272 | 266, 271 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) |
273 | | cnvimass 5485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ dom (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
274 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ V |
275 | 274, 263 | dmmpti 6023 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ dom
(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = ℝ |
276 | 273, 275 | sseqtri 3637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆
ℝ |
277 | | cnvimarndm 5486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡𝑓 “ ran 𝑓) = dom 𝑓 |
278 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:ℝ⟶ℝ →
dom 𝑓 =
ℝ) |
279 | 187, 278 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ dom 𝑓 =
ℝ) |
280 | 277, 279 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ (◡𝑓 “ ran 𝑓) = ℝ) |
281 | 276, 280 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓)) |
282 | | df-ss 3588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
283 | 281, 282 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
284 | 272, 283 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ dom ∫1
→ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
285 | 284 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞))) |
286 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:ℝ⟶ℝ →
ran 𝑓 ⊆
ℝ) |
287 | 187, 286 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ⊆
ℝ) |
288 | 287 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ran
𝑓 ⊆
ℝ) |
289 | 288 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → 𝑦 ∈ ℝ) |
290 | 185 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
291 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ) |
292 | 185, 291 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ) |
293 | 292 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ) |
294 | 290, 293 | 2thd 255 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ↔
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ)) |
295 | | ltaddsub 10502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
296 | 185, 295 | syl3an3 1361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝜑) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
297 | 296 | 3comr 1273 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
298 | 297 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦))) |
299 | 294, 298 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))) |
300 | | readdcl 10019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈ ℝ) |
301 | 300 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈
ℝ*) |
302 | 301 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → (𝑥 + 𝑦) ∈
ℝ*) |
303 | | elioopnf 12267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 + 𝑦) ∈ ℝ* →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
304 | 302, 303 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑥 + 𝑦) < (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
305 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
306 | 305 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ*) |
307 | | elioopnf 12267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℝ*
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))) |
308 | 306, 307 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧ 𝑥 < ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)))) |
309 | 299, 304,
308 | 3bitr4rd 301 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞))) |
310 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑓‘𝑡) = 𝑦 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦)) |
311 | 310 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞))) |
312 | 311 | bibi1d 333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)) ↔
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))) |
313 | 309, 312 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)))) |
314 | 313 | pm5.32rd 672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦))) |
315 | 314 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦))) |
316 | 289, 315 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦))) |
317 | 316 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
318 | 187 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ dom ∫1
→ 𝑓 = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡))) |
319 | 318 | cnveqd 5298 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ dom ∫1
→ ◡𝑓 = ◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡))) |
320 | 319 | imaeq1d 5465 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ dom ∫1
→ (◡𝑓 “ {𝑦}) = (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) |
321 | 320 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
322 | 263 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} |
323 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑦 ∈ V |
324 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) = (𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) |
325 | 324 | mptiniseg 5629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ V → (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
326 | 323, 325 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}) = {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦} |
327 | 322, 326 | ineq12i 3812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
328 | | inrab 3899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
329 | 327, 328 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
330 | 321, 329 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
331 | 330 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (𝑥(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
332 | 320 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
333 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) |
334 | 333 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) = {𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} |
335 | 334, 326 | ineq12i 3812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
336 | | inrab 3899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
337 | 335, 336 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)} |
338 | 332, 337 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
339 | 338 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ((𝑥 + 𝑦)(,)+∞) ∧ (𝑓‘𝑡) = 𝑦)}) |
340 | 317, 331,
339 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦}))) |
341 | 340 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∩ (◡𝑓 “ {𝑦})) = ∪
𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦}))) |
342 | 285, 341 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) = ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦}))) |
343 | | i1frn 23444 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ ran 𝑓 ∈
Fin) |
344 | 343 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ran
𝑓 ∈
Fin) |
345 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
346 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷) |
347 | 346 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷) |
348 | 347 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0) |
349 | 9 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
350 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡)) |
351 | 350 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) |
352 | 349, 351 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
353 | | iblmbf 23534 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹 ∈ 𝐿1
→ 𝐹 ∈
MblFn) |
354 | 8, 353 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐹 ∈ MblFn) |
355 | 352, 354 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn) |
356 | 7, 136, 345, 348, 355 | mbfss 23413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn) |
357 | 94 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
358 | 357 | ismbfcn2 23406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ MblFn ↔ ((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn))) |
359 | 356, 358 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn)) |
360 | 359 | simpld 475 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) |
361 | 185 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
362 | 361, 333 | fmptd 6385 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡),
0))):ℝ⟶ℝ) |
363 | | mbfima 23399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom
vol) |
364 | 360, 362,
363 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom
vol) |
365 | | i1fima 23445 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ (◡𝑓 “ {𝑦}) ∈ dom vol) |
366 | | inmbl 23310 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
367 | 364, 365,
366 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
368 | 367 | ralrimivw 2967 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
369 | | finiunmbl 23312 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝑓 ∈ Fin ∧
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
370 | 344, 368,
369 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
371 | 370 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ ((𝑥 + 𝑦)(,)+∞)) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
372 | 342, 371 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (𝑥(,)+∞)) ∈ dom
vol) |
373 | | iunin2 4584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪
𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) |
374 | 270 | ineq2i 3811 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ ∪
𝑦 ∈ ran 𝑓(◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) |
375 | 373, 374 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) |
376 | | cnvimass 5485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ dom (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) |
377 | 376, 275 | sseqtri 3637 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ ℝ |
378 | 377, 280 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓)) |
379 | | df-ss 3588 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ⊆ (◡𝑓 “ ran 𝑓) ↔ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
380 | 378, 379 | sylib 208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ ran 𝑓)) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
381 | 375, 380 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ dom ∫1
→ ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
382 | 381 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥))) |
383 | 293, 290 | 2thd 255 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ↔
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ)) |
384 | | ltsubadd 10498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
385 | 185, 384 | syl3an1 1359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
386 | 385 | 3expa 1265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
387 | 386 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦))) |
388 | 383, 387 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))) |
389 | | elioomnf 12268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℝ*
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥))) |
390 | 306, 389 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ ℝ ∧
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) < 𝑥))) |
391 | | elioomnf 12268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 + 𝑦) ∈ ℝ* →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))) |
392 | 302, 391 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < (𝑥 + 𝑦)))) |
393 | 388, 390,
392 | 3bitr4d 300 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)))) |
394 | 310 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥))) |
395 | 394 | bibi1d 333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘𝑡) = 𝑦 → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))) ↔ (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − 𝑦) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))) |
396 | 393, 395 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) → ((𝑓‘𝑡) = 𝑦 → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))))) |
397 | 396 | pm5.32rd 672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦))) |
398 | 397 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ℝ) →
((((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦))) |
399 | 289, 398 | syldan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦) ↔ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦))) |
400 | 399 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}) |
401 | 320 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
402 | 263 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} |
403 | 402, 326 | ineq12i 3812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
404 | | inrab 3899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥)} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} |
405 | 403, 404 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)} |
406 | 401, 405 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}) |
407 | 406 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) ∈ (-∞(,)𝑥) ∧ (𝑓‘𝑡) = 𝑦)}) |
408 | 320 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦}))) |
409 | 333 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) = {𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} |
410 | 409, 326 | ineq12i 3812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) |
411 | | inrab 3899 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑡 ∈ ℝ ∣
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦))} ∩ {𝑡 ∈ ℝ ∣ (𝑓‘𝑡) = 𝑦}) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)} |
412 | 410, 411 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡(𝑡 ∈ ℝ ↦ (𝑓‘𝑡)) “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)} |
413 | 408, 412 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ dom ∫1
→ ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}) |
414 | 413 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) = {𝑡 ∈ ℝ ∣
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ (-∞(,)(𝑥 + 𝑦)) ∧ (𝑓‘𝑡) = 𝑦)}) |
415 | 400, 407,
414 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) ∧ 𝑦 ∈ ran 𝑓) → ((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦}))) |
416 | 415 | iuneq2dv 4542 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∩ (◡𝑓 “ {𝑦})) = ∪
𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦}))) |
417 | 382, 416 | eqtr3d 2658 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) = ∪
𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦}))) |
418 | | mbfima 23399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn ∧ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ) → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol) |
419 | 360, 362,
418 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol) |
420 | | inmbl 23310 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∈ dom vol ∧ (◡𝑓 “ {𝑦}) ∈ dom vol) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
421 | 419, 365,
420 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → ((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
422 | 421 | ralrimivw 2967 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
423 | | finiunmbl 23312 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝑓 ∈ Fin ∧
∀𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
424 | 344, 422,
423 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) →
∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
425 | 424 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → ∪ 𝑦 ∈ ran 𝑓((◡(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) “ (-∞(,)(𝑥 + 𝑦))) ∩ (◡𝑓 “ {𝑦})) ∈ dom vol) |
426 | 417, 425 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ 𝑥 ∈ ℝ) → (◡(𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) “ (-∞(,)𝑥)) ∈ dom vol) |
427 | 264, 265,
372, 426 | ismbf2d 23408 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn) |
428 | | ftc1anclem1 33485 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
429 | 264, 427,
428 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (abs
∘ (𝑡 ∈ ℝ
↦ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
430 | 259, 429 | eqeltrrd 2702 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
431 | 430 | adantrr 753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∈ MblFn) |
432 | 160 | adantrr 753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ) |
433 | 178 | adantrl 752 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) |
434 | 431, 223,
432, 230, 433 | itg2addnc 33464 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘((𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
435 | 256, 434 | breqtrd 4679 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
436 | 435 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) |
437 | | itg2cl 23499 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))):ℝ⟶(0[,]+∞) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈
ℝ*) |
438 | 212, 437 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈
ℝ*) |
439 | 438 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) ∈
ℝ*) |
440 | | readdcl 10019 |
. . . . . . . . . . . 12
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) ∈ ℝ) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ) |
441 | 160, 178,
440 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ dom ∫1) ∧ (𝜑 ∧ 𝑔 ∈ dom ∫1)) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ) |
442 | 441 | anandis 873 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈ ℝ) |
443 | 442 | rexrd 10089 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈
ℝ*) |
444 | 443 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) ∈
ℝ*) |
445 | 1, 1 | rpaddcld 11887 |
. . . . . . . . . 10
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) + (𝑌 / 2)) ∈
ℝ+) |
446 | 445 | rpxrd 11873 |
. . . . . . . . 9
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) + (𝑌 / 2)) ∈
ℝ*) |
447 | 446 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((𝑌 / 2) + (𝑌 / 2)) ∈
ℝ*) |
448 | | xrlelttr 11987 |
. . . . . . . 8
⊢
(((∫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)))) |
449 | 439, 444,
447, 448 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ 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)))) |
450 | 436, 449 | mpand 711 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) < ((𝑌 / 2) + (𝑌 / 2)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
451 | 184, 450 | syld 47 |
. . . . 5
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)))) |
452 | | mulcl 10020 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) → (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) |
453 | 13, 195, 452 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) |
454 | 186, 453 | jca 554 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ)) |
455 | | mulcl 10020 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i · (𝑔‘𝑡)) ∈ ℂ) |
456 | 13, 198, 455 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (i · (𝑔‘𝑡)) ∈ ℂ) |
457 | 189, 456 | anim12i 590 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ (𝑔 ∈ dom
∫1 ∧ 𝑡
∈ ℝ)) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) |
458 | 457 | anandirs 874 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) |
459 | | addsub4 10324 |
. . . . . . . . . . . . 13
⊢
((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (i ·
(ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) ∧ ((𝑓‘𝑡) ∈ ℂ ∧ (i · (𝑔‘𝑡)) ∈ ℂ)) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
460 | 454, 458,
459 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ 𝑡 ∈ ℝ))
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
461 | 460 | anassrs 680 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
462 | 94 | replimd 13937 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
463 | 462 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
464 | 463 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + (i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
465 | 198 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1) ∧ 𝑡
∈ ℝ) → (𝑔‘𝑡) ∈ ℂ) |
466 | | subdi 10463 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℂ ∧ (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ (𝑔‘𝑡) ∈ ℂ) → (i ·
((ℑ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))) |
467 | 13, 195, 465, 466 | mp3an3an 1430 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)
∧ 𝑡 ∈ ℝ))
→ (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))) |
468 | 467 | anassrs 680 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))) = ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡)))) |
469 | 468 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + ((i · (ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − (i · (𝑔‘𝑡))))) |
470 | 461, 464,
469 | 3eqtr4rd 2667 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))) = (if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))) |
471 | 470 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
∧ 𝑡 ∈ ℝ)
→ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) = (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))) |
472 | 471 | mpteq2dva 4744 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (𝑡 ∈ ℝ
↦ (abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡)))))) = (𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) |
473 | 472 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1))
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))) |
474 | 473 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡)))))))) |
475 | | rpcn 11841 |
. . . . . . . 8
⊢ (𝑌 ∈ ℝ+
→ 𝑌 ∈
ℂ) |
476 | 475 | 2halvesd 11278 |
. . . . . . 7
⊢ (𝑌 ∈ ℝ+
→ ((𝑌 / 2) + (𝑌 / 2)) = 𝑌) |
477 | 476 | ad2antlr 763 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((𝑌 / 2) + (𝑌 / 2)) = 𝑌) |
478 | 474, 477 | breq12d 4666 |
. . . . 5
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) + (i · ((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))))) < ((𝑌 / 2) + (𝑌 / 2)) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
479 | 451, 478 | sylibd 229 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ (𝑓 ∈ dom ∫1
∧ 𝑔 ∈ dom
∫1)) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
480 | 479 | reximdvva 3019 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
481 | 123, 480 | syl5bir 233 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < (𝑌 / 2) ∧ ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℑ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑔‘𝑡))))) < (𝑌 / 2)) → ∃𝑓 ∈ dom ∫1∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌)) |
482 | 11, 122, 481 | mp2and 715 |
1
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1∃𝑔
∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) − ((𝑓‘𝑡) + (i · (𝑔‘𝑡))))))) < 𝑌) |