Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ftc1anclem5 Structured version   Visualization version   GIF version

Theorem ftc1anclem5 34360
Description: Lemma for ftc1anc 34364, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.)
Hypotheses
Ref Expression
ftc1anc.g 𝐺 = (𝑥 ∈ (𝐴[,]𝐵) ↦ ∫(𝐴(,)𝑥)(𝐹𝑡) d𝑡)
ftc1anc.a (𝜑𝐴 ∈ ℝ)
ftc1anc.b (𝜑𝐵 ∈ ℝ)
ftc1anc.le (𝜑𝐴𝐵)
ftc1anc.s (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷)
ftc1anc.d (𝜑𝐷 ⊆ ℝ)
ftc1anc.i (𝜑𝐹 ∈ 𝐿1)
ftc1anc.f (𝜑𝐹:𝐷⟶ℂ)
Assertion
Ref Expression
ftc1anclem5 ((𝜑𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌)
Distinct variable groups:   𝑡,𝑓,𝑥,𝐴   𝐵,𝑓,𝑡,𝑥   𝐷,𝑓,𝑡,𝑥   𝑓,𝐹,𝑡,𝑥   𝜑,𝑓,𝑡,𝑥   𝑓,𝐺   𝑓,𝑌,𝑡,𝑥
Allowed substitution hints:   𝐺(𝑥,𝑡)

Proof of Theorem ftc1anclem5
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 iftrue 4350 . . . . . . . . 9 (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
21mpteq2ia 5012 . . . . . . . 8 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
32fveq2i 6496 . . . . . . 7 (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
4 ftc1anc.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐷⟶ℂ)
54ffvelrnda 6670 . . . . . . . . . . . . 13 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
6 0cnd 10424 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
75, 6ifclda 4378 . . . . . . . . . . . 12 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
87recld 14404 . . . . . . . . . . 11 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
98adantr 473 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
10 ftc1anc.d . . . . . . . . . . 11 (𝜑𝐷 ⊆ ℝ)
11 rembl 23834 . . . . . . . . . . . 12 ℝ ∈ dom vol
1211a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ dom vol)
138adantr 473 . . . . . . . . . . 11 ((𝜑𝑡𝐷) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
14 eldifn 3990 . . . . . . . . . . . . 13 (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡𝐷)
1514adantl 474 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡𝐷)
16 iffalse 4353 . . . . . . . . . . . . . 14 𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = 0)
1716fveq2d 6497 . . . . . . . . . . . . 13 𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘0))
18 re0 14362 . . . . . . . . . . . . 13 (ℜ‘0) = 0
1917, 18syl6eq 2824 . . . . . . . . . . . 12 𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = 0)
2015, 19syl 17 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = 0)
21 iftrue 4350 . . . . . . . . . . . . . 14 (𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = (𝐹𝑡))
2221fveq2d 6497 . . . . . . . . . . . . 13 (𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘(𝐹𝑡)))
2322mpteq2ia 5012 . . . . . . . . . . . 12 (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡)))
244feqmptd 6556 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
25 ftc1anc.i . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ 𝐿1)
2624, 25eqeltrrd 2861 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
275iblcn 24092 . . . . . . . . . . . . . 14 (𝜑 → ((𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1 ↔ ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1 ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ 𝐿1)))
2826, 27mpbid 224 . . . . . . . . . . . . 13 (𝜑 → ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1 ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ 𝐿1))
2928simpld 487 . . . . . . . . . . . 12 (𝜑 → (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1)
3023, 29syl5eqel 2864 . . . . . . . . . . 11 (𝜑 → (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ 𝐿1)
3110, 12, 13, 20, 30iblss2 24099 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ 𝐿1)
328recnd 10460 . . . . . . . . . . . . 13 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
3332adantr 473 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
34 eqidd 2773 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
35 absf 14548 . . . . . . . . . . . . . 14 abs:ℂ⟶ℝ
3635a1i 11 . . . . . . . . . . . . 13 (𝜑 → abs:ℂ⟶ℝ)
3736feqmptd 6556 . . . . . . . . . . . 12 (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
38 fveq2 6493 . . . . . . . . . . . 12 (𝑥 = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3933, 34, 37, 38fmptco 6708 . . . . . . . . . . 11 (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
409fmpttd 6696 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ)
41 iblmbf 24061 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
4225, 41syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ MblFn)
4324, 42eqeltrrd 2861 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ MblFn)
445ismbfcn2 23932 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑡𝐷 ↦ (𝐹𝑡)) ∈ MblFn ↔ ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ MblFn)))
4543, 44mpbid 224 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ MblFn))
4645simpld 487 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn)
4723, 46syl5eqel 2864 . . . . . . . . . . . . 13 (𝜑 → (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
4810, 12, 13, 20, 47mbfss 23940 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
49 ftc1anclem1 34356 . . . . . . . . . . . 12 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
5040, 48, 49syl2anc 576 . . . . . . . . . . 11 (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
5139, 50eqeltrrd 2861 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
529, 31, 51iblabsnc 34345 . . . . . . . . 9 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ 𝐿1)
5332abscld 14647 . . . . . . . . . . 11 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ)
5453adantr 473 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ)
5532absge0d 14655 . . . . . . . . . . 11 (𝜑 → 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
5655adantr 473 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
5754, 56iblpos 24086 . . . . . . . . 9 (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ 𝐿1 ↔ ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ)))
5852, 57mpbid 224 . . . . . . . 8 (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ))
5958simprd 488 . . . . . . 7 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ)
603, 59syl5eqelr 2865 . . . . . 6 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ)
61 ltsubrp 12235 . . . . . 6 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))))
6260, 61sylan 572 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))))
63 rpre 12205 . . . . . . 7 (𝑌 ∈ ℝ+𝑌 ∈ ℝ)
64 resubcl 10743 . . . . . . 7 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
6560, 63, 64syl2an 586 . . . . . 6 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
6660adantr 473 . . . . . 6 ((𝜑𝑌 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ)
6765, 66ltnled 10579 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ↔ ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
6862, 67mpbid 224 . . . 4 ((𝜑𝑌 ∈ ℝ+) → ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))
6953rexrd 10482 . . . . . . . . 9 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ*)
70 elxrge0 12654 . . . . . . . . 9 ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞) ↔ ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ* ∧ 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
7169, 55, 70sylanbrc 575 . . . . . . . 8 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞))
7271adantr 473 . . . . . . 7 ((𝜑𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞))
7372fmpttd 6696 . . . . . 6 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))):ℝ⟶(0[,]+∞))
7473adantr 473 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))):ℝ⟶(0[,]+∞))
7565rexrd 10482 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ*)
76 itg2leub 24028 . . . . 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))))) − 𝑌))))
7774, 75, 76syl2anc 576 . . . 4 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))))
7868, 77mtbid 316 . . 3 ((𝜑𝑌 ∈ ℝ+) → ¬ ∀𝑔 ∈ dom ∫1(𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
79 rexanali 3205 . . 3 (∃𝑔 ∈ dom ∫1(𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) ↔ ¬ ∀𝑔 ∈ dom ∫1(𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
8078, 79sylibr 226 . 2 ((𝜑𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
8165ad2antrr 713 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
82 itg1cl 23979 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫1𝑔) ∈ ℝ)
8382ad2antlr 714 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫1𝑔) ∈ ℝ)
84 eqid 2772 . . . . . . . . . . . 12 (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
8584i1fpos 24000 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1)
86 0re 10433 . . . . . . . . . . . . . 14 0 ∈ ℝ
87 i1ff 23970 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
8887ffvelrnda 6670 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
89 max1 12388 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (𝑔𝑡) ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
9086, 88, 89sylancr 578 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
9190ralrimiva 3126 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
92 ax-resscn 10384 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
9392a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → ℝ ⊆ ℂ)
94 fvex 6506 . . . . . . . . . . . . . . . . 17 (𝑔𝑡) ∈ V
95 c0ex 10425 . . . . . . . . . . . . . . . . 17 0 ∈ V
9694, 95ifex 4392 . . . . . . . . . . . . . . . 16 if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ V
9796, 84fnmpti 6315 . . . . . . . . . . . . . . 15 (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ
9897a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ)
9993, 980pledm 23967 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 → (0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ (ℝ × {0}) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
100 reex 10418 . . . . . . . . . . . . . . 15 ℝ ∈ V
101100a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → ℝ ∈ V)
10295a1i 11 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → 0 ∈ V)
103 ifcl 4388 . . . . . . . . . . . . . . 15 (((𝑔𝑡) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
10488, 86, 103sylancl 577 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
105 fconstmpt 5457 . . . . . . . . . . . . . . 15 (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
106105a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
107 eqidd 2773 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
108101, 102, 104, 106, 107ofrfval2 7239 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 → ((ℝ × {0}) ∘𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
10999, 108bitrd 271 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → (0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
11091, 109mpbird 249 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 → 0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
111 itg2itg1 24030 . . . . . . . . . . 11 (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 ∧ 0𝑝𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
11285, 110, 111syl2anc 576 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
113 itg1cl 23979 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
11485, 113syl 17 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
115112, 114eqeltrd 2860 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
116115ad2antlr 714 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
117 ltnle 10512 . . . . . . . . . 10 ((((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ ∧ (∫1𝑔) ∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔) ↔ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
11865, 82, 117syl2an 586 . . . . . . . . 9 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔) ↔ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
119118biimpar 470 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔))
120 max2 12390 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (𝑔𝑡) ∈ ℝ) → (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
12186, 88, 120sylancr 578 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
122121ralrimiva 3126 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
12387feqmptd 6556 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1𝑔 = (𝑡 ∈ ℝ ↦ (𝑔𝑡)))
124101, 88, 104, 123, 107ofrfval2 7239 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → (𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
125122, 124mpbird 249 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
126 itg1le 24007 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1 ∧ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) → (∫1𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
12785, 125, 126mpd3an23 1442 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫1𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
128127, 112breqtrrd 4951 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫1𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
129128ad2antlr 714 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫1𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
13081, 83, 116, 119, 129ltletrd 10592 . . . . . . 7 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
131130adantrl 703 . . . . . 6 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
132 i1fmbf 23969 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
13385, 132syl 17 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
134133adantl 474 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
135 elrege0 12651 . . . . . . . . . . . . . . . . 17 (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
136104, 90, 135sylanbrc 575 . . . . . . . . . . . . . . . 16 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ (0[,)+∞))
137136fmpttd 6696 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)):ℝ⟶(0[,)+∞))
138137adantl 474 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)):ℝ⟶(0[,)+∞))
139115adantl 474 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
140104recnd 10460 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ)
141140negcld 10777 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ)
142140, 141ifcld 4389 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℂ)
143 subcl 10677 . . . . . . . . . . . . . . . . . . 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))) ∈ ℂ)
14432, 142, 143syl2an 586 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℂ)
145144anassrs 460 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℂ)
146145abscld 14647 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) ∈ ℝ)
147145absge0d 14655 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))
148 elrege0 12651 . . . . . . . . . . . . . . . 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))))))
149146, 147, 148sylanbrc 575 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) ∈ (0[,)+∞))
150149fmpttd 6696 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))):ℝ⟶(0[,)+∞))
151 eleq1w 2842 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → (𝑥𝐷𝑡𝐷))
152 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
153151, 152ifbieq1d 4367 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → if(𝑥𝐷, (𝐹𝑥), 0) = if(𝑡𝐷, (𝐹𝑡), 0))
154153fveq2d 6497 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
155 eqid 2772 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))
156 fvex 6506 . . . . . . . . . . . . . . . . . . . 20 (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ V
157154, 155, 156fvmpt 6589 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
158154breq2d 4935 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
159 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
160159breq2d 4935 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → (0 ≤ (𝑔𝑥) ↔ 0 ≤ (𝑔𝑡)))
161160, 159ifbieq1d 4367 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
162161negeqd 10672 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
163158, 161, 162ifbieq12d 4371 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
164 eqid 2772 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
165 negex 10676 . . . . . . . . . . . . . . . . . . . . 21 -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ V
16696, 165ifex 4392 . . . . . . . . . . . . . . . . . . . 20 if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ V
167163, 164, 166fvmpt 6589 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
168157, 167oveq12d 6988 . . . . . . . . . . . . . . . . . 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))))
169168fveq2d 6497 . . . . . . . . . . . . . . . . 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)))))
170169mpteq2ia 5012 . . . . . . . . . . . . . . . 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)))))
171170fveq2i 6496 . . . . . . . . . . . . . . 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))))))
172100a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℝ ∈ V)
173 fvex 6506 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔𝑥) ∈ V
174173, 95ifex 4392 . . . . . . . . . . . . . . . . . . . . 21 if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ V
175174, 95ifex 4392 . . . . . . . . . . . . . . . . . . . 20 if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) ∈ V
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) ∈ V)
177 ovex 7002 . . . . . . . . . . . . . . . . . . . . 21 (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) ∈ V
17895, 177ifex 4392 . . . . . . . . . . . . . . . . . . . 20 if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∈ V
179178a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∈ V)
180 ffn 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷)
181 frn 6344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ)
182 ref 14322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℜ:ℂ⟶ℝ
183 ffn 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ℜ:ℂ⟶ℝ → ℜ Fn ℂ)
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℜ Fn ℂ
185 fnco 6292 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℜ Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
186184, 185mp3an1 1427 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
187180, 181, 186syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷)
188 elpreima 6647 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℜ ∘ 𝐹) Fn 𝐷 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
1894, 187, 1883syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
190 fco 6355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘ 𝐹):𝐷⟶ℝ)
191182, 4, 190sylancr 578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ)
192191ffvelrnda 6670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ)
193192biantrurd 525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥))))
194 elrege0 12651 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥)))
195193, 194syl6bbr 281 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))
196 fvco3 6582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹:𝐷⟶ℂ ∧ 𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹𝑥)))
1974, 196sylan 572 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹𝑥)))
198197breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
199195, 198bitr3d 273 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
200199pm5.32da 571 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
201189, 200bitrd 271 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
202201adantr 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
203 0le0 11541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ 0
204203, 18breqtrri 4950 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≤ (ℜ‘0)
205204biantru 522 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐷 ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0)))
206 eldif 3835 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥𝐷))
207206baibr 529 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ → (¬ 𝑥𝐷𝑥 ∈ (ℝ ∖ 𝐷)))
208205, 207syl5rbbr 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
209208adantl 474 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
210202, 209orbi12d 902 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → ((𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥))) ∨ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0)))))
211 elun 4010 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)))
212 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥) → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘(𝐹𝑥)))
213212breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . 23 (if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥) → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
214 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥𝐷, (𝐹𝑥), 0) = 0 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘0))
215214breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . 23 (if(𝑥𝐷, (𝐹𝑥), 0) = 0 → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘0)))
216213, 215elimif 4380 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ ((𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥))) ∨ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
217210, 211, 2163bitr4g 306 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))))
218217ifbid 4366 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0))
219218mpteq2dva 5016 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)))
220217ifbid 4366 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))))
221220mpteq2dva 5016 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))))
222172, 176, 179, 219, 221offval2 7238 . . . . . . . . . . . . . . . . . 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))))))
223 ovif12 7063 . . . . . . . . . . . . . . . . . . . 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))))
22487ffvelrnda 6670 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
225224recnd 10460 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℂ)
226 0cn 10423 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℂ
227 ifcl 4388 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
228225, 226, 227sylancl 577 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
229228addid1d 10632 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) + 0) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
230228mulm1d 10885 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
231230oveq2d 6986 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = (0 + -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
232228negcld 10777 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
233232addid2d 10633 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
234231, 233eqtrd 2808 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
235229, 234ifeq12d 4364 . . . . . . . . . . . . . . . . . . . 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)))
236223, 235syl5eq 2820 . . . . . . . . . . . . . . . . . . 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)))
237236mpteq2dva 5016 . . . . . . . . . . . . . . . . . 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))))
238222, 237sylan9eq 2828 . . . . . . . . . . . . . . . . 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))))
239 0xr 10479 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
240 pnfxr 10486 . . . . . . . . . . . . . . . . . . . . . . 23 +∞ ∈ ℝ*
241 0ltpnf 12327 . . . . . . . . . . . . . . . . . . . . . . 23 0 < +∞
242 snunioo 12673 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
243239, 240, 241, 242mp3an 1440 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ∪ (0(,)+∞)) = (0[,)+∞)
244243imaeq2i 5762 . . . . . . . . . . . . . . . . . . . . 21 ((ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = ((ℜ ∘ 𝐹) “ (0[,)+∞))
245 imaundi 5842 . . . . . . . . . . . . . . . . . . . . 21 ((ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞)))
246244, 245eqtr3i 2798 . . . . . . . . . . . . . . . . . . . 20 ((ℜ ∘ 𝐹) “ (0[,)+∞)) = (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞)))
247 ismbfcn 23923 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
2484, 247syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
24942, 248mpbid 224 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))
250249simpld 487 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn)
251 mbfimasn 23926 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ) → ((ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
25286, 251mp3an3 1429 . . . . . . . . . . . . . . . . . . . . . 22 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
253 mbfima 23924 . . . . . . . . . . . . . . . . . . . . . 22 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
254 unmbl 23831 . . . . . . . . . . . . . . . . . . . . . 22 ((((ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ ((ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol) → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
255252, 253, 254syl2anc 576 . . . . . . . . . . . . . . . . . . . . 21 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
256250, 191, 255syl2anc 576 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
257246, 256syl5eqel 2864 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol)
2584fdmd 6347 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝐹 = 𝐷)
259 mbfdm 23920 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
26042, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝐹 ∈ dom vol)
261258, 260eqeltrrd 2861 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ dom vol)
262 difmbl 23837 . . . . . . . . . . . . . . . . . . . 20 ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol)
26311, 261, 262sylancr 578 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℝ ∖ 𝐷) ∈ dom vol)
264 unmbl 23831 . . . . . . . . . . . . . . . . . . 19 ((((ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol ∧ (ℝ ∖ 𝐷) ∈ dom vol) → (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
265257, 263, 264syl2anc 576 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
266 fveq2 6493 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑥 → (𝑔𝑡) = (𝑔𝑥))
267266breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑥 → (0 ≤ (𝑔𝑡) ↔ 0 ≤ (𝑔𝑥)))
268267, 266ifbieq1d 4367 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑥 → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
269268, 84, 174fvmpt 6589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
270269eqcomd 2778 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥))
271270ifeq1d 4362 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) = if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥), 0))
272271mpteq2ia 5012 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥), 0))
273272i1fres 23999 . . . . . . . . . . . . . . . . . . 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 11555 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
276275a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → -1 ∈ ℝ)
277274, 276i1fmulc 23997 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → ((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ dom ∫1)
278 cmmbl 23828 . . . . . . . . . . . . . . . . . . . 20 ((((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol → (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol)
279 ifnot 4394 . . . . . . . . . . . . . . . . . . . . . . 23 if(¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)), 0) = if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
280 eldif 3835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))))
281280baibr 529 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)))))
282 tru 1511 . . . . . . . . . . . . . . . . . . . . . . . . . 26
283 negex 10676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 -1 ∈ V
284283fconst 6388 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ × {-1}):ℝ⟶{-1}
285 ffn 6338 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℝ × {-1}):ℝ⟶{-1} → (ℝ × {-1}) Fn ℝ)
286284, 285mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → (ℝ × {-1}) Fn ℝ)
28797a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ)
288100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → ℝ ∈ V)
289 inidm 4077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ℝ ∩ ℝ) = ℝ
290283fvconst2 6787 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((ℝ × {-1})‘𝑥) = -1)
291290adantl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊤ ∧ 𝑥 ∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1)
292269adantl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊤ ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
293286, 287, 288, 288, 289, 291, 292ofval 7230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⊤ ∧ 𝑥 ∈ ℝ) → (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
294282, 293mpan 677 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ → (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
295294eqcomd 2778 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥))
296281, 295ifbieq1d 4367 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → if(¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
297279, 296syl5eqr 2822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
298297mpteq2ia 5012 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
299298i1fres 23999 . . . . . . . . . . . . . . . . . . . 20 ((((ℝ × {-1}) ∘𝑓 · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ dom ∫1 ∧ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) ∈ dom ∫1)
300277, 278, 299syl2an 586 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 ∧ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) ∈ dom ∫1)
301273, 300i1fadd 23989 . . . . . . . . . . . . . . . . . 18 (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 ∧ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))))) ∈ dom ∫1)
30285, 265, 301syl2anr 587 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) ∘𝑓 + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))))) ∈ dom ∫1)
303238, 302eqeltrrd 2861 . . . . . . . . . . . . . . . 16 ((𝜑𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∈ dom ∫1)
304154cbvmptv 5022 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
305304, 31syl5eqel 2864 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)
3069, 304fmptd 6695 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)
307305, 306jca 504 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
308307adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
309 ftc1anclem4 34359 . . . . . . . . . . . . . . . . 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)))‘𝑡))))) ∈ ℝ)
3103093expb 1100 . . . . . . . . . . . . . . . 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)))‘𝑡))))) ∈ ℝ)
311303, 308, 310syl2anc 576 . . . . . . . . . . . . . . 15 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡))))) ∈ ℝ)
312171, 311syl5eqelr 2865 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) ∈ ℝ)
313134, 138, 139, 150, 312itg2addnc 34335 . . . . . . . . . . . . 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))))))))
314100a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑔 ∈ dom ∫1) → ℝ ∈ V)
31596a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ V)
316 eqidd 2773 . . . . . . . . . . . . . . 15 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
317 eqidd 2773 . . . . . . . . . . . . . . 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))))))
318314, 315, 146, 316, 317offval2 7238 . . . . . . . . . . . . . 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)))))))
319318fveq2d 6497 . . . . . . . . . . . . 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))))))))
320313, 319eqtr3d 2810 . . . . . . . . . . . 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))))))))
321320adantr 473 . . . . . . . . . . 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))))))))
322 nfv 1873 . . . . . . . . . . . . . 14 𝑡(𝜑𝑔 ∈ dom ∫1)
323 nfcv 2926 . . . . . . . . . . . . . . 15 𝑡𝑔
324 nfcv 2926 . . . . . . . . . . . . . . 15 𝑡𝑟
325 nfmpt1 5019 . . . . . . . . . . . . . . 15 𝑡(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
326323, 324, 325nfbr 4970 . . . . . . . . . . . . . 14 𝑡 𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
327322, 326nfan 1862 . . . . . . . . . . . . 13 𝑡((𝜑𝑔 ∈ dom ∫1) ∧ 𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
328 anass 461 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)))
32987ffnd 6339 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
330 fvex 6506 . . . . . . . . . . . . . . . . . . . . . 22 (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ V
331 eqid 2772 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
332330, 331fnmpti 6315 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) Fn ℝ
333332a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) Fn ℝ)
334 eqidd 2773 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) = (𝑔𝑡))
335331fvmpt2 6599 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ∧ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
336330, 335mpan2 678 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
337336adantl 474 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
338329, 333, 101, 101, 289, 334, 337ofrval 7231 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3393383com23 1106 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ ∧ 𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3403393expa 1098 . . . . . . . . . . . . . . . . 17 (((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) ∧ 𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
341340adantll 701 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ 𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
342 resubcl 10743 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
3438, 104, 342syl2an 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
344343ad2antrr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
345 absid 14507 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
3468, 345sylan 572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
347346breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
348347biimpa 469 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
349348an32s 639 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
350349adantllr 706 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
351 breq1 4926 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔𝑡) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → ((𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
352 breq1 4926 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
353351, 352ifboth 4382 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
354350, 353sylancom 579 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
355 subge0 10946 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3568, 104, 355syl2an 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
357356ad2antrr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
358354, 357mpbird 249 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
359344, 358absidd 14633 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
360 iftrue 4350 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
361360oveq2d 6986 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
362361fveq2d 6497 . . . . . . . . . . . . . . . . . . . . 21 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
363362adantl 474 . . . . . . . . . . . . . . . . . . . 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))))
3648ad2antrr 713 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
365345oveq1d 6985 . . . . . . . . . . . . . . . . . . . . 21 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
366364, 365sylan 572 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
367359, 363, 3663eqtr4d 2818 . . . . . . . . . . . . . . . . . . 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)))
368104renegcld 10860 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
369 resubcl 10743 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
3708, 368, 369syl2an 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
371370ad2antrr 713 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
37288ad3antlr 718 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ∈ ℝ)
3738ad3antrrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
3748adantr 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
375 ltnle 10512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
37686, 375mpan2 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
377 ltle 10521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
37886, 377mpan2 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
379376, 378sylbird 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
380379imp 398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
381 absnid 14509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
382380, 381syldan 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
383382breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
384383biimpa 469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
385384an32s 639 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
386374, 385sylanl1 667 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
387372, 373, 386lenegcon2d 11016 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡))
388 simpll 754 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → 𝜑)
38986a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 ∈ ℝ)
3908, 389ltnled 10579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3918, 86, 377sylancl 577 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
392390, 391sylbird 252 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
393392imp 398 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
394388, 393sylan 572 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
395 negeq 10670 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔𝑡) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → -(𝑔𝑡) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
396395breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑡) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
397 neg0 10725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -0 = 0
398 negeq 10670 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → -0 = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
399397, 398syl5eqr 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → 0 = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
400399breq2d 4935 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
401396, 400ifboth 4382 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡) ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
402387, 394, 401syl2anc 576 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
403 suble0 10947 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
4048, 368, 403syl2an 586 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
405404ad2antrr 713 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
406402, 405mpbird 249 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0)
407371, 406absnidd 14624 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
408 subneg 10728 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
409408negeqd 10672 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
410 negdi2 10737 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
411409, 410eqtrd 2808 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
41232, 140, 411syl2an 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
413412ad2antrr 713 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
414407, 413eqtrd 2808 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
415 iffalse 4353 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
416415oveq2d 6986 . . . . . . . . . . . . . . . . . . . . . 22 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
417416fveq2d 6497 . . . . . . . . . . . . . . . . . . . . 21 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
418417adantl 474 . . . . . . . . . . . . . . . . . . . 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))))
4198, 381sylan 572 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
420393, 419syldan 582 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
421420oveq1d 6985 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
422388, 421sylan 572 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
423414, 418, 4223eqtr4d 2818 . . . . . . . . . . . . . . . . . . 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)))
424367, 423pm2.61dan 800 . . . . . . . . . . . . . . . . . 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)))
425424oveq2d 6986 . . . . . . . . . . . . . . . . 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))))
42653recnd 10460 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ)
427 pncan3 10686 . . . . . . . . . . . . . . . . . . 19 ((if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ ∧ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
428140, 426, 427syl2anr 587 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
429428adantr 473 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
430425, 429eqtrd 2808 . . . . . . . . . . . . . . . 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))))
431341, 430syldan 582 . . . . . . . . . . . . . . 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))))
432328, 431sylanb 573 . . . . . . . . . . . . . 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))))
433432an32s 639 . . . . . . . . . . . . 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))))
434327, 433mpteq2da 5015 . . . . . . . . . . . 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)))))
435434fveq2d 6497 . . . . . . . . . . 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))))))
436321, 435eqtrd 2808 . . . . . . . . . 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))))))
437436breq1d 4933 . . . . . . . . 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))) + 𝑌)))
438437adantllr 706 . . . . . . . 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))) + 𝑌)))
439312adantlr 702 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) ∈ ℝ)
44063ad2antlr 714 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → 𝑌 ∈ ℝ)
441115adantl 474 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
442439, 440, 441ltadd2d 10588 . . . . . . . . 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))) + 𝑌)))
443442adantr 473 . . . . . . . 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))) + 𝑌)))
444 ltsubadd 10903 . . . . . . . . . . 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))) + 𝑌)))
44560, 63, 115, 444syl3an 1140 . . . . . . . . . 10 ((𝜑𝑌 ∈ ℝ+𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
4464453expa 1098 . . . . . . . . 9 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
447446adantr 473 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
448438, 443, 4473bitr4d 303 . . . . . . 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)))))
449448adantrr 704 . . . . . 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)))))
450131, 449mpbird 249 . . . . 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)))))) < 𝑌)
451450ex 405 . . . 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)))))) < 𝑌))
452451reximdva 3213 . . 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)))))) < 𝑌))
453 fveq1 6492 . . . . . . . . . . . . . 14 (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) → (𝑓𝑡) = ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡))
454453, 167sylan9eq 2828 . . . . . . . . . . . . 13 ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
455454oveq2d 6986 . . . . . . . . . . . 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))))
456455fveq2d 6497 . . . . . . . . . . 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)))))
457456mpteq2dva 5016 . . . . . . . . . 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))))))
458457fveq2d 6497 . . . . . . . . 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)))))))
459458breq1d 4933 . . . . . . . 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)))))) < 𝑌))
460459rspcev 3529 . . . . . . 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)) − (𝑓𝑡))))) < 𝑌)
461460ex 405 . . . . . 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)) − (𝑓𝑡))))) < 𝑌))
462303, 461syl 17 . . . . 5 ((𝜑𝑔 ∈ dom ∫1) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌))
463462rexlimdva 3223 . . . 4 (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌))
464463adantr 473 . . 3 ((𝜑𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌))
465452, 464syld 47 . 2 ((𝜑𝑌 ∈ ℝ+) → (∃𝑔 ∈ dom ∫1(𝑔𝑟 ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌))
46680, 465mpd 15 1 ((𝜑𝑌 ∈ ℝ+) → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 833   = wceq 1507  wtru 1508  wcel 2048  wral 3082  wrex 3083  Vcvv 3409  cdif 3822  cun 3823  wss 3825  ifcif 4344  {csn 4435   class class class wbr 4923  cmpt 5002   × cxp 5398  ccnv 5399  dom cdm 5400  ran crn 5401  cima 5403  ccom 5404   Fn wfn 6177  wf 6178  cfv 6182  (class class class)co 6970  𝑓 cof 7219  𝑟 cofr 7220  cc 10325  cr 10326  0cc0 10327  1c1 10328   + caddc 10330   · cmul 10332  +∞cpnf 10463  *cxr 10465   < clt 10466  cle 10467  cmin 10662  -cneg 10663  +crp 12197  (,)cioo 12547  [,)cico 12549  [,]cicc 12550  cre 14307  cim 14308  abscabs 14444  volcvol 23757  MblFncmbf 23908  1citg1 23909  2citg2 23910  𝐿1cibl 23911  citg 23912  0𝑝c0p 23963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-inf2 8890  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404  ax-pre-sup 10405  ax-addf 10406
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-int 4744  df-iun 4788  df-disj 4892  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-ofr 7222  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-1o 7897  df-2o 7898  df-oadd 7901  df-er 8081  df-map 8200  df-pm 8201  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-fi 8662  df-sup 8693  df-inf 8694  df-oi 8761  df-dju 9116  df-card 9154  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-div 11091  df-nn 11432  df-2 11496  df-3 11497  df-4 11498  df-n0 11701  df-z 11787  df-uz 12052  df-q 12156  df-rp 12198  df-xneg 12317  df-xadd 12318  df-xmul 12319  df-ioo 12551  df-ico 12553  df-icc 12554  df-fz 12702  df-fzo 12843  df-fl 12970  df-mod 13046  df-seq 13178  df-exp 13238  df-hash 13499  df-cj 14309  df-re 14310  df-im 14311  df-sqrt 14445  df-abs 14446  df-clim 14696  df-sum 14894  df-rest 16542  df-topgen 16563  df-psmet 20229  df-xmet 20230  df-met 20231  df-bl 20232  df-mopn 20233  df-top 21196  df-topon 21213  df-bases 21248  df-cmp 21689  df-ovol 23758  df-vol 23759  df-mbf 23913  df-itg1 23914  df-itg2 23915  df-ibl 23916  df-0p 23964
This theorem is referenced by:  ftc1anclem6  34361
  Copyright terms: Public domain W3C validator