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 36041
Description: Lemma for ftc1anc 36045, 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 4491 . . . . . . . . 9 (𝑑 ∈ ℝ β†’ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
21mpteq2ia 5207 . . . . . . . 8 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0)) = (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
32fveq2i 6841 . . . . . . 7 (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0))) = (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
4 ftc1anc.f . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:π·βŸΆβ„‚)
54ffvelcdmda 7030 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
6 0cnd 11082 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ β„‚)
75, 6ifclda 4520 . . . . . . . . . . . 12 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚)
87recld 15013 . . . . . . . . . . 11 (πœ‘ β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
98adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
10 ftc1anc.d . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 βŠ† ℝ)
11 rembl 24826 . . . . . . . . . . . 12 ℝ ∈ dom vol
1211a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ ℝ ∈ dom vol)
138adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
14 eldifn 4086 . . . . . . . . . . . . 13 (𝑑 ∈ (ℝ βˆ– 𝐷) β†’ Β¬ 𝑑 ∈ 𝐷)
1514adantl 483 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ (ℝ βˆ– 𝐷)) β†’ Β¬ 𝑑 ∈ 𝐷)
16 iffalse 4494 . . . . . . . . . . . . . 14 (Β¬ 𝑑 ∈ 𝐷 β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) = 0)
1716fveq2d 6842 . . . . . . . . . . . . 13 (Β¬ 𝑑 ∈ 𝐷 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = (β„œβ€˜0))
18 re0 14971 . . . . . . . . . . . . 13 (β„œβ€˜0) = 0
1917, 18eqtrdi 2794 . . . . . . . . . . . 12 (Β¬ 𝑑 ∈ 𝐷 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = 0)
2015, 19syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ (ℝ βˆ– 𝐷)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = 0)
21 iftrue 4491 . . . . . . . . . . . . . 14 (𝑑 ∈ 𝐷 β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) = (πΉβ€˜π‘‘))
2221fveq2d 6842 . . . . . . . . . . . . 13 (𝑑 ∈ 𝐷 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = (β„œβ€˜(πΉβ€˜π‘‘)))
2322mpteq2ia 5207 . . . . . . . . . . . 12 (𝑑 ∈ 𝐷 ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘)))
244feqmptd 6906 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)))
25 ftc1anc.i . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 ∈ 𝐿1)
2624, 25eqeltrrd 2840 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
275iblcn 25085 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1 ↔ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ 𝐿1 ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ 𝐿1)))
2826, 27mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ 𝐿1 ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ 𝐿1))
2928simpld 496 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ 𝐿1)
3023, 29eqeltrid 2843 . . . . . . . . . . 11 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ 𝐿1)
3110, 12, 13, 20, 30iblss2 25092 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ 𝐿1)
328recnd 11117 . . . . . . . . . . . . 13 (πœ‘ β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚)
3332adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚)
34 eqidd 2739 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
35 absf 15157 . . . . . . . . . . . . . 14 abs:β„‚βŸΆβ„
3635a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ abs:β„‚βŸΆβ„)
3736feqmptd 6906 . . . . . . . . . . . 12 (πœ‘ β†’ abs = (π‘₯ ∈ β„‚ ↦ (absβ€˜π‘₯)))
38 fveq2 6838 . . . . . . . . . . . 12 (π‘₯ = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (absβ€˜π‘₯) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3933, 34, 37, 38fmptco 7070 . . . . . . . . . . 11 (πœ‘ β†’ (abs ∘ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) = (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
409fmpttd 7058 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))):β„βŸΆβ„)
41 iblmbf 25054 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ 𝐿1 β†’ 𝐹 ∈ MblFn)
4225, 41syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ MblFn)
4324, 42eqeltrrd 2840 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ MblFn)
445ismbfcn2 24924 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ MblFn ↔ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ MblFn ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ MblFn)))
4543, 44mpbid 231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ MblFn ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ MblFn))
4645simpld 496 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ MblFn)
4723, 46eqeltrid 2843 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ MblFn)
4810, 12, 13, 20, 47mbfss 24932 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ MblFn)
49 ftc1anclem1 36037 . . . . . . . . . . . 12 (((𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))):β„βŸΆβ„ ∧ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ MblFn) β†’ (abs ∘ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ MblFn)
5040, 48, 49syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ (abs ∘ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ MblFn)
5139, 50eqeltrrd 2840 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ MblFn)
529, 31, 51iblabsnc 36028 . . . . . . . . 9 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ 𝐿1)
5332abscld 15256 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ)
5453adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ)
5532absge0d 15264 . . . . . . . . . . 11 (πœ‘ β†’ 0 ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
5655adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
5754, 56iblpos 25079 . . . . . . . . 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 497 . . . . . . 7 (πœ‘ β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0))) ∈ ℝ)
603, 59eqeltrrid 2844 . . . . . 6 (πœ‘ β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ)
61 ltsubrp 12880 . . . . . 6 (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))))
6260, 61sylan 581 . . . . 5 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))))
63 rpre 12852 . . . . . . 7 (π‘Œ ∈ ℝ+ β†’ π‘Œ ∈ ℝ)
64 resubcl 11399 . . . . . . 7 (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ ∧ π‘Œ ∈ ℝ) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ)
6560, 63, 64syl2an 597 . . . . . 6 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ)
6660adantr 482 . . . . . 6 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ)
6765, 66ltnled 11236 . . . . 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 11139 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ*)
70 elxrge0 13303 . . . . . . . . 9 ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ (0[,]+∞) ↔ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ* ∧ 0 ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
7169, 55, 70sylanbrc 584 . . . . . . . 8 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ (0[,]+∞))
7271adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ (0[,]+∞))
7372fmpttd 7058 . . . . . 6 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))):β„βŸΆ(0[,]+∞))
7473adantr 482 . . . . 5 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))):β„βŸΆ(0[,]+∞))
7565rexrd 11139 . . . . 5 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ*)
76 itg2leub 25021 . . . . 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 585 . . . 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 3104 . . 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 725 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ)
82 itg1cl 24971 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ (∫1β€˜π‘”) ∈ ℝ)
8382ad2antlr 726 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ (∫1β€˜π‘”) ∈ ℝ)
84 eqid 2738 . . . . . . . . . . . 12 (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
8584i1fpos 24993 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1)
86 0re 11091 . . . . . . . . . . . . . 14 0 ∈ ℝ
87 i1ff 24962 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 β†’ 𝑔:β„βŸΆβ„)
8887ffvelcdmda 7030 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
89 max1 13033 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (π‘”β€˜π‘‘) ∈ ℝ) β†’ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
9086, 88, 89sylancr 588 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
9190ralrimiva 3142 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ βˆ€π‘‘ ∈ ℝ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
92 ax-resscn 11042 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
9392a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ ℝ βŠ† β„‚)
94 fvex 6851 . . . . . . . . . . . . . . . . 17 (π‘”β€˜π‘‘) ∈ V
95 c0ex 11083 . . . . . . . . . . . . . . . . 17 0 ∈ V
9694, 95ifex 4535 . . . . . . . . . . . . . . . 16 if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ V
9796, 84fnmpti 6640 . . . . . . . . . . . . . . 15 (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) Fn ℝ
9897a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) Fn ℝ)
9993, 980pledm 24959 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 β†’ (0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ (ℝ Γ— {0}) ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
100 reex 11076 . . . . . . . . . . . . . . 15 ℝ ∈ V
101100a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ ℝ ∈ V)
10295a1i 11 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ 0 ∈ V)
103 ifcl 4530 . . . . . . . . . . . . . . 15 (((π‘”β€˜π‘‘) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ)
10488, 86, 103sylancl 587 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ)
105 fconstmpt 5691 . . . . . . . . . . . . . . 15 (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0)
106105a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0))
107 eqidd 2739 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
108101, 102, 104, 106, 107ofrfval2 7629 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 β†’ ((ℝ Γ— {0}) ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
10999, 108bitrd 279 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ (0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
11091, 109mpbird 257 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 β†’ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
111 itg2itg1 25023 . . . . . . . . . . 11 (((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
11285, 110, 111syl2anc 585 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
113 itg1cl 24971 . . . . . . . . . . 11 ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
11485, 113syl 17 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
115112, 114eqeltrd 2839 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
116115ad2antlr 726 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
117 ltnle 11168 . . . . . . . . . 10 ((((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ ∧ (∫1β€˜π‘”) ∈ ℝ) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫1β€˜π‘”) ↔ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)))
11865, 82, 117syl2an 597 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫1β€˜π‘”) ↔ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)))
119118biimpar 479 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫1β€˜π‘”))
120 max2 13035 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (π‘”β€˜π‘‘) ∈ ℝ) β†’ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
12186, 88, 120sylancr 588 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
122121ralrimiva 3142 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ βˆ€π‘‘ ∈ ℝ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
12387feqmptd 6906 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 β†’ 𝑔 = (𝑑 ∈ ℝ ↦ (π‘”β€˜π‘‘)))
124101, 88, 104, 123, 107ofrfval2 7629 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ (𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ βˆ€π‘‘ ∈ ℝ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
125122, 124mpbird 257 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 β†’ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
126 itg1le 25000 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1 ∧ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) β†’ (∫1β€˜π‘”) ≀ (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
12785, 125, 126mpd3an23 1464 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (∫1β€˜π‘”) ≀ (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
128127, 112breqtrrd 5132 . . . . . . . . 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 11249 . . . . . . 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 24961 . . . . . . . . . . . . . . . 16 ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ MblFn)
13385, 132syl 17 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ MblFn)
134133adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ MblFn)
135 elrege0 13300 . . . . . . . . . . . . . . . . 17 (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ (0[,)+∞) ↔ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ ∧ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
136104, 90, 135sylanbrc 584 . . . . . . . . . . . . . . . 16 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ (0[,)+∞))
137136fmpttd 7058 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)):β„βŸΆ(0[,)+∞))
138137adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)):β„βŸΆ(0[,)+∞))
139115adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
140104recnd 11117 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚)
141140negcld 11433 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚)
142140, 141ifcld 4531 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ β„‚)
143 subcl 11334 . . . . . . . . . . . . . . . . . . 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 597 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ β„‚)
145144anassrs 469 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ β„‚)
146145abscld 15256 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) ∈ ℝ)
147145absge0d 15264 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))
148 elrege0 13300 . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) ∈ (0[,)+∞))
150149fmpttd 7058 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))):β„βŸΆ(0[,)+∞))
151 eleq1w 2821 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ (π‘₯ ∈ 𝐷 ↔ 𝑑 ∈ 𝐷))
152 fveq2 6838 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘‘))
153151, 152ifbieq1d 4509 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
154153fveq2d 6842 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑑 β†’ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
155 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) = (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)))
156 fvex 6851 . . . . . . . . . . . . . . . . . . . 20 (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ V
157154, 155, 156fvmpt 6944 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ ℝ β†’ ((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)))β€˜π‘‘) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
158154breq2d 5116 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
159 fveq2 6838 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑑 β†’ (π‘”β€˜π‘₯) = (π‘”β€˜π‘‘))
160159breq2d 5116 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ (0 ≀ (π‘”β€˜π‘₯) ↔ 0 ≀ (π‘”β€˜π‘‘)))
161160, 159ifbieq1d 4509 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
162161negeqd 11329 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
163158, 161, 162ifbieq12d 4513 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑑 β†’ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
164 eqid 2738 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
165 negex 11333 . . . . . . . . . . . . . . . . . . . . 21 -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ V
16696, 165ifex 4535 . . . . . . . . . . . . . . . . . . . 20 if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ V
167163, 164, 166fvmpt 6944 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ ℝ β†’ ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))β€˜π‘‘) = if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
168157, 167oveq12d 7368 . . . . . . . . . . . . . . . . . 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 6842 . . . . . . . . . . . . . . . . 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 5207 . . . . . . . . . . . . . . . 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 6841 . . . . . . . . . . . . . . 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 6851 . . . . . . . . . . . . . . . . . . . . . 22 (π‘”β€˜π‘₯) ∈ V
174173, 95ifex 4535 . . . . . . . . . . . . . . . . . . . . 21 if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ V
175174, 95ifex 4535 . . . . . . . . . . . . . . . . . . . 20 if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) ∈ V
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) ∈ V)
177 ovex 7383 . . . . . . . . . . . . . . . . . . . . 21 (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) ∈ V
17895, 177ifex 4535 . . . . . . . . . . . . . . . . . . . 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 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:π·βŸΆβ„‚ β†’ 𝐹 Fn 𝐷)
181 frn 6671 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:π·βŸΆβ„‚ β†’ ran 𝐹 βŠ† β„‚)
182 ref 14931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„œ:β„‚βŸΆβ„
183 ffn 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (β„œ:β„‚βŸΆβ„ β†’ β„œ Fn β„‚)
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 β„œ Fn β„‚
185 fnco 6614 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((β„œ Fn β„‚ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 βŠ† β„‚) β†’ (β„œ ∘ 𝐹) Fn 𝐷)
186184, 185mp3an1 1449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 Fn 𝐷 ∧ ran 𝐹 βŠ† β„‚) β†’ (β„œ ∘ 𝐹) Fn 𝐷)
187180, 181, 186syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:π·βŸΆβ„‚ β†’ (β„œ ∘ 𝐹) Fn 𝐷)
188 elpreima 7004 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((β„œ ∘ 𝐹) Fn 𝐷 β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞))))
1894, 187, 1883syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞))))
190 fco 6688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((β„œ:β„‚βŸΆβ„ ∧ 𝐹:π·βŸΆβ„‚) β†’ (β„œ ∘ 𝐹):π·βŸΆβ„)
191182, 4, 190sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (β„œ ∘ 𝐹):π·βŸΆβ„)
192191ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ ℝ)
193192biantrurd 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯) ↔ (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ ℝ ∧ 0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯))))
194 elrege0 13300 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞) ↔ (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ ℝ ∧ 0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯)))
195193, 194bitr4di 289 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯) ↔ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞)))
196 fvco3 6936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹:π·βŸΆβ„‚ ∧ π‘₯ ∈ 𝐷) β†’ ((β„œ ∘ 𝐹)β€˜π‘₯) = (β„œβ€˜(πΉβ€˜π‘₯)))
1974, 196sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ ((β„œ ∘ 𝐹)β€˜π‘₯) = (β„œβ€˜(πΉβ€˜π‘₯)))
198197breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯) ↔ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))))
199195, 198bitr3d 281 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞) ↔ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))))
200199pm5.32da 580 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ ((π‘₯ ∈ 𝐷 ∧ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯)))))
201189, 200bitrd 279 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯)))))
202201adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯)))))
203 eldif 3919 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ (ℝ βˆ– 𝐷) ↔ (π‘₯ ∈ ℝ ∧ Β¬ π‘₯ ∈ 𝐷))
204203baibr 538 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ ℝ β†’ (Β¬ π‘₯ ∈ 𝐷 ↔ π‘₯ ∈ (ℝ βˆ– 𝐷)))
205 0le0 12188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≀ 0
206205, 18breqtrri 5131 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≀ (β„œβ€˜0)
207206biantru 531 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Β¬ π‘₯ ∈ 𝐷 ↔ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0)))
208204, 207bitr3di 286 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ ℝ β†’ (π‘₯ ∈ (ℝ βˆ– 𝐷) ↔ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0))))
209208adantl 483 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ (ℝ βˆ– 𝐷) ↔ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0))))
210202, 209orbi12d 918 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∨ π‘₯ ∈ (ℝ βˆ– 𝐷)) ↔ ((π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))) ∨ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0)))))
211 elun 4107 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ↔ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∨ π‘₯ ∈ (ℝ βˆ– 𝐷)))
212 fveq2 6838 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = (πΉβ€˜π‘₯) β†’ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) = (β„œβ€˜(πΉβ€˜π‘₯)))
213212breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . 23 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = (πΉβ€˜π‘₯) β†’ (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))))
214 fveq2 6838 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = 0 β†’ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) = (β„œβ€˜0))
215214breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . 23 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = 0 β†’ (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ 0 ≀ (β„œβ€˜0)))
216213, 215elimif 4522 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ ((π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))) ∨ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0))))
217210, 211, 2163bitr4g 314 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ↔ 0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))))
218217ifbid 4508 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) = if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0))
219218mpteq2dva 5204 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0)) = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0)))
220217ifbid 4508 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))))
221220mpteq2dva 5204 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))) = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))))
222172, 176, 179, 219, 221offval2 7628 . . . . . . . . . . . . . . . . . 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 7449 . . . . . . . . . . . . . . . . . . . 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))))
22487ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
225224recnd 11117 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ β„‚)
226 0cn 11081 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ β„‚
227 ifcl 4530 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘”β€˜π‘₯) ∈ β„‚ ∧ 0 ∈ β„‚) β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ β„‚)
228225, 226, 227sylancl 587 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ β„‚)
229228addid1d 11289 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) + 0) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
230228mulm1d 11541 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
231230oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (0 + (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = (0 + -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
232228negcld 11433 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ β„‚)
233232addid2d 11290 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (0 + -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
234231, 233eqtrd 2778 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (0 + (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
235229, 234ifeq12d 4506 . . . . . . . . . . . . . . . . . . . 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 2790 . . . . . . . . . . . . . . . . . . 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 5204 . . . . . . . . . . . . . . . . . 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 2798 . . . . . . . . . . . . . . . . 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 11136 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
240 pnfxr 11143 . . . . . . . . . . . . . . . . . . . . . . 23 +∞ ∈ ℝ*
241 0ltpnf 12972 . . . . . . . . . . . . . . . . . . . . . . 23 0 < +∞
242 snunioo 13324 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) β†’ ({0} βˆͺ (0(,)+∞)) = (0[,)+∞))
243239, 240, 241, 242mp3an 1462 . . . . . . . . . . . . . . . . . . . . . 22 ({0} βˆͺ (0(,)+∞)) = (0[,)+∞)
244243imaeq2i 6008 . . . . . . . . . . . . . . . . . . . . 21 (β—‘(β„œ ∘ 𝐹) β€œ ({0} βˆͺ (0(,)+∞))) = (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞))
245 imaundi 6099 . . . . . . . . . . . . . . . . . . . . 21 (β—‘(β„œ ∘ 𝐹) β€œ ({0} βˆͺ (0(,)+∞))) = ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞)))
246244, 245eqtr3i 2768 . . . . . . . . . . . . . . . . . . . 20 (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) = ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞)))
247 ismbfcn 24915 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:π·βŸΆβ„‚ β†’ (𝐹 ∈ MblFn ↔ ((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„‘ ∘ 𝐹) ∈ MblFn)))
2484, 247syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝐹 ∈ MblFn ↔ ((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„‘ ∘ 𝐹) ∈ MblFn)))
24942, 248mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„‘ ∘ 𝐹) ∈ MblFn))
250249simpld 496 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β„œ ∘ 𝐹) ∈ MblFn)
251 mbfimasn 24918 . . . . . . . . . . . . . . . . . . . . . . 23 (((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„œ ∘ 𝐹):π·βŸΆβ„ ∧ 0 ∈ ℝ) β†’ (β—‘(β„œ ∘ 𝐹) β€œ {0}) ∈ dom vol)
25286, 251mp3an3 1451 . . . . . . . . . . . . . . . . . . . . . 22 (((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„œ ∘ 𝐹):π·βŸΆβ„) β†’ (β—‘(β„œ ∘ 𝐹) β€œ {0}) ∈ dom vol)
253 mbfima 24916 . . . . . . . . . . . . . . . . . . . . . 22 (((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„œ ∘ 𝐹):π·βŸΆβ„) β†’ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞)) ∈ dom vol)
254 unmbl 24823 . . . . . . . . . . . . . . . . . . . . . 22 (((β—‘(β„œ ∘ 𝐹) β€œ {0}) ∈ dom vol ∧ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞)) ∈ dom vol) β†’ ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞))) ∈ dom vol)
255252, 253, 254syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„œ ∘ 𝐹):π·βŸΆβ„) β†’ ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞))) ∈ dom vol)
256250, 191, 255syl2anc 585 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞))) ∈ dom vol)
257246, 256eqeltrid 2843 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∈ dom vol)
2584fdmd 6675 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ dom 𝐹 = 𝐷)
259 mbfdm 24912 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ MblFn β†’ dom 𝐹 ∈ dom vol)
26042, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ dom 𝐹 ∈ dom vol)
261258, 260eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐷 ∈ dom vol)
262 difmbl 24829 . . . . . . . . . . . . . . . . . . . 20 ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) β†’ (ℝ βˆ– 𝐷) ∈ dom vol)
26311, 261, 262sylancr 588 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (ℝ βˆ– 𝐷) ∈ dom vol)
264 unmbl 24823 . . . . . . . . . . . . . . . . . . 19 (((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∈ dom vol ∧ (ℝ βˆ– 𝐷) ∈ dom vol) β†’ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ∈ dom vol)
265257, 263, 264syl2anc 585 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ∈ dom vol)
266 fveq2 6838 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = π‘₯ β†’ (π‘”β€˜π‘‘) = (π‘”β€˜π‘₯))
267266breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = π‘₯ β†’ (0 ≀ (π‘”β€˜π‘‘) ↔ 0 ≀ (π‘”β€˜π‘₯)))
268267, 266ifbieq1d 4509 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = π‘₯ β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
269268, 84, 174fvmpt 6944 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ ∈ ℝ β†’ ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
270269eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) = ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯))
271270ifeq1d 4504 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ ℝ β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) = if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯), 0))
272271mpteq2ia 5207 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0)) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯), 0))
273272i1fres 24992 . . . . . . . . . . . . . . . . . . 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 12202 . . . . . . . . . . . . . . . . . . . . . 22 -1 ∈ ℝ
276275a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 β†’ -1 ∈ ℝ)
277274, 276i1fmulc 24990 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 β†’ ((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ dom ∫1)
278 cmmbl 24820 . . . . . . . . . . . . . . . . . . . 20 (((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ∈ dom vol β†’ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))) ∈ dom vol)
279 ifnot 4537 . . . . . . . . . . . . . . . . . . . . . . 23 if(Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)), 0) = if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
280 eldif 3919 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))) ↔ (π‘₯ ∈ ℝ ∧ Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))))
281280baibr 538 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ ℝ β†’ (Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ↔ π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)))))
282 tru 1546 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊀
283 negex 11333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 -1 ∈ V
284283fconst 6724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ Γ— {-1}):β„βŸΆ{-1}
285 ffn 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℝ Γ— {-1}):β„βŸΆ{-1} β†’ (ℝ Γ— {-1}) Fn ℝ)
286284, 285mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊀ β†’ (ℝ Γ— {-1}) Fn ℝ)
28797a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊀ β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) Fn ℝ)
288100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊀ β†’ ℝ ∈ V)
289 inidm 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ℝ ∩ ℝ) = ℝ
290283fvconst2 7148 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∈ ℝ β†’ ((ℝ Γ— {-1})β€˜π‘₯) = -1)
291290adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊀ ∧ π‘₯ ∈ ℝ) β†’ ((ℝ Γ— {-1})β€˜π‘₯) = -1)
292269adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊀ ∧ π‘₯ ∈ ℝ) β†’ ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
293286, 287, 288, 288, 289, 291, 292ofval 7619 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⊀ ∧ π‘₯ ∈ ℝ) β†’ (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯) = (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
294282, 293mpan 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ ℝ β†’ (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯) = (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
295294eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ ℝ β†’ (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯))
296281, 295ifbieq1d 4509 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ ∈ ℝ β†’ if(Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)), 0) = if(π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))), (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯), 0))
297279, 296eqtr3id 2792 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = if(π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))), (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯), 0))
298297mpteq2ia 5207 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))) = (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))), (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯), 0))
299298i1fres 24992 . . . . . . . . . . . . . . . . . . . 20 ((((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ dom ∫1 ∧ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))) ∈ dom vol) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))) ∈ dom ∫1)
300277, 278, 299syl2an 597 . . . . . . . . . . . . . . . . . . 19 (((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 ∧ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ∈ dom vol) β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))) ∈ dom ∫1)
301273, 300i1fadd 24981 . . . . . . . . . . . . . . . . . 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 598 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0)) ∘f + (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))))) ∈ dom ∫1)
303238, 302eqeltrrd 2840 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) ∈ dom ∫1)
304154cbvmptv 5217 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) = (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
305304, 31eqeltrid 2843 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) ∈ 𝐿1)
3069, 304fmptd 7057 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))):β„βŸΆβ„)
307305, 306jca 513 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) ∈ 𝐿1 ∧ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))):β„βŸΆβ„))
308307adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ ((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) ∈ 𝐿1 ∧ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))):β„βŸΆβ„))
309 ftc1anclem4 36040 . . . . . . . . . . . . . . . . 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 1121 . . . . . . . . . . . . . . . 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 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)))β€˜π‘‘) βˆ’ ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))β€˜π‘‘))))) ∈ ℝ)
312171, 311eqeltrrid 2844 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) ∈ ℝ)
313134, 138, 139, 150, 312itg2addnc 36018 . . . . . . . . . . . . 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 2739 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
317 eqidd 2739 . . . . . . . . . . . . . . 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 7628 . . . . . . . . . . . . . 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 6842 . . . . . . . . . . . . 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 2780 . . . . . . . . . . . 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 482 . . . . . . . . . . 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 1918 . . . . . . . . . . . . . 14 Ⅎ𝑑(πœ‘ ∧ 𝑔 ∈ dom ∫1)
323 nfcv 2906 . . . . . . . . . . . . . . 15 Ⅎ𝑑𝑔
324 nfcv 2906 . . . . . . . . . . . . . . 15 Ⅎ𝑑 ∘r ≀
325 nfmpt1 5212 . . . . . . . . . . . . . . 15 Ⅎ𝑑(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
326323, 324, 325nfbr 5151 . . . . . . . . . . . . . 14 Ⅎ𝑑 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
327322, 326nfan 1903 . . . . . . . . . . . . 13 Ⅎ𝑑((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
328 anass 470 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ↔ (πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)))
32987ffnd 6665 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 β†’ 𝑔 Fn ℝ)
330 fvex 6851 . . . . . . . . . . . . . . . . . . . . . 22 (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ V
331 eqid 2738 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) = (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
332330, 331fnmpti 6640 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) Fn ℝ
333332a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) Fn ℝ)
334 eqidd 2739 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) = (π‘”β€˜π‘‘))
335331fvmpt2 6955 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ∈ ℝ ∧ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ V) β†’ ((𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))β€˜π‘‘) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
336330, 335mpan2 690 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ ℝ β†’ ((𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))β€˜π‘‘) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
337336adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ ((𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))β€˜π‘‘) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
338329, 333, 101, 101, 289, 334, 337ofrval 7620 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3393383com23 1127 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3403393expa 1119 . . . . . . . . . . . . . . . . 17 (((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
341340adantll 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
342 resubcl 11399 . . . . . . . . . . . . . . . . . . . . . . 23 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
3438, 104, 342syl2an 597 . . . . . . . . . . . . . . . . . . . . . 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 15116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
3468, 345sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
347346breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ↔ (π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
348347biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . 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 5107 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘”β€˜π‘‘) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ ((π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
352 breq1 5107 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
353351, 352ifboth 4524 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
354350, 353sylancom 589 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
355 subge0 11602 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ (0 ≀ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3568, 104, 355syl2an 597 . . . . . . . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ 0 ≀ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
359344, 358absidd 15242 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
360 iftrue 4491 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
361360oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
362361fveq2d 6842 . . . . . . . . . . . . . . . . . . . . 21 (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) = (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
363362adantl 483 . . . . . . . . . . . . . . . . . . . 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 7365 . . . . . . . . . . . . . . . . . . . . 21 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
366364, 365sylan 581 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
367359, 363, 3663eqtr4d 2788 . . . . . . . . . . . . . . . . . . 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 11516 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ)
369 resubcl 11399 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
3708, 368, 369syl2an 597 . . . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
375 ltnle 11168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 ↔ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
37686, 375mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 ↔ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
377 ltle 11177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
37886, 377mpan2 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
379376, 378sylbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ β†’ (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
380379imp 408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0)
381 absnid 15118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
382380, 381syldan 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
383382breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ↔ (π‘”β€˜π‘‘) ≀ -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
384383biimpa 478 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11672 . . . . . . . . . . . . . . . . . . . . . . . 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 11236 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 ↔ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3918, 86, 377sylancl 587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
392390, 391sylbird 260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
393392imp 408 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0)
394388, 393sylan 581 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0)
395 negeq 11327 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘”β€˜π‘‘) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ -(π‘”β€˜π‘‘) = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
396395breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘”β€˜π‘‘) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -(π‘”β€˜π‘‘) ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
397 neg0 11381 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -0 = 0
398 negeq 11327 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ -0 = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
399397, 398eqtr3id 2792 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ 0 = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
400399breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0 ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
401396, 400ifboth 4524 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -(π‘”β€˜π‘‘) ∧ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
402387, 394, 401syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
403 suble0 11603 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ≀ 0 ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
4048, 368, 403syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ≀ 0)
407371, 406absnidd 15233 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
408 subneg 11384 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) + if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
409408negeqd 11329 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) + if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
410 negdi2 11393 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) + if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
411409, 410eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . 23 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
41232, 140, 411syl2an 597 . . . . . . . . . . . . . . . . . . . . . 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 2778 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
415 iffalse 4494 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
416415oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . 22 (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
417416fveq2d 6842 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) = (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
418417adantl 483 . . . . . . . . . . . . . . . . . . . 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 581 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
420393, 419syldan 592 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
421420oveq1d 7365 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
422388, 421sylan 581 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
423414, 418, 4223eqtr4d 2788 . . . . . . . . . . . . . . . . . . 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 7366 . . . . . . . . . . . . . . . . 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 11117 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ β„‚)
427 pncan3 11343 . . . . . . . . . . . . . . . . . . 19 ((if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚ ∧ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ β„‚) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
428140, 426, 427syl2anr 598 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
429428adantr 482 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
430425, 429eqtrd 2778 . . . . . . . . . . . . . . . 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 592 . . . . . . . . . . . . . . 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 582 . . . . . . . . . . . . . 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 5202 . . . . . . . . . . . 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 6842 . . . . . . . . . . 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 2778 . . . . . . . . . 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 5114 . . . . . . . . 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 483 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
442439, 440, 441ltadd2d 11245 . . . . . . . . 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 482 . . . . . . . 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 11559 . . . . . . . . . . 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 1161 . . . . . . . . . 10 ((πœ‘ ∧ π‘Œ ∈ ℝ+ ∧ 𝑔 ∈ dom ∫1) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ↔ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) < ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + π‘Œ)))
4464453expa 1119 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ↔ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) < ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + π‘Œ)))
447446adantr 482 . . . . . . . 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 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 257 . . . . 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 414 . . . 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 3164 . . 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 6837 . . . . . . . . . . . . . 14 (𝑓 = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) β†’ (π‘“β€˜π‘‘) = ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))β€˜π‘‘))
454453, 167sylan9eq 2798 . . . . . . . . . . . . 13 ((𝑓 = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) = if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
455454oveq2d 7366 . . . . . . . . . . . 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 6842 . . . . . . . . . . 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 5204 . . . . . . . . . 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 6842 . . . . . . . . 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 5114 . . . . . . . 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 3580 . . . . . . 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 414 . . . . . 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 3151 . . . 4 (πœ‘ β†’ (βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ))
464463adantr 482 . . 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 397   ∨ wo 846   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  βˆ€wral 3063  βˆƒwrex 3072  Vcvv 3444   βˆ– cdif 3906   βˆͺ cun 3907   βŠ† wss 3909  ifcif 4485  {csn 4585   class class class wbr 5104   ↦ cmpt 5187   Γ— cxp 5629  β—‘ccnv 5630  dom cdm 5631  ran crn 5632   β€œ cima 5634   ∘ ccom 5635   Fn wfn 6487  βŸΆwf 6488  β€˜cfv 6492  (class class class)co 7350   ∘f cof 7606   ∘r cofr 7607  β„‚cc 10983  β„cr 10984  0cc0 10985  1c1 10986   + caddc 10988   Β· cmul 10990  +∞cpnf 11120  β„*cxr 11122   < clt 11123   ≀ cle 11124   βˆ’ cmin 11319  -cneg 11320  β„+crp 12844  (,)cioo 13193  [,)cico 13195  [,]cicc 13196  β„œcre 14916  β„‘cim 14917  abscabs 15053  volcvol 24749  MblFncmbf 24900  βˆ«1citg1 24901  βˆ«2citg2 24902  πΏ1cibl 24903  βˆ«citg 24904  0𝑝c0p 24955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063  ax-addf 11064
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-disj 5070  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-ofr 7609  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fi 9281  df-sup 9312  df-inf 9313  df-oi 9380  df-dju 9771  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-n0 12348  df-z 12434  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-mod 13704  df-seq 13836  df-exp 13897  df-hash 14159  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-clim 15305  df-sum 15506  df-rest 17239  df-topgen 17260  df-psmet 20711  df-xmet 20712  df-met 20713  df-bl 20714  df-mopn 20715  df-top 22165  df-topon 22182  df-bases 22218  df-cmp 22660  df-ovol 24750  df-vol 24751  df-mbf 24905  df-itg1 24906  df-itg2 24907  df-ibl 24908  df-0p 24956
This theorem is referenced by:  ftc1anclem6  36042
  Copyright terms: Public domain W3C validator