Step | Hyp | Ref
| Expression |
1 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ,
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0) =
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
2 | 1 | mpteq2ia 4740 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
3 | 2 | fveq2i 6194 |
. . . . . . 7
⊢
(∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) =
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
4 | | ftc1anc.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
5 | 4 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
6 | | 0cnd 10033 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
7 | 5, 6 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
8 | 7 | recld 13934 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
9 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
10 | | ftc1anc.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
11 | | rembl 23308 |
. . . . . . . . . . . 12
⊢ ℝ
∈ dom vol |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ℝ ∈ dom
vol) |
13 | 8 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
14 | | eldifn 3733 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷) |
15 | 14 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷) |
16 | | iffalse 4095 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0) |
17 | 16 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (¬
𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘0)) |
18 | | re0 13892 |
. . . . . . . . . . . . 13
⊢
(ℜ‘0) = 0 |
19 | 17, 18 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (¬
𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0) |
20 | 15, 19 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0) |
21 | | iftrue 4092 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡)) |
22 | 21 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(𝐹‘𝑡))) |
23 | 22 | mpteq2ia 4740 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) |
24 | 4 | feqmptd 6249 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
25 | | ftc1anc.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
26 | 24, 25 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
27 | 5 | iblcn 23565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1))) |
28 | 26, 27 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1)) |
29 | 28 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈
𝐿1) |
30 | 23, 29 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
𝐿1) |
31 | 10, 12, 13, 20, 30 | iblss2 23572 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈
𝐿1) |
32 | 8 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
33 | 32 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
34 | | eqidd 2623 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
35 | | absf 14077 |
. . . . . . . . . . . . . 14
⊢
abs:ℂ⟶ℝ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
37 | 36 | feqmptd 6249 |
. . . . . . . . . . . 12
⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥))) |
38 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
39 | 33, 34, 37, 38 | fmptco 6396 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
40 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) |
41 | 9, 40 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡),
0))):ℝ⟶ℝ) |
42 | | iblmbf 23534 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ 𝐿1
→ 𝐹 ∈
MblFn) |
43 | 25, 42 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ MblFn) |
44 | 24, 43 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn) |
45 | 5 | ismbfcn2 23406 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))) |
46 | 44, 45 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)) |
47 | 46 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn) |
48 | 23, 47 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) |
49 | 10, 12, 13, 20, 48 | mbfss 23413 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) |
50 | | ftc1anclem1 33485 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) → (abs ∘
(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn) |
51 | 41, 49, 50 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn) |
52 | 39, 51 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn) |
53 | 9, 31, 52 | iblabsnc 33474 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈
𝐿1) |
54 | 32 | abscld 14175 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ) |
55 | 54 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ) |
56 | 32 | absge0d 14183 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
57 | 56 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
58 | 55, 57 | iblpos 23559 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1 ↔
((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈
ℝ))) |
59 | 53, 58 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈
ℝ)) |
60 | 59 | simprd 479 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈
ℝ) |
61 | 3, 60 | syl5eqelr 2706 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ) |
62 | | ltsubrp 11866 |
. . . . . 6
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+)
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))) |
63 | 61, 62 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))) |
64 | | rpre 11839 |
. . . . . . 7
⊢ (𝑌 ∈ ℝ+
→ 𝑌 ∈
ℝ) |
65 | | resubcl 10345 |
. . . . . . 7
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ) |
66 | 61, 64, 65 | syl2an 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ) |
67 | 61 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ) |
68 | 66, 67 | ltnled 10184 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ↔ ¬
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
69 | 63, 68 | mpbid 222 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) |
70 | 54 | rexrd 10089 |
. . . . . . . . 9
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
ℝ*) |
71 | | elxrge0 12281 |
. . . . . . . . 9
⊢
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞) ↔
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ* ∧ 0
≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
72 | 70, 56, 71 | sylanbrc 698 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
(0[,]+∞)) |
73 | 72 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
(0[,]+∞)) |
74 | | eqid 2622 |
. . . . . . 7
⊢ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
75 | 73, 74 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡),
0)))):ℝ⟶(0[,]+∞)) |
76 | 75 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡),
0)))):ℝ⟶(0[,]+∞)) |
77 | 66 | rexrd 10089 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈
ℝ*) |
78 | | itg2leub 23501 |
. . . . 5
⊢ (((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞) ∧
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))) |
79 | 76, 77, 78 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))) |
80 | 69, 79 | mtbid 314 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬
∀𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
81 | | rexanali 2998 |
. . 3
⊢
(∃𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) ↔ ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
82 | 80, 81 | sylibr 224 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
83 | 66 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ) |
84 | | itg1cl 23452 |
. . . . . . . . 9
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ∈ ℝ) |
85 | 84 | ad2antlr 763 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ∈
ℝ) |
86 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
87 | 86 | i1fpos 23473 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom
∫1) |
88 | | 0re 10040 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
89 | | i1ff 23443 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
90 | 89 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
91 | | max1 12016 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → 0 ≤ if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0)) |
92 | 88, 90, 91 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
93 | 92 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ ∀𝑡 ∈
ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
94 | | ax-resscn 9993 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ ℝ ⊆ ℂ) |
96 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔‘𝑡) ∈ V |
97 | | c0ex 10034 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
98 | 96, 97 | ifex 4156 |
. . . . . . . . . . . . . . . 16
⊢ if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V |
99 | 98, 86 | fnmpti 6022 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ |
100 | 99 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ) |
101 | 95, 100 | 0pledm 23440 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ (0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ (ℝ × {0})
∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
102 | | reex 10027 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ ℝ ∈ V) |
104 | 97 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ∈ V) |
105 | | ifcl 4130 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔‘𝑡) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) |
106 | 90, 88, 105 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) |
107 | | fconstmpt 5163 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
× {0}) = (𝑡 ∈
ℝ ↦ 0) |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)) |
109 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
110 | 103, 104,
106, 108, 109 | ofrfval2 6915 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ ((ℝ × {0}) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
111 | 101, 110 | bitrd 268 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ (0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
112 | 93, 111 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ dom ∫1
→ 0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
113 | | itg2itg1 23503 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
0𝑝 ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
114 | 87, 112, 113 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
115 | | itg1cl 23452 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
(∫1‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
116 | 87, 115 | syl 17 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
117 | 114, 116 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (𝑔 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
118 | 117 | ad2antlr 763 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
119 | | ltnle 10117 |
. . . . . . . . . 10
⊢
((((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ ∧
(∫1‘𝑔)
∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
120 | 66, 84, 119 | syl2an 494 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
121 | 120 | biimpar 502 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔)) |
122 | | max2 12018 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
123 | 88, 90, 122 | sylancr 695 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
124 | 123 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ ∀𝑡 ∈
ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
125 | 89 | feqmptd 6249 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡))) |
126 | 103, 90, 106, 125, 109 | ofrfval2 6915 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ (𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
127 | 124, 126 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ dom ∫1
→ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
128 | | itg1le 23480 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ dom ∫1
∧ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫1‘𝑔) ≤
(∫1‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
129 | 87, 127, 128 | mpd3an23 1426 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
130 | 129, 114 | breqtrrd 4681 |
. . . . . . . . 9
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
131 | 130 | ad2antlr 763 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
132 | 83, 85, 118, 121, 131 | ltletrd 10197 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
133 | 132 | adantrl 752 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ (𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
134 | | i1fmbf 23442 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
(𝑡 ∈ ℝ ↦
if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn) |
135 | 87, 134 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn) |
136 | 135 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn) |
137 | | elrege0 12278 |
. . . . . . . . . . . . . . . . 17
⊢ (if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0))) |
138 | 106, 92, 137 | sylanbrc 698 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞)) |
139 | 138, 86 | fmptd 6385 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡),
0)):ℝ⟶(0[,)+∞)) |
140 | 139 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡),
0)):ℝ⟶(0[,)+∞)) |
141 | 117 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
142 | 106 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) |
143 | 142 | negcld 10379 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) |
144 | 142, 143 | ifcld 4131 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ) |
145 | | subcl 10280 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ) |
146 | 32, 144, 145 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ) |
147 | 146 | anassrs 680 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ) |
148 | 147 | abscld 14175 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ) |
149 | 147 | absge0d 14183 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
150 | | elrege0 12278 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ (0[,)+∞) ↔
((abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ ∧ 0 ≤
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) |
151 | 148, 149,
150 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈
(0[,)+∞)) |
152 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
153 | 151, 152 | fmptd 6385 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡),
0))))):ℝ⟶(0[,)+∞)) |
154 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷)) |
155 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡)) |
156 | 154, 155 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
157 | 156 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
158 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) |
159 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V |
160 | 157, 158,
159 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
161 | 157 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
162 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡)) |
163 | 162 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑡 → (0 ≤ (𝑔‘𝑥) ↔ 0 ≤ (𝑔‘𝑡))) |
164 | 163, 162 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
165 | 164 | negeqd 10275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
166 | 161, 164,
165 | ifbieq12d 4113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
167 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
168 | | negex 10279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ -if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V |
169 | 98, 168 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ V |
170 | 166, 167,
169 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
171 | 160, 170 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ ℝ → (((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
172 | 171 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 ∈ ℝ →
(abs‘(((𝑥 ∈
ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
173 | 172 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ℝ ↦
(abs‘(((𝑥 ∈
ℝ ↦ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
174 | 173 | fveq2i 6194 |
. . . . . . . . . . . . . . 15
⊢
(∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) |
175 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ℝ ∈
V) |
176 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔‘𝑥) ∈ V |
177 | 176, 97 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ V |
178 | 177, 97 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V |
179 | 178 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V) |
180 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) ∈ V |
181 | 97, 180 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V |
182 | 181 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V) |
183 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷) |
184 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ) |
185 | | ref 13852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
ℜ:ℂ⟶ℝ |
186 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(ℜ:ℂ⟶ℝ → ℜ Fn
ℂ) |
187 | 185, 186 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ℜ Fn
ℂ |
188 | | fnco 5999 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ℜ
Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘
𝐹) Fn 𝐷) |
189 | 187, 188 | mp3an1 1411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘
𝐹) Fn 𝐷) |
190 | 183, 184,
189 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷) |
191 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℜ
∘ 𝐹) Fn 𝐷 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))) |
192 | 4, 190, 191 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))) |
193 | | fco 6058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘
𝐹):𝐷⟶ℝ) |
194 | 185, 4, 193 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ) |
195 | 194 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ) |
196 | 195 | biantrurd 529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ
∘ 𝐹)‘𝑥)))) |
197 | | elrege0 12278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((ℜ
∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔
(((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ
∘ 𝐹)‘𝑥))) |
198 | 196, 197 | syl6bbr 278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))) |
199 | | fvco3 6275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹:𝐷⟶ℂ ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥))) |
200 | 4, 199 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥))) |
201 | 200 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥)))) |
202 | 198, 201 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤
(ℜ‘(𝐹‘𝑥)))) |
203 | 202 | pm5.32da 673 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))))) |
204 | 192, 203 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))))) |
205 | 204 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))))) |
206 | | 0le0 11110 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ≤
0 |
207 | 206, 18 | breqtrri 4680 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤
(ℜ‘0) |
208 | 207 | biantru 526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑥 ∈ 𝐷 ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0))) |
209 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐷)) |
210 | 209 | baibr 945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℝ → (¬
𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ 𝐷))) |
211 | 208, 210 | syl5rbbr 275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0)))) |
212 | 211 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0)))) |
213 | 205, 212 | orbi12d 746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0))))) |
214 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ↔ (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷))) |
215 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘(𝐹‘𝑥))) |
216 | 215 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥)))) |
217 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘0)) |
218 | 217 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤
(ℜ‘0))) |
219 | 216, 218 | elimif 4122 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0)))) |
220 | 213, 214,
219 | 3bitr4g 303 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ↔ 0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))) |
221 | 220 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) |
222 | 221 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0))) |
223 | 220 | ifbid 4108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) |
224 | 223 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) |
225 | 175, 179,
182, 222, 224 | offval2 6914 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 +
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ (if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))))) |
226 | | ovif12 6739 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0), (0 + (-1 · if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0)))) |
227 | 89 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑔‘𝑥) ∈
ℝ) |
228 | 227 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑔‘𝑥) ∈
ℂ) |
229 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℂ |
230 | | ifcl 4130 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ)
→ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ) |
231 | 228, 229,
230 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ) |
232 | 231 | addid1d 10236 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
233 | 231 | mulm1d 10482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
234 | 233 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
235 | 231 | negcld 10379 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ) |
236 | 235 | addid2d 10237 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
237 | 234, 236 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
238 | 232, 237 | ifeq12d 4106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0), (0 + (-1 · if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0)))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
239 | 226, 238 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
240 | 239 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∈ dom ∫1
→ (𝑥 ∈ ℝ
↦ (if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) |
241 | 225, 240 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 +
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) |
242 | | 0xr 10086 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ* |
243 | | pnfxr 10092 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ +∞
∈ ℝ* |
244 | | 0ltpnf 11956 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
+∞ |
245 | | snunioo 12298 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
< +∞) → ({0} ∪ (0(,)+∞)) =
(0[,)+∞)) |
246 | 242, 243,
244, 245 | mp3an 1424 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({0}
∪ (0(,)+∞)) = (0[,)+∞) |
247 | 246 | imaeq2i 5464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) =
(◡(ℜ ∘ 𝐹) “ (0[,)+∞)) |
248 | | imaundi 5545 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) =
((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) |
249 | 247, 248 | eqtr3i 2646 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) |
250 | | ismbfcn 23398 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn))) |
251 | 4, 250 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn))) |
252 | 43, 251 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn)) |
253 | 252 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn) |
254 | | mbfimasn 23401 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ)
→ (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom
vol) |
255 | 88, 254 | mp3an3 1413 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom
vol) |
256 | | mbfima 23399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom
vol) |
257 | | unmbl 23305 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
→ ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom
vol) |
258 | 255, 256,
257 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom
vol) |
259 | 253, 194,
258 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom
vol) |
260 | 249, 259 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom
vol) |
261 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝐷⟶ℂ → dom 𝐹 = 𝐷) |
262 | 4, 261 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom 𝐹 = 𝐷) |
263 | | mbfdm 23395 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
264 | 43, 263 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
265 | 262, 264 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∈ dom vol) |
266 | | difmbl 23311 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℝ
∈ dom vol ∧ 𝐷
∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol) |
267 | 11, 265, 266 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℝ ∖ 𝐷) ∈ dom
vol) |
268 | | unmbl 23305 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol
∧ (ℝ ∖ 𝐷)
∈ dom vol) → ((◡(ℜ
∘ 𝐹) “
(0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) |
269 | 260, 267,
268 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom
vol) |
270 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑥 → (𝑔‘𝑡) = (𝑔‘𝑥)) |
271 | 270 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑥 → (0 ≤ (𝑔‘𝑡) ↔ 0 ≤ (𝑔‘𝑥))) |
272 | 271, 270 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑥 → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
273 | 272, 86, 177 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
274 | 273 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥)) |
275 | 274 | ifeq1d 4104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0)) |
276 | 275 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0)) |
277 | 276 | i1fres 23472 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∈ dom
∫1) |
278 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
(𝑡 ∈ ℝ ↦
if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom
∫1) |
279 | | neg1rr 11125 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ -1 ∈
ℝ |
280 | 279 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → -1
∈ ℝ) |
281 | 278, 280 | i1fmulc 23470 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom
∫1) |
282 | | cmmbl 23302 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol
→ (ℝ ∖ ((◡(ℜ
∘ 𝐹) “
(0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol) |
283 | | ifnot 4133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), (-1 ·
if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
284 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)))) |
285 | 284 | baibr 945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ → (¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))))) |
286 | | tru 1487 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
⊤ |
287 | | negex 10279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ -1 ∈
V |
288 | 287 | fconst 6091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℝ
× {-1}):ℝ⟶{-1} |
289 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ℝ
× {-1}):ℝ⟶{-1} → (ℝ × {-1}) Fn
ℝ) |
290 | 288, 289 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (⊤
→ (ℝ × {-1}) Fn ℝ) |
291 | 99 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (⊤
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ) |
292 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (⊤
→ ℝ ∈ V) |
293 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℝ
∩ ℝ) = ℝ |
294 | 287 | fvconst2 6469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ ℝ → ((ℝ
× {-1})‘𝑥) =
-1) |
295 | 294 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((⊤ ∧ 𝑥
∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1) |
296 | 273 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((⊤ ∧ 𝑥
∈ ℝ) → ((𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
297 | 290, 291,
292, 292, 293, 295, 296 | ofval 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (((ℝ × {-1}) ∘𝑓
· (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
298 | 286, 297 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℝ →
(((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
299 | 298 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ → (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = (((ℝ × {-1})
∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥)) |
300 | 285, 299 | ifbieq1d 4109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → if(¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), (-1 ·
if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))), (((ℝ
× {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0)) |
301 | 283, 300 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))), (((ℝ
× {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0)) |
302 | 301 | mpteq2ia 4740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))), (((ℝ
× {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0)) |
303 | 302 | i1fres 23472 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1 ∧
(ℝ ∖ ((◡(ℜ ∘
𝐹) “ (0[,)+∞))
∪ (ℝ ∖ 𝐷)))
∈ dom vol) → (𝑥
∈ ℝ ↦ if(𝑥
∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪
(ℝ ∖ 𝐷)), 0,
(-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom
∫1) |
304 | 281, 282,
303 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom
∫1) |
305 | 277, 304 | i1fadd 23462 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol)
→ ((𝑥 ∈ ℝ
↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 +
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom
∫1) |
306 | 87, 269, 305 | syl2anr 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘𝑓 +
(𝑥 ∈ ℝ ↦
if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom
∫1) |
307 | 241, 306 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom
∫1) |
308 | 157 | cbvmptv 4750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) |
309 | 308, 31 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1) |
310 | 9, 308 | fmptd 6385 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ) |
311 | 309, 310 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
312 | 311 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
313 | | ftc1anclem4 33488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ) |
314 | 313 | 3expb 1266 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 ∧
((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))):ℝ⟶ℝ)) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ) |
315 | 307, 312,
314 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ) |
316 | 174, 315 | syl5eqelr 2706 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ) |
317 | 136, 140,
141, 153, 316 | itg2addnc 33464 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) =
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))))) |
318 | 102 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ℝ
∈ V) |
319 | 98 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V) |
320 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
321 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) |
322 | 318, 319,
148, 320, 321 | offval2 6914 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) = (𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) |
323 | 322 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘𝑓 + (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))))) |
324 | 317, 323 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))))) |
325 | 324 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦ (if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))))) |
326 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(𝜑 ∧ 𝑔 ∈ dom
∫1) |
327 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑔 |
328 | | nfcv 2764 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡
∘𝑟 ≤ |
329 | | nfmpt1 4747 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
330 | 327, 328,
329 | nfbr 4699 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
331 | 326, 330 | nfan 1828 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
332 | | anass 681 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈
ℝ))) |
333 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔:ℝ⟶ℝ →
𝑔 Fn
ℝ) |
334 | 89, 333 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 Fn
ℝ) |
335 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V |
336 | 335, 74 | fnmpti 6022 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ |
337 | 336 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ) |
338 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) = (𝑔‘𝑡)) |
339 | 74 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
340 | 335, 339 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
341 | 340 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ ((𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
342 | 334, 337,
103, 103, 293, 338, 341 | ofrval 6907 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
343 | 342 | 3com23 1271 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ
∧ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
344 | 343 | 3expa 1265 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
345 | 344 | adantll 750 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
346 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
347 | 8, 106, 346 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
348 | 347 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
349 | | absid 14036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
350 | 8, 349 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
351 | 350 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
352 | 351 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
353 | 352 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
354 | 353 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
355 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
356 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
357 | 355, 356 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
358 | 354, 357 | sylancom 701 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
359 | | subge0 10541 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (0 ≤
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
360 | 8, 106, 359 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (0 ≤
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
361 | 360 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (0 ≤
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
362 | 358, 361 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
363 | 348, 362 | absidd 14161 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
364 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
365 | 364 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
366 | 365 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
367 | 366 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
368 | 8 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
369 | 349 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
370 | 368, 369 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
371 | 363, 367,
370 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
372 | 106 | renegcld 10457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) |
373 | | resubcl 10345 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
374 | 8, 372, 373 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
375 | 374 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
376 | 90 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ∈ ℝ) |
377 | 8 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
378 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
379 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
380 | 88, 379 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
381 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
382 | 88, 381 | mpan2 707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
383 | 380, 382 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → (¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
384 | 383 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) |
385 | | absnid 14038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ≤ 0) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
386 | 384, 385 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
387 | 386 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
388 | 387 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
389 | 388 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
390 | 378, 389 | sylanl1 682 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
391 | 376, 377,
390 | lenegcon2d 10610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡)) |
392 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → 𝜑) |
393 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 0 ∈
ℝ) |
394 | 8, 393 | ltnled 10184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
395 | 8, 88, 381 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
396 | 394, 395 | sylbird 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
397 | 396 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) |
398 | 392, 397 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) |
399 | | negeq 10273 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -(𝑔‘𝑡) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
400 | 399 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
401 | | neg0 10327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ -0 =
0 |
402 | | negeq 10273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
403 | 401, 402 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → 0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
404 | 403 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
405 | 400, 404 | ifboth 4124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
406 | 391, 398,
405 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
407 | | suble0 10542 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
408 | 8, 372, 407 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
409 | 408 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
410 | 406, 409 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0) |
411 | 375, 410 | absnidd 14152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
412 | | subneg 10330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
413 | 412 | negeqd 10275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
414 | | negdi2 10339 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
415 | 413, 414 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
416 | 32, 142, 415 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
417 | 416 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
418 | 411, 417 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
419 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬ 0
≤ (ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
420 | 419 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬ 0
≤ (ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
421 | 420 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬ 0
≤ (ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
422 | 421 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
423 | 8, 385 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
424 | 397, 423 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
425 | 424 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
426 | 392, 425 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
427 | 418, 422,
426 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
428 | 371, 427 | pm2.61dan 832 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
429 | 428 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
430 | 54 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) |
431 | | pncan3 10289 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ ∧
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) → (if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
432 | 142, 430,
431 | syl2anr 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
433 | 432 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
434 | 429, 433 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
435 | 345, 434 | syldan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
436 | 332, 435 | sylanb 489 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
437 | 436 | an32s 846 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∧ 𝑡 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
438 | 331, 437 | mpteq2da 4743 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
439 | 438 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
(∫2‘(𝑡
∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))) |
440 | 325, 439 | eqtrd 2656 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))) |
441 | 440 | breq1d 4663 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘𝑟
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
(((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌) ↔ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
442 | 441 | adantllr 755 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
(((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌) ↔ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
443 | 316 | adantlr 751 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ) |
444 | 64 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ 𝑌 ∈
ℝ) |
445 | 117 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
446 | 443, 444,
445 | ltadd2d 10193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
447 | 446 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
448 | | ltsubadd 10498 |
. . . . . . . . . . 11
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ ∧
(∫2‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) →
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
449 | 61, 64, 117, 448 | syl3an 1368 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+ ∧ 𝑔 ∈ dom ∫1)
→ (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
450 | 449 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
451 | 450 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
452 | 442, 447,
451 | 3bitr4d 300 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
453 | 452 | adantrr 753 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ (𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 ↔ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
454 | 133, 453 | mpbird 247 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ (𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌) |
455 | 454 | ex 450 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ ((𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌)) |
456 | 455 | reximdva 3017 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌)) |
457 | | fveq1 6190 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → (𝑓‘𝑡) = ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡)) |
458 | 457, 170 | sylan9eq 2676 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
459 | 458 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
460 | 459 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
461 | 460 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡)))) = (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) |
462 | 461 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) |
463 | 462 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌 ↔ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌)) |
464 | 463 | rspcev 3309 |
. . . . . . 7
⊢ (((𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 ∧
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌) → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌) |
465 | 464 | ex 450 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom ∫1 →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)) |
466 | 307, 465 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)) |
467 | 466 | rexlimdva 3031 |
. . . 4
⊢ (𝜑 → (∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)) |
468 | 467 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)) |
469 | 456, 468 | syld 47 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑔 ∈ dom
∫1(𝑔
∘𝑟 ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)) |
470 | 82, 469 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌) |