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 35850
Description: Lemma for ftc1anc 35854, 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 4471 . . . . . . . . 9 (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
21mpteq2ia 5182 . . . . . . . 8 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
32fveq2i 6774 . . . . . . 7 (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
4 ftc1anc.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐷⟶ℂ)
54ffvelrnda 6958 . . . . . . . . . . . . 13 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
6 0cnd 10969 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
75, 6ifclda 4500 . . . . . . . . . . . 12 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
87recld 14903 . . . . . . . . . . 11 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
98adantr 481 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
10 ftc1anc.d . . . . . . . . . . 11 (𝜑𝐷 ⊆ ℝ)
11 rembl 24702 . . . . . . . . . . . 12 ℝ ∈ dom vol
1211a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ dom vol)
138adantr 481 . . . . . . . . . . 11 ((𝜑𝑡𝐷) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
14 eldifn 4067 . . . . . . . . . . . . 13 (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡𝐷)
1514adantl 482 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡𝐷)
16 iffalse 4474 . . . . . . . . . . . . . 14 𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = 0)
1716fveq2d 6775 . . . . . . . . . . . . 13 𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘0))
18 re0 14861 . . . . . . . . . . . . 13 (ℜ‘0) = 0
1917, 18eqtrdi 2796 . . . . . . . . . . . 12 𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = 0)
2015, 19syl 17 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = 0)
21 iftrue 4471 . . . . . . . . . . . . . 14 (𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = (𝐹𝑡))
2221fveq2d 6775 . . . . . . . . . . . . 13 (𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘(𝐹𝑡)))
2322mpteq2ia 5182 . . . . . . . . . . . 12 (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡)))
244feqmptd 6834 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
25 ftc1anc.i . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ 𝐿1)
2624, 25eqeltrrd 2842 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
275iblcn 24961 . . . . . . . . . . . . . 14 (𝜑 → ((𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1 ↔ ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1 ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ 𝐿1)))
2826, 27mpbid 231 . . . . . . . . . . . . 13 (𝜑 → ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1 ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ 𝐿1))
2928simpld 495 . . . . . . . . . . . 12 (𝜑 → (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1)
3023, 29eqeltrid 2845 . . . . . . . . . . 11 (𝜑 → (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ 𝐿1)
3110, 12, 13, 20, 30iblss2 24968 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ 𝐿1)
328recnd 11004 . . . . . . . . . . . . 13 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
3332adantr 481 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
34 eqidd 2741 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
35 absf 15047 . . . . . . . . . . . . . 14 abs:ℂ⟶ℝ
3635a1i 11 . . . . . . . . . . . . 13 (𝜑 → abs:ℂ⟶ℝ)
3736feqmptd 6834 . . . . . . . . . . . 12 (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
38 fveq2 6771 . . . . . . . . . . . 12 (𝑥 = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3933, 34, 37, 38fmptco 6998 . . . . . . . . . . 11 (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
409fmpttd 6986 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ)
41 iblmbf 24930 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
4225, 41syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ MblFn)
4324, 42eqeltrrd 2842 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ MblFn)
445ismbfcn2 24800 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑡𝐷 ↦ (𝐹𝑡)) ∈ MblFn ↔ ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ MblFn)))
4543, 44mpbid 231 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ MblFn))
4645simpld 495 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn)
4723, 46eqeltrid 2845 . . . . . . . . . . . . 13 (𝜑 → (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
4810, 12, 13, 20, 47mbfss 24808 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
49 ftc1anclem1 35846 . . . . . . . . . . . 12 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
5040, 48, 49syl2anc 584 . . . . . . . . . . 11 (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
5139, 50eqeltrrd 2842 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
529, 31, 51iblabsnc 35837 . . . . . . . . 9 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ 𝐿1)
5332abscld 15146 . . . . . . . . . . 11 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ)
5453adantr 481 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ)
5532absge0d 15154 . . . . . . . . . . 11 (𝜑 → 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
5655adantr 481 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
5754, 56iblpos 24955 . . . . . . . . 9 (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ 𝐿1 ↔ ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ)))
5852, 57mpbid 231 . . . . . . . 8 (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ))
5958simprd 496 . . . . . . 7 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ)
603, 59eqeltrrid 2846 . . . . . 6 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ)
61 ltsubrp 12765 . . . . . 6 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))))
6260, 61sylan 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))))) − 𝑌) ∈ ℝ)
6560, 63, 64syl2an 596 . . . . . 6 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
6660adantr 481 . . . . . 6 ((𝜑𝑌 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ)
6765, 66ltnled 11122 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ↔ ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
6862, 67mpbid 231 . . . 4 ((𝜑𝑌 ∈ ℝ+) → ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))
6953rexrd 11026 . . . . . . . . 9 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ*)
70 elxrge0 13188 . . . . . . . . 9 ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞) ↔ ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ* ∧ 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
7169, 55, 70sylanbrc 583 . . . . . . . 8 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞))
7271adantr 481 . . . . . . 7 ((𝜑𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞))
7372fmpttd 6986 . . . . . 6 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))):ℝ⟶(0[,]+∞))
7473adantr 481 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))):ℝ⟶(0[,]+∞))
7565rexrd 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))))) − 𝑌))))
7774, 75, 76syl2anc 584 . . . 4 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))))
7868, 77mtbid 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))))) − 𝑌)))
8078, 79sylibr 233 . 2 ((𝜑𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
8165ad2antrr 723 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
82 itg1cl 24847 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫1𝑔) ∈ ℝ)
8382ad2antlr 724 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫1𝑔) ∈ ℝ)
84 eqid 2740 . . . . . . . . . . . 12 (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
8584i1fpos 24869 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1)
86 0re 10978 . . . . . . . . . . . . . 14 0 ∈ ℝ
87 i1ff 24838 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
8887ffvelrnda 6958 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
89 max1 12918 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (𝑔𝑡) ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
9086, 88, 89sylancr 587 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
9190ralrimiva 3110 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
92 ax-resscn 10929 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
9392a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → ℝ ⊆ ℂ)
94 fvex 6784 . . . . . . . . . . . . . . . . 17 (𝑔𝑡) ∈ V
95 c0ex 10970 . . . . . . . . . . . . . . . . 17 0 ∈ V
9694, 95ifex 4515 . . . . . . . . . . . . . . . 16 if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ V
9796, 84fnmpti 6574 . . . . . . . . . . . . . . 15 (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ
9897a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ)
9993, 980pledm 24835 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 → (0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ (ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
100 reex 10963 . . . . . . . . . . . . . . 15 ℝ ∈ V
101100a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → ℝ ∈ V)
10295a1i 11 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → 0 ∈ V)
103 ifcl 4510 . . . . . . . . . . . . . . 15 (((𝑔𝑡) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
10488, 86, 103sylancl 586 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
105 fconstmpt 5650 . . . . . . . . . . . . . . 15 (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
106105a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
107 eqidd 2741 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
108101, 102, 104, 106, 107ofrfval2 7548 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 → ((ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
10999, 108bitrd 278 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → (0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
11091, 109mpbird 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))))
11285, 110, 111syl2anc 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))) ∈ ℝ)
11485, 113syl 17 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
115112, 114eqeltrd 2841 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
116115ad2antlr 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))))) − 𝑌)))
11865, 82, 117syl2an 596 . . . . . . . . 9 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔) ↔ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
119118biimpar 478 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔))
120 max2 12920 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (𝑔𝑡) ∈ ℝ) → (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
12186, 88, 120sylancr 587 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
122121ralrimiva 3110 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
12387feqmptd 6834 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1𝑔 = (𝑡 ∈ ℝ ↦ (𝑔𝑡)))
124101, 88, 104, 123, 107ofrfval2 7548 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → (𝑔r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
125122, 124mpbird 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))))
12785, 125, 126mpd3an23 1462 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫1𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
128127, 112breqtrrd 5107 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫1𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
129128ad2antlr 724 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫1𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
13081, 83, 116, 119, 129ltletrd 11135 . . . . . . 7 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
131130adantrl 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)
13385, 132syl 17 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
134133adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
135 elrege0 13185 . . . . . . . . . . . . . . . . 17 (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
136104, 90, 135sylanbrc 583 . . . . . . . . . . . . . . . 16 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ (0[,)+∞))
137136fmpttd 6986 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)):ℝ⟶(0[,)+∞))
138137adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)):ℝ⟶(0[,)+∞))
139115adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
140104recnd 11004 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ)
141140negcld 11319 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ)
142140, 141ifcld 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))) ∈ ℂ)
14432, 142, 143syl2an 596 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℂ)
145144anassrs 468 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℂ)
146145abscld 15146 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) ∈ ℝ)
147145absge0d 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))))))
149146, 147, 148sylanbrc 583 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) ∈ (0[,)+∞))
150149fmpttd 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 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
153151, 152ifbieq1d 4489 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → if(𝑥𝐷, (𝐹𝑥), 0) = if(𝑡𝐷, (𝐹𝑡), 0))
154153fveq2d 6775 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
155 eqid 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))
156 fvex 6784 . . . . . . . . . . . . . . . . . . . 20 (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ V
157154, 155, 156fvmpt 6872 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
158154breq2d 5091 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
159 fveq2 6771 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
160159breq2d 5091 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → (0 ≤ (𝑔𝑥) ↔ 0 ≤ (𝑔𝑡)))
161160, 159ifbieq1d 4489 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
162161negeqd 11215 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
163158, 161, 162ifbieq12d 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
16696, 165ifex 4515 . . . . . . . . . . . . . . . . . . . 20 if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ V
167163, 164, 166fvmpt 6872 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
168157, 167oveq12d 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))))
169168fveq2d 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)))))
170169mpteq2ia 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)))))
171170fveq2i 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))))))
172100a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ℝ ∈ V)
173 fvex 6784 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔𝑥) ∈ V
174173, 95ifex 4515 . . . . . . . . . . . . . . . . . . . . 21 if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ V
175174, 95ifex 4515 . . . . . . . . . . . . . . . . . . . 20 if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) ∈ V
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) ∈ V)
177 ovex 7304 . . . . . . . . . . . . . . . . . . . . 21 (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) ∈ V
17895, 177ifex 4515 . . . . . . . . . . . . . . . . . . . 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 6598 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷)
181 frn 6605 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ)
182 ref 14821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℜ:ℂ⟶ℝ
183 ffn 6598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ℜ:ℂ⟶ℝ → ℜ Fn ℂ)
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℜ Fn ℂ
185 fnco 6547 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℜ Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
186184, 185mp3an1 1447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
187180, 181, 186syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷)
188 elpreima 6932 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℜ ∘ 𝐹) Fn 𝐷 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
1894, 187, 1883syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
190 fco 6622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘ 𝐹):𝐷⟶ℝ)
191182, 4, 190sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ)
192191ffvelrnda 6958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ)
193192biantrurd 533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥))))
194 elrege0 13185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥)))
195193, 194bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))
196 fvco3 6864 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹:𝐷⟶ℂ ∧ 𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹𝑥)))
1974, 196sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹𝑥)))
198197breq2d 5091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
199195, 198bitr3d 280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
200199pm5.32da 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
201189, 200bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
202201adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
203 eldif 3902 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥𝐷))
204203baibr 537 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ → (¬ 𝑥𝐷𝑥 ∈ (ℝ ∖ 𝐷)))
205 0le0 12074 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ 0
206205, 18breqtrri 5106 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≤ (ℜ‘0)
207206biantru 530 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐷 ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0)))
208204, 207bitr3di 286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
209208adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
210202, 209orbi12d 916 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → ((𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥))) ∨ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0)))))
211 elun 4088 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)))
212 fveq2 6771 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥) → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘(𝐹𝑥)))
213212breq2d 5091 . . . . . . . . . . . . . . . . . . . . . . 23 (if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥) → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
214 fveq2 6771 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥𝐷, (𝐹𝑥), 0) = 0 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘0))
215214breq2d 5091 . . . . . . . . . . . . . . . . . . . . . . 23 (if(𝑥𝐷, (𝐹𝑥), 0) = 0 → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘0)))
216213, 215elimif 4502 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ ((𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥))) ∨ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
217210, 211, 2163bitr4g 314 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))))
218217ifbid 4488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0))
219218mpteq2dva 5179 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)))
220217ifbid 4488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))))
221220mpteq2dva 5179 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))))
222172, 176, 179, 219, 221offval2 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))))
22487ffvelrnda 6958 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
225224recnd 11004 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℂ)
226 0cn 10968 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℂ
227 ifcl 4510 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
228225, 226, 227sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
229228addid1d 11175 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) + 0) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
230228mulm1d 11427 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
231230oveq2d 7287 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = (0 + -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
232228negcld 11319 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
233232addid2d 11176 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
234231, 233eqtrd 2780 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
235229, 234ifeq12d 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)))
236223, 235eqtrid 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)))
237236mpteq2dva 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))))
238222, 237sylan9eq 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[,)+∞))
243239, 240, 241, 242mp3an 1460 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ∪ (0(,)+∞)) = (0[,)+∞)
244243imaeq2i 5966 . . . . . . . . . . . . . . . . . . . . 21 ((ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = ((ℜ ∘ 𝐹) “ (0[,)+∞))
245 imaundi 6052 . . . . . . . . . . . . . . . . . . . . 21 ((ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞)))
246244, 245eqtr3i 2770 . . . . . . . . . . . . . . . . . . . 20 ((ℜ ∘ 𝐹) “ (0[,)+∞)) = (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞)))
247 ismbfcn 24791 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
2484, 247syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
24942, 248mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))
250249simpld 495 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn)
251 mbfimasn 24794 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ) → ((ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
25286, 251mp3an3 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)
255252, 253, 254syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
256250, 191, 255syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
257246, 256eqeltrid 2845 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol)
2584fdmd 6609 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝐹 = 𝐷)
259 mbfdm 24788 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
26042, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝐹 ∈ dom vol)
261258, 260eqeltrrd 2842 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ dom vol)
262 difmbl 24705 . . . . . . . . . . . . . . . . . . . 20 ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol)
26311, 261, 262sylancr 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℝ ∖ 𝐷) ∈ dom vol)
264 unmbl 24699 . . . . . . . . . . . . . . . . . . 19 ((((ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol ∧ (ℝ ∖ 𝐷) ∈ dom vol) → (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
265257, 263, 264syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
266 fveq2 6771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑥 → (𝑔𝑡) = (𝑔𝑥))
267266breq2d 5091 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑥 → (0 ≤ (𝑔𝑡) ↔ 0 ≤ (𝑔𝑥)))
268267, 266ifbieq1d 4489 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑥 → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
269268, 84, 174fvmpt 6872 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
270269eqcomd 2746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥))
271270ifeq1d 4484 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) = if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥), 0))
272271mpteq2ia 5182 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥), 0))
273272i1fres 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 ∈ ℝ
276275a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → -1 ∈ ℝ)
277274, 276i1fmulc 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[,)+∞)) ∪ (ℝ ∖ 𝐷))))
281280baibr 537 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)))))
282 tru 1546 . . . . . . . . . . . . . . . . . . . . . . . . . 26
283 negex 11219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 -1 ∈ V
284283fconst 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ × {-1}):ℝ⟶{-1}
285 ffn 6598 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℝ × {-1}):ℝ⟶{-1} → (ℝ × {-1}) Fn ℝ)
286284, 285mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → (ℝ × {-1}) Fn ℝ)
28797a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ)
288100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → ℝ ∈ V)
289 inidm 4158 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ℝ ∩ ℝ) = ℝ
290283fvconst2 7076 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((ℝ × {-1})‘𝑥) = -1)
291290adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊤ ∧ 𝑥 ∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1)
292269adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊤ ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
293286, 287, 288, 288, 289, 291, 292ofval 7538 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⊤ ∧ 𝑥 ∈ ℝ) → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
294282, 293mpan 687 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
295294eqcomd 2746 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥))
296281, 295ifbieq1d 4489 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → if(¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
297279, 296eqtr3id 2794 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
298297mpteq2ia 5182 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
299298i1fres 24868 . . . . . . . . . . . . . . . . . . . 20 ((((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ dom ∫1 ∧ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) ∈ dom ∫1)
300277, 278, 299syl2an 596 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 ∧ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) ∈ dom ∫1)
301273, 300i1fadd 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)
30285, 265, 301syl2anr 597 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))))) ∈ dom ∫1)
303238, 302eqeltrrd 2842 . . . . . . . . . . . . . . . 16 ((𝜑𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∈ dom ∫1)
304154cbvmptv 5192 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
305304, 31eqeltrid 2845 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)
3069, 304fmptd 6985 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)
307305, 306jca 512 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
308307adantr 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)))‘𝑡))))) ∈ ℝ)
3103093expb 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)))‘𝑡))))) ∈ ℝ)
311303, 308, 310syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡))))) ∈ ℝ)
312171, 311eqeltrrid 2846 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) ∈ ℝ)
313134, 138, 139, 150, 312itg2addnc 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))))))))
314100a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑔 ∈ dom ∫1) → ℝ ∈ V)
31596a1i 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))))))
318314, 315, 146, 316, 317offval2 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)))))))
319318fveq2d 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))))))))
320313, 319eqtr3d 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))))))))
321320adantr 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))))
326323, 324, 325nfbr 5126 . . . . . . . . . . . . . 14 𝑡 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
327322, 326nfan 1906 . . . . . . . . . . . . 13 𝑡((𝜑𝑔 ∈ dom ∫1) ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
328 anass 469 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)))
32987ffnd 6599 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
330 fvex 6784 . . . . . . . . . . . . . . . . . . . . . 22 (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ V
331 eqid 2740 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
332330, 331fnmpti 6574 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) Fn ℝ
333332a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) Fn ℝ)
334 eqidd 2741 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) = (𝑔𝑡))
335331fvmpt2 6883 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ∧ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
336330, 335mpan2 688 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
337336adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
338329, 333, 101, 101, 289, 334, 337ofrval 7539 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3393383com23 1125 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3403393expa 1117 . . . . . . . . . . . . . . . . 17 (((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
341340adantll 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)) ∈ ℝ)
3438, 104, 342syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
344343ad2antrr 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)))
3468, 345sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
347346breq2d 5091 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
348347biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
349348an32s 649 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
350349adantllr 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))))
353351, 352ifboth 4504 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
354350, 353sylancom 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))))
3568, 104, 355syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
357356ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
358354, 357mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
359344, 358absidd 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))
361360oveq2d 7287 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
362361fveq2d 6775 . . . . . . . . . . . . . . . . . . . . 21 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
363362adantl 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))))
3648ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
365345oveq1d 7286 . . . . . . . . . . . . . . . . . . . . 21 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
366364, 365sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
367359, 363, 3663eqtr4d 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)))
368104renegcld 11402 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
369 resubcl 11285 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
3708, 368, 369syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
371370ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
37288ad3antlr 728 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ∈ ℝ)
3738ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
3748adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
375 ltnle 11055 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
37686, 375mpan2 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
377 ltle 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
37886, 377mpan2 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
379376, 378sylbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
380379imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
381 absnid 15008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
382380, 381syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
383382breq2d 5091 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
384383biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
385384an32s 649 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
386374, 385sylanl1 677 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
387372, 373, 386lenegcon2d 11558 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡))
388 simpll 764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → 𝜑)
38986a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 ∈ ℝ)
3908, 389ltnled 11122 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3918, 86, 377sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
392390, 391sylbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
393392imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
394388, 393sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
395 negeq 11213 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔𝑡) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → -(𝑔𝑡) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
396395breq2d 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))
399397, 398eqtr3id 2794 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → 0 = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
400399breq2d 5091 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
401396, 400ifboth 4504 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡) ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
402387, 394, 401syl2anc 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)))
4048, 368, 403syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
405404ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
406402, 405mpbird 256 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0)
407371, 406absnidd 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)))
409408negeqd 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)))
411409, 410eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
41232, 140, 411syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
413412ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
414407, 413eqtrd 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))
416415oveq2d 7287 . . . . . . . . . . . . . . . . . . . . . 22 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
417416fveq2d 6775 . . . . . . . . . . . . . . . . . . . . 21 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
418417adantl 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))))
4198, 381sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
420393, 419syldan 591 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
421420oveq1d 7286 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
422388, 421sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
423414, 418, 4223eqtr4d 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)))
424367, 423pm2.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)))
425424oveq2d 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))))
42653recnd 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))))
428140, 426, 427syl2anr 597 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
429428adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
430425, 429eqtrd 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))))
431341, 430syldan 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))))
432328, 431sylanb 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))))
433432an32s 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))))
434327, 433mpteq2da 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)))))
435434fveq2d 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))))))
436321, 435eqtrd 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))))))
437436breq1d 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))) + 𝑌)))
438437adantllr 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))) + 𝑌)))
439312adantlr 712 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) ∈ ℝ)
44063ad2antlr 724 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → 𝑌 ∈ ℝ)
441115adantl 482 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
442439, 440, 441ltadd2d 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))) + 𝑌)))
443442adantr 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))) + 𝑌)))
44560, 63, 115, 444syl3an 1159 . . . . . . . . . 10 ((𝜑𝑌 ∈ ℝ+𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
4464453expa 1117 . . . . . . . . 9 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
447446adantr 481 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
448438, 443, 4473bitr4d 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)))))
449448adantrr 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)))))
450131, 449mpbird 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)))))) < 𝑌)
451450ex 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)))))) < 𝑌))
452451reximdva 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)))‘𝑡))
454453, 167sylan9eq 2800 . . . . . . . . . . . . 13 ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
455454oveq2d 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))))
456455fveq2d 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)))))
457456mpteq2dva 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))))))
458457fveq2d 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)))))))
459458breq1d 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)))))) < 𝑌))
460459rspcev 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)) − (𝑓𝑡))))) < 𝑌)
461460ex 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)) − (𝑓𝑡))))) < 𝑌))
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 3215 . . . 4 (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌))
464463adantr 481 . . 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(𝑔r ≤ (𝑡 ∈ ℝ ↦ (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 205  wa 396  wo 844   = wceq 1542  wtru 1543  wcel 2110  wral 3066  wrex 3067  Vcvv 3431  cdif 3889  cun 3890  wss 3892  ifcif 4465  {csn 4567   class class class wbr 5079  cmpt 5162   × cxp 5588  ccnv 5589  dom cdm 5590  ran crn 5591  cima 5593  ccom 5594   Fn wfn 6427  wf 6428  cfv 6432  (class class class)co 7271  f cof 7525  r cofr 7526  cc 10870  cr 10871  0cc0 10872  1c1 10873   + caddc 10875   · cmul 10877  +∞cpnf 11007  *cxr 11009   < clt 11010  cle 11011  cmin 11205  -cneg 11206  +crp 12729  (,)cioo 13078  [,)cico 13080  [,]cicc 13081  cre 14806  cim 14807  abscabs 14943  volcvol 24625  MblFncmbf 24776  1citg1 24777  2citg2 24778  𝐿1cibl 24779  citg 24780  0𝑝c0p 24831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-inf2 9377  ax-cnex 10928  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-addrcl 10933  ax-mulcl 10934  ax-mulrcl 10935  ax-mulcom 10936  ax-addass 10937  ax-mulass 10938  ax-distr 10939  ax-i2m1 10940  ax-1ne0 10941  ax-1rid 10942  ax-rnegex 10943  ax-rrecex 10944  ax-cnre 10945  ax-pre-lttri 10946  ax-pre-lttrn 10947  ax-pre-ltadd 10948  ax-pre-mulgt0 10949  ax-pre-sup 10950  ax-addf 10951
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rmo 3074  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-disj 5045  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-se 5546  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6201  df-ord 6268  df-on 6269  df-lim 6270  df-suc 6271  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-isom 6441  df-riota 7228  df-ov 7274  df-oprab 7275  df-mpo 7276  df-of 7527  df-ofr 7528  df-om 7707  df-1st 7824  df-2nd 7825  df-frecs 8088  df-wrecs 8119  df-recs 8193  df-rdg 8232  df-1o 8288  df-2o 8289  df-er 8481  df-map 8600  df-pm 8601  df-en 8717  df-dom 8718  df-sdom 8719  df-fin 8720  df-fi 9148  df-sup 9179  df-inf 9180  df-oi 9247  df-dju 9660  df-card 9698  df-pnf 11012  df-mnf 11013  df-xr 11014  df-ltxr 11015  df-le 11016  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-4 12038  df-n0 12234  df-z 12320  df-uz 12582  df-q 12688  df-rp 12730  df-xneg 12847  df-xadd 12848  df-xmul 12849  df-ioo 13082  df-ico 13084  df-icc 13085  df-fz 13239  df-fzo 13382  df-fl 13510  df-mod 13588  df-seq 13720  df-exp 13781  df-hash 14043  df-cj 14808  df-re 14809  df-im 14810  df-sqrt 14944  df-abs 14945  df-clim 15195  df-sum 15396  df-rest 17131  df-topgen 17152  df-psmet 20587  df-xmet 20588  df-met 20589  df-bl 20590  df-mopn 20591  df-top 22041  df-topon 22058  df-bases 22094  df-cmp 22536  df-ovol 24626  df-vol 24627  df-mbf 24781  df-itg1 24782  df-itg2 24783  df-ibl 24784  df-0p 24832
This theorem is referenced by:  ftc1anclem6  35851
  Copyright terms: Public domain W3C validator