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 36043
Description: Lemma for ftc1anc 36045. (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 7030 . . . . . . . . . 10 ((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ ℝ)
32recnd 11117 . . . . . . . . 9 ((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ β„‚)
4 ax-icn 11044 . . . . . . . . . 10 i ∈ β„‚
5 i1ff 24962 . . . . . . . . . . . 12 (𝑔 ∈ dom ∫1 β†’ 𝑔:β„βŸΆβ„)
65ffvelcdmda 7030 . . . . . . . . . . 11 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ ℝ)
76recnd 11117 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (π‘”β€˜π‘₯) ∈ β„‚)
8 mulcl 11069 . . . . . . . . . 10 ((i ∈ β„‚ ∧ (π‘”β€˜π‘₯) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚)
94, 7, 8sylancr 588 . . . . . . . . 9 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚)
10 addcl 11067 . . . . . . . . 9 (((π‘“β€˜π‘₯) ∈ β„‚ ∧ (i Β· (π‘”β€˜π‘₯)) ∈ β„‚) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
113, 9, 10syl2an 597 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) ∧ (𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ)) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
1211anandirs 678 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) ∈ β„‚)
13 reex 11076 . . . . . . . . 9 ℝ ∈ V
1413a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ℝ ∈ V)
152adantlr 714 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ (π‘“β€˜π‘₯) ∈ ℝ)
16 ovexd 7385 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘₯)) ∈ V)
171feqmptd 6906 . . . . . . . . 9 (𝑓 ∈ dom ∫1 β†’ 𝑓 = (π‘₯ ∈ ℝ ↦ (π‘“β€˜π‘₯)))
1817adantr 482 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 𝑓 = (π‘₯ ∈ ℝ ↦ (π‘“β€˜π‘₯)))
1913a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ ℝ ∈ V)
204a1i 11 . . . . . . . . . 10 ((𝑔 ∈ dom ∫1 ∧ π‘₯ ∈ ℝ) β†’ i ∈ β„‚)
21 fconstmpt 5691 . . . . . . . . . . 11 (ℝ Γ— {i}) = (π‘₯ ∈ ℝ ↦ i)
2221a1i 11 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ (ℝ Γ— {i}) = (π‘₯ ∈ ℝ ↦ i))
235feqmptd 6906 . . . . . . . . . 10 (𝑔 ∈ dom ∫1 β†’ 𝑔 = (π‘₯ ∈ ℝ ↦ (π‘”β€˜π‘₯)))
2419, 20, 6, 22, 23offval2 7628 . . . . . . . . 9 (𝑔 ∈ dom ∫1 β†’ ((ℝ Γ— {i}) ∘f Β· 𝑔) = (π‘₯ ∈ ℝ ↦ (i Β· (π‘”β€˜π‘₯))))
2524adantl 483 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ((ℝ Γ— {i}) ∘f Β· 𝑔) = (π‘₯ ∈ ℝ ↦ (i Β· (π‘”β€˜π‘₯))))
2614, 15, 16, 18, 25offval2 7628 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔)) = (π‘₯ ∈ ℝ ↦ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
27 absf 15157 . . . . . . . . 9 abs:β„‚βŸΆβ„
2827a1i 11 . . . . . . . 8 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ abs:β„‚βŸΆβ„)
2928feqmptd 6906 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ abs = (𝑑 ∈ β„‚ ↦ (absβ€˜π‘‘)))
30 fveq2 6838 . . . . . . 7 (𝑑 = ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) β†’ (absβ€˜π‘‘) = (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
3112, 26, 29, 30fmptco 7070 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs ∘ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔))) = (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))))
32 ftc1anclem3 36039 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs ∘ (𝑓 ∘f + ((ℝ Γ— {i}) ∘f Β· 𝑔))) ∈ dom ∫1)
3331, 32eqeltrrd 2840 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) ∈ dom ∫1)
34 ioombl 24851 . . . . 5 (𝑒(,)𝑀) ∈ dom vol
35 fveq2 6838 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (π‘“β€˜π‘₯) = (π‘“β€˜π‘‘))
36 fveq2 6838 . . . . . . . . . . . . 13 (π‘₯ = 𝑑 β†’ (π‘”β€˜π‘₯) = (π‘”β€˜π‘‘))
3736oveq2d 7366 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (i Β· (π‘”β€˜π‘₯)) = (i Β· (π‘”β€˜π‘‘)))
3835, 37oveq12d 7368 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ ((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))) = ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))
3938fveq2d 6842 . . . . . . . . . 10 (π‘₯ = 𝑑 β†’ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
40 eqid 2738 . . . . . . . . . 10 (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯))))) = (π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))
41 fvex 6851 . . . . . . . . . 10 (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ V
4239, 40, 41fvmpt 6944 . . . . . . . . 9 (𝑑 ∈ ℝ β†’ ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
4342eqcomd 2744 . . . . . . . 8 (𝑑 ∈ ℝ β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘))
4443ifeq1d 4504 . . . . . . 7 (𝑑 ∈ ℝ β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = if(𝑑 ∈ (𝑒(,)𝑀), ((π‘₯ ∈ ℝ ↦ (absβ€˜((π‘“β€˜π‘₯) + (i Β· (π‘”β€˜π‘₯)))))β€˜π‘‘), 0))
4544mpteq2ia 5207 . . . . . 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 587 . . . 4 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1)
48 breq2 5108 . . . . . . 7 ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) β†’ (0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ↔ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
49 breq2 5108 . . . . . . 7 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
50 elioore 13223 . . . . . . . 8 (𝑑 ∈ (𝑒(,)𝑀) β†’ 𝑑 ∈ ℝ)
51 eleq1w 2821 . . . . . . . . . . . 12 (π‘₯ = 𝑑 β†’ (π‘₯ ∈ ℝ ↔ 𝑑 ∈ ℝ))
5251anbi2d 630 . . . . . . . . . . 11 (π‘₯ = 𝑑 β†’ (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘₯ ∈ ℝ) ↔ ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ)))
5338eleq1d 2823 . . . . . . . . . . 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 15264 . . . . . . . 8 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
5750, 56sylan2 594 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
58 0le0 12188 . . . . . . . 8 0 ≀ 0
5958a1i 11 . . . . . . 7 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ 0)
6048, 49, 57, 59ifbothda 4523 . . . . . 6 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
6160ralrimivw 3146 . . . . 5 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆ€π‘‘ ∈ ℝ 0 ≀ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
62 ax-resscn 11042 . . . . . . . 8 ℝ βŠ† β„‚
6362a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ℝ βŠ† β„‚)
64 c0ex 11083 . . . . . . . . . 10 0 ∈ V
6541, 64ifex 4535 . . . . . . . . 9 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ∈ V
66 eqid 2738 . . . . . . . . 9 (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))
6765, 66fnmpti 6640 . . . . . . . 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 5691 . . . . . . . 8 (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0)
7372a1i 11 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ℝ Γ— {0}) = (𝑑 ∈ ℝ ↦ 0))
74 eqidd 2739 . . . . . . 7 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)))
7514, 70, 71, 73, 74ofrfval2 7629 . . . . . 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 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 482 . . . . 5 (((𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)) ∈ dom ∫1 ∧ 0𝑝 ∘r ≀ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) β†’ (∫1β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0))) ∈ ℝ)
8178, 80eqeltrd 2839 . . . 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 11139 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐴 ∈ ℝ*)
87 ftc1anc.b . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐡 ∈ ℝ)
8887rexrd 11139 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 ∈ ℝ*)
8986, 88jca 513 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*))
90 df-icc 13200 . . . . . . . . . . . . . . . . . . . . . 22 [,] = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑑 ∈ ℝ* ∣ (π‘₯ ≀ 𝑑 ∧ 𝑑 ≀ 𝑦)})
9190elixx3g 13206 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑒 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡)))
9291simprbi 498 . . . . . . . . . . . . . . . . . . . 20 (𝑒 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑒 ∧ 𝑒 ≀ 𝐡))
9392simpld 496 . . . . . . . . . . . . . . . . . . 19 (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝐴 ≀ 𝑒)
9490elixx3g 13206 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (𝐴[,]𝐡) ↔ ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝑀 ∈ ℝ*) ∧ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡)))
9594simprbi 498 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (𝐴[,]𝐡) β†’ (𝐴 ≀ 𝑀 ∧ 𝑀 ≀ 𝐡))
9695simprd 497 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ (𝐴[,]𝐡) β†’ 𝑀 ≀ 𝐡)
9793, 96anim12i 614 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡))
98 ioossioo 13287 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ*) ∧ (𝐴 ≀ 𝑒 ∧ 𝑀 ≀ 𝐡)) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
9989, 97, 98syl2an 597 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† (𝐴(,)𝐡))
100 ftc1anc.s . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝐴(,)𝐡) βŠ† 𝐷)
101100adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝐴(,)𝐡) βŠ† 𝐷)
10299, 101sstrd 3953 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
1031023adantr3 1172 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ (𝑒(,)𝑀) βŠ† 𝐷)
104103sselda 3943 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
105 ftc1anc.f . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐹:π·βŸΆβ„‚)
106105ffvelcdmda 7030 . . . . . . . . . . . . . . 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 11446 . . . . . . . . . . 11 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
114113abscld 15256 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
115114rexrd 11139 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
116113absge0d 15264 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
117 elxrge0 13303 . . . . . . . . 9 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞) ↔ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ* ∧ 0 ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
118115, 116, 117sylanbrc 584 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ (0[,]+∞))
119 0e0iccpnf 13305 . . . . . . . . 9 0 ∈ (0[,]+∞)
120119a1i 11 . . . . . . . 8 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ Β¬ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 0 ∈ (0[,]+∞))
121118, 120ifclda 4520 . . . . . . 7 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
122121adantr 482 . . . . . 6 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡) ∧ 𝑒 ≀ 𝑀)) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
123122fmpttd 7058 . . . . 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 12852 . . . . . 6 (𝑦 ∈ ℝ+ β†’ 𝑦 ∈ ℝ)
126125rehalfcld 12334 . . . . 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 3943 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
130129adantllr 718 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ 𝑑 ∈ 𝐷)
131106adantlr 714 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (πΉβ€˜π‘‘) ∈ β„‚)
132 ftc1anc.d . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝐷 βŠ† ℝ)
133132sselda 3943 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑑 ∈ 𝐷) β†’ 𝑑 ∈ ℝ)
134133adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ 𝑑 ∈ ℝ)
135134, 110syldan 592 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))) ∈ β„‚)
136131, 135subcld 11446 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ ((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ β„‚)
137136abscld 15256 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
138137rexrd 11139 . . . . . . . . . . . . . . 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 15264 . . . . . . . . . . . . . . 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 4520 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
147146adantr 482 . . . . . . . . . 10 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ (0[,]+∞))
148147fmpttd 7058 . . . . . . . . 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 581 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) ∈ ℝ*)
152 rphalfcl 12871 . . . . . . . . 9 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ+)
153152rpxrd 12887 . . . . . . . 8 (𝑦 ∈ ℝ+ β†’ (𝑦 / 2) ∈ ℝ*)
154153ad2antlr 726 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑦 / 2) ∈ ℝ*)
155 0cnd 11082 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ Β¬ 𝑑 ∈ 𝐷) β†’ 0 ∈ β„‚)
156106, 155ifclda 4520 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) ∈ β„‚)
157 subcl 11334 . . . . . . . . . . . . . . . 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 15256 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ)
161160rexrd 11139 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ ℝ*)
162159absge0d 15264 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ ℝ) β†’ 0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
163 elxrge0 13303 . . . . . . . . . . . 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 7058 . . . . . . . . . 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 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 5107 . . . . . . . . . . . . 13 ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) β†’ ((absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
171 breq1 5107 . . . . . . . . . . . . 13 (0 = if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) β†’ (0 ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ↔ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
172137leidd 11655 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ≀ (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
173 iftrue 4491 . . . . . . . . . . . . . . . . . . 19 (𝑑 ∈ 𝐷 β†’ if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) = (πΉβ€˜π‘‘))
174173fvoveq1d 7372 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ 𝐷 β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
175174adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ 𝑑 ∈ 𝐷) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) = (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
176172, 175breqtrrd 5132 . . . . . . . . . . . . . . . 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 4523 . . . . . . . . . . . 12 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
183182ralrimiva 3142 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ≀ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
18413a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ ℝ ∈ V)
185 fvex 6851 . . . . . . . . . . . . . . 15 (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V
186185, 64ifex 4535 . . . . . . . . . . . . . 14 if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V
187186a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0) ∈ V)
188 fvexd 6853 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))) ∈ V)
189 eqidd 2739 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0)))
190 eqidd 2739 . . . . . . . . . . . . 13 (πœ‘ β†’ (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))) = (𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))))
191184, 187, 188, 189, 190ofrfval2 7629 . . . . . . . . . . . 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 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 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 13008 . . . . . . 7 (((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ (∫2β€˜(𝑑 ∈ ℝ ↦ (absβ€˜(if(𝑑 ∈ 𝐷, (πΉβ€˜π‘‘), 0) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))) < (𝑦 / 2)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (∫2β€˜(𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((πΉβ€˜π‘‘) βˆ’ ((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))), 0))) < (𝑦 / 2))
199151, 154, 198xrltled 12998 . . . . . 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 25025 . . . 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 12849 . . . . . . . . 9 2 ∈ ℝ+
208 imassrn 6021 . . . . . . . . . . . . . . . 16 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ran abs
209 frn 6671 . . . . . . . . . . . . . . . . 17 (abs:β„‚βŸΆβ„ β†’ ran abs βŠ† ℝ)
21027, 209ax-mp 5 . . . . . . . . . . . . . . . 16 ran abs βŠ† ℝ
211208, 210sstri 3952 . . . . . . . . . . . . . . 15 (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ
212211a1i 11 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) βŠ† ℝ)
2131frnd 6672 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ dom ∫1 β†’ ran 𝑓 βŠ† ℝ)
214213adantr 482 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑓 βŠ† ℝ)
2155frnd 6672 . . . . . . . . . . . . . . . . . . 19 (𝑔 ∈ dom ∫1 β†’ ran 𝑔 βŠ† ℝ)
216215adantl 483 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ ran 𝑔 βŠ† ℝ)
217214, 216unssd 4145 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† ℝ)
218217, 62sstrdi 3955 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) βŠ† β„‚)
219 i1f0rn 24968 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ dom ∫1 β†’ 0 ∈ ran 𝑓)
220 elun1 4135 . . . . . . . . . . . . . . . . . 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 6664 . . . . . . . . . . . . . . . . . 18 (abs:β„‚βŸΆβ„ β†’ abs Fn β„‚)
22427, 223ax-mp 5 . . . . . . . . . . . . . . . . 17 abs Fn β„‚
225 fnfvima 7178 . . . . . . . . . . . . . . . . 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 4294 . . . . . . . . . . . . . 14 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)) β‰  βˆ…)
229 ffun 6667 . . . . . . . . . . . . . . . . 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 9050 . . . . . . . . . . . . . . . . 17 ((ran 𝑓 ∈ Fin ∧ ran 𝑔 ∈ Fin) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
234231, 232, 233syl2an 597 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (ran 𝑓 βˆͺ ran 𝑔) ∈ Fin)
235 imafi 9053 . . . . . . . . . . . . . . . 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 12034 . . . . . . . . . . . . . . 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 12049 . . . . . . . . . . . . . 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 11092 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 ∈ ℝ)
243218sselda 3943 . . . . . . . . . . . . . . 15 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ π‘Ÿ ∈ β„‚)
244243abscld 15256 . . . . . . . . . . . . . 14 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
245244adantrr 716 . . . . . . . . . . . . 13 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ (absβ€˜π‘Ÿ) ∈ ℝ)
246 absgt0 15144 . . . . . . . . . . . . . . . 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 7178 . . . . . . . . . . . . . . . . 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 12050 . . . . . . . . . . . . . . 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 11249 . . . . . . . . . . . 12 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ 0 < sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ))
259241, 258elrpd 12883 . . . . . . . . . . 11 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ (π‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔) ∧ π‘Ÿ β‰  0)) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ ℝ+)
260259rexlimdvaa 3152 . . . . . . . . . 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 12867 . . . . . . . . 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 12917 . . . . . . 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 13275 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
27085, 87, 269syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
271270, 62sstrdi 3955 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† β„‚)
272271sselda 3943 . . . . . . . . . 10 ((πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡)) β†’ 𝑀 ∈ β„‚)
273271sselda 3943 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) β†’ 𝑒 ∈ β„‚)
274 subcl 11334 . . . . . . . . . 10 ((𝑀 ∈ β„‚ ∧ 𝑒 ∈ β„‚) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
275272, 273, 274syl2anr 598 . . . . . . . . 9 (((πœ‘ ∧ 𝑒 ∈ (𝐴[,]𝐡)) ∧ (πœ‘ ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
276275anandis 677 . . . . . . . 8 ((πœ‘ ∧ (𝑒 ∈ (𝐴[,]𝐡) ∧ 𝑀 ∈ (𝐴[,]𝐡))) β†’ (𝑀 βˆ’ 𝑒) ∈ β„‚)
277276abscld 15256 . . . . . . 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 12869 . . . . . . . . 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 12886 . . . . . . 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 3942 . . . . . . . . . . 11 (πœ‘ β†’ (𝑒 ∈ (𝐴[,]𝐡) β†’ 𝑒 ∈ ℝ))
288270sseld 3942 . . . . . . . . . . 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 15256 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ)
294293rexrd 11139 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ*)
295 elxrge0 13303 . . . . . . . . . . . . . . . . . 18 ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞) ↔ ((absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ ℝ* ∧ 0 ≀ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘))))))
296294, 56, 295sylanbrc 584 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))) ∈ (0[,]+∞))
297 ifcl 4530 . . . . . . . . . . . . . . . . 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 7058 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0)):β„βŸΆ(0[,]+∞))
300240recnd 11117 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) ∈ β„‚)
3013002timesd 12330 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) = (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
302240, 240readdcld 11118 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ)
303302rexrd 11139 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ ℝ*)
304 abs0 15105 . . . . . . . . . . . . . . . . . . . . . . 23 (absβ€˜0) = 0
305304, 227eqeltrrid 2844 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ∈ (abs β€œ (ran 𝑓 βˆͺ ran 𝑔)))
306 suprub 12050 . . . . . . . . . . . . . . . . . . . . . 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 11665 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ 0 ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
309 elxrge0 13303 . . . . . . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ (0[,]+∞))
312 ifcl 4530 . . . . . . . . . . . . . . . . . 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 7058 . . . . . . . . . . . . . . 15 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)):β„βŸΆ(0[,]+∞))
3161ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ℝ)
317316recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ β„‚)
318317abscld 15256 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘“β€˜π‘‘)) ∈ ℝ)
3195ffvelcdmda 7030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ℝ)
320319recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ β„‚)
321320abscld 15256 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ ℝ)
322 readdcl 11068 . . . . . . . . . . . . . . . . . . . . . . . . 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 11069 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
3274, 320, 326sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (i Β· (π‘”β€˜π‘‘)) ∈ β„‚)
328 abstri 15150 . . . . . . . . . . . . . . . . . . . . . . . . . 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 15114 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((i ∈ β„‚ ∧ (π‘”β€˜π‘‘) ∈ β„‚) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))))
3324, 320, 331sylancr 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))))
333 absi 15106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (absβ€˜i) = 1
334333oveq1i 7360 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((absβ€˜i) Β· (absβ€˜(π‘”β€˜π‘‘))) = (1 Β· (absβ€˜(π‘”β€˜π‘‘)))
335332, 334eqtrdi 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (1 Β· (absβ€˜(π‘”β€˜π‘‘))))
336321recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(π‘”β€˜π‘‘)) ∈ β„‚)
337336mulid2d 11107 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (1 Β· (absβ€˜(π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
338335, 337eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
339338adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (absβ€˜(i Β· (π‘”β€˜π‘‘))) = (absβ€˜(π‘”β€˜π‘‘)))
340339oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(i Β· (π‘”β€˜π‘‘)))) = ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))))
341330, 340breqtrd 5130 . . . . . . . . . . . . . . . . . . . . . . 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 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 ∈ dom ∫1 β†’ 𝑓 Fn ℝ)
348 fnfvelrn 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑓 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
349347, 348sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ ran 𝑓)
350 elun1 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘“β€˜π‘‘) ∈ ran 𝑓 β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
351349, 350syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
352351adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (π‘“β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
353 fnfvima 7178 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12050 . . . . . . . . . . . . . . . . . . . . . . . . 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 6665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑔 ∈ dom ∫1 β†’ 𝑔 Fn ℝ)
359 fnfvelrn 7027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔 Fn ℝ ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
360358, 359sylan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ ran 𝑔)
361 elun2 4136 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((π‘”β€˜π‘‘) ∈ ran 𝑔 β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
362360, 361syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑔 ∈ dom ∫1 ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
363362adantll 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ (π‘”β€˜π‘‘) ∈ (ran 𝑓 βˆͺ ran 𝑔))
364 fnfvima 7178 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12050 . . . . . . . . . . . . . . . . . . . . . . . . 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 11708 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ ℝ) β†’ ((absβ€˜(π‘“β€˜π‘‘)) + (absβ€˜(π‘”β€˜π‘‘))) ≀ (sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < ) + sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )))
370293, 324, 325, 341, 369letrd 11246 . . . . . . . . . . . . . . . . . . . . . 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 5132 . . . . . . . . . . . . . . . . . . . . 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 4491 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
375374adantl 483 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) ∧ 𝑑 ∈ (𝑒(,)𝑀)) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))))
376 iftrue 4491 . . . . . . . . . . . . . . . . . . . . 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 5136 . . . . . . . . . . . . . . . . . . 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 4494 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) = 0)
382 iffalse 4494 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑑 ∈ (𝑒(,)𝑀) β†’ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0) = 0)
383380, 381, 3823brtr4d 5136 . . . . . . . . . . . . . . . . . 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 3146 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ βˆ€π‘‘ ∈ ℝ if(𝑑 ∈ (𝑒(,)𝑀), (absβ€˜((π‘“β€˜π‘‘) + (i Β· (π‘”β€˜π‘‘)))), 0) ≀ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0))
386 ovex 7383 . . . . . . . . . . . . . . . . . . 19 (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )) ∈ V
387386, 64ifex 4535 . . . . . . . . . . . . . . . . . 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 2739 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1) β†’ (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)) = (𝑑 ∈ ℝ ↦ if(𝑑 ∈ (𝑒(,)𝑀), (2 Β· sup((abs β€œ (ran 𝑓 βˆͺ ran 𝑔)), ℝ, < )), 0)))
39014, 71, 388, 74, 389ofrfval2 7629 . . . . . . . . . . . . . . . 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 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 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 24816 . . . . . . . . . . . . . . . . 17 ((𝑒(,)𝑀) ∈ dom vol β†’ (volβ€˜(𝑒(,)𝑀)) = (vol*β€˜(𝑒(,)𝑀)))
39634, 395ax-mp 5 . . . . . . . . . . . . . . . 16 (volβ€˜(𝑒(,)𝑀)) = (vol*β€˜(𝑒(,)𝑀))
397 ovolioo 24854 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (vol*β€˜(𝑒(,)𝑀)) = (𝑀 βˆ’ 𝑒))
398396, 397eqtrid 2790 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) = (𝑀 βˆ’ 𝑒))
399 resubcl 11399 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑒 ∈ ℝ) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
400399ancoms 460 . . . . . . . . . . . . . . . 16 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
4014003adant3 1133 . . . . . . . . . . . . . . 15 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (𝑀 βˆ’ 𝑒) ∈ ℝ)
402398, 401eqeltrd 2839 . . . . . . . . . . . . . 14 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) ∈ ℝ)
403 elrege0 13300 . . . . . . . . . . . . . . . . 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 13306 . . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . 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 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 5130 . . . . . . . . . . . 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 12939 . . . . . . . . . 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 15147 . . . . . . . . . . . 12 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (absβ€˜(𝑀 βˆ’ 𝑒)) = (𝑀 βˆ’ 𝑒))
421397, 420eqtr4d 2781 . . . . . . . . . . 11 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (vol*β€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
422396, 421eqtrid 2790 . . . . . . . . . 10 ((𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀) β†’ (volβ€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
423422adantl 483 . . . . . . . . 9 ((((πœ‘ ∧ (𝑓 ∈ dom ∫1 ∧ 𝑔 ∈ dom ∫1)) ∧ βˆƒπ‘Ÿ ∈ (ran 𝑓 βˆͺ ran 𝑔)π‘Ÿ β‰  0) ∧ (𝑒 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑒 ≀ 𝑀)) β†’ (volβ€˜(𝑒(,)𝑀)) = (absβ€˜(𝑀 βˆ’ 𝑒)))
424419, 423breqtrd 5130 . . . . . . . 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 11247 . . 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 12931 . . . 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 11712 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 2942  βˆ€wral 3063  βˆƒwrex 3072  Vcvv 3444   βˆͺ cun 3907   βŠ† wss 3909  βˆ…c0 4281  ifcif 4485  {csn 4585   class class class wbr 5104   ↦ cmpt 5187   Γ— cxp 5629  dom cdm 5631  ran crn 5632   β€œ cima 5634   ∘ ccom 5635  Fun wfun 6486   Fn wfn 6487  βŸΆwf 6488  β€˜cfv 6492  (class class class)co 7350   ∘f cof 7606   ∘r cofr 7607  Fincfn 8817  supcsup 9310  β„‚cc 10983  β„cr 10984  0cc0 10985  1c1 10986  ici 10987   + caddc 10988   Β· cmul 10990  +∞cpnf 11120  β„*cxr 11122   < clt 11123   ≀ cle 11124   βˆ’ cmin 11319   / cdiv 11746  2c2 12142  β„+crp 12844  (,)cioo 13193  [,)cico 13195  [,]cicc 13196  abscabs 15053  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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-inf2 9511  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063  ax-addf 11064
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-disj 5070  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-se 5587  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-of 7608  df-ofr 7609  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-map 8701  df-pm 8702  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-fi 9281  df-sup 9312  df-inf 9313  df-oi 9380  df-dju 9771  df-card 9809  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-n0 12348  df-z 12434  df-uz 12697  df-q 12803  df-rp 12845  df-xneg 12962  df-xadd 12963  df-xmul 12964  df-ioo 13197  df-ico 13199  df-icc 13200  df-fz 13354  df-fzo 13497  df-fl 13626  df-seq 13836  df-exp 13897  df-hash 14159  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-clim 15305  df-rlim 15306  df-sum 15506  df-rest 17239  df-topgen 17260  df-psmet 20711  df-xmet 20712  df-met 20713  df-bl 20714  df-mopn 20715  df-top 22165  df-topon 22182  df-bases 22218  df-cmp 22660  df-ovol 24750  df-vol 24751  df-mbf 24905  df-itg1 24906  df-itg2 24907  df-0p 24956
This theorem is referenced by:  ftc1anclem8  36044
  Copyright terms: Public domain W3C validator