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 35133
Description: Lemma for ftc1anc 35137, 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 4434 . . . . . . . . 9 (𝑡 ∈ ℝ → if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
21mpteq2ia 5124 . . . . . . . 8 (𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0)) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
32fveq2i 6652 . . . . . . 7 (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) = (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
4 ftc1anc.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐷⟶ℂ)
54ffvelrnda 6832 . . . . . . . . . . . . 13 ((𝜑𝑡𝐷) → (𝐹𝑡) ∈ ℂ)
6 0cnd 10627 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑡𝐷) → 0 ∈ ℂ)
75, 6ifclda 4462 . . . . . . . . . . . 12 (𝜑 → if(𝑡𝐷, (𝐹𝑡), 0) ∈ ℂ)
87recld 14549 . . . . . . . . . . 11 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
98adantr 484 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
10 ftc1anc.d . . . . . . . . . . 11 (𝜑𝐷 ⊆ ℝ)
11 rembl 24148 . . . . . . . . . . . 12 ℝ ∈ dom vol
1211a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ ∈ dom vol)
138adantr 484 . . . . . . . . . . 11 ((𝜑𝑡𝐷) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
14 eldifn 4058 . . . . . . . . . . . . 13 (𝑡 ∈ (ℝ ∖ 𝐷) → ¬ 𝑡𝐷)
1514adantl 485 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → ¬ 𝑡𝐷)
16 iffalse 4437 . . . . . . . . . . . . . 14 𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = 0)
1716fveq2d 6653 . . . . . . . . . . . . 13 𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘0))
18 re0 14507 . . . . . . . . . . . . 13 (ℜ‘0) = 0
1917, 18eqtrdi 2852 . . . . . . . . . . . 12 𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = 0)
2015, 19syl 17 . . . . . . . . . . 11 ((𝜑𝑡 ∈ (ℝ ∖ 𝐷)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = 0)
21 iftrue 4434 . . . . . . . . . . . . . 14 (𝑡𝐷 → if(𝑡𝐷, (𝐹𝑡), 0) = (𝐹𝑡))
2221fveq2d 6653 . . . . . . . . . . . . 13 (𝑡𝐷 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) = (ℜ‘(𝐹𝑡)))
2322mpteq2ia 5124 . . . . . . . . . . . 12 (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡)))
244feqmptd 6712 . . . . . . . . . . . . . . 15 (𝜑𝐹 = (𝑡𝐷 ↦ (𝐹𝑡)))
25 ftc1anc.i . . . . . . . . . . . . . . 15 (𝜑𝐹 ∈ 𝐿1)
2624, 25eqeltrrd 2894 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1)
275iblcn 24406 . . . . . . . . . . . . . 14 (𝜑 → ((𝑡𝐷 ↦ (𝐹𝑡)) ∈ 𝐿1 ↔ ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1 ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ 𝐿1)))
2826, 27mpbid 235 . . . . . . . . . . . . 13 (𝜑 → ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1 ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ 𝐿1))
2928simpld 498 . . . . . . . . . . . 12 (𝜑 → (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ 𝐿1)
3023, 29eqeltrid 2897 . . . . . . . . . . 11 (𝜑 → (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ 𝐿1)
3110, 12, 13, 20, 30iblss2 24413 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ 𝐿1)
328recnd 10662 . . . . . . . . . . . . 13 (𝜑 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
3332adantr 484 . . . . . . . . . . . 12 ((𝜑𝑡 ∈ ℝ) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ)
34 eqidd 2802 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
35 absf 14693 . . . . . . . . . . . . . 14 abs:ℂ⟶ℝ
3635a1i 11 . . . . . . . . . . . . 13 (𝜑 → abs:ℂ⟶ℝ)
3736feqmptd 6712 . . . . . . . . . . . 12 (𝜑 → abs = (𝑥 ∈ ℂ ↦ (abs‘𝑥)))
38 fveq2 6649 . . . . . . . . . . . 12 (𝑥 = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘𝑥) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3933, 34, 37, 38fmptco 6872 . . . . . . . . . . 11 (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
409fmpttd 6860 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ)
41 iblmbf 24375 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ 𝐿1𝐹 ∈ MblFn)
4225, 41syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹 ∈ MblFn)
4324, 42eqeltrrd 2894 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑡𝐷 ↦ (𝐹𝑡)) ∈ MblFn)
445ismbfcn2 24246 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑡𝐷 ↦ (𝐹𝑡)) ∈ MblFn ↔ ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ MblFn)))
4543, 44mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn ∧ (𝑡𝐷 ↦ (ℑ‘(𝐹𝑡))) ∈ MblFn))
4645simpld 498 . . . . . . . . . . . . . 14 (𝜑 → (𝑡𝐷 ↦ (ℜ‘(𝐹𝑡))) ∈ MblFn)
4723, 46eqeltrid 2897 . . . . . . . . . . . . 13 (𝜑 → (𝑡𝐷 ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
4810, 12, 13, 20, 47mbfss 24254 . . . . . . . . . . . 12 (𝜑 → (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn)
49 ftc1anclem1 35129 . . . . . . . . . . . 12 (((𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))):ℝ⟶ℝ ∧ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ MblFn) → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
5040, 48, 49syl2anc 587 . . . . . . . . . . 11 (𝜑 → (abs ∘ (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
5139, 50eqeltrrd 2894 . . . . . . . . . 10 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn)
529, 31, 51iblabsnc 35120 . . . . . . . . 9 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ 𝐿1)
5332abscld 14792 . . . . . . . . . . 11 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ)
5453adantr 484 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ)
5532absge0d 14800 . . . . . . . . . . 11 (𝜑 → 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
5655adantr 484 . . . . . . . . . 10 ((𝜑𝑡 ∈ ℝ) → 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
5754, 56iblpos 24400 . . . . . . . . 9 (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ 𝐿1 ↔ ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ)))
5852, 57mpbid 235 . . . . . . . 8 (𝜑 → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∈ MblFn ∧ (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ))
5958simprd 499 . . . . . . 7 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ if(𝑡 ∈ ℝ, (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))), 0))) ∈ ℝ)
603, 59eqeltrrid 2898 . . . . . 6 (𝜑 → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ)
61 ltsubrp 12417 . . . . . 6 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))))
6260, 61sylan 583 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))))
63 rpre 12389 . . . . . . 7 (𝑌 ∈ ℝ+𝑌 ∈ ℝ)
64 resubcl 10943 . . . . . . 7 (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ ∧ 𝑌 ∈ ℝ) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
6560, 63, 64syl2an 598 . . . . . 6 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
6660adantr 484 . . . . . 6 ((𝜑𝑌 ∈ ℝ+) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ∈ ℝ)
6765, 66ltnled 10780 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ↔ ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
6862, 67mpbid 235 . . . 4 ((𝜑𝑌 ∈ ℝ+) → ¬ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))
6953rexrd 10684 . . . . . . . . 9 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ*)
70 elxrge0 12839 . . . . . . . . 9 ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞) ↔ ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℝ* ∧ 0 ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
7169, 55, 70sylanbrc 586 . . . . . . . 8 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞))
7271adantr 484 . . . . . . 7 ((𝜑𝑡 ∈ ℝ) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ (0[,]+∞))
7372fmpttd 6860 . . . . . 6 (𝜑 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))):ℝ⟶(0[,]+∞))
7473adantr 484 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))):ℝ⟶(0[,]+∞))
7565rexrd 10684 . . . . 5 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ*)
76 itg2leub 24342 . . . . 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 587 . . . 4 ((𝜑𝑌 ∈ ℝ+) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ↔ ∀𝑔 ∈ dom ∫1(𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))))
7868, 77mtbid 327 . . 3 ((𝜑𝑌 ∈ ℝ+) → ¬ ∀𝑔 ∈ dom ∫1(𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
79 rexanali 3227 . . 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 237 . 2 ((𝜑𝑌 ∈ ℝ+) → ∃𝑔 ∈ dom ∫1(𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
8165ad2antrr 725 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ)
82 itg1cl 24293 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫1𝑔) ∈ ℝ)
8382ad2antlr 726 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫1𝑔) ∈ ℝ)
84 eqid 2801 . . . . . . . . . . . 12 (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
8584i1fpos 24314 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1)
86 0re 10636 . . . . . . . . . . . . . 14 0 ∈ ℝ
87 i1ff 24284 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1𝑔:ℝ⟶ℝ)
8887ffvelrnda 6832 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ∈ ℝ)
89 max1 12570 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (𝑔𝑡) ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
9086, 88, 89sylancr 590 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
9190ralrimiva 3152 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
92 ax-resscn 10587 . . . . . . . . . . . . . . 15 ℝ ⊆ ℂ
9392a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → ℝ ⊆ ℂ)
94 fvex 6662 . . . . . . . . . . . . . . . . 17 (𝑔𝑡) ∈ V
95 c0ex 10628 . . . . . . . . . . . . . . . . 17 0 ∈ V
9694, 95ifex 4476 . . . . . . . . . . . . . . . 16 if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ V
9796, 84fnmpti 6467 . . . . . . . . . . . . . . 15 (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ
9897a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ)
9993, 980pledm 24281 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 → (0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ (ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
100 reex 10621 . . . . . . . . . . . . . . 15 ℝ ∈ V
101100a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → ℝ ∈ V)
10295a1i 11 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → 0 ∈ V)
103 ifcl 4472 . . . . . . . . . . . . . . 15 (((𝑔𝑡) ∈ ℝ ∧ 0 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
10488, 86, 103sylancl 589 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
105 fconstmpt 5582 . . . . . . . . . . . . . . 15 (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0)
106105a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (ℝ × {0}) = (𝑡 ∈ ℝ ↦ 0))
107 eqidd 2802 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
108101, 102, 104, 106, 107ofrfval2 7411 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 → ((ℝ × {0}) ∘r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
10999, 108bitrd 282 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → (0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
11091, 109mpbird 260 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 → 0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
111 itg2itg1 24344 . . . . . . . . . . 11 (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 ∧ 0𝑝r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
11285, 110, 111syl2anc 587 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
113 itg1cl 24293 . . . . . . . . . . 11 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
11485, 113syl 17 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
115112, 114eqeltrd 2893 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
116115ad2antlr 726 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
117 ltnle 10713 . . . . . . . . . 10 ((((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) ∈ ℝ ∧ (∫1𝑔) ∈ ℝ) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔) ↔ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
11865, 82, 117syl2an 598 . . . . . . . . 9 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔) ↔ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)))
119118biimpar 481 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫1𝑔))
120 max2 12572 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (𝑔𝑡) ∈ ℝ) → (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
12186, 88, 120sylancr 590 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
122121ralrimiva 3152 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → ∀𝑡 ∈ ℝ (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
12387feqmptd 6712 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1𝑔 = (𝑡 ∈ ℝ ↦ (𝑔𝑡)))
124101, 88, 104, 123, 107ofrfval2 7411 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 → (𝑔r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ ∀𝑡 ∈ ℝ (𝑔𝑡) ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
125122, 124mpbird 260 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1𝑔r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
126 itg1le 24321 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1 ∧ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1𝑔r ≤ (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) → (∫1𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
12785, 125, 126mpd3an23 1460 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 → (∫1𝑔) ≤ (∫1‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
128127, 112breqtrrd 5061 . . . . . . . . 9 (𝑔 ∈ dom ∫1 → (∫1𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
129128ad2antlr 726 . . . . . . . 8 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → (∫1𝑔) ≤ (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
13081, 83, 116, 119, 129ltletrd 10793 . . . . . . 7 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌)) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
131130adantrl 715 . . . . . 6 ((((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ (∫1𝑔) ≤ ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌))) → ((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
132 i1fmbf 24283 . . . . . . . . . . . . . . . 16 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
13385, 132syl 17 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
134133adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ MblFn)
135 elrege0 12836 . . . . . . . . . . . . . . . . 17 (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ (0[,)+∞) ↔ (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ ∧ 0 ≤ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
136104, 90, 135sylanbrc 586 . . . . . . . . . . . . . . . 16 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ (0[,)+∞))
137136fmpttd 6860 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)):ℝ⟶(0[,)+∞))
138137adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)):ℝ⟶(0[,)+∞))
139115adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
140104recnd 10662 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ)
141140negcld 10977 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ)
142140, 141ifcld 4473 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℂ)
143 subcl 10878 . . . . . . . . . . . . . . . . . . 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 598 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℂ)
145144anassrs 471 . . . . . . . . . . . . . . . . 17 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℂ)
146145abscld 14792 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) ∈ ℝ)
147145absge0d 14800 . . . . . . . . . . . . . . . 16 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → 0 ≤ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))
148 elrege0 12836 . . . . . . . . . . . . . . . 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 586 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) ∈ (0[,)+∞))
150149fmpttd 6860 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))):ℝ⟶(0[,)+∞))
151 eleq1w 2875 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → (𝑥𝐷𝑡𝐷))
152 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → (𝐹𝑥) = (𝐹𝑡))
153151, 152ifbieq1d 4451 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → if(𝑥𝐷, (𝐹𝑥), 0) = if(𝑡𝐷, (𝐹𝑡), 0))
154153fveq2d 6653 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
155 eqid 2801 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))
156 fvex 6662 . . . . . . . . . . . . . . . . . . . 20 (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ V
157154, 155, 156fvmpt 6749 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
158154breq2d 5045 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
159 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑡 → (𝑔𝑥) = (𝑔𝑡))
160159breq2d 5045 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑡 → (0 ≤ (𝑔𝑥) ↔ 0 ≤ (𝑔𝑡)))
161160, 159ifbieq1d 4451 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
162161negeqd 10873 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = 𝑡 → -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
163158, 161, 162ifbieq12d 4455 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑡 → if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
164 eqid 2801 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
165 negex 10877 . . . . . . . . . . . . . . . . . . . . 21 -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ V
16696, 165ifex 4476 . . . . . . . . . . . . . . . . . . . 20 if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ V
167163, 164, 166fvmpt 6749 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ ℝ → ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
168157, 167oveq12d 7157 . . . . . . . . . . . . . . . . . 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 6653 . . . . . . . . . . . . . . . . 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 5124 . . . . . . . . . . . . . . . 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 6652 . . . . . . . . . . . . . . 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 6662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔𝑥) ∈ V
174173, 95ifex 4476 . . . . . . . . . . . . . . . . . . . . 21 if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ V
175174, 95ifex 4476 . . . . . . . . . . . . . . . . . . . 20 if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) ∈ V
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ ℝ) → if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) ∈ V)
177 ovex 7172 . . . . . . . . . . . . . . . . . . . . 21 (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) ∈ V
17895, 177ifex 4476 . . . . . . . . . . . . . . . . . . . 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 6491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐷⟶ℂ → 𝐹 Fn 𝐷)
181 frn 6497 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:𝐷⟶ℂ → ran 𝐹 ⊆ ℂ)
182 ref 14467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ℜ:ℂ⟶ℝ
183 ffn 6491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (ℜ:ℂ⟶ℝ → ℜ Fn ℂ)
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ℜ Fn ℂ
185 fnco 6441 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℜ Fn ℂ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
186184, 185mp3an1 1445 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 Fn 𝐷 ∧ ran 𝐹 ⊆ ℂ) → (ℜ ∘ 𝐹) Fn 𝐷)
187180, 181, 186syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:𝐷⟶ℂ → (ℜ ∘ 𝐹) Fn 𝐷)
188 elpreima 6809 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((ℜ ∘ 𝐹) Fn 𝐷 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
1894, 187, 1883syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞))))
190 fco 6509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((ℜ:ℂ⟶ℝ ∧ 𝐹:𝐷⟶ℂ) → (ℜ ∘ 𝐹):𝐷⟶ℝ)
191182, 4, 190sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝜑 → (ℜ ∘ 𝐹):𝐷⟶ℝ)
192191ffvelrnda 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ)
193192biantrurd 536 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥))))
194 elrege0 12836 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ (((ℜ ∘ 𝐹)‘𝑥) ∈ ℝ ∧ 0 ≤ ((ℜ ∘ 𝐹)‘𝑥)))
195193, 194syl6bbr 292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)))
196 fvco3 6741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹:𝐷⟶ℂ ∧ 𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹𝑥)))
1974, 196sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑥𝐷) → ((ℜ ∘ 𝐹)‘𝑥) = (ℜ‘(𝐹𝑥)))
198197breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐷) → (0 ≤ ((ℜ ∘ 𝐹)‘𝑥) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
199195, 198bitr3d 284 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑥𝐷) → (((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
200199pm5.32da 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑥𝐷 ∧ ((ℜ ∘ 𝐹)‘𝑥) ∈ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
201189, 200bitrd 282 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
202201adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ↔ (𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥)))))
203 eldif 3894 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥𝐷))
204203baibr 540 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ → (¬ 𝑥𝐷𝑥 ∈ (ℝ ∖ 𝐷)))
205 0le0 11730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ 0
206205, 18breqtrri 5060 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≤ (ℜ‘0)
207206biantru 533 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐷 ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0)))
208204, 207bitr3di 289 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
209208adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ 𝐷) ↔ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
210202, 209orbi12d 916 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥 ∈ ℝ) → ((𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)) ↔ ((𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥))) ∨ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0)))))
211 elun 4079 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ (𝑥 ∈ ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∨ 𝑥 ∈ (ℝ ∖ 𝐷)))
212 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥) → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘(𝐹𝑥)))
213212breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . 23 (if(𝑥𝐷, (𝐹𝑥), 0) = (𝐹𝑥) → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘(𝐹𝑥))))
214 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥𝐷, (𝐹𝑥), 0) = 0 → (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) = (ℜ‘0))
215214breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . 23 (if(𝑥𝐷, (𝐹𝑥), 0) = 0 → (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ 0 ≤ (ℜ‘0)))
216213, 215elimif 4464 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)) ↔ ((𝑥𝐷 ∧ 0 ≤ (ℜ‘(𝐹𝑥))) ∨ (¬ 𝑥𝐷 ∧ 0 ≤ (ℜ‘0))))
217210, 211, 2163bitr4g 317 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑥 ∈ ℝ) → (𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))))
218217ifbid 4450 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) = if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0))
219218mpteq2dva 5128 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)))
220217ifbid 4450 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ ℝ) → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))))
221220mpteq2dva 5128 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))))
222172, 176, 179, 219, 221offval2 7410 . . . . . . . . . . . . . . . . . 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 7236 . . . . . . . . . . . . . . . . . . . 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 6832 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℝ)
225224recnd 10662 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (𝑔𝑥) ∈ ℂ)
226 0cn 10626 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℂ
227 ifcl 4472 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
228225, 226, 227sylancl 589 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
229228addid1d 10833 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) + 0) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
230228mulm1d 11085 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
231230oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = (0 + -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
232228negcld 10977 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) ∈ ℂ)
233232addid2d 10834 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
234231, 233eqtrd 2836 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1𝑥 ∈ ℝ) → (0 + (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
235229, 234ifeq12d 4448 . . . . . . . . . . . . . . . . . . . 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 2848 . . . . . . . . . . . . . . . . . . 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 5128 . . . . . . . . . . . . . . . . . 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 2856 . . . . . . . . . . . . . . . . 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 10681 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
240 pnfxr 10688 . . . . . . . . . . . . . . . . . . . . . . 23 +∞ ∈ ℝ*
241 0ltpnf 12509 . . . . . . . . . . . . . . . . . . . . . . 23 0 < +∞
242 snunioo 12860 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) → ({0} ∪ (0(,)+∞)) = (0[,)+∞))
243239, 240, 241, 242mp3an 1458 . . . . . . . . . . . . . . . . . . . . . 22 ({0} ∪ (0(,)+∞)) = (0[,)+∞)
244243imaeq2i 5898 . . . . . . . . . . . . . . . . . . . . 21 ((ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = ((ℜ ∘ 𝐹) “ (0[,)+∞))
245 imaundi 5979 . . . . . . . . . . . . . . . . . . . . 21 ((ℜ ∘ 𝐹) “ ({0} ∪ (0(,)+∞))) = (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞)))
246244, 245eqtr3i 2826 . . . . . . . . . . . . . . . . . . . 20 ((ℜ ∘ 𝐹) “ (0[,)+∞)) = (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞)))
247 ismbfcn 24237 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:𝐷⟶ℂ → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
2484, 247syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹 ∈ MblFn ↔ ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn)))
24942, 248mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℑ ∘ 𝐹) ∈ MblFn))
250249simpld 498 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (ℜ ∘ 𝐹) ∈ MblFn)
251 mbfimasn 24240 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ ∧ 0 ∈ ℝ) → ((ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
25286, 251mp3an3 1447 . . . . . . . . . . . . . . . . . . . . . 22 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((ℜ ∘ 𝐹) “ {0}) ∈ dom vol)
253 mbfima 24238 . . . . . . . . . . . . . . . . . . . . . 22 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → ((ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol)
254 unmbl 24145 . . . . . . . . . . . . . . . . . . . . . 22 ((((ℜ ∘ 𝐹) “ {0}) ∈ dom vol ∧ ((ℜ ∘ 𝐹) “ (0(,)+∞)) ∈ dom vol) → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
255252, 253, 254syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (((ℜ ∘ 𝐹) ∈ MblFn ∧ (ℜ ∘ 𝐹):𝐷⟶ℝ) → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
256250, 191, 255syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((ℜ ∘ 𝐹) “ {0}) ∪ ((ℜ ∘ 𝐹) “ (0(,)+∞))) ∈ dom vol)
257246, 256eqeltrid 2897 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol)
2584fdmd 6501 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝐹 = 𝐷)
259 mbfdm 24234 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
26042, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → dom 𝐹 ∈ dom vol)
261258, 260eqeltrrd 2894 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐷 ∈ dom vol)
262 difmbl 24151 . . . . . . . . . . . . . . . . . . . 20 ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) → (ℝ ∖ 𝐷) ∈ dom vol)
26311, 261, 262sylancr 590 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℝ ∖ 𝐷) ∈ dom vol)
264 unmbl 24145 . . . . . . . . . . . . . . . . . . 19 ((((ℜ ∘ 𝐹) “ (0[,)+∞)) ∈ dom vol ∧ (ℝ ∖ 𝐷) ∈ dom vol) → (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
265257, 263, 264syl2anc 587 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol)
266 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 = 𝑥 → (𝑔𝑡) = (𝑔𝑥))
267266breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑡 = 𝑥 → (0 ≤ (𝑔𝑡) ↔ 0 ≤ (𝑔𝑥)))
268267, 266ifbieq1d 4451 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑡 = 𝑥 → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
269268, 84, 174fvmpt 6749 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
270269eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0) = ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥))
271270ifeq1d 4446 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0) = if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥), 0))
272271mpteq2ia 5124 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥), 0))
273272i1fres 24313 . . . . . . . . . . . . . . . . . . 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 11744 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
276275a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → -1 ∈ ℝ)
277274, 276i1fmulc 24311 . . . . . . . . . . . . . . . . . . . 20 ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 → ((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ dom ∫1)
278 cmmbl 24142 . . . . . . . . . . . . . . . . . . . 20 ((((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol → (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol)
279 ifnot 4478 . . . . . . . . . . . . . . . . . . . . . . 23 if(¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)), 0) = if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
280 eldif 3894 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))))
281280baibr 540 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ↔ 𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)))))
282 tru 1542 . . . . . . . . . . . . . . . . . . . . . . . . . 26
283 negex 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 -1 ∈ V
284283fconst 6543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ × {-1}):ℝ⟶{-1}
285 ffn 6491 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℝ × {-1}):ℝ⟶{-1} → (ℝ × {-1}) Fn ℝ)
286284, 285mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → (ℝ × {-1}) Fn ℝ)
28797a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) Fn ℝ)
288100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊤ → ℝ ∈ V)
289 inidm 4148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ℝ ∩ ℝ) = ℝ
290283fvconst2 6947 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑥 ∈ ℝ → ((ℝ × {-1})‘𝑥) = -1)
291290adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊤ ∧ 𝑥 ∈ ℝ) → ((ℝ × {-1})‘𝑥) = -1)
292269adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊤ ∧ 𝑥 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))‘𝑥) = if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))
293286, 287, 288, 288, 289, 291, 292ofval 7402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⊤ ∧ 𝑥 ∈ ℝ) → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
294282, 293mpan 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 ∈ ℝ → (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥) = (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))
295294eqcomd 2807 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℝ → (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)) = (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥))
296281, 295ifbieq1d 4451 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℝ → if(¬ 𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)), 0) = if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
297279, 296syl5eqr 2850 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℝ → if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) = if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
298297mpteq2ia 5124 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))), (((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))‘𝑥), 0))
299298i1fres 24313 . . . . . . . . . . . . . . . . . . . 20 ((((ℝ × {-1}) ∘f · (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ dom ∫1 ∧ (ℝ ∖ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷))) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) ∈ dom ∫1)
300277, 278, 299syl2an 598 . . . . . . . . . . . . . . . . . . 19 (((𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ dom ∫1 ∧ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)) ∈ dom vol) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))) ∈ dom ∫1)
301273, 300i1fadd 24303 . . . . . . . . . . . . . . . . . 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 599 . . . . . . . . . . . . . . . . 17 ((𝜑𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), 0)) ∘f + (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (((ℜ ∘ 𝐹) “ (0[,)+∞)) ∪ (ℝ ∖ 𝐷)), 0, (-1 · if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))))) ∈ dom ∫1)
303238, 302eqeltrrd 2894 . . . . . . . . . . . . . . . 16 ((𝜑𝑔 ∈ dom ∫1) → (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∈ dom ∫1)
304154cbvmptv 5136 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) = (𝑡 ∈ ℝ ↦ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
305304, 31eqeltrid 2897 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1)
3069, 304fmptd 6859 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ)
307305, 306jca 515 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
308307adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑔 ∈ dom ∫1) → ((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))) ∈ 𝐿1 ∧ (𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0))):ℝ⟶ℝ))
309 ftc1anclem4 35132 . . . . . . . . . . . . . . . . 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 1117 . . . . . . . . . . . . . . . 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 587 . . . . . . . . . . . . . . 15 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(((𝑥 ∈ ℝ ↦ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)))‘𝑡) − ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡))))) ∈ ℝ)
312171, 311eqeltrrid 2898 . . . . . . . . . . . . . 14 ((𝜑𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) ∈ ℝ)
313134, 138, 139, 150, 312itg2addnc 35110 . . . . . . . . . . . . 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 2802 . . . . . . . . . . . . . . 15 ((𝜑𝑔 ∈ dom ∫1) → (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
317 eqidd 2802 . . . . . . . . . . . . . . 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 7410 . . . . . . . . . . . . . 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 6653 . . . . . . . . . . . . 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 2838 . . . . . . . . . . . 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 484 . . . . . . . . . . 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 1915 . . . . . . . . . . . . . 14 𝑡(𝜑𝑔 ∈ dom ∫1)
323 nfcv 2958 . . . . . . . . . . . . . . 15 𝑡𝑔
324 nfcv 2958 . . . . . . . . . . . . . . 15 𝑡r
325 nfmpt1 5131 . . . . . . . . . . . . . . 15 𝑡(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
326323, 324, 325nfbr 5080 . . . . . . . . . . . . . 14 𝑡 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
327322, 326nfan 1900 . . . . . . . . . . . . 13 𝑡((𝜑𝑔 ∈ dom ∫1) ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))))
328 anass 472 . . . . . . . . . . . . . . 15 (((𝜑𝑔 ∈ dom ∫1) ∧ 𝑡 ∈ ℝ) ↔ (𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)))
32987ffnd 6492 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1𝑔 Fn ℝ)
330 fvex 6662 . . . . . . . . . . . . . . . . . . . . . 22 (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ V
331 eqid 2801 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) = (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
332330, 331fnmpti 6467 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) Fn ℝ
333332a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 → (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) Fn ℝ)
334 eqidd 2802 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → (𝑔𝑡) = (𝑔𝑡))
335331fvmpt2 6760 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑡 ∈ ℝ ∧ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ V) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
336330, 335mpan2 690 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ ℝ → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
337336adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → ((𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))‘𝑡) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
338329, 333, 101, 101, 289, 334, 337ofrval 7403 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 𝑡 ∈ ℝ) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3393383com23 1123 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3403393expa 1115 . . . . . . . . . . . . . . . . 17 (((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
341340adantll 713 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ 𝑔r ≤ (𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) → (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
342 resubcl 10943 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
3438, 104, 342syl2an 598 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
344343ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
345 absid 14652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
3468, 345sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
347346breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
348347biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
349348an32s 651 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
350349adantllr 718 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
351 breq1 5036 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔𝑡) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → ((𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
352 breq1 5036 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
353351, 352ifboth 4466 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔𝑡) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
354350, 353sylancom 591 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
355 subge0 11146 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3568, 104, 355syl2an 598 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
357356ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ↔ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
358354, 357mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → 0 ≤ ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
359344, 358absidd 14778 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
360 iftrue 4434 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
361360oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
362361fveq2d 6653 . . . . . . . . . . . . . . . . . . . . 21 (0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
363362adantl 485 . . . . . . . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
365345oveq1d 7154 . . . . . . . . . . . . . . . . . . . . 21 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
366364, 365sylan 583 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
367359, 363, 3663eqtr4d 2846 . . . . . . . . . . . . . . . . . . 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 11060 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1𝑡 ∈ ℝ) → -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ)
369 resubcl 10943 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
3708, 368, 369syl2an 598 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
371370ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ∈ ℝ)
37288ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ∈ ℝ)
3738ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
3748adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ)
375 ltnle 10713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
37686, 375mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
377 ltle 10722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
37886, 377mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
379376, 378sylbird 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ → (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
380379imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
381 absnid 14654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
382380, 381syldan 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
383382breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ↔ (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
384383biimpa 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
385384an32s 651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
386374, 385sylanl1 679 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (𝑔𝑡) ≤ -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
387372, 373, 386lenegcon2d 11216 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡))
388 simpll 766 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → 𝜑)
38986a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → 0 ∈ ℝ)
3908, 389ltnled 10780 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 ↔ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
3918, 86, 377sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) < 0 → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
392390, 391sylbird 263 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0))
393392imp 410 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
394388, 393sylan 583 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0)
395 negeq 10871 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔𝑡) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → -(𝑔𝑡) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
396395breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑡) = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡) ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
397 neg0 10925 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -0 = 0
398 negeq 10871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → -0 = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
399397, 398syl5eqr 2850 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → 0 = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
400399breq2d 5045 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
401396, 400ifboth 4466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -(𝑔𝑡) ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
402387, 394, 401syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
403 suble0 11147 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℝ ∧ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℝ) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
4048, 368, 403syl2an 598 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
405404ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0 ↔ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
406402, 405mpbird 260 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) ≤ 0)
407371, 406absnidd 14769 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
408 subneg 10928 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
409408negeqd 10873 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
410 negdi2 10937 . . . . . . . . . . . . . . . . . . . . . . . 24 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) + if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
411409, 410eqtrd 2836 . . . . . . . . . . . . . . . . . . . . . . 23 (((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ∈ ℂ ∧ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
41232, 140, 411syl2an 598 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
413412ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → -((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
414407, 413eqtrd 2836 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
415 iffalse 4437 . . . . . . . . . . . . . . . . . . . . . . 23 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))
416415oveq2d 7155 . . . . . . . . . . . . . . . . . . . . . 22 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = ((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
417416fveq2d 6653 . . . . . . . . . . . . . . . . . . . . 21 (¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) → (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))) = (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))))
418417adantl 485 . . . . . . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) ≤ 0) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
420393, 419syldan 594 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) = -(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))
421420oveq1d 7154 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
422388, 421sylan 583 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) ∧ ¬ 0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) → ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)) = (-(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
423414, 418, 4223eqtr4d 2846 . . . . . . . . . . . . . . . . . . 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 812 . . . . . . . . . . . . . . . . . 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 7155 . . . . . . . . . . . . . . . . 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 10662 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ)
427 pncan3 10887 . . . . . . . . . . . . . . . . . . 19 ((if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) ∈ ℂ ∧ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) ∈ ℂ) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
428140, 426, 427syl2anr 599 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
429428adantr 484 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 ∈ dom ∫1𝑡 ∈ ℝ)) ∧ (𝑔𝑡) ≤ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)))) → (if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0) + ((abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))) − if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) = (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))
430425, 429eqtrd 2836 . . . . . . . . . . . . . . . 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 594 . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . 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 651 . . . . . . . . . . . . 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 5127 . . . . . . . . . . . 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 6653 . . . . . . . . . . 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 2836 . . . . . . . . . 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 5043 . . . . . . . . 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 718 . . . . . . . 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 714 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) ∈ ℝ)
44063ad2antlr 726 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → 𝑌 ∈ ℝ)
441115adantl 485 . . . . . . . . . 10 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ∈ ℝ)
442439, 440, 441ltadd2d 10789 . . . . . . . . 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 484 . . . . . . . 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 11103 . . . . . . . . . . 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 1157 . . . . . . . . . 10 ((𝜑𝑌 ∈ ℝ+𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
4464453expa 1115 . . . . . . . . 9 (((𝜑𝑌 ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) → (((∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) − 𝑌) < (∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) ↔ (∫2‘(𝑡 ∈ ℝ ↦ (abs‘(ℜ‘if(𝑡𝐷, (𝐹𝑡), 0))))) < ((∫2‘(𝑡 ∈ ℝ ↦ if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0))) + 𝑌)))
447446adantr 484 . . . . . . . 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 314 . . . . . . 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 716 . . . . . 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 260 . . . . 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 416 . . . 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 3236 . . 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 6648 . . . . . . . . . . . . . 14 (𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) → (𝑓𝑡) = ((𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0)))‘𝑡))
454453, 167sylan9eq 2856 . . . . . . . . . . . . 13 ((𝑓 = (𝑥 ∈ ℝ ↦ if(0 ≤ (ℜ‘if(𝑥𝐷, (𝐹𝑥), 0)), if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0), -if(0 ≤ (𝑔𝑥), (𝑔𝑥), 0))) ∧ 𝑡 ∈ ℝ) → (𝑓𝑡) = if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))
455454oveq2d 7155 . . . . . . . . . . . 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 6653 . . . . . . . . . . 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 5128 . . . . . . . . . 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 6653 . . . . . . . . 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 5043 . . . . . . . 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 3574 . . . . . . 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 416 . . . . . 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 3246 . . . 4 (𝜑 → (∃𝑔 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − if(0 ≤ (ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)), if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0), -if(0 ≤ (𝑔𝑡), (𝑔𝑡), 0)))))) < 𝑌 → ∃𝑓 ∈ dom ∫1(∫2‘(𝑡 ∈ ℝ ↦ (abs‘((ℜ‘if(𝑡𝐷, (𝐹𝑡), 0)) − (𝑓𝑡))))) < 𝑌))
464463adantr 484 . . 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 209  wa 399  wo 844   = wceq 1538  wtru 1539  wcel 2112  wral 3109  wrex 3110  Vcvv 3444  cdif 3881  cun 3882  wss 3884  ifcif 4428  {csn 4528   class class class wbr 5033  cmpt 5113   × cxp 5521  ccnv 5522  dom cdm 5523  ran crn 5524  cima 5526  ccom 5527   Fn wfn 6323  wf 6324  cfv 6328  (class class class)co 7139  f cof 7391  r cofr 7392  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  +∞cpnf 10665  *cxr 10667   < clt 10668  cle 10669  cmin 10863  -cneg 10864  +crp 12381  (,)cioo 12730  [,)cico 12732  [,]cicc 12733  cre 14452  cim 14453  abscabs 14589  volcvol 24071  MblFncmbf 24222  1citg1 24223  2citg2 24224  𝐿1cibl 24225  citg 24226  0𝑝c0p 24277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-disj 4999  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-ofr 7394  df-om 7565  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-mod 13237  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-clim 14841  df-sum 15039  df-rest 16692  df-topgen 16713  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-top 21503  df-topon 21520  df-bases 21555  df-cmp 21996  df-ovol 24072  df-vol 24073  df-mbf 24227  df-itg1 24228  df-itg2 24229  df-ibl 24230  df-0p 24278
This theorem is referenced by:  ftc1anclem6  35134
  Copyright terms: Public domain W3C validator