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 36052
Description: Lemma for ftc1anc 36054. (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 24962 . . . . . . . . . . 11 (𝑓 ∈ dom ∫1 β†’ 𝑓:β„βŸΆβ„)
21ffvelcdmda 7029 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ ℝ)
32recnd 11116 . . . . . . . . 9 ((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ β„‚)
4 ax-icn 11043 . . . . . . . . . 10 i ∈ β„‚
5 i1ff 24962 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ 𝑔:β„βŸΆβ„)
65ffvelcdmda 7029 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
76recnd 11116 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ β„‚)
8 mulcl 11068 . . . . . . . . . 10 ((i ∈ β„‚ ∧ (π‘”β€˜π‘₯) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚)
94, 7, 8sylancr 587 . . . . . . . . 9 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚)
10 addcl 11066 . . . . . . . . 9 (((π‘“β€˜π‘₯) ∈ β„‚ ∧ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
113, 9, 10syl2an 596 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ)) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
1211anandirs 677 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
13 reex 11075 . . . . . . . . 9 ℝ ∈ V
1413a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ℝ ∈ V)
152adantlr 713 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ ℝ)
16 ovexd 7384 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ V)
171feqmptd 6905 . . . . . . . . 9 (𝑓 ∈ dom ∫1 β†’ 𝑓 = (π‘₯ ∈ ℝ ↦ (π‘“β€˜π‘₯)))
1817adantr 481 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 𝑓 = (π‘₯ ∈ ℝ ↦ (π‘“β€˜π‘₯)))
1913a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ ℝ ∈ V)
204a1i 11 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ i ∈ β„‚)
21 fconstmpt 5690 . . . . . . . . . . 11 (ℝ Γ— {i}) = (π‘₯ ∈ ℝ ↦ i)
2221a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (ℝ Γ— {i}) = (π‘₯ ∈ ℝ ↦ i))
235feqmptd 6905 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ 𝑔 = (π‘₯ ∈ ℝ ↦ (π‘”β€˜π‘₯)))
2419, 20, 6, 22, 23offval2 7627 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ ((ℝ Γ— {i}) ∘f Β· 𝑔) = (π‘₯ ∈ ℝ ↦ (i Β· (π‘”β€˜π‘₯))))
2524adantl 482 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((ℝ Γ— {i}) ∘f Β· 𝑔) = (π‘₯ ∈ ℝ ↦ (i Β· (π‘”β€˜π‘₯))))
2614, 15, 16, 18, 25offval2 7627 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔)) = (π‘₯ ∈ ℝ ↦ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
27 absf 15156 . . . . . . . . 9 abs:β„‚βŸΆβ„
2827a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ abs:β„‚βŸΆβ„)
2928feqmptd 6905 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ abs = (𝑑 ∈ β„‚ ↦ (absβ€˜π‘‘)))
30 fveq2 6837 . . . . . . 7 (𝑑 = ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) β†’ (absβ€˜π‘‘) = (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
3112, 26, 29, 30fmptco 7069 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs ∘ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔))) = (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))))
32 ftc1anclem3 36048 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs ∘ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔))) ∈ dom ∫1)
3331, 32eqeltrrd 2839 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) ∈ dom ∫1)
34 ioombl 24851 . . . . 5 (𝑒(,)𝑀) ∈ dom vol
35 fveq2 6837 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (π‘“β€˜π‘₯) = (π‘“β€˜π‘‘))
36 fveq2 6837 . . . . . . . . . . . . 13 (π‘₯ = 𝑑 β†’ (π‘”β€˜π‘₯) = (π‘”β€˜π‘‘))
3736oveq2d 7365 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (i Β· (π‘”β€˜π‘₯)) = (i Β· (π‘”β€˜π‘‘)))
3835, 37oveq12d 7367 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) = ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))
3938fveq2d 6841 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
40 eqid 2737 . . . . . . . . . 10 (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) = (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
41 fvex 6850 . . . . . . . . . 10 (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ V
4239, 40, 41fvmpt 6943 . . . . . . . . 9 (𝑑 ∈ ℝ β†’ ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
4342eqcomd 2743 . . . . . . . 8 (𝑑 ∈ ℝ β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘))
4443ifeq1d 4503 . . . . . . 7 (𝑑 ∈ ℝ β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = if(𝑑 ∈ (𝑒(,)𝑀), ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘), 0))
4544mpteq2ia 5206 . . . . . 6 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘), 0))
4645i1fres 24992 . . . . 5 (((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) ∈ dom ∫1 ∧ (𝑒(,)𝑀) ∈ dom vol) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1)
4733, 34, 46sylancl 586 . . . 4 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1)
48 breq2 5107 . . . . . . 7 ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) β†’ (0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ↔ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
49 breq2 5107 . . . . . . 7 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
50 elioore 13222 . . . . . . . 8 (𝑑 ∈ (𝑒(,)𝑀) β†’ 𝑑 ∈ ℝ)
51 eleq1w 2820 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (π‘₯ ∈ ℝ ↔ 𝑑 ∈ ℝ))
5251anbi2d 629 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) ↔ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ)))
5338eleq1d 2822 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ (((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚ ↔ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚))
5452, 53imbi12d 344 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚) ↔ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)))
5554, 12chvarvv 2002 . . . . . . . . 9 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
5655absge0d 15263 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
5750, 56sylan2 593 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
58 0le0 12187 . . . . . . . 8 0 ≀ 0
5958a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ 0)
6048, 49, 57, 59ifbothda 4522 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
6160ralrimivw 3145 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆ€π‘‘ ∈ ℝ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
62 ax-resscn 11041 . . . . . . . 8 ℝ βŠ† β„‚
6362a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ℝ βŠ† β„‚)
64 c0ex 11082 . . . . . . . . . 10 0 ∈ V
6541, 64ifex 4534 . . . . . . . . 9 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ V
66 eqid 2737 . . . . . . . . 9 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
6765, 66fnmpti 6639 . . . . . . . 8 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) Fn ℝ
6867a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) Fn ℝ)
6963, 680pledm 24959 . . . . . 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 5690 . . . . . . . 8 (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0)
7372a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0))
74 eqidd 2738 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
7514, 70, 71, 73, 74ofrfval2 7628 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((ℝ Γ— {0}) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
7669, 75bitrd 278 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ↔ βˆ€π‘‘ ∈ ℝ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
7761, 76mpbird 256 . . . 4 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
78 itg2itg1 25023 . . . . 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 24971 . . . . . 6 ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8079adantr 481 . . . . 5 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8178, 80eqeltrd 2838 . . . 4 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8247, 77, 81syl2anc 584 . . 3 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8382ad6antlr 735 . 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 773 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
85 ftc1anc.a . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐴 ∈ ℝ)
8685rexrd 11138 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 ∈ ℝ*)
87 ftc1anc.b . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐡 ∈ ℝ)
8887rexrd 11138 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 ∈ ℝ*)
8986, 88jca 512 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*))
90 df-icc 13199 . . . . . . . . . . . . . . . . . . . . . 22 [,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑑 ∈ ℝ* ∣ (π‘₯ ≀ 𝑑 ∧ 𝑑 ≀ 𝑦)})
9190elixx3g 13205 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑒 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
9291simprbi 497 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡))
9392simpld 495 . . . . . . . . . . . . . . . . . . 19 (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝐴 ≀ 𝑒)
9490elixx3g 13205 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑀 ∈ ℝ*) ∧ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡)))
9594simprbi 497 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡))
9695simprd 496 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (𝐴[,]𝐡) β†’ 𝑀 ≀ 𝐡)
9793, 96anim12i 613 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡))
98 ioossioo 13286 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡)) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
9989, 97, 98syl2an 596 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
100 ftc1anc.s . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† 𝐷)
101100adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝐴(,)𝐡) βŠ† 𝐷)
10299, 101sstrd 3952 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
1031023adantr3 1171 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
104103sselda 3942 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
105 ftc1anc.f . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:π·βŸΆβ„‚)
106105ffvelcdmda 7029 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
107106adantlr 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
108104, 107syldan 591 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
109108adantllr 717 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
11055adantll 712 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
11150, 110sylan2 593 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
112111adantlr 713 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
113109, 112subcld 11445 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
114113abscld 15255 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
115114rexrd 11138 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
116113absge0d 15263 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
117 elxrge0 13302 . . . . . . . . 9 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞) ↔ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ* ∧ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
118115, 116, 117sylanbrc 583 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
119 0e0iccpnf 13304 . . . . . . . . 9 0 ∈ (0[,]+∞)
120119a1i 11 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
121118, 120ifclda 4519 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
122121adantr 481 . . . . . 6 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
123122fmpttd 7057 . . . . 5 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞))
12484, 123sylan 580 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞))
125 rpre 12851 . . . . . 6 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
126125rehalfcld 12333 . . . . 5 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ)
127126ad2antlr 725 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑦 / 2) ∈ ℝ)
128 simpll 765 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) β†’ (πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)))
129102sselda 3942 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
130129adantllr 717 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
131106adantlr 713 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
132 ftc1anc.d . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐷 βŠ† ℝ)
133132sselda 3942 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 𝑑 ∈ ℝ)
134133adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ 𝑑 ∈ ℝ)
135134, 110syldan 591 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
136131, 135subcld 11445 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
137136abscld 15255 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
138137rexrd 11138 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
139138adantlr 713 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
140130, 139syldan 591 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
141136absge0d 15263 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
142141adantlr 713 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
143130, 142syldan 591 . . . . . . . . . . . . 13 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
144140, 143, 117sylanbrc 583 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
145119a1i 11 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
146144, 145ifclda 4519 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
147146adantr 481 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
148147fmpttd 7057 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞))
149 itg2cl 25019 . . . . . . . . 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 580 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
152 rphalfcl 12870 . . . . . . . . 9 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ+)
153152rpxrd 12886 . . . . . . . 8 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ*)
154153ad2antlr 725 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑦 / 2) ∈ ℝ*)
155 0cnd 11081 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ β„‚)
156106, 155ifclda 4519 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚)
157 subcl 11333 . . . . . . . . . . . . . . . 16 ((if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚ ∧ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
158156, 55, 157syl2an 596 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ)) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
159158anassrs 468 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
160159abscld 15255 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
161160rexrd 11138 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
162159absge0d 15263 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
163 elxrge0 13302 . . . . . . . . . . . 12 ((absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞) ↔ ((absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ* ∧ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
164161, 162, 163sylanbrc 583 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
165164fmpttd 7057 . . . . . . . . . 10 ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))):β„βŸΆ(0[,]+∞))
166 itg2cl 25019 . . . . . . . . . 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 728 . . . . . . . 8 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) ∈ ℝ*)
169165adantr 481 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))):β„βŸΆ(0[,]+∞))
170 breq1 5106 . . . . . . . . . . . . 13 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
171 breq1 5106 . . . . . . . . . . . . 13 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) β†’ (0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
172137leidd 11654 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
173 iftrue 4490 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝐷 β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) = (πΉβ€˜π‘‘))
174173fvoveq1d 7371 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ 𝐷 β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
175174adantl 482 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
176172, 175breqtrrd 5131 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
177176adantlr 713 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
178130, 177syldan 591 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
179178adantlr 713 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
180162adantlr 713 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
181180adantr 481 . . . . . . . . . . . . 13 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
182170, 171, 179, 181ifbothda 4522 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
183182ralrimiva 3141 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
18413a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ℝ ∈ V)
185 fvex 6850 . . . . . . . . . . . . . . 15 (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V
186185, 64ifex 4534 . . . . . . . . . . . . . 14 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V
187186a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V)
188 fvexd 6852 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V)
189 eqidd 2738 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
190 eqidd 2738 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) = (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
191184, 187, 188, 189, 190ofrfval2 7628 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
192191ad2antrr 724 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ ((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) ↔ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
193183, 192mpbird 256 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
194 itg2le 25026 . . . . . . . . . 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 1371 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))))
196128, 195sylan 580 . . . . . . . 8 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))))
197 simpllr 774 . . . . . . . 8 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2))
198151, 168, 154, 196, 197xrlelttrd 13007 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
199151, 154, 198xrltled 12997 . . . . . 6 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2))
200199adantllr 717 . . . . 5 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2))
2012003adantr3 1171 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2))
202 itg2lecl 25025 . . . 4 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)):β„βŸΆ(0[,]+∞) ∧ (𝑦 / 2) ∈ ℝ ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ≀ (𝑦 / 2)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ)
203124, 127, 201, 202syl3anc 1371 . . 3 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ)
204203adantr 481 . 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 729 . 2 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (𝑦 / 2) ∈ ℝ)
20682adantr 481 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
207 2rp 12848 . . . . . . . . 9 2 ∈ ℝ+
208 imassrn 6020 . . . . . . . . . . . . . . . 16 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ran abs
209 frn 6670 . . . . . . . . . . . . . . . . 17 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
21027, 209ax-mp 5 . . . . . . . . . . . . . . . 16 ran abs βŠ† ℝ
211208, 210sstri 3951 . . . . . . . . . . . . . . 15 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ
212211a1i 11 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ)
2131frnd 6671 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 βŠ† ℝ)
214213adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑓 βŠ† ℝ)
2155frnd 6671 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 βŠ† ℝ)
216215adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑔 βŠ† ℝ)
217214, 216unssd 4144 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† ℝ)
218217, 62sstrdi 3954 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚)
219 i1f0rn 24968 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 β†’ 0 ∈ ran 𝑓)
220 elun1 4134 . . . . . . . . . . . . . . . . . 18 (0 ∈ ran 𝑓 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
221219, 220syl 17 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
222221adantr 481 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔))
223 ffn 6663 . . . . . . . . . . . . . . . . . 18 (abs:β„‚βŸΆβ„ β†’ abs Fn β„‚)
22427, 223ax-mp 5 . . . . . . . . . . . . . . . . 17 abs Fn β„‚
225 fnfvima 7177 . . . . . . . . . . . . . . . . 17 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
226224, 225mp3an1 1448 . . . . . . . . . . . . . . . 16 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ 0 ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
227218, 222, 226syl2anc 584 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (absβ€˜0) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
228227ne0d 4293 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ…)
229 ffun 6666 . . . . . . . . . . . . . . . . 17 (abs:β„‚βŸΆβ„ β†’ Fun abs)
23027, 229ax-mp 5 . . . . . . . . . . . . . . . 16 Fun abs
231 i1frn 24963 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 ∈ Fin)
232 i1frn 24963 . . . . . . . . . . . . . . . . 17 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 ∈ Fin)
233 unfi 9049 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
234231, 232, 233syl2an 596 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
235 imafi 9052 . . . . . . . . . . . . . . . 16 ((Fun abs ∧ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
236230, 234, 235sylancr 587 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin)
237 fimaxre2 12033 . . . . . . . . . . . . . . 15 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) ∈ Fin) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
238211, 236, 237sylancr 587 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯)
239 suprcl 12048 . . . . . . . . . . . . . 14 (((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
240212, 228, 238, 239syl3anc 1371 . . . . . . . . . . . . 13 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
241240adantr 481 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
242 0red 11091 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 ∈ ℝ)
243218sselda 3942 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ π‘Ÿ ∈ β„‚)
244243abscld 15255 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
245244adantrr 715 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
246 absgt0 15143 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ β„‚ β†’ (π‘Ÿ β‰  0 ↔ 0 < (absβ€˜π‘Ÿ)))
247243, 246syl 17 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (π‘Ÿ β‰  0 ↔ 0 < (absβ€˜π‘Ÿ)))
248247biimpa 477 . . . . . . . . . . . . . 14 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) ∧ π‘Ÿ β‰  0) β†’ 0 < (absβ€˜π‘Ÿ))
249248anasss 467 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < (absβ€˜π‘Ÿ))
250212, 228, 2383jca 1128 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
251250adantr 481 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
252 fnfvima 7177 . . . . . . . . . . . . . . . . 17 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
253224, 252mp3an1 1448 . . . . . . . . . . . . . . . 16 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
254218, 253sylan 580 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
255 suprub 12049 . . . . . . . . . . . . . . 15 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜π‘Ÿ) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
256251, 254, 255syl2anc 584 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
257256adantrr 715 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
258242, 245, 241, 249, 257ltletrd 11248 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
259241, 258elrpd 12882 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+)
260259rexlimdvaa 3151 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0 β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+))
261260imp 407 . . . . . . . . 9 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+)
262 rpmulcl 12866 . . . . . . . . 9 ((2 ∈ ℝ+ ∧ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
263207, 261, 262sylancr 587 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
264206, 263rerpdivcld 12916 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
265264adantll 712 . . . . . 6 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
266265adantlr 713 . . . . 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 728 . . . 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 781 . . . . . 6 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ πœ‘)
269 iccssre 13274 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
27085, 87, 269syl2anc 584 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
271270, 62sstrdi 3954 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† β„‚)
272271sselda 3942 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ β„‚)
273271sselda 3942 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ β„‚)
274 subcl 11333 . . . . . . . . . 10 ((𝑀 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
275272, 273, 274syl2anr 597 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
276275anandis 676 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
277276abscld 15255 . . . . . . 7 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
2782773adantr3 1171 . . . . . 6 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
279268, 278sylan 580 . . . . 5 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
280279adantr 481 . . . 4 (((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ (absβ€˜(𝑀 βˆ’ 𝑒)) < ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) ∈ ℝ)
281 rpdivcl 12868 . . . . . . . . 9 (((𝑦 / 2) ∈ ℝ+ ∧ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
282152, 263, 281syl2anr 597 . . . . . . . 8 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ+)
283282rpred 12885 . . . . . . 7 ((((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
284283adantlll 716 . . . . . 6 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
285284adantllr 717 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ ((𝑦 / 2) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ∈ ℝ)
286285ad2antrr 724 . . . 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 3941 . . . . . . . . . . 11 (πœ‘ β†’ (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝑒 ∈ ℝ))
288270sseld 3941 . . . . . . . . . . 11 (πœ‘ β†’ (𝑀 ∈ (𝐴[,]𝐡) β†’ 𝑀 ∈ ℝ))
289 idd 24 . . . . . . . . . . 11 (πœ‘ β†’ (𝑒 ≀ 𝑀 β†’ 𝑒 ≀ 𝑀))
290287, 288, 2893anim123d 1443 . . . . . . . . . 10 (πœ‘ β†’ ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀) β†’ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)))
291290ad2antrr 724 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀) β†’ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)))
292291imp 407 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀))
29355abscld 15255 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
294293rexrd 11138 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ*)
295 elxrge0 13302 . . . . . . . . . . . . . . . . . 18 ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞) ↔ ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ* ∧ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
296294, 56, 295sylanbrc 583 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞))
297 ifcl 4529 . . . . . . . . . . . . . . . . 17 (((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ (0[,]+∞))
298296, 119, 297sylancl 586 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ (0[,]+∞))
299298fmpttd 7057 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)):β„βŸΆ(0[,]+∞))
300240recnd 11116 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ β„‚)
3013002timesd 12329 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) = (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
302240, 240readdcld 11117 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ)
303302rexrd 11138 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ*)
304 abs0 15104 . . . . . . . . . . . . . . . . . . . . . . 23 (absβ€˜0) = 0
305304, 227eqeltrrid 2843 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
306 suprub 12049 . . . . . . . . . . . . . . . . . . . . . 22 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ 0 ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ 0 ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
307250, 305, 306syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
308240, 240, 307, 307addge0d 11664 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
309 elxrge0 13302 . . . . . . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
311301, 310eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
312 ifcl 4529 . . . . . . . . . . . . . . . . . 18 (((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
313311, 119, 312sylancl 586 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
314313adantr 481 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) ∈ (0[,]+∞))
315314fmpttd 7057 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)):β„βŸΆ(0[,]+∞))
3161ffvelcdmda 7029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ℝ)
317316recnd 11116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ β„‚)
318317abscld 15255 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ ℝ)
3195ffvelcdmda 7029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
320319recnd 11116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ β„‚)
321320abscld 15255 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ ℝ)
322 readdcl 11067 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((absβ€˜(π‘“β€˜π‘‘)) ∈ ℝ ∧ (absβ€˜(π‘”β€˜π‘‘)) ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ∈ ℝ)
323318, 321, 322syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ∈ ℝ)
324323anandirs 677 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ∈ ℝ)
325302adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ)
326 mulcl 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
3274, 320, 326sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
328 abstri 15149 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘“β€˜π‘‘) ∈ β„‚ ∧ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))))
329317, 327, 328syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))))
330329anandirs 677 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))))
331 absmul 15113 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))))
3324, 320, 331sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))))
333 absi 15105 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (absβ€˜i) = 1
334333oveq1i 7359 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))) = (1 Β· (absβ€˜(π‘”β€˜π‘‘)))
335332, 334eqtrdi 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (1 Β· (absβ€˜(π‘”β€˜π‘‘))))
336321recnd 11116 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ β„‚)
337336mulid2d 11106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (1 Β· (absβ€˜(π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
338335, 337eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
339338adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
340339oveq2d 7365 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))) = ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))))
341330, 340breqtrd 5129 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))))
342318adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ ℝ)
343321adantll 712 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ ℝ)
344240adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ)
345250adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯))
346218adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚)
3471ffnd 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ dom ∫1 β†’ 𝑓 Fn ℝ)
348 fnfvelrn 7026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
349347, 348sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
350 elun1 4134 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘“β€˜π‘‘) ∈ ran 𝑓 β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
351349, 350syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
352351adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
353 fnfvima 7177 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
354224, 353mp3an1 1448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
355346, 352, 354syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
356 suprub 12049 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜(π‘“β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜(π‘“β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
357345, 355, 356syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
3585ffnd 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ dom ∫1 β†’ 𝑔 Fn ℝ)
359 fnfvelrn 7026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
360358, 359sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
361 elun2 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘”β€˜π‘‘) ∈ ran 𝑔 β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
362360, 361syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
363362adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
364 fnfvima 7177 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((abs Fn β„‚ ∧ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
365224, 364mp3an1 1448 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚ ∧ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
366346, 363, 365syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
367 suprub 12049 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ ∧ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ… ∧ βˆƒπ‘₯ ∈ ℝ βˆ€π‘¦ ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))𝑦 ≀ π‘₯) ∧ (absβ€˜(π‘”β€˜π‘‘)) ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔))) β†’ (absβ€˜(π‘”β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
368345, 366, 367syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
369342, 343, 344, 344, 357, 368le2addd 11707 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
370293, 324, 325, 341, 369letrd 11245 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
371301adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) = (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
372370, 371breqtrrd 5131 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
37350, 372sylan2 593 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ≀ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
374 iftrue 4490 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
375374adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
376 iftrue 4490 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) = (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
377376adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) = (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
378373, 375, 3773brtr4d 5135 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))
379378ex 413 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
38058a1i 11 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ 0 ≀ 0)
381 iffalse 4493 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = 0)
382 iffalse 4493 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) = 0)
383380, 381, 3823brtr4d 5135 . . . . . . . . . . . . . . . . . 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 3145 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))
386 ovex 7382 . . . . . . . . . . . . . . . . . . 19 (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ V
387386, 64ifex 4534 . . . . . . . . . . . . . . . . . 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 2738 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
39014, 71, 388, 74, 389ofrfval2 7628 . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
392 itg2le 25026 . . . . . . . . . . . . . . 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 1371 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))))
394393adantr 481 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))))
395 mblvol 24816 . . . . . . . . . . . . . . . . 17 ((𝑒(,)𝑀) ∈ dom vol β†’ (volβ€˜(𝑒(,)𝑀)) = (vol*β€˜(𝑒(,)𝑀)))
39634, 395ax-mp 5 . . . . . . . . . . . . . . . 16 (volβ€˜(𝑒(,)𝑀)) = (vol*β€˜(𝑒(,)𝑀))
397 ovolioo 24854 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (vol*β€˜(𝑒(,)𝑀)) = (𝑀 βˆ’ 𝑒))
398396, 397eqtrid 2789 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) = (𝑀 βˆ’ 𝑒))
399 resubcl 11398 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑒 ∈ ℝ) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
400399ancoms 459 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
4014003adant3 1132 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
402398, 401eqeltrd 2838 . . . . . . . . . . . . . 14 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) ∈ ℝ)
403 elrege0 13299 . . . . . . . . . . . . . . . . 17 (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ↔ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ ∧ 0 ≀ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
404240, 307, 403sylanbrc 583 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞))
405 ge0addcl 13305 . . . . . . . . . . . . . . . 16 ((sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞) ∧ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ (0[,)+∞)) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
406404, 404, 405syl2anc 584 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
407301, 406eqeltrd 2838 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,)+∞))
408 itg2const 25027 . . . . . . . . . . . . . . 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 1448 . . . . . . . . . . . . . 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 597 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))) = ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
411394, 410breqtrd 5129 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
412411adantll 712 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
413412adantlr 713 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ≀ ((2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) Β· (volβ€˜(𝑒(,)𝑀))))
41482ad3antlr 729 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
415402adantl 482 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (volβ€˜(𝑒(,)𝑀)) ∈ ℝ)
416263adantll 712 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
417416adantr 481 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
418414, 415, 417ledivmuld 12938 . . . . . . . . . 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 256 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (volβ€˜(𝑒(,)𝑀)))
420 abssubge0 15146 . . . . . . . . . . . 12 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (𝑀 βˆ’ 𝑒))
421397, 420eqtr4d 2780 . . . . . . . . . . 11 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (vol*β€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
422396, 421eqtrid 2789 . . . . . . . . . 10 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
423422adantl 482 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (volβ€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
424419, 423breqtrd 5129 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (absβ€˜(𝑀 βˆ’ 𝑒)))
425292, 424syldan 591 . . . . . . 7 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ ((∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) / (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))) ≀ (absβ€˜(𝑀 βˆ’ 𝑒)))
426425adantllr 717 . . . . . 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 713 . . . . 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 481 . . . 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 485 . . . 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 11246 . . 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 482 . . . . . 6 ((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
432431ad3antrrr 728 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
433126adantl 482 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (𝑦 / 2) ∈ ℝ)
434416adantlr 713 . . . . . 6 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
435434adantr 481 . . . . 5 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ+)
436432, 433, 435ltdiv1d 12930 . . . 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 724 . . 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 256 . 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 717 . . . 4 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
4404393adantr3 1171 . . 3 ((((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
441440adantr 481 . 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 11711 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 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3443   βˆͺ cun 3906   βŠ† wss 3908  βˆ…c0 4280  ifcif 4484  {csn 4584   class class class wbr 5103   ↦ cmpt 5186   Γ— cxp 5628  dom cdm 5630  ran crn 5631   β€œ cima 5633   ∘ ccom 5634  Fun wfun 6485   Fn wfn 6486  βŸΆwf 6487  β€˜cfv 6491  (class class class)co 7349   ∘f cof 7605   ∘r cofr 7606  Fincfn 8816  supcsup 9309  β„‚cc 10982  β„cr 10983  0cc0 10984  1c1 10985  ici 10986   + caddc 10987   Β· cmul 10989  +∞cpnf 11119  β„*cxr 11121   < clt 11122   ≀ cle 11123   βˆ’ cmin 11318   / cdiv 11745  2c2 12141  β„+crp 12843  (,)cioo 13192  [,)cico 13194  [,]cicc 13195  abscabs 15052  vol*covol 24748  volcvol 24749  βˆ«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-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-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-rlim 15305  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-0p 24956
This theorem is referenced by:  ftc1anclem8  36053
  Copyright terms: Public domain W3C validator