Metamath Proof Explorer

Theorem o1rlimmul

Description: The product of an eventually bounded function and a function of limit zero has limit zero. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion o1rlimmul ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ( 𝐹 ∘f · 𝐺 ) ⇝𝑟 0 )

Proof

Step Hyp Ref Expression
1 o1f ⊢ ( 𝐹 ∈ 𝑂(1) → 𝐹 : dom 𝐹 ⟶ ℂ )
2 1 adantr ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → 𝐹 : dom 𝐹 ⟶ ℂ )
3 2 ffnd ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → 𝐹 Fn dom 𝐹 )
4 rlimf ⊢ ( 𝐺 ⇝𝑟 0 → 𝐺 : dom 𝐺 ⟶ ℂ )
5 4 adantl ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → 𝐺 : dom 𝐺 ⟶ ℂ )
6 5 ffnd ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → 𝐺 Fn dom 𝐺 )
7 o1dm ⊢ ( 𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ )
8 7 adantr ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → dom 𝐹 ⊆ ℝ )
9 reex ⊢ ℝ ∈ V
10 ssexg ⊢ ( ( dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V ) → dom 𝐹 ∈ V )
11 8 9 10 sylancl ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → dom 𝐹 ∈ V )
12 rlimss ⊢ ( 𝐺 ⇝𝑟 0 → dom 𝐺 ⊆ ℝ )
13 12 adantl ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → dom 𝐺 ⊆ ℝ )
14 ssexg ⊢ ( ( dom 𝐺 ⊆ ℝ ∧ ℝ ∈ V ) → dom 𝐺 ∈ V )
15 13 9 14 sylancl ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → dom 𝐺 ∈ V )
16 eqid ⊢ ( dom 𝐹 ∩ dom 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 )
17 eqidd ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
18 eqidd ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
19 3 6 11 15 16 17 18 offval ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ( 𝐹 ∘f · 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
20 o1bdd ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : dom 𝐹 ⟶ ℂ ) → ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) )
21 1 20 mpdan ⊢ ( 𝐹 ∈ 𝑂(1) → ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) )
22 21 ad2antrr ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) )
23 fvexd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ V )
24 23 ralrimiva ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ∀ 𝑥 ∈ dom 𝐺 ( 𝐺 ‘ 𝑥 ) ∈ V )
25 simplr ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝑦 ∈ ℝ+ )
26 recn ⊢ ( 𝑚 ∈ ℝ → 𝑚 ∈ ℂ )
27 26 ad2antll ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝑚 ∈ ℂ )
28 27 abscld ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( abs ‘ 𝑚 ) ∈ ℝ )
29 27 absge0d ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 0 ≤ ( abs ‘ 𝑚 ) )
30 28 29 ge0p1rpd ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ( abs ‘ 𝑚 ) + 1 ) ∈ ℝ+ )
31 25 30 rpdivcld ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ∈ ℝ+ )
32 5 feqmptd ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → 𝐺 = ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) )
33 simpr ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → 𝐺 ⇝𝑟 0 )
34 32 33 eqbrtrrd ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ⇝𝑟 0 )
35 34 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ⇝𝑟 0 )
36 24 31 35 rlimi ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) )
37 inss1 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹
38 ssralv ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹 → ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ) )
39 37 38 ax-mp ⊢ ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) )
40 inss2 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺
41 ssralv ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺 → ( ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
42 40 41 ax-mp ⊢ ( ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) )
43 39 42 anim12i ⊢ ( ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
44 r19.26 ⊢ ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) ↔ ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
45 43 44 sylibr ⊢ ( ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
46 anim12 ⊢ ( ( ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ( ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
47 46 ralimi ⊢ ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
48 45 47 syl ⊢ ( ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
49 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑎 ∈ ℝ )
50 simprl ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑏 ∈ ℝ )
51 37 8 sstrid ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ( dom 𝐹 ∩ dom 𝐺 ) ⊆ ℝ )
52 51 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( dom 𝐹 ∩ dom 𝐺 ) ⊆ ℝ )
53 simprr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) )
54 52 53 sseldd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑥 ∈ ℝ )
55 maxle ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 ↔ ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) ) )
56 49 50 54 55 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 ↔ ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) ) )
57 56 biimpd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 → ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) ) )
58 5 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝐺 : dom 𝐺 ⟶ ℂ )
59 40 sseli ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
60 59 ad2antll ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑥 ∈ dom 𝐺 )
61 58 60 ffvelrnd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
62 61 subid1d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) − 0 ) = ( 𝐺 ‘ 𝑥 ) )
63 62 fveq2d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) = ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) )
64 63 breq1d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ↔ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) )
65 61 abscld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
66 31 adantr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ∈ ℝ+ )
67 66 rpred ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ∈ ℝ )
68 ltle ⊢ ( ( ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ ∧ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ∈ ℝ ) → ( ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) )
69 65 67 68 syl2anc ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) )
70 64 69 sylbid ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) → ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) )
71 70 anim2d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
72 2 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
73 37 sseli ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐹 )
74 73 ad2antll ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑥 ∈ dom 𝐹 )
75 72 74 ffvelrnd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
76 75 abscld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
77 75 absge0d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
78 76 77 jca ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
79 simplrr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑚 ∈ ℝ )
80 61 absge0d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) )
81 65 80 jca ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
82 lemul12a ⊢ ( ( ( ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ℝ ) ∧ ( ( ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
83 78 79 81 67 82 syl22anc ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ≤ ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
84 75 61 absmuld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
85 84 breq1d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ↔ ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) )
86 79 recnd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑚 ∈ ℂ )
87 25 adantr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑦 ∈ ℝ+ )
88 87 rpcnd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑦 ∈ ℂ )
89 30 adantr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ 𝑚 ) + 1 ) ∈ ℝ+ )
90 89 rpcnd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ 𝑚 ) + 1 ) ∈ ℂ )
91 89 rpne0d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ 𝑚 ) + 1 ) ≠ 0 )
92 86 88 90 91 divassd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( 𝑚 · 𝑦 ) / ( ( abs ‘ 𝑚 ) + 1 ) ) = ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) )
93 peano2re ⊢ ( ( abs ‘ 𝑚 ) ∈ ℝ → ( ( abs ‘ 𝑚 ) + 1 ) ∈ ℝ )
94 28 93 syl ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ( abs ‘ 𝑚 ) + 1 ) ∈ ℝ )
95 94 adantr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ 𝑚 ) + 1 ) ∈ ℝ )
96 28 adantr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( abs ‘ 𝑚 ) ∈ ℝ )
97 79 leabsd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑚 ≤ ( abs ‘ 𝑚 ) )
98 96 ltp1d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( abs ‘ 𝑚 ) < ( ( abs ‘ 𝑚 ) + 1 ) )
99 79 96 95 97 98 lelttrd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑚 < ( ( abs ‘ 𝑚 ) + 1 ) )
100 79 95 87 99 ltmul1dd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝑚 · 𝑦 ) < ( ( ( abs ‘ 𝑚 ) + 1 ) · 𝑦 ) )
101 87 rpred ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → 𝑦 ∈ ℝ )
102 79 101 remulcld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝑚 · 𝑦 ) ∈ ℝ )
103 102 101 89 ltdivmuld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( ( 𝑚 · 𝑦 ) / ( ( abs ‘ 𝑚 ) + 1 ) ) < 𝑦 ↔ ( 𝑚 · 𝑦 ) < ( ( ( abs ‘ 𝑚 ) + 1 ) · 𝑦 ) ) )
104 100 103 mpbird ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( 𝑚 · 𝑦 ) / ( ( abs ‘ 𝑚 ) + 1 ) ) < 𝑦 )
105 92 104 eqbrtrrd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) < 𝑦 )
106 75 61 mulcld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
107 106 abscld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
108 79 67 remulcld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ∈ ℝ )
109 lelttr ⊢ ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ ∧ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ∧ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
110 107 108 101 109 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ∧ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) < 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
111 105 110 mpan2d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
112 85 111 sylbird ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) · ( abs ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑚 · ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
113 71 83 112 3syld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
114 57 113 imim12d ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) ) → ( ( ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
115 114 anassrs ⊢ ( ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
116 115 ralimdva ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) → ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
117 simpr ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
118 simplrl ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) → 𝑎 ∈ ℝ )
119 117 118 ifcld ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ )
120 116 119 jctild ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) → ( ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥 ) → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
121 breq1 ⊢ ( 𝑧 = if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) → ( 𝑧 ≤ 𝑥 ↔ if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 ) )
122 121 rspceaimv ⊢ ( ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( if ( 𝑎 ≤ 𝑏 , 𝑏 , 𝑎 ) ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
123 48 120 122 syl56 ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) → ( ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ∧ ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
124 123 expcomd ⊢ ( ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑏 ∈ ℝ ) → ( ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
125 124 rexlimdva ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ dom 𝐺 ( 𝑏 ≤ 𝑥 → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − 0 ) ) < ( 𝑦 / ( ( abs ‘ 𝑚 ) + 1 ) ) ) → ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
126 36 125 mpd ⊢ ( ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
127 126 rexlimdvva ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) → ( ∃ 𝑎 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ dom 𝐹 ( 𝑎 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
128 22 127 mpd ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
129 128 ralrimiva ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) )
130 ffvelrn ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
131 2 73 130 syl2an ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
132 ffvelrn ⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
133 5 59 132 syl2an ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
134 131 133 mulcld ⊢ ( ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
135 134 ralrimiva ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
136 135 51 rlim0 ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ⇝𝑟 0 ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ ∀ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ( 𝑧 ≤ 𝑥 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) < 𝑦 ) ) )
137 129 136 mpbird ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ⇝𝑟 0 )
138 19 137 eqbrtrd ⊢ ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝𝑟 0 ) → ( 𝐹 ∘f · 𝐺 ) ⇝𝑟 0 )