Step | Hyp | Ref
| Expression |
1 | | iftrue 4471 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ,
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0) =
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
2 | 1 | mpteq2ia 5182 |
. . . . . . . 8
⊢ (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
3 | 2 | fveq2i 6774 |
. . . . . . 7
⊢
(∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ,
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) =
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
4 | | ftc1anc.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
5 | 4 | ffvelrnda 6958 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝐹‘𝑡) ∈ ℂ) |
6 | | 0cnd 10969 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑡 ∈ 𝐷) → 0 ∈ ℂ) |
7 | 5, 6 | ifclda 4500 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) ∈ ℂ) |
8 | 7 | recld 14903 |
. . . . . . . . . . 11
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
9 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
10 | | ftc1anc.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
11 | | rembl 24702 |
. . . . . . . . . . . 12
⊢ ℝ
∈ dom vol |
12 | 11 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ℝ ∈ dom
vol) |
13 | 8 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
14 | | eldifn 4067 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡 ∈ 𝐷) |
15 | 14 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡 ∈ 𝐷) |
16 | | iffalse 4474 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = 0) |
17 | 16 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ (¬
𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘0)) |
18 | | re0 14861 |
. . . . . . . . . . . . 13
⊢
(ℜ‘0) = 0 |
19 | 17, 18 | eqtrdi 2796 |
. . . . . . . . . . . 12
⊢ (¬
𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0) |
20 | 15, 19 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = 0) |
21 | | iftrue 4471 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝐷 → if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0) = (𝐹‘𝑡)) |
22 | 21 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝐷 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) = (ℜ‘(𝐹‘𝑡))) |
23 | 22 | mpteq2ia 5182 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) |
24 | 4 | feqmptd 6834 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡))) |
25 | | ftc1anc.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 ∈
𝐿1) |
26 | 24, 25 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈
𝐿1) |
27 | 5 | iblcn 24961 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ 𝐿1 ↔
((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1))) |
28 | 26, 27 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ 𝐿1 ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈
𝐿1)) |
29 | 28 | simpld 495 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈
𝐿1) |
30 | 23, 29 | eqeltrid 2845 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
𝐿1) |
31 | 10, 12, 13, 20, 30 | iblss2 24968 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈
𝐿1) |
32 | 8 | recnd 11004 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
33 | 32 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℂ) |
34 | | eqidd 2741 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) = (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
35 | | absf 15047 |
. . . . . . . . . . . . . 14
⊢
abs:ℂ⟶ℝ |
36 | 35 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
abs:ℂ⟶ℝ) |
37 | 36 | feqmptd 6834 |
. . . . . . . . . . . 12
⊢ (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥))) |
38 | | fveq2 6771 |
. . . . . . . . . . . 12
⊢ (𝑥 = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
39 | 33, 34, 37, 38 | fmptco 6998 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
40 | 9 | fmpttd 6986 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡),
0))):ℝ⟶ℝ) |
41 | | iblmbf 24930 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ 𝐿1
→ 𝐹 ∈
MblFn) |
42 | 25, 41 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ MblFn) |
43 | 24, 42 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn) |
44 | 5 | ismbfcn2 24800 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (𝐹‘𝑡)) ∈ MblFn ↔ ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn))) |
45 | 43, 44 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn ∧ (𝑡 ∈ 𝐷 ↦ (ℑ‘(𝐹‘𝑡))) ∈ MblFn)) |
46 | 45 | simpld 495 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘(𝐹‘𝑡))) ∈ MblFn) |
47 | 23, 46 | eqeltrid 2845 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑡 ∈ 𝐷 ↦ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) |
48 | 10, 12, 13, 20, 47 | mbfss 24808 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) |
49 | | ftc1anclem1 35846 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∈ MblFn) → (abs ∘
(𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn) |
50 | 40, 48, 49 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn) |
51 | 39, 50 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn) |
52 | 9, 31, 51 | iblabsnc 35837 |
. . . . . . . . 9
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈
𝐿1) |
53 | 32 | abscld 15146 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ) |
54 | 53 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ) |
55 | 32 | absge0d 15154 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
56 | 55 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
57 | 54, 56 | iblpos 24955 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ 𝐿1 ↔
((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈
ℝ))) |
58 | 52, 57 | mpbid 231 |
. . . . . . . 8
⊢ (𝜑 → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∈ MblFn ∧
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈
ℝ)) |
59 | 58 | simprd 496 |
. . . . . . 7
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ if(𝑡
∈ ℝ, (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))), 0))) ∈
ℝ) |
60 | 3, 59 | eqeltrrid 2846 |
. . . . . 6
⊢ (𝜑 →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ) |
61 | | ltsubrp 12765 |
. . . . . 6
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+)
→ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))) |
62 | 60, 61 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))) |
63 | | rpre 12737 |
. . . . . . 7
⊢ (𝑌 ∈ ℝ+
→ 𝑌 ∈
ℝ) |
64 | | resubcl 11285 |
. . . . . . 7
⊢
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ) |
65 | 60, 63, 64 | syl2an 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ) |
66 | 60 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∈ ℝ) |
67 | 65, 66 | ltnled 11122 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ↔ ¬
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
68 | 62, 67 | mpbid 231 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) |
69 | 53 | rexrd 11026 |
. . . . . . . . 9
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
ℝ*) |
70 | | elxrge0 13188 |
. . . . . . . . 9
⊢
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ (0[,]+∞) ↔
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℝ* ∧ 0
≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
71 | 69, 55, 70 | sylanbrc 583 |
. . . . . . . 8
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
(0[,]+∞)) |
72 | 71 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈
(0[,]+∞)) |
73 | 72 | fmpttd 6986 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡),
0)))):ℝ⟶(0[,]+∞)) |
74 | 73 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡),
0)))):ℝ⟶(0[,]+∞)) |
75 | 65 | rexrd 11026 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈
ℝ*) |
76 | | itg2leub 24897 |
. . . . 5
⊢ (((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))):ℝ⟶(0[,]+∞) ∧
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ*) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))) |
77 | 74, 75, 76 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ≤
((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)))) |
78 | 68, 77 | mtbid 324 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) → ¬
∀𝑔 ∈ dom
∫1(𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
79 | | rexanali 3194 |
. . 3
⊢
(∃𝑔 ∈ dom
∫1(𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) ↔ ¬ ∀𝑔 ∈ dom ∫1(𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) →
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
80 | 78, 79 | sylibr 233 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑔 ∈ dom
∫1(𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
81 | 65 | ad2antrr 723 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ) |
82 | | itg1cl 24847 |
. . . . . . . . 9
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ∈ ℝ) |
83 | 82 | ad2antlr 724 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ∈
ℝ) |
84 | | eqid 2740 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
85 | 84 | i1fpos 24869 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom
∫1) |
86 | | 0re 10978 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ |
87 | | i1ff 24838 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ dom ∫1
→ 𝑔:ℝ⟶ℝ) |
88 | 87 | ffvelrnda 6958 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ∈
ℝ) |
89 | | max1 12918 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → 0 ≤ if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0)) |
90 | 86, 88, 89 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
91 | 90 | ralrimiva 3110 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ ∀𝑡 ∈
ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
92 | | ax-resscn 10929 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ ℝ ⊆ ℂ) |
94 | | fvex 6784 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔‘𝑡) ∈ V |
95 | | c0ex 10970 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
96 | 94, 95 | ifex 4515 |
. . . . . . . . . . . . . . . 16
⊢ if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V |
97 | 96, 84 | fnmpti 6574 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ) |
99 | 93, 98 | 0pledm 24835 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ (ℝ × {0})
∘r ≤ (𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
100 | | reex 10963 |
. . . . . . . . . . . . . . 15
⊢ ℝ
∈ V |
101 | 100 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ ℝ ∈ V) |
102 | 95 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ 0 ∈ V) |
103 | | ifcl 4510 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔‘𝑡) ∈ ℝ ∧ 0 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) |
104 | 88, 86, 103 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) |
105 | | fconstmpt 5650 |
. . . . . . . . . . . . . . 15
⊢ (ℝ
× {0}) = (𝑡 ∈
ℝ ↦ 0) |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)) |
107 | | eqidd 2741 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
108 | 101, 102,
104, 106, 107 | ofrfval2 7548 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ ((ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
109 | 99, 108 | bitrd 278 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ (0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
110 | 91, 109 | mpbird 256 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ dom ∫1
→ 0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
111 | | itg2itg1 24899 |
. . . . . . . . . . 11
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
0𝑝 ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) →
(∫2‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
112 | 85, 110, 111 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
113 | | itg1cl 24847 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
(∫1‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
114 | 85, 113 | syl 17 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
115 | 112, 114 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (𝑔 ∈ dom ∫1
→ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
116 | 115 | ad2antlr 724 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
117 | | ltnle 11055 |
. . . . . . . . . 10
⊢
((((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) ∈ ℝ ∧
(∫1‘𝑔)
∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
118 | 65, 82, 117 | syl2an 596 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔) ↔ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) |
119 | 118 | biimpar 478 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫1‘𝑔)) |
120 | | max2 12920 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ (𝑔‘𝑡) ∈ ℝ) → (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
121 | 86, 88, 120 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
122 | 121 | ralrimiva 3110 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ ∀𝑡 ∈
ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
123 | 87 | feqmptd 6834 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 = (𝑡 ∈ ℝ ↦ (𝑔‘𝑡))) |
124 | 101, 88, 104, 123, 107 | ofrfval2 7548 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ dom ∫1
→ (𝑔
∘r ≤ (𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔‘𝑡) ≤ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
125 | 122, 124 | mpbird 256 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ dom ∫1
→ 𝑔
∘r ≤ (𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
126 | | itg1le 24876 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ dom ∫1
∧ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
𝑔 ∘r ≤
(𝑡 ∈ ℝ ↦
if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) → (∫1‘𝑔) ≤
(∫1‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
127 | 85, 125, 126 | mpd3an23 1462 |
. . . . . . . . . 10
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
128 | 127, 112 | breqtrrd 5107 |
. . . . . . . . 9
⊢ (𝑔 ∈ dom ∫1
→ (∫1‘𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
129 | 128 | ad2antlr 724 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫1‘𝑔) ≤
(∫2‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
130 | 81, 83, 116, 119, 129 | ltletrd 11135 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ ¬ (∫1‘𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
131 | 130 | adantrl 713 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ (𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
132 | | i1fmbf 24837 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
(𝑡 ∈ ℝ ↦
if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn) |
133 | 85, 132 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn) |
134 | 133 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ MblFn) |
135 | | elrege0 13185 |
. . . . . . . . . . . . . . . . 17
⊢ (if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0))) |
136 | 104, 90, 135 | sylanbrc 583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ (0[,)+∞)) |
137 | 136 | fmpttd 6986 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡),
0)):ℝ⟶(0[,)+∞)) |
138 | 137 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡),
0)):ℝ⟶(0[,)+∞)) |
139 | 115 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
140 | 104 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) |
141 | 140 | negcld 11319 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) |
142 | 140, 141 | ifcld 4511 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℂ) |
143 | | subcl 11220 |
. . . . . . . . . . . . . . . . . . 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))) ∈ ℂ) |
144 | 32, 142, 143 | syl2an 596 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ) |
145 | 144 | anassrs 468 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℂ) |
146 | 145 | abscld 15146 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈ ℝ) |
147 | 145 | absge0d 15154 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) |
148 | | elrege0 13185 |
. . . . . . . . . . . . . . . 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)))))) |
149 | 146, 147,
148 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) ∈
(0[,)+∞)) |
150 | 149 | fmpttd 6986 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡),
0))))):ℝ⟶(0[,)+∞)) |
151 | | eleq1w 2823 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑡 → (𝑥 ∈ 𝐷 ↔ 𝑡 ∈ 𝐷)) |
152 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑡 → (𝐹‘𝑥) = (𝐹‘𝑡)) |
153 | 151, 152 | ifbieq1d 4489 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) |
154 | 153 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑡 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
155 | | eqid 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) |
156 | | fvex 6784 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ V |
157 | 154, 155,
156 | fvmpt 6872 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
158 | 154 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
159 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡)) |
160 | 159 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑡 → (0 ≤ (𝑔‘𝑥) ↔ 0 ≤ (𝑔‘𝑡))) |
161 | 160, 159 | ifbieq1d 4489 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
162 | 161 | negeqd 11215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑡 → -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
163 | 158, 161,
162 | ifbieq12d 4493 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
164 | | eqid 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
165 | | negex 11219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ -if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V |
166 | 96, 165 | ifex 4515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ V |
167 | 163, 164,
166 | fvmpt 6872 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
168 | 157, 167 | oveq12d 7289 |
. . . . . . . . . . . . . . . . . 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)))) |
169 | 168 | fveq2d 6775 |
. . . . . . . . . . . . . . . . 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))))) |
170 | 169 | mpteq2ia 5182 |
. . . . . . . . . . . . . . . 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))))) |
171 | 170 | fveq2i 6774 |
. . . . . . . . . . . . . . 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)))))) |
172 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ℝ ∈
V) |
173 | | fvex 6784 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑔‘𝑥) ∈ V |
174 | 173, 95 | ifex 4515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ V |
175 | 174, 95 | ifex 4515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V |
176 | 175 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) ∈ V) |
177 | | ovex 7304 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) ∈ V |
178 | 95, 177 | ifex 4515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V |
179 | 178 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ V) |
180 | | ffn 6598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷) |
181 | | frn 6605 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ) |
182 | | ref 14821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
ℜ:ℂ⟶ℝ |
183 | | ffn 6598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(ℜ:ℂ⟶ℝ → ℜ Fn
ℂ) |
184 | 182, 183 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ℜ Fn
ℂ |
185 | | fnco 6547 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ℜ
Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘
𝐹) Fn 𝐷) |
186 | 184, 185 | mp3an1 1447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘
𝐹) Fn 𝐷) |
187 | 180, 181,
186 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷) |
188 | | elpreima 6932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℜ
∘ 𝐹) Fn 𝐷 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))) |
189 | 4, 187, 188 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))) |
190 | | fco 6622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘
𝐹):𝐷⟶ℝ) |
191 | 182, 4, 190 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ) |
192 | 191 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ) |
193 | 192 | biantrurd 533 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ
∘ 𝐹)‘𝑥)))) |
194 | | elrege0 13185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((ℜ
∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔
(((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ
∘ 𝐹)‘𝑥))) |
195 | 193, 194 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))) |
196 | | fvco3 6864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐹:𝐷⟶ℂ ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥))) |
197 | 4, 196 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹‘𝑥))) |
198 | 197 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥)))) |
199 | 195, 198 | bitr3d 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤
(ℜ‘(𝐹‘𝑥)))) |
200 | 199 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝑥 ∈ 𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))))) |
201 | 189, 200 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))))) |
202 | 201 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))))) |
203 | | eldif 3902 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ 𝐷)) |
204 | 203 | baibr 537 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℝ → (¬
𝑥 ∈ 𝐷 ↔ 𝑥 ∈ (ℝ ∖ 𝐷))) |
205 | | 0le0 12074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ≤
0 |
206 | 205, 18 | breqtrri 5106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ≤
(ℜ‘0) |
207 | 206 | biantru 530 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
𝑥 ∈ 𝐷 ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0))) |
208 | 204, 207 | bitr3di 286 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0)))) |
209 | 208 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0)))) |
210 | 202, 209 | orbi12d 916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ((𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0))))) |
211 | | elun 4088 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ↔ (𝑥 ∈ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷))) |
212 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘(𝐹‘𝑥))) |
213 | 212 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = (𝐹‘𝑥) → (0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹‘𝑥)))) |
214 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)) = (ℜ‘0)) |
215 | 214 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0) = 0 → (0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ↔ 0 ≤
(ℜ‘0))) |
216 | 213, 215 | elimif 4502 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)) ↔ ((𝑥 ∈ 𝐷 ∧ 0 ≤ (ℜ‘(𝐹‘𝑥))) ∨ (¬ 𝑥 ∈ 𝐷 ∧ 0 ≤
(ℜ‘0)))) |
217 | 210, 211,
216 | 3bitr4g 314 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ↔ 0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))) |
218 | 217 | ifbid 4488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) |
219 | 218 | mpteq2dva 5179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0))) |
220 | 217 | ifbid 4488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) |
221 | 220 | mpteq2dva 5179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) |
222 | 172, 176,
179, 219, 221 | offval2 7547 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ (if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), 0) + if(0 ≤ (ℜ‘if(𝑥 ∈ 𝐷, (𝐹‘𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))))) |
223 | | ovif12 7368 |
. . . . . . . . . . . . . . . . . . . 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)))) |
224 | 87 | ffvelrnda 6958 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑔‘𝑥) ∈
ℝ) |
225 | 224 | recnd 11004 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (𝑔‘𝑥) ∈
ℂ) |
226 | | 0cn 10968 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℂ |
227 | | ifcl 4510 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ)
→ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ) |
228 | 225, 226,
227 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ) |
229 | 228 | addid1d 11175 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) + 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
230 | 228 | mulm1d 11427 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
231 | 230 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
232 | 228 | negcld 11319 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0) ∈ ℂ) |
233 | 232 | addid2d 11176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 + -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
234 | 231, 233 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑥 ∈ ℝ)
→ (0 + (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
235 | 229, 234 | ifeq12d 4486 |
. . . . . . . . . . . . . . . . . . . 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))) |
236 | 223, 235 | eqtrid 2792 |
. . . . . . . . . . . . . . . . . . 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))) |
237 | 236 | mpteq2dva 5179 |
. . . . . . . . . . . . . . . . . 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)))) |
238 | 222, 237 | sylan9eq 2800 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) |
239 | | 0xr 11023 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 ∈
ℝ* |
240 | | pnfxr 11030 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ +∞
∈ ℝ* |
241 | | 0ltpnf 12857 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 0 <
+∞ |
242 | | snunioo 13209 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
< +∞) → ({0} ∪ (0(,)+∞)) =
(0[,)+∞)) |
243 | 239, 240,
241, 242 | mp3an 1460 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({0}
∪ (0(,)+∞)) = (0[,)+∞) |
244 | 243 | imaeq2i 5966 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) =
(◡(ℜ ∘ 𝐹) “ (0[,)+∞)) |
245 | | imaundi 6052 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (◡(ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) =
((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) |
246 | 244, 245 | eqtr3i 2770 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) = ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) |
247 | | ismbfcn 24791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn))) |
248 | 4, 247 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn))) |
249 | 42, 248 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ
∘ 𝐹) ∈
MblFn)) |
250 | 249 | simpld 495 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn) |
251 | | mbfimasn 24794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ)
→ (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom
vol) |
252 | 86, 251 | mp3an3 1449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ {0}) ∈ dom
vol) |
253 | | mbfima 24792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom
vol) |
254 | | unmbl 24699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((◡(ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ (◡(ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
→ ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom
vol) |
255 | 252, 253,
254 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℜ
∘ 𝐹) ∈ MblFn
∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom
vol) |
256 | 250, 191,
255 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ {0}) ∪ (◡(ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom
vol) |
257 | 246, 256 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom
vol) |
258 | 4 | fdmd 6609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom 𝐹 = 𝐷) |
259 | | mbfdm 24788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
260 | 42, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
261 | 258, 260 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∈ dom vol) |
262 | | difmbl 24705 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℝ
∈ dom vol ∧ 𝐷
∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol) |
263 | 11, 261, 262 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ℝ ∖ 𝐷) ∈ dom
vol) |
264 | | unmbl 24699 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol
∧ (ℝ ∖ 𝐷)
∈ dom vol) → ((◡(ℜ
∘ 𝐹) “
(0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) |
265 | 257, 263,
264 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom
vol) |
266 | | fveq2 6771 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 = 𝑥 → (𝑔‘𝑡) = (𝑔‘𝑥)) |
267 | 266 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑡 = 𝑥 → (0 ≤ (𝑔‘𝑡) ↔ 0 ≤ (𝑔‘𝑥))) |
268 | 267, 266 | ifbieq1d 4489 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 𝑥 → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
269 | 268, 84, 174 | fvmpt 6872 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
270 | 269 | eqcomd 2746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥)) |
271 | 270 | ifeq1d 4484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0)) |
272 | 271 | mpteq2ia 5182 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥), 0)) |
273 | 272 | i1fres 24868 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∈ dom
∫1) |
274 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
(𝑡 ∈ ℝ ↦
if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom
∫1) |
275 | | neg1rr 12088 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ -1 ∈
ℝ |
276 | 275 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 → -1
∈ ℝ) |
277 | 274, 276 | i1fmulc 24866 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 →
((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom
∫1) |
278 | | cmmbl 24696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol
→ (ℝ ∖ ((◡(ℜ
∘ 𝐹) “
(0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol) |
279 | | ifnot 4517 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), (-1 ·
if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
280 | | eldif 3902 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)))) |
281 | 280 | baibr 537 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ → (¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))))) |
282 | | tru 1546 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
⊤ |
283 | | negex 11219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ -1 ∈
V |
284 | 283 | fconst 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℝ
× {-1}):ℝ⟶{-1} |
285 | | ffn 6598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ℝ
× {-1}):ℝ⟶{-1} → (ℝ × {-1}) Fn
ℝ) |
286 | 284, 285 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (⊤
→ (ℝ × {-1}) Fn ℝ) |
287 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (⊤
→ (𝑡 ∈ ℝ
↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) Fn ℝ) |
288 | 100 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (⊤
→ ℝ ∈ V) |
289 | | inidm 4158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℝ
∩ ℝ) = ℝ |
290 | 283 | fvconst2 7076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 ∈ ℝ → ((ℝ
× {-1})‘𝑥) =
-1) |
291 | 290 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((⊤ ∧ 𝑥
∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1) |
292 | 269 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((⊤ ∧ 𝑥
∈ ℝ) → ((𝑡
∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))‘𝑥) = if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) |
293 | 286, 287,
288, 288, 289, 291, 292 | ofval 7538 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((⊤ ∧ 𝑥
∈ ℝ) → (((ℝ × {-1}) ∘f ·
(𝑡 ∈ ℝ ↦
if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
294 | 282, 293 | mpan 687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℝ →
(((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) |
295 | 294 | eqcomd 2746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ → (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)) = (((ℝ × {-1})
∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥)) |
296 | 281, 295 | ifbieq1d 4489 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ → if(¬
𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), (-1 ·
if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))), (((ℝ
× {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0)) |
297 | 279, 296 | eqtr3id 2794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))), (((ℝ
× {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0)) |
298 | 297 | mpteq2ia 5182 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷))), (((ℝ
× {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))‘𝑥), 0)) |
299 | 298 | i1fres 24868 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ dom ∫1 ∧
(ℝ ∖ ((◡(ℜ ∘
𝐹) “ (0[,)+∞))
∪ (ℝ ∖ 𝐷)))
∈ dom vol) → (𝑥
∈ ℝ ↦ if(𝑥
∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪
(ℝ ∖ 𝐷)), 0,
(-1 · if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom
∫1) |
300 | 277, 278,
299 | syl2an 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol)
→ (𝑥 ∈ ℝ
↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))) ∈ dom
∫1) |
301 | 273, 300 | i1fadd 24857 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ dom ∫1 ∧
((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)) ∈ dom vol)
→ ((𝑥 ∈ ℝ
↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom
∫1) |
302 | 85, 265, 301 | syl2anr 597 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), if(0 ≤
(𝑔‘𝑥), (𝑔‘𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ((◡(ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ
∖ 𝐷)), 0, (-1
· if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))))) ∈ dom
∫1) |
303 | 238, 302 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0
≤ (ℜ‘if(𝑥
∈ 𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∈ dom
∫1) |
304 | 154 | cbvmptv 5192 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) = (𝑡 ∈ ℝ ↦
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) |
305 | 304, 31 | eqeltrid 2845 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈
𝐿1) |
306 | 9, 304 | fmptd 6985 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ) |
307 | 305, 306 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
308 | 307 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0))) ∈ 𝐿1 ∧
(𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥),
0))):ℝ⟶ℝ)) |
309 | | ftc1anclem4 35849 |
. . . . . . . . . . . . . . . . 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)))‘𝑡))))) ∈ ℝ) |
310 | 309 | 3expb 1119 |
. . . . . . . . . . . . . . . 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)))‘𝑡))))) ∈ ℝ) |
311 | 303, 308,
310 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡))))) ∈ ℝ) |
312 | 171, 311 | eqeltrrid 2846 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘(𝑡
∈ ℝ ↦ (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ) |
313 | 134, 138,
139, 150, 312 | itg2addnc 35827 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘f + (𝑡 ∈ ℝ ↦
(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)))))))) |
314 | 100 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ℝ
∈ V) |
315 | 96 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ V) |
316 | | eqidd 2741 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
317 | | eqidd 2741 |
. . . . . . . . . . . . . . 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)))))) |
318 | 314, 315,
146, 316, 317 | offval2 7547 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) → ((𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘f + (𝑡 ∈ ℝ ↦
(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))))))) |
319 | 318 | fveq2d 6775 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑔 ∈ dom ∫1) →
(∫2‘((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∘f + (𝑡 ∈ ℝ ↦
(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)))))))) |
320 | 313, 319 | eqtr3d 2782 |
. . . . . . . . . . . 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)))))))) |
321 | 320 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(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)))))))) |
322 | | nfv 1921 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡(𝜑 ∧ 𝑔 ∈ dom
∫1) |
323 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡𝑔 |
324 | | nfcv 2909 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡
∘r ≤ |
325 | | nfmpt1 5187 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑡(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
326 | 323, 324,
325 | nfbr 5126 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑡 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
327 | 322, 326 | nfan 1906 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑡((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
328 | | anass 469 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈
ℝ))) |
329 | 87 | ffnd 6599 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 ∈ dom ∫1
→ 𝑔 Fn
ℝ) |
330 | | fvex 6784 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V |
331 | | eqid 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
332 | 330, 331 | fnmpti 6574 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ |
333 | 332 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 ∈ dom ∫1
→ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) Fn ℝ) |
334 | | eqidd 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ (𝑔‘𝑡) = (𝑔‘𝑡)) |
335 | 331 | fvmpt2 6883 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 ∈ ℝ ∧
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
336 | 330, 335 | mpan2 688 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
337 | 336 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ ((𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
338 | 329, 333,
101, 101, 289, 334, 337 | ofrval 7539 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑔 ∘r
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
339 | 338 | 3com23 1125 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ
∧ 𝑔 ∘r
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
340 | 339 | 3expa 1117 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
∧ 𝑔 ∘r
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
341 | 340 | adantll 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
342 | | resubcl 11285 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
343 | 8, 104, 342 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
344 | 343 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
345 | | absid 15006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
346 | 8, 345 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
347 | 346 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
348 | 347 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
349 | 348 | an32s 649 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
350 | 349 | adantllr 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
351 | | breq1 5082 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
352 | | breq1 5082 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → (0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
353 | 351, 352 | ifboth 4504 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔‘𝑡) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
354 | 350, 353 | sylancom 588 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
355 | | subge0 11488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) → (0 ≤
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
356 | 8, 104, 355 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (0 ≤
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
357 | 356 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → (0 ≤
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ↔ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
358 | 354, 357 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
359 | 344, 358 | absidd 15132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
360 | | iftrue 4471 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
361 | 360 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
362 | 361 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
363 | 362 | 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)))) |
364 | 8 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
365 | 345 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
366 | 364, 365 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
367 | 359, 363,
366 | 3eqtr4d 2790 |
. . . . . . . . . . . . . . . . . . 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))) |
368 | 104 | renegcld 11402 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 ∈ dom ∫1
∧ 𝑡 ∈ ℝ)
→ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) |
369 | | resubcl 11285 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
370 | 8, 368, 369 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
371 | 370 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ∈ ℝ) |
372 | 88 | ad3antlr 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ∈ ℝ) |
373 | 8 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
374 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ∈ ℝ) |
375 | | ltnle 11055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
376 | 86, 375 | mpan2 688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
377 | | ltle 11064 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ)
→ ((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
378 | 86, 377 | mpan2 688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
379 | 376, 378 | sylbird 259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ → (¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
380 | 379 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) |
381 | | absnid 15008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) ≤ 0) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
382 | 380, 381 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
383 | 382 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ↔ (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
384 | 383 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
385 | 384 | an32s 649 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
386 | 374, 385 | sylanl1 677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (𝑔‘𝑡) ≤ -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
387 | 372, 373,
386 | lenegcon2d 11558 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡)) |
388 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → 𝜑) |
389 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 0 ∈
ℝ) |
390 | 8, 389 | ltnled 11122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 ↔ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)))) |
391 | 8, 86, 377 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) < 0 → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
392 | 390, 391 | sylbird 259 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0)) |
393 | 392 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) |
394 | 388, 393 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) |
395 | | negeq 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -(𝑔‘𝑡) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
396 | 395 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑔‘𝑡) = if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
397 | | neg0 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ -0 =
0 |
398 | | negeq 11213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → -0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
399 | 397, 398 | eqtr3id 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → 0 = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
400 | 399 | breq2d 5091 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 = if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
401 | 396, 400 | ifboth 4504 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -(𝑔‘𝑡) ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
402 | 387, 394,
401 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
403 | | suble0 11489 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℝ) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
404 | 8, 368, 403 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
(((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
405 | 404 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → (((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
406 | 402, 405 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) ≤ 0) |
407 | 371, 406 | absnidd 15123 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
408 | | subneg 11270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
409 | 408 | negeqd 11215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
410 | | negdi2 11279 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) + if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
411 | 409, 410 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
412 | 32, 140, 411 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) →
-((ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
413 | 412 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) → -((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
414 | 407, 413 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
415 | | iffalse 4474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (¬ 0
≤ (ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) → if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) |
416 | 415 | oveq2d 7287 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬ 0
≤ (ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) → ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = ((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
417 | 416 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬ 0
≤ (ℜ‘if(𝑡
∈ 𝐷, (𝐹‘𝑡), 0)) →
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) = (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))) |
418 | 417 | 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)))) |
419 | 8, 381 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) ≤ 0) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
420 | 393, 419 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) = -(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) |
421 | 420 | oveq1d 7286 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
422 | 388, 421 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬ 0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0))) →
((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)) = (-(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
423 | 414, 418,
422 | 3eqtr4d 2790 |
. . . . . . . . . . . . . . . . . . 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))) |
424 | 367, 423 | pm2.61dan 810 |
. . . . . . . . . . . . . . . . . 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))) |
425 | 424 | oveq2d 7287 |
. . . . . . . . . . . . . . . . 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)))) |
426 | 53 | recnd 11004 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) |
427 | | pncan3 11229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) ∈ ℂ ∧
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) ∈ ℂ) → (if(0 ≤
(𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
428 | 140, 426,
427 | syl2anr 597 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) → (if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
429 | 428 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ (𝑔‘𝑡) ≤ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + ((abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))) − if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
430 | 425, 429 | eqtrd 2780 |
. . . . . . . . . . . . . . . 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)))) |
431 | 341, 430 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑔 ∈ dom ∫1 ∧ 𝑡 ∈ ℝ)) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
432 | 328, 431 | sylanb 581 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
433 | 432 | an32s 649 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) ∧ 𝑡 ∈ ℝ) → (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))) = (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) |
434 | 327, 433 | mpteq2da 5177 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) → (𝑡 ∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) = (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) |
435 | 434 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
(∫2‘(𝑡
∈ ℝ ↦ (if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0) + (abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))))))) = (∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))))) |
436 | 321, 435 | eqtrd 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(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)))))) |
437 | 436 | breq1d 5089 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≤ (𝑡 ∈ ℝ ↦
(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))) + 𝑌))) |
438 | 437 | adantllr 716 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔 ∘r
≤ (𝑡 ∈ ℝ
↦ (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))) + 𝑌))) |
439 | 312 | adantlr 712 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) ∈ ℝ) |
440 | 63 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ 𝑌 ∈
ℝ) |
441 | 115 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ∈ ℝ) |
442 | 439, 440,
441 | ltadd2d 11131 |
. . . . . . . . 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))) + 𝑌))) |
443 | 442 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔 ∘r
≤ (𝑡 ∈ ℝ
↦ (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))) + 𝑌))) |
444 | | ltsubadd 11445 |
. . . . . . . . . . 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))) + 𝑌))) |
445 | 60, 63, 115, 444 | syl3an 1159 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+ ∧ 𝑔 ∈ dom ∫1)
→ (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
446 | 445 | 3expa 1117 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ (((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
447 | 446 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔 ∘r
≤ (𝑡 ∈ ℝ
↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) →
(((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0
≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) ↔
(∫2‘(𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) <
((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) + 𝑌))) |
448 | 438, 443,
447 | 3bitr4d 311 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ 𝑔 ∘r
≤ (𝑡 ∈ ℝ
↦ (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))))) |
449 | 448 | adantrr 714 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ (𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (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))))) |
450 | 131, 449 | mpbird 256 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
∧ (𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌))) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌) |
451 | 450 | ex 413 |
. . . 4
⊢ (((𝜑 ∧ 𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1)
→ ((𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌)) |
452 | 451 | reximdva 3205 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑔 ∈ dom
∫1(𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌)) |
453 | | fveq1 6770 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) → (𝑓‘𝑡) = ((𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0)))‘𝑡)) |
454 | 453, 167 | sylan9eq 2800 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤
(ℜ‘if(𝑥 ∈
𝐷, (𝐹‘𝑥), 0)), if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0), -if(0 ≤ (𝑔‘𝑥), (𝑔‘𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓‘𝑡) = if(0 ≤ (ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0))) |
455 | 454 | oveq2d 7287 |
. . . . . . . . . . . 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)))) |
456 | 455 | fveq2d 6775 |
. . . . . . . . . . 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))))) |
457 | 456 | mpteq2dva 5179 |
. . . . . . . . . 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)))))) |
458 | 457 | fveq2d 6775 |
. . . . . . . . 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))))))) |
459 | 458 | breq1d 5089 |
. . . . . . . 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)))))) < 𝑌)) |
460 | 459 | rspcev 3561 |
. . . . . . 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)) − (𝑓‘𝑡))))) < 𝑌) |
461 | 460 | ex 413 |
. . . . . 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)) − (𝑓‘𝑡))))) < 𝑌)) |
462 | 303, 461 | 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)) − (𝑓‘𝑡))))) < 𝑌)) |
463 | 462 | rexlimdva 3215 |
. . . 4
⊢ (𝜑 → (∃𝑔 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − if(0 ≤
(ℜ‘if(𝑡 ∈
𝐷, (𝐹‘𝑡), 0)), if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0), -if(0 ≤ (𝑔‘𝑡), (𝑔‘𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)) |
464 | 463 | 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)) − (𝑓‘𝑡))))) < 𝑌)) |
465 | 452, 464 | syld 47 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
(∃𝑔 ∈ dom
∫1(𝑔
∘r ≤ (𝑡
∈ ℝ ↦ (abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)))) ∧ ¬
(∫1‘𝑔)
≤ ((∫2‘(𝑡 ∈ ℝ ↦
(abs‘(ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0))))) − 𝑌)) → ∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌)) |
466 | 80, 465 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑌 ∈ ℝ+) →
∃𝑓 ∈ dom
∫1(∫2‘(𝑡 ∈ ℝ ↦
(abs‘((ℜ‘if(𝑡 ∈ 𝐷, (𝐹‘𝑡), 0)) − (𝑓‘𝑡))))) < 𝑌) |