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

Theorem ftc1anclem7 36556
Description: Lemma for ftc1anc 36558. (Contributed by Brendan Leahy, 13-May-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
ftc1anclem7 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) + (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2)))
Distinct variable groups:   𝑓,𝑔,π‘Ÿ,𝑑,𝑒,𝑀,π‘₯,𝑦,𝐴   𝐡,𝑓,𝑔,π‘Ÿ,𝑑,𝑒,𝑀,π‘₯,𝑦   𝐷,𝑓,𝑔,π‘Ÿ,𝑑,𝑒,𝑀,π‘₯,𝑦   𝑓,𝐹,𝑔,π‘Ÿ,𝑑,𝑒,𝑀,π‘₯,𝑦   πœ‘,𝑓,𝑔,π‘Ÿ,𝑑,𝑒,𝑀,π‘₯,𝑦   𝑓,𝐺,𝑔,π‘Ÿ,𝑒,𝑀,𝑦
Allowed substitution hints:   𝐺(π‘₯,𝑑)

Proof of Theorem ftc1anclem7
StepHypRef Expression
1 i1ff 25185 . . . . . . . . . . 11 (𝑓 ∈ dom ∫1 β†’ 𝑓:β„βŸΆβ„)
21ffvelcdmda 7084 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ ℝ)
32recnd 11239 . . . . . . . . 9 ((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ β„‚)
4 ax-icn 11166 . . . . . . . . . 10 i ∈ β„‚
5 i1ff 25185 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ 𝑔:β„βŸΆβ„)
65ffvelcdmda 7084 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
76recnd 11239 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ β„‚)
8 mulcl 11191 . . . . . . . . . 10 ((i ∈ β„‚ ∧ (π‘”β€˜π‘₯) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚)
94, 7, 8sylancr 588 . . . . . . . . 9 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚)
10 addcl 11189 . . . . . . . . 9 (((π‘“β€˜π‘₯) ∈ β„‚ ∧ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
113, 9, 10syl2an 597 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ)) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
1211anandirs 678 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
13 reex 11198 . . . . . . . . 9 ℝ ∈ V
1413a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ℝ ∈ V)
152adantlr 714 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ ℝ)
16 ovexd 7441 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ V)
171feqmptd 6958 . . . . . . . . 9 (𝑓 ∈ dom ∫1 β†’ 𝑓 = (π‘₯ ∈ ℝ ↦ (π‘“β€˜π‘₯)))
1817adantr 482 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 𝑓 = (π‘₯ ∈ ℝ ↦ (π‘“β€˜π‘₯)))
1913a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ ℝ ∈ V)
204a1i 11 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ i ∈ β„‚)
21 fconstmpt 5737 . . . . . . . . . . 11 (ℝ Γ— {i}) = (π‘₯ ∈ ℝ ↦ i)
2221a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (ℝ Γ— {i}) = (π‘₯ ∈ ℝ ↦ i))
235feqmptd 6958 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ 𝑔 = (π‘₯ ∈ ℝ ↦ (π‘”β€˜π‘₯)))
2419, 20, 6, 22, 23offval2 7687 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ ((ℝ Γ— {i}) ∘f Β· 𝑔) = (π‘₯ ∈ ℝ ↦ (i Β· (π‘”β€˜π‘₯))))
2524adantl 483 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((ℝ Γ— {i}) ∘f Β· 𝑔) = (π‘₯ ∈ ℝ ↦ (i Β· (π‘”β€˜π‘₯))))
2614, 15, 16, 18, 25offval2 7687 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔)) = (π‘₯ ∈ ℝ ↦ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
27 absf 15281 . . . . . . . . 9 abs:β„‚βŸΆβ„
2827a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ abs:β„‚βŸΆβ„)
2928feqmptd 6958 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ abs = (𝑑 ∈ β„‚ ↦ (absβ€˜π‘‘)))
30 fveq2 6889 . . . . . . 7 (𝑑 = ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) β†’ (absβ€˜π‘‘) = (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
3112, 26, 29, 30fmptco 7124 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs ∘ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔))) = (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))))
32 ftc1anclem3 36552 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs ∘ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔))) ∈ dom ∫1)
3331, 32eqeltrrd 2835 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) ∈ dom ∫1)
34 ioombl 25074 . . . . 5 (𝑒(,)𝑀) ∈ dom vol
35 fveq2 6889 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (π‘“β€˜π‘₯) = (π‘“β€˜π‘‘))
36 fveq2 6889 . . . . . . . . . . . . 13 (π‘₯ = 𝑑 β†’ (π‘”β€˜π‘₯) = (π‘”β€˜π‘‘))
3736oveq2d 7422 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (i Β· (π‘”β€˜π‘₯)) = (i Β· (π‘”β€˜π‘‘)))
3835, 37oveq12d 7424 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) = ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))
3938fveq2d 6893 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
40 eqid 2733 . . . . . . . . . 10 (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) = (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
41 fvex 6902 . . . . . . . . . 10 (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ V
4239, 40, 41fvmpt 6996 . . . . . . . . 9 (𝑑 ∈ ℝ β†’ ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
4342eqcomd 2739 . . . . . . . 8 (𝑑 ∈ ℝ β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘))
4443ifeq1d 4547 . . . . . . 7 (𝑑 ∈ ℝ β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = if(𝑑 ∈ (𝑒(,)𝑀), ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘), 0))
4544mpteq2ia 5251 . . . . . 6 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘), 0))
4645i1fres 25215 . . . . 5 (((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) ∈ dom ∫1 ∧ (𝑒(,)𝑀) ∈ dom vol) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1)
4733, 34, 46sylancl 587 . . . 4 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1)
48 breq2 5152 . . . . . . 7 ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) β†’ (0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ↔ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
49 breq2 5152 . . . . . . 7 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
50 elioore 13351 . . . . . . . 8 (𝑑 ∈ (𝑒(,)𝑀) β†’ 𝑑 ∈ ℝ)
51 eleq1w 2817 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (π‘₯ ∈ ℝ ↔ 𝑑 ∈ ℝ))
5251anbi2d 630 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) ↔ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ)))
5338eleq1d 2819 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ (((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚ ↔ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚))
5452, 53imbi12d 345 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚) ↔ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)))
5554, 12chvarvv 2003 . . . . . . . . 9 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
5655absge0d 15388 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
5750, 56sylan2 594 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
58 0le0 12310 . . . . . . . 8 0 ≀ 0
5958a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ 0)
6048, 49, 57, 59ifbothda 4566 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
6160ralrimivw 3151 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆ€π‘‘ ∈ ℝ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
62 ax-resscn 11164 . . . . . . . 8 ℝ βŠ† β„‚
6362a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ℝ βŠ† β„‚)
64 c0ex 11205 . . . . . . . . . 10 0 ∈ V
6541, 64ifex 4578 . . . . . . . . 9 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ V
66 eqid 2733 . . . . . . . . 9 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
6765, 66fnmpti 6691 . . . . . . . 8 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) Fn ℝ
6867a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) Fn ℝ)
6963, 680pledm 25182 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ↔ (ℝ Γ— {0}) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))))
7064a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ∈ V)
7165a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ V)
72 fconstmpt 5737 . . . . . . . 8 (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0)
7372a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0))
74 eqidd 2734 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
7514, 70, 71, 73, 74ofrfval2 7688 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((ℝ Γ— {0}) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
7669, 75bitrd 279 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
7761, 76mpbird 257 . . . 4 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
78 itg2itg1 25246 . . . . 5 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) = (∫1β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))))
79 itg1cl 25194 . . . . . 6 ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8079adantr 482 . . . . 5 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8178, 80eqeltrd 2834 . . . 4 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8247, 77, 81syl2anc 585 . . 3 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8382ad6antlr 736 . 2 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
84 simplll 774 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
85 ftc1anc.a . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐴 ∈ ℝ)
8685rexrd 11261 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 ∈ ℝ*)
87 ftc1anc.b . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐡 ∈ ℝ)
8887rexrd 11261 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 ∈ ℝ*)
8986, 88jca 513 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*))
90 df-icc 13328 . . . . . . . . . . . . . . . . . . . . . 22 [,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑑 ∈ ℝ* ∣ (π‘₯ ≀ 𝑑 ∧ 𝑑 ≀ 𝑦)})
9190elixx3g 13334 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑒 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
9291simprbi 498 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡))
9392simpld 496 . . . . . . . . . . . . . . . . . . 19 (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝐴 ≀ 𝑒)
9490elixx3g 13334 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑀 ∈ ℝ*) ∧ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡)))
9594simprbi 498 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡))
9695simprd 497 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (𝐴[,]𝐡) β†’ 𝑀 ≀ 𝐡)
9793, 96anim12i 614 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡))
98 ioossioo 13415 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡)) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
9989, 97, 98syl2an 597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
100 ftc1anc.s . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† 𝐷)
101100adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝐴(,)𝐡) βŠ† 𝐷)
10299, 101sstrd 3992 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
1031023adantr3 1172 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
104103sselda 3982 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
105 ftc1anc.f . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:π·βŸΆβ„‚)
106105ffvelcdmda 7084 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
107106adantlr 714 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
108104, 107syldan 592 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
109108adantllr 718 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
11055adantll 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
11150, 110sylan2 594 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
112111adantlr 714 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
113109, 112subcld 11568 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
114113abscld 15380 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
115114rexrd 11261 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
116113absge0d 15388 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
117 elxrge0 13431 . . . . . . . . 9 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞) ↔ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ* ∧ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
118115, 116, 117sylanbrc 584 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
119 0e0iccpnf 13433 . . . . . . . . 9 0 ∈ (0[,]+∞)
120119a1i 11 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
121118, 120ifclda 4563 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
122121adantr 482 . . . . . 6 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
123122fmpttd 7112 . . . . 5 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞))
12484, 123sylan 581 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞))
125 rpre 12979 . . . . . 6 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
126125rehalfcld 12456 . . . . 5 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ)
127126ad2antlr 726 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑦 / 2) ∈ ℝ)
128 simpll 766 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
129102sselda 3982 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
130129adantllr 718 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
131106adantlr 714 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
132 ftc1anc.d . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐷 βŠ† ℝ)
133132sselda 3982 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 𝑑 ∈ ℝ)
134133adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ 𝑑 ∈ ℝ)
135134, 110syldan 592 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
136131, 135subcld 11568 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
137136abscld 15380 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
138137rexrd 11261 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
139138adantlr 714 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
140130, 139syldan 592 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
141136absge0d 15388 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
142141adantlr 714 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
143130, 142syldan 592 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
144140, 143, 117sylanbrc 584 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
145119a1i 11 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
146144, 145ifclda 4563 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
147146adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
148147fmpttd 7112 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞))
149 itg2cl 25242 . . . . . . . . 9 ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
150148, 149syl 17 . . . . . . . 8 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
151128, 150sylan 581 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
152 rphalfcl 12998 . . . . . . . . 9 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ+)
153152rpxrd 13014 . . . . . . . 8 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ*)
154153ad2antlr 726 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑦 / 2) ∈ ℝ*)
155 0cnd 11204 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ β„‚)
156106, 155ifclda 4563 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚)
157 subcl 11456 . . . . . . . . . . . . . . . 16 ((if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚ ∧ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
158156, 55, 157syl2an 597 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ)) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
159158anassrs 469 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
160159abscld 15380 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
161160rexrd 11261 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
162159absge0d 15388 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
163 elxrge0 13431 . . . . . . . . . . . 12 ((absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞) ↔ ((absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ* ∧ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
164161, 162, 163sylanbrc 584 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
165164fmpttd 7112 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))):β„βŸΆ(0[,]+∞))
166 itg2cl 25242 . . . . . . . . . 10 ((𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))):β„βŸΆ(0[,]+∞) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) ∈ ℝ*)
167165, 166syl 17 . . . . . . . . 9 ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) ∈ ℝ*)
168167ad3antrrr 729 . . . . . . . 8 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) ∈ ℝ*)
169165adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))):β„βŸΆ(0[,]+∞))
170 breq1 5151 . . . . . . . . . . . . 13 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
171 breq1 5151 . . . . . . . . . . . . 13 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) β†’ (0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
172137leidd 11777 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
173 iftrue 4534 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝐷 β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) = (πΉβ€˜π‘‘))
174173fvoveq1d 7428 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ 𝐷 β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
175174adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
176172, 175breqtrrd 5176 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
177176adantlr 714 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
178130, 177syldan 592 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
179178adantlr 714 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
180162adantlr 714 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
181180adantr 482 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
182170, 171, 179, 181ifbothda 4566 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
183182ralrimiva 3147 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
18413a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ℝ ∈ V)
185 fvex 6902 . . . . . . . . . . . . . . 15 (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V
186185, 64ifex 4578 . . . . . . . . . . . . . 14 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V
187186a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V)
188 fvexd 6904 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V)
189 eqidd 2734 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
190 eqidd 2734 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) = (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
191184, 187, 188, 189, 190ofrfval2 7688 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
192191ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
193183, 192mpbird 257 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
194 itg2le 25249 . . . . . . . . . 10 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))))
195148, 169, 193, 194syl3anc 1372 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))))
196128, 195sylan 581 . . . . . . . 8 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))))
197 simpllr 775 . . . . . . . 8 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
198151, 168, 154, 196, 197xrlelttrd 13136 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
199151, 154, 198xrltled 13126 . . . . . 6 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2))
200199adantllr 718 . . . . 5 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2))
2012003adantr3 1172 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2))
202 itg2lecl 25248 . . . 4 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑦 / 2) ∈ ℝ ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ)
203124, 127, 201, 202syl3anc 1372 . . 3 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ)
204203adantr 482 . 2 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ)
205126ad3antlr 730 . 2 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (𝑦 / 2) ∈ ℝ)
20682adantr 482 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
207 2rp 12976 . . . . . . . . 9 2 ∈ ℝ+
208 imassrn 6069 . . . . . . . . . . . . . . . 16 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ran abs
209 frn 6722 . . . . . . . . . . . . . . . . 17 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
21027, 209ax-mp 5 . . . . . . . . . . . . . . . 16 ran abs βŠ† ℝ
211208, 210sstri 3991 . . . . . . . . . . . . . . 15 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ
212211a1i 11 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ)
2131frnd 6723 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 βŠ† ℝ)
214213adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑓 βŠ† ℝ)
2155frnd 6723 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 βŠ† ℝ)
216215adantl 483 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑔 βŠ† ℝ)
217214, 216unssd 4186 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† ℝ)
218217, 62sstrdi 3994 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚)
219 i1f0rn 25191 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 β†’ 0 ∈ ran 𝑓)
220 elun1 4176 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran 𝑓 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
221219, 220syl 17 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
222221adantr 482 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
223 ffn 6715 . . . . . . . . . . . . . . . . . 18 (abs:β„‚βŸΆβ„ β†’ abs Fn β„‚)
22427, 223ax-mp 5 . . . . . . . . . . . . . . . . 17 abs Fn β„‚
225 fnfvima 7232 . . . . . . . . . . . . . . . . 17 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
226224, 225mp3an1 1449 . . . . . . . . . . . . . . . 16 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
227218, 222, 226syl2anc 585 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
228227ne0d 4335 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ…)
229 ffun 6718 . . . . . . . . . . . . . . . . 17 (abs:β„‚βŸΆβ„ β†’ Fun abs)
23027, 229ax-mp 5 . . . . . . . . . . . . . . . 16 Fun abs
231 i1frn 25186 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 ∈ Fin)
232 i1frn 25186 . . . . . . . . . . . . . . . . 17 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 ∈ Fin)
233 unfi 9169 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
234231, 232, 233syl2an 597 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
235 imafi 9172 . . . . . . . . . . . . . . . 16 ((Fun abs ∧ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
236230, 234, 235sylancr 588 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
237 fimaxre2 12156 . . . . . . . . . . . . . . 15 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
238211, 236, 237sylancr 588 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
239 suprcl 12171 . . . . . . . . . . . . . 14 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
240212, 228, 238, 239syl3anc 1372 . . . . . . . . . . . . 13 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
241240adantr 482 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
242 0red 11214 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 ∈ ℝ)
243218sselda 3982 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ π‘Ÿ ∈ β„‚)
244243abscld 15380 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
245244adantrr 716 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
246 absgt0 15268 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ β„‚ β†’ (π‘Ÿ β‰  0 ↔ 0 < (absβ€˜π‘Ÿ)))
247243, 246syl 17 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (π‘Ÿ β‰  0 ↔ 0 < (absβ€˜π‘Ÿ)))
248247biimpa 478 . . . . . . . . . . . . . 14 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) ∧ π‘Ÿ β‰  0) β†’ 0 < (absβ€˜π‘Ÿ))
249248anasss 468 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < (absβ€˜π‘Ÿ))
250212, 228, 2383jca 1129 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
251250adantr 482 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
252 fnfvima 7232 . . . . . . . . . . . . . . . . 17 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
253224, 252mp3an1 1449 . . . . . . . . . . . . . . . 16 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
254218, 253sylan 581 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
255 suprub 12172 . . . . . . . . . . . . . . 15 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
256251, 254, 255syl2anc 585 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
257256adantrr 716 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
258242, 245, 241, 249, 257ltletrd 11371 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
259241, 258elrpd 13010 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+)
260259rexlimdvaa 3157 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0 β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+))
261260imp 408 . . . . . . . . 9 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+)
262 rpmulcl 12994 . . . . . . . . 9 ((2 ∈ ℝ+ ∧ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
263207, 261, 262sylancr 588 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
264206, 263rerpdivcld 13044 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
265264adantll 713 . . . . . 6 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
266265adantlr 714 . . . . 5 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
267266ad3antrrr 729 . . . 4 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
268 simp-4l 782 . . . . . 6 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ πœ‘)
269 iccssre 13403 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
27085, 87, 269syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
271270, 62sstrdi 3994 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† β„‚)
272271sselda 3982 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ β„‚)
273271sselda 3982 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ β„‚)
274 subcl 11456 . . . . . . . . . 10 ((𝑀 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
275272, 273, 274syl2anr 598 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
276275anandis 677 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
277276abscld 15380 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
2782773adantr3 1172 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
279268, 278sylan 581 . . . . 5 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
280279adantr 482 . . . 4 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
281 rpdivcl 12996 . . . . . . . . 9 (((𝑦 / 2) ∈ ℝ+ ∧ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
282152, 263, 281syl2anr 598 . . . . . . . 8 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
283282rpred 13013 . . . . . . 7 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
284283adantlll 717 . . . . . 6 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
285284adantllr 718 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
286285ad2antrr 725 . . . 4 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
287270sseld 3981 . . . . . . . . . . 11 (πœ‘ β†’ (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝑒 ∈ ℝ))
288270sseld 3981 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀 ∈ (𝐴[,]𝐡) β†’ 𝑀 ∈ ℝ))
289 idd 24 . . . . . . . . . . 11 (πœ‘ β†’ (𝑒 ≀ 𝑀 β†’ 𝑒 ≀ 𝑀))
290287, 288, 2893anim123d 1444 . . . . . . . . . 10 (πœ‘ β†’ ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀) β†’ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)))
291290ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀) β†’ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)))
292291imp 408 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀))
29355abscld 15380 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
294293rexrd 11261 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ*)
295 elxrge0 13431 . . . . . . . . . . . . . . . . . 18 ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞) ↔ ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ* ∧ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
296294, 56, 295sylanbrc 584 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞))
297 ifcl 4573 . . . . . . . . . . . . . . . . 17 (((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ (0[,]+∞))
298296, 119, 297sylancl 587 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ (0[,]+∞))
299298fmpttd 7112 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)):β„βŸΆ(0[,]+∞))
300240recnd 11239 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ β„‚)
3013002timesd 12452 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) = (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
302240, 240readdcld 11240 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ)
303302rexrd 11261 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ*)
304 abs0 15229 . . . . . . . . . . . . . . . . . . . . . . 23 (absβ€˜0) = 0
305304, 227eqeltrrid 2839 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
306 suprub 12172 . . . . . . . . . . . . . . . . . . . . . 22 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ 0 ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ 0 ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
307250, 305, 306syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
308240, 240, 307, 307addge0d 11787 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
309 elxrge0 13431 . . . . . . . . . . . . . . . . . . . 20 ((sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞) ↔ ((sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ* ∧ 0 ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))))
310303, 308, 309sylanbrc 584 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
311301, 310eqeltrd 2834 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
312 ifcl 4573 . . . . . . . . . . . . . . . . . 18 (((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
313311, 119, 312sylancl 587 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
314313adantr 482 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
315314fmpttd 7112 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)):β„βŸΆ(0[,]+∞))
3161ffvelcdmda 7084 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ℝ)
317316recnd 11239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ β„‚)
318317abscld 15380 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ ℝ)
3195ffvelcdmda 7084 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
320319recnd 11239 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ β„‚)
321320abscld 15380 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ ℝ)
322 readdcl 11190 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((absβ€˜(π‘“β€˜π‘‘)) ∈ ℝ ∧ (absβ€˜(π‘”β€˜π‘‘)) ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ∈ ℝ)
323318, 321, 322syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ∈ ℝ)
324323anandirs 678 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ∈ ℝ)
325302adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ)
326 mulcl 11191 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
3274, 320, 326sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
328 abstri 15274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘“β€˜π‘‘) ∈ β„‚ ∧ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))))
329317, 327, 328syl2an 597 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))))
330329anandirs 678 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))))
331 absmul 15238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))))
3324, 320, 331sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))))
333 absi 15230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (absβ€˜i) = 1
334333oveq1i 7416 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))) = (1 Β· (absβ€˜(π‘”β€˜π‘‘)))
335332, 334eqtrdi 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (1 Β· (absβ€˜(π‘”β€˜π‘‘))))
336321recnd 11239 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ β„‚)
337336mullidd 11229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (1 Β· (absβ€˜(π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
338335, 337eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
339338adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
340339oveq2d 7422 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))) = ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))))
341330, 340breqtrd 5174 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))))
342318adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ ℝ)
343321adantll 713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ ℝ)
344240adantr 482 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
345250adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
346218adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚)
3471ffnd 6716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ dom ∫1 β†’ 𝑓 Fn ℝ)
348 fnfvelrn 7080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
349347, 348sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
350 elun1 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘“β€˜π‘‘) ∈ ran 𝑓 β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
351349, 350syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
352351adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
353 fnfvima 7232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
354224, 353mp3an1 1449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
355346, 352, 354syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
356 suprub 12172 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜(π‘“β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
357345, 355, 356syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
3585ffnd 6716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ dom ∫1 β†’ 𝑔 Fn ℝ)
359 fnfvelrn 7080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
360358, 359sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
361 elun2 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘”β€˜π‘‘) ∈ ran 𝑔 β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
362360, 361syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
363362adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
364 fnfvima 7232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
365224, 364mp3an1 1449 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
366346, 363, 365syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
367 suprub 12172 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜(π‘”β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
368345, 366, 367syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
369342, 343, 344, 344, 357, 368le2addd 11830 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
370293, 324, 325, 341, 369letrd 11368 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
371301adantr 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) = (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
372370, 371breqtrrd 5176 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
37350, 372sylan2 594 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
374 iftrue 4534 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
375374adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
376 iftrue 4534 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) = (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
377376adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) = (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
378373, 375, 3773brtr4d 5180 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))
379378ex 414 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
38058a1i 11 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ 0 ≀ 0)
381 iffalse 4537 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = 0)
382 iffalse 4537 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) = 0)
383380, 381, 3823brtr4d 5180 . . . . . . . . . . . . . . . . . 18 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))
384379, 383pm2.61d1 180 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))
385384ralrimivw 3151 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))
386 ovex 7439 . . . . . . . . . . . . . . . . . . 19 (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ V
387386, 64ifex 4578 . . . . . . . . . . . . . . . . . 18 if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ V
388387a1i 11 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ V)
389 eqidd 2734 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
39014, 71, 388, 74, 389ofrfval2 7688 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
391385, 390mpbird 257 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
392 itg2le 25249 . . . . . . . . . . . . . . 15 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))))
393299, 315, 391, 392syl3anc 1372 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))))
394393adantr 482 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))))
395 mblvol 25039 . . . . . . . . . . . . . . . . 17 ((𝑒(,)𝑀) ∈ dom vol β†’ (volβ€˜(𝑒(,)𝑀)) = (vol*β€˜(𝑒(,)𝑀)))
39634, 395ax-mp 5 . . . . . . . . . . . . . . . 16 (volβ€˜(𝑒(,)𝑀)) = (vol*β€˜(𝑒(,)𝑀))
397 ovolioo 25077 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (vol*β€˜(𝑒(,)𝑀)) = (𝑀 βˆ’ 𝑒))
398396, 397eqtrid 2785 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) = (𝑀 βˆ’ 𝑒))
399 resubcl 11521 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑒 ∈ ℝ) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
400399ancoms 460 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
4014003adant3 1133 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
402398, 401eqeltrd 2834 . . . . . . . . . . . . . 14 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) ∈ ℝ)
403 elrege0 13428 . . . . . . . . . . . . . . . . 17 (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ↔ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ ∧ 0 ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
404240, 307, 403sylanbrc 584 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞))
405 ge0addcl 13434 . . . . . . . . . . . . . . . 16 ((sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ∧ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞)) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
406404, 404, 405syl2anc 585 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
407301, 406eqeltrd 2834 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
408 itg2const 25250 . . . . . . . . . . . . . . 15 (((𝑒(,)𝑀) ∈ dom vol ∧ (volβ€˜(𝑒(,)𝑀)) ∈ ℝ ∧ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))) = ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
40934, 408mp3an1 1449 . . . . . . . . . . . . . 14 (((volβ€˜(𝑒(,)𝑀)) ∈ ℝ ∧ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))) = ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
410402, 407, 409syl2anr 598 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))) = ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
411394, 410breqtrd 5174 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
412411adantll 713 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
413412adantlr 714 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
41482ad3antlr 730 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
415402adantl 483 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (volβ€˜(𝑒(,)𝑀)) ∈ ℝ)
416263adantll 713 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
417416adantr 482 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
418414, 415, 417ledivmuld 13066 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (volβ€˜(𝑒(,)𝑀)) ↔ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀)))))
419413, 418mpbird 257 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (volβ€˜(𝑒(,)𝑀)))
420 abssubge0 15271 . . . . . . . . . . . 12 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (𝑀 βˆ’ 𝑒))
421397, 420eqtr4d 2776 . . . . . . . . . . 11 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (vol*β€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
422396, 421eqtrid 2785 . . . . . . . . . 10 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
423422adantl 483 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (volβ€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
424419, 423breqtrd 5174 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (absβ€˜(𝑀 βˆ’ 𝑒)))
425292, 424syldan 592 . . . . . . 7 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (absβ€˜(𝑀 βˆ’ 𝑒)))
426425adantllr 718 . . . . . 6 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (absβ€˜(𝑀 βˆ’ 𝑒)))
427426adantlr 714 . . . . 5 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (absβ€˜(𝑀 βˆ’ 𝑒)))
428427adantr 482 . . . 4 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (absβ€˜(𝑀 βˆ’ 𝑒)))
429 simpr 486 . . . 4 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))))
430267, 280, 286, 428, 429lelttrd 11369 . . 3 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))))
43182adantl 483 . . . . . 6 ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
432431ad3antrrr 729 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
433126adantl 483 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (𝑦 / 2) ∈ ℝ)
434416adantlr 714 . . . . . 6 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
435434adantr 482 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
436432, 433, 435ltdiv1d 13058 . . . 4 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) < (𝑦 / 2) ↔ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
437436ad2antrr 725 . . 3 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) < (𝑦 / 2) ↔ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))))
438430, 437mpbird 257 . 2 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) < (𝑦 / 2))
439198adantllr 718 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
4404393adantr3 1172 . . 3 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
441440adantr 482 . 2 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
44283, 204, 205, 205, 438, 441lt2addd 11834 1 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) + (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))) < ((𝑦 / 2) + (𝑦 / 2)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3475   βˆͺ cun 3946   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  dom cdm 5676  ran crn 5677   β€œ cima 5679   ∘ ccom 5680  Fun wfun 6535   Fn wfn 6536  βŸΆwf 6537  β€˜cfv 6541  (class class class)co 7406   ∘f cof 7665   ∘r cofr 7666  Fincfn 8936  supcsup 9432  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108  ici 11109   + caddc 11110   Β· cmul 11112  +∞cpnf 11242  β„*cxr 11244   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441   / cdiv 11868  2c2 12264  β„+crp 12971  (,)cioo 13321  [,)cico 13323  [,]cicc 13324  abscabs 15178  vol*covol 24971  volcvol 24972  βˆ«1citg1 25124  βˆ«2citg2 25125  πΏ1cibl 25126  βˆ«citg 25127  0𝑝c0p 25178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-ofr 7668  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-2o 8464  df-er 8700  df-map 8819  df-pm 8820  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-dju 9893  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-n0 12470  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-clim 15429  df-rlim 15430  df-sum 15630  df-rest 17365  df-topgen 17386  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-top 22388  df-topon 22405  df-bases 22441  df-cmp 22883  df-ovol 24973  df-vol 24974  df-mbf 25128  df-itg1 25129  df-itg2 25130  df-0p 25179
This theorem is referenced by:  ftc1anclem8  36557
  Copyright terms: Public domain W3C validator