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 36050
Description: Lemma for ftc1anc 36054, 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 4490 . . . . . . . . 9 (𝑑 ∈ ℝ β†’ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
21mpteq2ia 5206 . . . . . . . 8 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0)) = (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
32fveq2i 6840 . . . . . . 7 (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0))) = (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
4 ftc1anc.f . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:π·βŸΆβ„‚)
54ffvelcdmda 7029 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
6 0cnd 11081 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ β„‚)
75, 6ifclda 4519 . . . . . . . . . . . 12 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚)
87recld 15012 . . . . . . . . . . 11 (πœ‘ β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
98adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
10 ftc1anc.d . . . . . . . . . . 11 (πœ‘ β†’ 𝐷 βŠ† ℝ)
11 rembl 24826 . . . . . . . . . . . 12 ℝ ∈ dom vol
1211a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ ℝ ∈ dom vol)
138adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
14 eldifn 4085 . . . . . . . . . . . . 13 (𝑑 ∈ (ℝ βˆ– 𝐷) β†’ Β¬ 𝑑 ∈ 𝐷)
1514adantl 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ (ℝ βˆ– 𝐷)) β†’ Β¬ 𝑑 ∈ 𝐷)
16 iffalse 4493 . . . . . . . . . . . . . 14 (Β¬ 𝑑 ∈ 𝐷 β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) = 0)
1716fveq2d 6841 . . . . . . . . . . . . 13 (Β¬ 𝑑 ∈ 𝐷 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = (β„œβ€˜0))
18 re0 14970 . . . . . . . . . . . . 13 (β„œβ€˜0) = 0
1917, 18eqtrdi 2793 . . . . . . . . . . . 12 (Β¬ 𝑑 ∈ 𝐷 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = 0)
2015, 19syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑑 ∈ (ℝ βˆ– 𝐷)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = 0)
21 iftrue 4490 . . . . . . . . . . . . . 14 (𝑑 ∈ 𝐷 β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) = (πΉβ€˜π‘‘))
2221fveq2d 6841 . . . . . . . . . . . . 13 (𝑑 ∈ 𝐷 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) = (β„œβ€˜(πΉβ€˜π‘‘)))
2322mpteq2ia 5206 . . . . . . . . . . . 12 (𝑑 ∈ 𝐷 ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘)))
244feqmptd 6905 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 = (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)))
25 ftc1anc.i . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 ∈ 𝐿1)
2624, 25eqeltrrd 2839 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1)
275iblcn 25085 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ 𝐿1 ↔ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ 𝐿1 ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ 𝐿1)))
2826, 27mpbid 231 . . . . . . . . . . . . 13 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ 𝐿1 ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ 𝐿1))
2928simpld 495 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ 𝐿1)
3023, 29eqeltrid 2842 . . . . . . . . . . 11 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ 𝐿1)
3110, 12, 13, 20, 30iblss2 25092 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ 𝐿1)
328recnd 11116 . . . . . . . . . . . . 13 (πœ‘ β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚)
3332adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚)
34 eqidd 2738 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
35 absf 15156 . . . . . . . . . . . . . 14 abs:β„‚βŸΆβ„
3635a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ abs:β„‚βŸΆβ„)
3736feqmptd 6905 . . . . . . . . . . . 12 (πœ‘ β†’ abs = (π‘₯ ∈ β„‚ ↦ (absβ€˜π‘₯)))
38 fveq2 6837 . . . . . . . . . . . 12 (π‘₯ = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (absβ€˜π‘₯) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3933, 34, 37, 38fmptco 7069 . . . . . . . . . . 11 (πœ‘ β†’ (abs ∘ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) = (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
409fmpttd 7057 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))):β„βŸΆβ„)
41 iblmbf 25054 . . . . . . . . . . . . . . . . . 18 (𝐹 ∈ 𝐿1 β†’ 𝐹 ∈ MblFn)
4225, 41syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝐹 ∈ MblFn)
4324, 42eqeltrrd 2839 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ MblFn)
445ismbfcn2 24924 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (πΉβ€˜π‘‘)) ∈ MblFn ↔ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ MblFn ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ MblFn)))
4543, 44mpbid 231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ MblFn ∧ (𝑑 ∈ 𝐷 ↦ (β„‘β€˜(πΉβ€˜π‘‘))) ∈ MblFn))
4645simpld 495 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜(πΉβ€˜π‘‘))) ∈ MblFn)
4723, 46eqeltrid 2842 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ 𝐷 ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ MblFn)
4810, 12, 13, 20, 47mbfss 24932 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ MblFn)
49 ftc1anclem1 36046 . . . . . . . . . . . 12 (((𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))):β„βŸΆβ„ ∧ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ MblFn) β†’ (abs ∘ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ MblFn)
5040, 48, 49syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ (abs ∘ (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ MblFn)
5139, 50eqeltrrd 2839 . . . . . . . . . 10 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ MblFn)
529, 31, 51iblabsnc 36037 . . . . . . . . 9 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∈ 𝐿1)
5332abscld 15255 . . . . . . . . . . 11 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ)
5453adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ)
5532absge0d 15263 . . . . . . . . . . 11 (πœ‘ β†’ 0 ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
5655adantr 481 . . . . . . . . . 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 496 . . . . . . 7 (πœ‘ β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ ℝ, (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))), 0))) ∈ ℝ)
603, 59eqeltrrid 2843 . . . . . 6 (πœ‘ β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ)
61 ltsubrp 12879 . . . . . 6 (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))))
6260, 61sylan 580 . . . . 5 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))))
63 rpre 12851 . . . . . . 7 (π‘Œ ∈ ℝ+ β†’ π‘Œ ∈ ℝ)
64 resubcl 11398 . . . . . . 7 (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ ∧ π‘Œ ∈ ℝ) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ)
6560, 63, 64syl2an 596 . . . . . 6 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ)
6660adantr 481 . . . . . 6 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ∈ ℝ)
6765, 66ltnled 11235 . . . . 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 11138 . . . . . . . . 9 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ*)
70 elxrge0 13302 . . . . . . . . 9 ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ (0[,]+∞) ↔ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ ℝ* ∧ 0 ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
7169, 55, 70sylanbrc 583 . . . . . . . 8 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ (0[,]+∞))
7271adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ (0[,]+∞))
7372fmpttd 7057 . . . . . 6 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))):β„βŸΆ(0[,]+∞))
7473adantr 481 . . . . 5 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))):β„βŸΆ(0[,]+∞))
7565rexrd 11138 . . . . 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 584 . . . 4 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ↔ βˆ€π‘” ∈ dom ∫1(𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ))))
7868, 77mtbid 323 . . 3 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ Β¬ βˆ€π‘” ∈ dom ∫1(𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)))
79 rexanali 3103 . . 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 724 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ)
82 itg1cl 24971 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ (∫1β€˜π‘”) ∈ ℝ)
8382ad2antlr 725 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ (∫1β€˜π‘”) ∈ ℝ)
84 eqid 2737 . . . . . . . . . . . 12 (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
8584i1fpos 24993 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1)
86 0re 11090 . . . . . . . . . . . . . 14 0 ∈ ℝ
87 i1ff 24962 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 β†’ 𝑔:β„βŸΆβ„)
8887ffvelcdmda 7029 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
89 max1 13032 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (π‘”β€˜π‘‘) ∈ ℝ) β†’ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
9086, 88, 89sylancr 587 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
9190ralrimiva 3141 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ βˆ€π‘‘ ∈ ℝ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
92 ax-resscn 11041 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
9392a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ ℝ βŠ† β„‚)
94 fvex 6850 . . . . . . . . . . . . . . . . 17 (π‘”β€˜π‘‘) ∈ V
95 c0ex 11082 . . . . . . . . . . . . . . . . 17 0 ∈ V
9694, 95ifex 4534 . . . . . . . . . . . . . . . 16 if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ V
9796, 84fnmpti 6639 . . . . . . . . . . . . . . 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 11075 . . . . . . . . . . . . . . 15 ℝ ∈ V
101100a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ ℝ ∈ V)
10295a1i 11 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ 0 ∈ V)
103 ifcl 4529 . . . . . . . . . . . . . . 15 (((π‘”β€˜π‘‘) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ)
10488, 86, 103sylancl 586 . . . . . . . . . . . . . 14 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ)
105 fconstmpt 5690 . . . . . . . . . . . . . . 15 (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0)
106105a1i 11 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0))
107 eqidd 2738 . . . . . . . . . . . . . 14 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
108101, 102, 104, 106, 107ofrfval2 7628 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 β†’ ((ℝ Γ— {0}) ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
10999, 108bitrd 278 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ (0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
11091, 109mpbird 256 . . . . . . . . . . 11 (𝑔 ∈ dom ∫1 β†’ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
111 itg2itg1 25023 . . . . . . . . . . 11 (((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
11285, 110, 111syl2anc 584 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
113 itg1cl 24971 . . . . . . . . . . 11 ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ dom ∫1 β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
11485, 113syl 17 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
115112, 114eqeltrd 2838 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
116115ad2antlr 725 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
117 ltnle 11167 . . . . . . . . . 10 ((((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) ∈ ℝ ∧ (∫1β€˜π‘”) ∈ ℝ) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫1β€˜π‘”) ↔ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)))
11865, 82, 117syl2an 596 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫1β€˜π‘”) ↔ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)))
119118biimpar 478 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫1β€˜π‘”))
120 max2 13034 . . . . . . . . . . . . . 14 ((0 ∈ ℝ ∧ (π‘”β€˜π‘‘) ∈ ℝ) β†’ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
12186, 88, 120sylancr 587 . . . . . . . . . . . . 13 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
122121ralrimiva 3141 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ βˆ€π‘‘ ∈ ℝ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
12387feqmptd 6905 . . . . . . . . . . . . 13 (𝑔 ∈ dom ∫1 β†’ 𝑔 = (𝑑 ∈ ℝ ↦ (π‘”β€˜π‘‘)))
124101, 88, 104, 123, 107ofrfval2 7628 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ (𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ βˆ€π‘‘ ∈ ℝ (π‘”β€˜π‘‘) ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
125122, 124mpbird 256 . . . . . . . . . . 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 1463 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (∫1β€˜π‘”) ≀ (∫1β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
128127, 112breqtrrd 5131 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ (∫1β€˜π‘”) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
129128ad2antlr 725 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ (∫1β€˜π‘”) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
13081, 83, 116, 119, 129ltletrd 11248 . . . . . . 7 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
131130adantrl 714 . . . . . 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 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ MblFn)
135 elrege0 13299 . . . . . . . . . . . . . . . . 17 (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ (0[,)+∞) ↔ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ ∧ 0 ≀ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
136104, 90, 135sylanbrc 583 . . . . . . . . . . . . . . . 16 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ (0[,)+∞))
137136fmpttd 7057 . . . . . . . . . . . . . . 15 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)):β„βŸΆ(0[,)+∞))
138137adantl 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)):β„βŸΆ(0[,)+∞))
139115adantl 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
140104recnd 11116 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚)
141140negcld 11432 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚)
142140, 141ifcld 4530 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ β„‚)
143 subcl 11333 . . . . . . . . . . . . . . . . . . 19 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ β„‚) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ β„‚)
14432, 142, 143syl2an 596 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ β„‚)
145144anassrs 468 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ β„‚)
146145abscld 15255 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) ∈ ℝ)
147145absge0d 15263 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))
148 elrege0 13299 . . . . . . . . . . . . . . . 16 ((absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) ∈ (0[,)+∞) ↔ ((absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) ∈ ℝ ∧ 0 ≀ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))))
149146, 147, 148sylanbrc 583 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) ∈ (0[,)+∞))
150149fmpttd 7057 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))):β„βŸΆ(0[,)+∞))
151 eleq1w 2820 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ (π‘₯ ∈ 𝐷 ↔ 𝑑 ∈ 𝐷))
152 fveq2 6837 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘‘))
153151, 152ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))
154153fveq2d 6841 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑑 β†’ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
155 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) = (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)))
156 fvex 6850 . . . . . . . . . . . . . . . . . . . 20 (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ V
157154, 155, 156fvmpt 6943 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ ℝ β†’ ((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)))β€˜π‘‘) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
158154breq2d 5115 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
159 fveq2 6837 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = 𝑑 β†’ (π‘”β€˜π‘₯) = (π‘”β€˜π‘‘))
160159breq2d 5115 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = 𝑑 β†’ (0 ≀ (π‘”β€˜π‘₯) ↔ 0 ≀ (π‘”β€˜π‘‘)))
161160, 159ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
162161negeqd 11328 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = 𝑑 β†’ -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
163158, 161, 162ifbieq12d 4512 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = 𝑑 β†’ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
164 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
165 negex 11332 . . . . . . . . . . . . . . . . . . . . 21 -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ V
16696, 165ifex 4534 . . . . . . . . . . . . . . . . . . . 20 if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ V
167163, 164, 166fvmpt 6943 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ ℝ β†’ ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))β€˜π‘‘) = if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
168157, 167oveq12d 7367 . . . . . . . . . . . . . . . . . 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 6841 . . . . . . . . . . . . . . . . 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 5206 . . . . . . . . . . . . . . . 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 6840 . . . . . . . . . . . . . . 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 6850 . . . . . . . . . . . . . . . . . . . . . 22 (π‘”β€˜π‘₯) ∈ V
174173, 95ifex 4534 . . . . . . . . . . . . . . . . . . . . 21 if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ V
175174, 95ifex 4534 . . . . . . . . . . . . . . . . . . . 20 if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) ∈ V
176175a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) ∈ V)
177 ovex 7382 . . . . . . . . . . . . . . . . . . . . 21 (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) ∈ V
17895, 177ifex 4534 . . . . . . . . . . . . . . . . . . . 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 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:π·βŸΆβ„‚ β†’ 𝐹 Fn 𝐷)
181 frn 6670 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹:π·βŸΆβ„‚ β†’ ran 𝐹 βŠ† β„‚)
182 ref 14930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 β„œ:β„‚βŸΆβ„
183 ffn 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (β„œ:β„‚βŸΆβ„ β†’ β„œ Fn β„‚)
184182, 183ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 β„œ Fn β„‚
185 fnco 6613 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((β„œ Fn β„‚ ∧ 𝐹 Fn 𝐷 ∧ ran 𝐹 βŠ† β„‚) β†’ (β„œ ∘ 𝐹) Fn 𝐷)
186184, 185mp3an1 1448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 Fn 𝐷 ∧ ran 𝐹 βŠ† β„‚) β†’ (β„œ ∘ 𝐹) Fn 𝐷)
187180, 181, 186syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹:π·βŸΆβ„‚ β†’ (β„œ ∘ 𝐹) Fn 𝐷)
188 elpreima 7003 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((β„œ ∘ 𝐹) Fn 𝐷 β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞))))
1894, 187, 1883syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞))))
190 fco 6687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((β„œ:β„‚βŸΆβ„ ∧ 𝐹:π·βŸΆβ„‚) β†’ (β„œ ∘ 𝐹):π·βŸΆβ„)
191182, 4, 190sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (πœ‘ β†’ (β„œ ∘ 𝐹):π·βŸΆβ„)
192191ffvelcdmda 7029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ ℝ)
193192biantrurd 533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯) ↔ (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ ℝ ∧ 0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯))))
194 elrege0 13299 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞) ↔ (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ ℝ ∧ 0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯)))
195193, 194bitr4di 288 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯) ↔ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞)))
196 fvco3 6935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐹:π·βŸΆβ„‚ ∧ π‘₯ ∈ 𝐷) β†’ ((β„œ ∘ 𝐹)β€˜π‘₯) = (β„œβ€˜(πΉβ€˜π‘₯)))
1974, 196sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ ((β„œ ∘ 𝐹)β€˜π‘₯) = (β„œβ€˜(πΉβ€˜π‘₯)))
198197breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (0 ≀ ((β„œ ∘ 𝐹)β€˜π‘₯) ↔ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))))
199195, 198bitr3d 280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ π‘₯ ∈ 𝐷) β†’ (((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞) ↔ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))))
200199pm5.32da 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ ((π‘₯ ∈ 𝐷 ∧ ((β„œ ∘ 𝐹)β€˜π‘₯) ∈ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯)))))
201189, 200bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯)))))
202201adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ↔ (π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯)))))
203 eldif 3918 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ (ℝ βˆ– 𝐷) ↔ (π‘₯ ∈ ℝ ∧ Β¬ π‘₯ ∈ 𝐷))
204203baibr 537 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ ℝ β†’ (Β¬ π‘₯ ∈ 𝐷 ↔ π‘₯ ∈ (ℝ βˆ– 𝐷)))
205 0le0 12187 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≀ 0
206205, 18breqtrri 5130 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ≀ (β„œβ€˜0)
207206biantru 530 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Β¬ π‘₯ ∈ 𝐷 ↔ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0)))
208204, 207bitr3di 285 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ ℝ β†’ (π‘₯ ∈ (ℝ βˆ– 𝐷) ↔ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0))))
209208adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ (ℝ βˆ– 𝐷) ↔ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0))))
210202, 209orbi12d 917 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ ((π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∨ π‘₯ ∈ (ℝ βˆ– 𝐷)) ↔ ((π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))) ∨ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0)))))
211 elun 4106 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ↔ (π‘₯ ∈ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∨ π‘₯ ∈ (ℝ βˆ– 𝐷)))
212 fveq2 6837 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = (πΉβ€˜π‘₯) β†’ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) = (β„œβ€˜(πΉβ€˜π‘₯)))
213212breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . 23 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = (πΉβ€˜π‘₯) β†’ (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))))
214 fveq2 6837 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = 0 β†’ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) = (β„œβ€˜0))
215214breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . 23 (if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0) = 0 β†’ (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ 0 ≀ (β„œβ€˜0)))
216213, 215elimif 4521 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)) ↔ ((π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜(πΉβ€˜π‘₯))) ∨ (Β¬ π‘₯ ∈ 𝐷 ∧ 0 ≀ (β„œβ€˜0))))
217210, 211, 2163bitr4g 313 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ↔ 0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))))
218217ifbid 4507 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) = if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0))
219218mpteq2dva 5203 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0)) = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0)))
220217ifbid 4507 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))))
221220mpteq2dva 5203 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))) = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))))
222172, 176, 179, 219, 221offval2 7627 . . . . . . . . . . . . . . . . . 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 7448 . . . . . . . . . . . . . . . . . . . 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 7029 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
225224recnd 11116 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ β„‚)
226 0cn 11080 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ β„‚
227 ifcl 4529 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘”β€˜π‘₯) ∈ β„‚ ∧ 0 ∈ β„‚) β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ β„‚)
228225, 226, 227sylancl 586 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ β„‚)
229228addid1d 11288 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) + 0) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
230228mulm1d 11540 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
231230oveq2d 7365 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (0 + (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = (0 + -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
232228negcld 11432 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) ∈ β„‚)
233232addid2d 11289 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (0 + -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
234231, 233eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (0 + (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
235229, 234ifeq12d 4505 . . . . . . . . . . . . . . . . . . . 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 2789 . . . . . . . . . . . . . . . . . . 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 5203 . . . . . . . . . . . . . . . . . 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 2797 . . . . . . . . . . . . . . . . 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 11135 . . . . . . . . . . . . . . . . . . . . . . 23 0 ∈ ℝ*
240 pnfxr 11142 . . . . . . . . . . . . . . . . . . . . . . 23 +∞ ∈ ℝ*
241 0ltpnf 12971 . . . . . . . . . . . . . . . . . . . . . . 23 0 < +∞
242 snunioo 13323 . . . . . . . . . . . . . . . . . . . . . . 23 ((0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0 < +∞) β†’ ({0} βˆͺ (0(,)+∞)) = (0[,)+∞))
243239, 240, 241, 242mp3an 1461 . . . . . . . . . . . . . . . . . . . . . 22 ({0} βˆͺ (0(,)+∞)) = (0[,)+∞)
244243imaeq2i 6007 . . . . . . . . . . . . . . . . . . . . 21 (β—‘(β„œ ∘ 𝐹) β€œ ({0} βˆͺ (0(,)+∞))) = (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞))
245 imaundi 6098 . . . . . . . . . . . . . . . . . . . . 21 (β—‘(β„œ ∘ 𝐹) β€œ ({0} βˆͺ (0(,)+∞))) = ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞)))
246244, 245eqtr3i 2767 . . . . . . . . . . . . . . . . . . . 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 495 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (β„œ ∘ 𝐹) ∈ MblFn)
251 mbfimasn 24918 . . . . . . . . . . . . . . . . . . . . . . 23 (((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„œ ∘ 𝐹):π·βŸΆβ„ ∧ 0 ∈ ℝ) β†’ (β—‘(β„œ ∘ 𝐹) β€œ {0}) ∈ dom vol)
25286, 251mp3an3 1450 . . . . . . . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . . . . . . . . 21 (((β„œ ∘ 𝐹) ∈ MblFn ∧ (β„œ ∘ 𝐹):π·βŸΆβ„) β†’ ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞))) ∈ dom vol)
256250, 191, 255syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((β—‘(β„œ ∘ 𝐹) β€œ {0}) βˆͺ (β—‘(β„œ ∘ 𝐹) β€œ (0(,)+∞))) ∈ dom vol)
257246, 256eqeltrid 2842 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∈ dom vol)
2584fdmd 6674 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ dom 𝐹 = 𝐷)
259 mbfdm 24912 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹 ∈ MblFn β†’ dom 𝐹 ∈ dom vol)
26042, 259syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ dom 𝐹 ∈ dom vol)
261258, 260eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐷 ∈ dom vol)
262 difmbl 24829 . . . . . . . . . . . . . . . . . . . 20 ((ℝ ∈ dom vol ∧ 𝐷 ∈ dom vol) β†’ (ℝ βˆ– 𝐷) ∈ dom vol)
26311, 261, 262sylancr 587 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (ℝ βˆ– 𝐷) ∈ dom vol)
264 unmbl 24823 . . . . . . . . . . . . . . . . . . 19 (((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) ∈ dom vol ∧ (ℝ βˆ– 𝐷) ∈ dom vol) β†’ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ∈ dom vol)
265257, 263, 264syl2anc 584 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ∈ dom vol)
266 fveq2 6837 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = π‘₯ β†’ (π‘”β€˜π‘‘) = (π‘”β€˜π‘₯))
267266breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = π‘₯ β†’ (0 ≀ (π‘”β€˜π‘‘) ↔ 0 ≀ (π‘”β€˜π‘₯)))
268267, 266ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = π‘₯ β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
269268, 84, 174fvmpt 6943 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ ∈ ℝ β†’ ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
270269eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0) = ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯))
271270ifeq1d 4503 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ ℝ β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0) = if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯), 0))
272271mpteq2ia 5206 . . . . . . . . . . . . . . . . . . . 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 12201 . . . . . . . . . . . . . . . . . . . . . 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 4536 . . . . . . . . . . . . . . . . . . . . . . 23 if(Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)), 0) = if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
280 eldif 3918 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))) ↔ (π‘₯ ∈ ℝ ∧ Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))))
281280baibr 537 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ ℝ β†’ (Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)) ↔ π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)))))
282 tru 1545 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊀
283 negex 11332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 -1 ∈ V
284283fconst 6723 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (ℝ Γ— {-1}):β„βŸΆ{-1}
285 ffn 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((ℝ Γ— {-1}):β„βŸΆ{-1} β†’ (ℝ Γ— {-1}) Fn ℝ)
286284, 285mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊀ β†’ (ℝ Γ— {-1}) Fn ℝ)
28797a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊀ β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) Fn ℝ)
288100a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (⊀ β†’ ℝ ∈ V)
289 inidm 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (ℝ ∩ ℝ) = ℝ
290283fvconst2 7147 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘₯ ∈ ℝ β†’ ((ℝ Γ— {-1})β€˜π‘₯) = -1)
291290adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊀ ∧ π‘₯ ∈ ℝ) β†’ ((ℝ Γ— {-1})β€˜π‘₯) = -1)
292269adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((⊀ ∧ π‘₯ ∈ ℝ) β†’ ((𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))β€˜π‘₯) = if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))
293286, 287, 288, 288, 289, 291, 292ofval 7618 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⊀ ∧ π‘₯ ∈ ℝ) β†’ (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯) = (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
294282, 293mpan 688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ ∈ ℝ β†’ (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯) = (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))
295294eqcomd 2743 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ ∈ ℝ β†’ (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)) = (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯))
296281, 295ifbieq1d 4508 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ ∈ ℝ β†’ if(Β¬ π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)), 0) = if(π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))), (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯), 0))
297279, 296eqtr3id 2791 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ ℝ β†’ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) = if(π‘₯ ∈ (ℝ βˆ– ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷))), (((ℝ Γ— {-1}) ∘f Β· (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))β€˜π‘₯), 0))
298297mpteq2ia 5206 . . . . . . . . . . . . . . . . . . . . 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 596 . . . . . . . . . . . . . . . . . . 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 597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ ((π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), 0)) ∘f + (π‘₯ ∈ ℝ ↦ if(π‘₯ ∈ ((β—‘(β„œ ∘ 𝐹) β€œ (0[,)+∞)) βˆͺ (ℝ βˆ– 𝐷)), 0, (-1 Β· if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))))) ∈ dom ∫1)
303238, 302eqeltrrd 2839 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) ∈ dom ∫1)
304154cbvmptv 5216 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) = (𝑑 ∈ ℝ ↦ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
305304, 31eqeltrid 2842 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) ∈ 𝐿1)
3069, 304fmptd 7056 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))):β„βŸΆβ„)
307305, 306jca 512 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) ∈ 𝐿1 ∧ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))):β„βŸΆβ„))
308307adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ ((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) ∈ 𝐿1 ∧ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))):β„βŸΆβ„))
309 ftc1anclem4 36049 . . . . . . . . . . . . . . . . 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 1120 . . . . . . . . . . . . . . . 16 (((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) ∈ dom ∫1 ∧ ((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))) ∈ 𝐿1 ∧ (π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0))):β„βŸΆβ„)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)))β€˜π‘‘) βˆ’ ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))β€˜π‘‘))))) ∈ ℝ)
311303, 308, 310syl2anc 584 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(((π‘₯ ∈ ℝ ↦ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)))β€˜π‘‘) βˆ’ ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))β€˜π‘‘))))) ∈ ℝ)
312171, 311eqeltrrid 2843 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) ∈ ℝ)
313134, 138, 139, 150, 312itg2addnc 36027 . . . . . . . . . . . . 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 2738 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
317 eqidd 2738 . . . . . . . . . . . . . . 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 7627 . . . . . . . . . . . . . 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 6841 . . . . . . . . . . . . 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 2779 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))))) = (∫2β€˜(𝑑 ∈ ℝ ↦ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))))))
321320adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))))) = (∫2β€˜(𝑑 ∈ ℝ ↦ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))))))
322 nfv 1917 . . . . . . . . . . . . . 14 Ⅎ𝑑(πœ‘ ∧ 𝑔 ∈ dom ∫1)
323 nfcv 2905 . . . . . . . . . . . . . . 15 Ⅎ𝑑𝑔
324 nfcv 2905 . . . . . . . . . . . . . . 15 Ⅎ𝑑 ∘r ≀
325 nfmpt1 5211 . . . . . . . . . . . . . . 15 Ⅎ𝑑(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
326323, 324, 325nfbr 5150 . . . . . . . . . . . . . 14 Ⅎ𝑑 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
327322, 326nfan 1902 . . . . . . . . . . . . 13 Ⅎ𝑑((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))))
328 anass 469 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ↔ (πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)))
32987ffnd 6664 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 β†’ 𝑔 Fn ℝ)
330 fvex 6850 . . . . . . . . . . . . . . . . . . . . . 22 (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ V
331 eqid 2737 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) = (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
332330, 331fnmpti 6639 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) Fn ℝ
333332a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑔 ∈ dom ∫1 β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) Fn ℝ)
334 eqidd 2738 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) = (π‘”β€˜π‘‘))
335331fvmpt2 6954 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ∈ ℝ ∧ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ V) β†’ ((𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))β€˜π‘‘) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
336330, 335mpan2 689 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ ℝ β†’ ((𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))β€˜π‘‘) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
337336adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ ((𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))β€˜π‘‘) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
338329, 333, 101, 101, 289, 334, 337ofrval 7619 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom ∫1 ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3393383com23 1126 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3403393expa 1118 . . . . . . . . . . . . . . . . 17 (((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
341340adantll 712 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
342 resubcl 11398 . . . . . . . . . . . . . . . . . . . . . . 23 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
3438, 104, 342syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
344343ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
345 absid 15115 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
3468, 345sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((πœ‘ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
347346breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ↔ (π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
348347biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
349348an32s 650 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
350349adantllr 717 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
351 breq1 5106 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘”β€˜π‘‘) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ ((π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
352 breq1 5106 . . . . . . . . . . . . . . . . . . . . . . . 24 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
353351, 352ifboth 4523 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘”β€˜π‘‘) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
354350, 353sylancom 588 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
355 subge0 11601 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ (0 ≀ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3568, 104, 355syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (0 ≀ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
357356ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (0 ≀ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ↔ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
358354, 357mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ 0 ≀ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
359344, 358absidd 15241 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
360 iftrue 4490 . . . . . . . . . . . . . . . . . . . . . . 23 (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
361360oveq2d 7365 . . . . . . . . . . . . . . . . . . . . . 22 (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
362361fveq2d 6841 . . . . . . . . . . . . . . . . . . . . 21 (0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) = (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
363362adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) = (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
3648ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
365345oveq1d 7364 . . . . . . . . . . . . . . . . . . . . 21 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
366364, 365sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
367359, 363, 3663eqtr4d 2787 . . . . . . . . . . . . . . . . . . 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 11515 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ)
369 resubcl 11398 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
3708, 368, 369syl2an 596 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
371370ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ∈ ℝ)
37288ad3antlr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
3738ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
3748adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ)
375 ltnle 11167 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 ↔ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
37686, 375mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 ↔ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
377 ltle 11176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ 0 ∈ ℝ) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
37886, 377mpan2 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
379376, 378sylbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ β†’ (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
380379imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0)
381 absnid 15117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
382380, 381syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
383382breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ↔ (π‘”β€˜π‘‘) ≀ -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
384383biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (π‘”β€˜π‘‘) ≀ -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
385384an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (π‘”β€˜π‘‘) ≀ -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
386374, 385sylanl1 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (π‘”β€˜π‘‘) ≀ -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
387372, 373, 386lenegcon2d 11671 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -(π‘”β€˜π‘‘))
388 simpll 765 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ πœ‘)
38986a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ 0 ∈ ℝ)
3908, 389ltnled 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 ↔ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
3918, 86, 377sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) < 0 β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
392390, 391sylbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0))
393392imp 407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((πœ‘ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0)
394388, 393sylan 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0)
395 negeq 11326 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘”β€˜π‘‘) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ -(π‘”β€˜π‘‘) = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
396395breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((π‘”β€˜π‘‘) = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -(π‘”β€˜π‘‘) ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
397 neg0 11380 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 -0 = 0
398 negeq 11326 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ -0 = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
399397, 398eqtr3id 2791 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ 0 = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
400399breq2d 5115 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 = if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0 ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
401396, 400ifboth 4523 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -(π‘”β€˜π‘‘) ∧ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
402387, 394, 401syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
403 suble0 11602 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ ℝ ∧ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ ℝ) β†’ (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ≀ 0 ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
4048, 368, 403syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ≀ 0 ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
405404ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ≀ 0 ↔ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
406402, 405mpbird 256 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) ≀ 0)
407371, 406absnidd 15232 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
408 subneg 11383 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) + if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
409408negeqd 11328 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) + if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
410 negdi2 11392 . . . . . . . . . . . . . . . . . . . . . . . 24 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) + if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
411409, 410eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . 23 (((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ∈ β„‚ ∧ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
41232, 140, 411syl2an 596 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
413412ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ -((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
414407, 413eqtrd 2777 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
415 iffalse 4493 . . . . . . . . . . . . . . . . . . . . . . 23 (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))
416415oveq2d 7365 . . . . . . . . . . . . . . . . . . . . . 22 (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = ((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
417416fveq2d 6841 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) = (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
418417adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))) = (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))
4198, 381sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) ≀ 0) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
420393, 419syldan 591 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) = -(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))
421420oveq1d 7364 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
422388, 421sylan 580 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ 0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) β†’ ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)) = (-(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
423414, 418, 4223eqtr4d 2787 . . . . . . . . . . . . . . . . . . 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 811 . . . . . . . . . . . . . . . . . 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 7365 . . . . . . . . . . . . . . . . 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 11116 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ β„‚)
427 pncan3 11342 . . . . . . . . . . . . . . . . . . 19 ((if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) ∈ β„‚ ∧ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) ∈ β„‚) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
428140, 426, 427syl2anr 597 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
429428adantr 481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + ((absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))) βˆ’ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
430425, 429eqtrd 2777 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ (π‘”β€˜π‘‘) ≀ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
431341, 430syldan 591 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
432328, 431sylanb 581 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0) + (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))) = (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))
433432an32s 650 . . . . . . . . . . . . 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 5201 . . . . . . . . . . . 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 6841 . . . . . . . . . . 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 2777 . . . . . . . . . 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 5113 . . . . . . . . 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 717 . . . . . . . 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 713 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) ∈ ℝ)
44063ad2antlr 725 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ π‘Œ ∈ ℝ)
441115adantl 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ∈ ℝ)
442439, 440, 441ltadd2d 11244 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ ↔ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))))) < ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + π‘Œ)))
443442adantr 481 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ ↔ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))))))) < ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + π‘Œ)))
444 ltsubadd 11558 . . . . . . . . . . 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 1160 . . . . . . . . . 10 ((πœ‘ ∧ π‘Œ ∈ ℝ+ ∧ 𝑔 ∈ dom ∫1) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ↔ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) < ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + π‘Œ)))
4464453expa 1118 . . . . . . . . 9 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ↔ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) < ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + π‘Œ)))
447446adantr 481 . . . . . . . 8 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ 𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) ↔ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) < ((∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0))) + π‘Œ)))
448438, 443, 4473bitr4d 310 . . . . . . 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 715 . . . . . 6 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ ↔ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ) < (∫2β€˜(𝑑 ∈ ℝ ↦ if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))
450131, 449mpbird 256 . . . . 5 ((((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) ∧ (𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ)
451450ex 413 . . . 4 (((πœ‘ ∧ π‘Œ ∈ ℝ+) ∧ 𝑔 ∈ dom ∫1) β†’ ((𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ))
452451reximdva 3163 . . 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 6836 . . . . . . . . . . . . . 14 (𝑓 = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) β†’ (π‘“β€˜π‘‘) = ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0)))β€˜π‘‘))
454453, 167sylan9eq 2797 . . . . . . . . . . . . 13 ((𝑓 = (π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) = if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))
455454oveq2d 7365 . . . . . . . . . . . 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 6841 . . . . . . . . . . 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 5203 . . . . . . . . . 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 6841 . . . . . . . . 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 5113 . . . . . . . 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 3579 . . . . . . 7 (((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) ∈ dom ∫1 ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ) β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ)
461460ex 413 . . . . . 6 ((π‘₯ ∈ ℝ ↦ if(0 ≀ (β„œβ€˜if(π‘₯ ∈ 𝐷, (πΉβ€˜π‘₯), 0)), if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0), -if(0 ≀ (π‘”β€˜π‘₯), (π‘”β€˜π‘₯), 0))) ∈ dom ∫1 β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ))
462303, 461syl 17 . . . . 5 ((πœ‘ ∧ 𝑔 ∈ dom ∫1) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ))
463462rexlimdva 3150 . . . 4 (πœ‘ β†’ (βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ))
464463adantr 481 . . 3 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ (βˆƒπ‘” ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ if(0 ≀ (β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)), if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0), -if(0 ≀ (π‘”β€˜π‘‘), (π‘”β€˜π‘‘), 0)))))) < π‘Œ β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ))
465452, 464syld 47 . 2 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ (βˆƒπ‘” ∈ dom ∫1(𝑔 ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)))) ∧ Β¬ (∫1β€˜π‘”) ≀ ((∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0))))) βˆ’ π‘Œ)) β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ))
46680, 465mpd 15 1 ((πœ‘ ∧ π‘Œ ∈ ℝ+) β†’ βˆƒπ‘“ ∈ dom ∫1(∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜((β„œβ€˜if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0)) βˆ’ (π‘“β€˜π‘‘))))) < π‘Œ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3443   βˆ– cdif 3905   βˆͺ cun 3906   βŠ† wss 3908  ifcif 4484  {csn 4584   class class class wbr 5103   ↦ cmpt 5186   Γ— cxp 5628  β—‘ccnv 5629  dom cdm 5630  ran crn 5631   β€œ cima 5633   ∘ ccom 5634   Fn wfn 6486  βŸΆwf 6487  β€˜cfv 6491  (class class class)co 7349   ∘f cof 7605   ∘r cofr 7606  β„‚cc 10982  β„cr 10983  0cc0 10984  1c1 10985   + caddc 10987   Β· cmul 10989  +∞cpnf 11119  β„*cxr 11121   < clt 11122   ≀ cle 11123   βˆ’ cmin 11318  -cneg 11319  β„+crp 12843  (,)cioo 13192  [,)cico 13194  [,]cicc 13195  β„œcre 14915  β„‘cim 14916  abscabs 15052  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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-inf2 9510  ax-cnex 11040  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-addrcl 11045  ax-mulcl 11046  ax-mulrcl 11047  ax-mulcom 11048  ax-addass 11049  ax-mulass 11050  ax-distr 11051  ax-i2m1 11052  ax-1ne0 11053  ax-1rid 11054  ax-rnegex 11055  ax-rrecex 11056  ax-cnre 11057  ax-pre-lttri 11058  ax-pre-lttrn 11059  ax-pre-ltadd 11060  ax-pre-mulgt0 11061  ax-pre-sup 11062  ax-addf 11063
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-disj 5069  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5528  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5585  df-se 5586  df-we 5587  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-res 5642  df-ima 5643  df-pred 6249  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6443  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-isom 6500  df-riota 7305  df-ov 7352  df-oprab 7353  df-mpo 7354  df-of 7607  df-ofr 7608  df-om 7793  df-1st 7911  df-2nd 7912  df-frecs 8179  df-wrecs 8210  df-recs 8284  df-rdg 8323  df-1o 8379  df-2o 8380  df-er 8581  df-map 8700  df-pm 8701  df-en 8817  df-dom 8818  df-sdom 8819  df-fin 8820  df-fi 9280  df-sup 9311  df-inf 9312  df-oi 9379  df-dju 9770  df-card 9808  df-pnf 11124  df-mnf 11125  df-xr 11126  df-ltxr 11127  df-le 11128  df-sub 11320  df-neg 11321  df-div 11746  df-nn 12087  df-2 12149  df-3 12150  df-4 12151  df-n0 12347  df-z 12433  df-uz 12696  df-q 12802  df-rp 12844  df-xneg 12961  df-xadd 12962  df-xmul 12963  df-ioo 13196  df-ico 13198  df-icc 13199  df-fz 13353  df-fzo 13496  df-fl 13625  df-mod 13703  df-seq 13835  df-exp 13896  df-hash 14158  df-cj 14917  df-re 14918  df-im 14919  df-sqrt 15053  df-abs 15054  df-clim 15304  df-sum 15505  df-rest 17238  df-topgen 17259  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  36051
  Copyright terms: Public domain W3C validator