MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  o1rlimmul Structured version   Visualization version   GIF version

Theorem o1rlimmul 14540
Description: The product of an eventually bounded function and a function of limit zero has limit zero. (Contributed by Mario Carneiro, 18-Sep-2014.)
Assertion
Ref Expression
o1rlimmul ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → (𝐹𝑓 · 𝐺) ⇝𝑟 0)

Proof of Theorem o1rlimmul
Dummy variables 𝑥 𝑦 𝑧 𝑎 𝑏 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 o1f 14451 . . . . 5 (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
21adantr 472 . . . 4 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → 𝐹:dom 𝐹⟶ℂ)
3 ffn 6198 . . . 4 (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹)
42, 3syl 17 . . 3 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → 𝐹 Fn dom 𝐹)
5 rlimf 14423 . . . . 5 (𝐺𝑟 0 → 𝐺:dom 𝐺⟶ℂ)
65adantl 473 . . . 4 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → 𝐺:dom 𝐺⟶ℂ)
7 ffn 6198 . . . 4 (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺)
86, 7syl 17 . . 3 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → 𝐺 Fn dom 𝐺)
9 o1dm 14452 . . . . 5 (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
109adantr 472 . . . 4 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → dom 𝐹 ⊆ ℝ)
11 reex 10211 . . . 4 ℝ ∈ V
12 ssexg 4948 . . . 4 ((dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐹 ∈ V)
1310, 11, 12sylancl 697 . . 3 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → dom 𝐹 ∈ V)
14 rlimss 14424 . . . . 5 (𝐺𝑟 0 → dom 𝐺 ⊆ ℝ)
1514adantl 473 . . . 4 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → dom 𝐺 ⊆ ℝ)
16 ssexg 4948 . . . 4 ((dom 𝐺 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐺 ∈ V)
1715, 11, 16sylancl 697 . . 3 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → dom 𝐺 ∈ V)
18 eqid 2752 . . 3 (dom 𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺)
19 eqidd 2753 . . 3 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) = (𝐹𝑥))
20 eqidd 2753 . . 3 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑥 ∈ dom 𝐺) → (𝐺𝑥) = (𝐺𝑥))
214, 8, 13, 17, 18, 19, 20offval 7061 . 2 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → (𝐹𝑓 · 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥) · (𝐺𝑥))))
22 o1bdd 14453 . . . . . . 7 ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚))
231, 22mpdan 705 . . . . . 6 (𝐹 ∈ 𝑂(1) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚))
2423ad2antrr 764 . . . . 5 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚))
25 fvexd 6356 . . . . . . . . 9 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑥 ∈ dom 𝐺) → (𝐺𝑥) ∈ V)
2625ralrimiva 3096 . . . . . . . 8 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∀𝑥 ∈ dom 𝐺(𝐺𝑥) ∈ V)
27 simplr 809 . . . . . . . . 9 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑦 ∈ ℝ+)
28 recn 10210 . . . . . . . . . . . 12 (𝑚 ∈ ℝ → 𝑚 ∈ ℂ)
2928ad2antll 767 . . . . . . . . . . 11 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑚 ∈ ℂ)
3029abscld 14366 . . . . . . . . . 10 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (abs‘𝑚) ∈ ℝ)
3129absge0d 14374 . . . . . . . . . 10 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 0 ≤ (abs‘𝑚))
3230, 31ge0p1rpd 12087 . . . . . . . . 9 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈ ℝ+)
3327, 32rpdivcld 12074 . . . . . . . 8 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ+)
346feqmptd 6403 . . . . . . . . . 10 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺𝑥)))
35 simpr 479 . . . . . . . . . 10 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → 𝐺𝑟 0)
3634, 35eqbrtrrd 4820 . . . . . . . . 9 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → (𝑥 ∈ dom 𝐺 ↦ (𝐺𝑥)) ⇝𝑟 0)
3736ad2antrr 764 . . . . . . . 8 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑥 ∈ dom 𝐺 ↦ (𝐺𝑥)) ⇝𝑟 0)
3826, 33, 37rlimi 14435 . . . . . . 7 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))
39 inss1 3968 . . . . . . . . . . . . . 14 (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹
40 ssralv 3799 . . . . . . . . . . . . . 14 ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚)))
4139, 40ax-mp 5 . . . . . . . . . . . . 13 (∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚))
42 inss2 3969 . . . . . . . . . . . . . 14 (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺
43 ssralv 3799 . . . . . . . . . . . . . 14 ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → (∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
4442, 43ax-mp 5 . . . . . . . . . . . . 13 (∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))
4541, 44anim12i 591 . . . . . . . . . . . 12 ((∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
46 r19.26 3194 . . . . . . . . . . . 12 (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ (𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) ↔ (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
4745, 46sylibr 224 . . . . . . . . . . 11 ((∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ (𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
48 prth 596 . . . . . . . . . . . 12 (((𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ (𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ((𝑎𝑥𝑏𝑥) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
4948ralimi 3082 . . . . . . . . . . 11 (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ (𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑥𝑏𝑥) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
5047, 49syl 17 . . . . . . . . . 10 ((∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑥𝑏𝑥) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
51 simplrl 819 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑎 ∈ ℝ)
52 simprl 811 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑏 ∈ ℝ)
5339, 10syl5ss 3747 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
5453ad3antrrr 768 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
55 simprr 813 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))
5654, 55sseldd 3737 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ ℝ)
57 maxle 12207 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎𝑥𝑏𝑥)))
5851, 52, 56, 57syl3anc 1473 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎𝑥𝑏𝑥)))
5958biimpd 219 . . . . . . . . . . . . . 14 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (𝑎𝑥𝑏𝑥)))
606ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐺:dom 𝐺⟶ℂ)
6142sseli 3732 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺)
6261ad2antll 767 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐺)
6360, 62ffvelrnd 6515 . . . . . . . . . . . . . . . . . . . 20 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐺𝑥) ∈ ℂ)
6463subid1d 10565 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐺𝑥) − 0) = (𝐺𝑥))
6564fveq2d 6348 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐺𝑥) − 0)) = (abs‘(𝐺𝑥)))
6665breq1d 4806 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) ↔ (abs‘(𝐺𝑥)) < (𝑦 / ((abs‘𝑚) + 1))))
6763abscld 14366 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐺𝑥)) ∈ ℝ)
6833adantr 472 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ+)
6968rpred 12057 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ)
70 ltle 10310 . . . . . . . . . . . . . . . . . 18 (((abs‘(𝐺𝑥)) ∈ ℝ ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ) → ((abs‘(𝐺𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))
7167, 69, 70syl2anc 696 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))
7266, 71sylbid 230 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))
7372anim2d 590 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))))
742ad3antrrr 768 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐹:dom 𝐹⟶ℂ)
7539sseli 3732 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹)
7675ad2antll 767 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐹)
7774, 76ffvelrnd 6515 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐹𝑥) ∈ ℂ)
7877abscld 14366 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐹𝑥)) ∈ ℝ)
7977absge0d 14374 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐹𝑥)))
8078, 79jca 555 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐹𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐹𝑥))))
81 simplrr 820 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℝ)
8263absge0d 14374 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐺𝑥)))
8367, 82jca 555 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐺𝑥))))
84 lemul12a 11065 . . . . . . . . . . . . . . . 16 (((((abs‘(𝐹𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐹𝑥))) ∧ 𝑚 ∈ ℝ) ∧ (((abs‘(𝐺𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐺𝑥))) ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ)) → (((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹𝑥)) · (abs‘(𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))))
8580, 81, 83, 69, 84syl22anc 1474 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹𝑥)) · (abs‘(𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))))
8677, 63absmuld 14384 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹𝑥) · (𝐺𝑥))) = ((abs‘(𝐹𝑥)) · (abs‘(𝐺𝑥))))
8786breq1d 4806 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹𝑥) · (𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ↔ ((abs‘(𝐹𝑥)) · (abs‘(𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))))
8881recnd 10252 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℂ)
8927adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ+)
9089rpcnd 12059 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℂ)
9132adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℝ+)
9291rpcnd 12059 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℂ)
9391rpne0d 12062 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ≠ 0)
9488, 90, 92, 93divassd 11020 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) = (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))
95 peano2re 10393 . . . . . . . . . . . . . . . . . . . . . 22 ((abs‘𝑚) ∈ ℝ → ((abs‘𝑚) + 1) ∈ ℝ)
9630, 95syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈ ℝ)
9796adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℝ)
9830adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) ∈ ℝ)
9981leabsd 14344 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ≤ (abs‘𝑚))
10098ltp1d 11138 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) < ((abs‘𝑚) + 1))
10181, 98, 97, 99, 100lelttrd 10379 . . . . . . . . . . . . . . . . . . . 20 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 < ((abs‘𝑚) + 1))
10281, 97, 89, 101ltmul1dd 12112 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦))
10389rpred 12057 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ)
10481, 103remulcld 10254 . . . . . . . . . . . . . . . . . . . 20 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) ∈ ℝ)
105104, 103, 91ltdivmuld 12108 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦 ↔ (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦)))
106102, 105mpbird 247 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦)
10794, 106eqbrtrrd 4820 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦)
10877, 63mulcld 10244 . . . . . . . . . . . . . . . . . . 19 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐹𝑥) · (𝐺𝑥)) ∈ ℂ)
109108abscld 14366 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹𝑥) · (𝐺𝑥))) ∈ ℝ)
11081, 69remulcld 10254 . . . . . . . . . . . . . . . . . 18 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ)
111 lelttr 10312 . . . . . . . . . . . . . . . . . 18 (((abs‘((𝐹𝑥) · (𝐺𝑥))) ∈ ℝ ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((abs‘((𝐹𝑥) · (𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
112109, 110, 103, 111syl3anc 1473 . . . . . . . . . . . . . . . . 17 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘((𝐹𝑥) · (𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
113107, 112mpan2d 712 . . . . . . . . . . . . . . . 16 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹𝑥) · (𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
11487, 113sylbird 250 . . . . . . . . . . . . . . 15 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹𝑥)) · (abs‘(𝐺𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
11573, 85, 1143syld 60 . . . . . . . . . . . . . 14 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
11659, 115imim12d 81 . . . . . . . . . . . . 13 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑎𝑥𝑏𝑥) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
117116anassrs 683 . . . . . . . . . . . 12 ((((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎𝑥𝑏𝑥) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
118117ralimdva 3092 . . . . . . . . . . 11 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑥𝑏𝑥) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
119 simpr 479 . . . . . . . . . . . 12 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℝ)
120 simplrl 819 . . . . . . . . . . . 12 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑎 ∈ ℝ)
121119, 120ifcld 4267 . . . . . . . . . . 11 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ)
122118, 121jctild 567 . . . . . . . . . 10 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎𝑥𝑏𝑥) → ((abs‘(𝐹𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))))
123 breq1 4799 . . . . . . . . . . . . 13 (𝑧 = if(𝑎𝑏, 𝑏, 𝑎) → (𝑧𝑥 ↔ if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥))
124123imbi1d 330 . . . . . . . . . . . 12 (𝑧 = if(𝑎𝑏, 𝑏, 𝑎) → ((𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦) ↔ (if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
125124ralbidv 3116 . . . . . . . . . . 11 (𝑧 = if(𝑎𝑏, 𝑏, 𝑎) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦) ↔ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
126125rspcev 3441 . . . . . . . . . 10 ((if(𝑎𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
12750, 122, 126syl56 36 . . . . . . . . 9 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → ((∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
128127expcomd 453 . . . . . . . 8 (((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → (∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))))
129128rexlimdva 3161 . . . . . . 7 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏𝑥 → (abs‘((𝐺𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))))
13038, 129mpd 15 . . . . . 6 ((((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
131130rexlimdvva 3168 . . . . 5 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) → (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎𝑥 → (abs‘(𝐹𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
13224, 131mpd 15 . . . 4 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑦 ∈ ℝ+) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
133132ralrimiva 3096 . . 3 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦))
134 ffvelrn 6512 . . . . . . 7 ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹𝑥) ∈ ℂ)
1352, 75, 134syl2an 495 . . . . . 6 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹𝑥) ∈ ℂ)
136 ffvelrn 6512 . . . . . . 7 ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺𝑥) ∈ ℂ)
1376, 61, 136syl2an 495 . . . . . 6 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺𝑥) ∈ ℂ)
138135, 137mulcld 10244 . . . . 5 (((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹𝑥) · (𝐺𝑥)) ∈ ℂ)
139138ralrimiva 3096 . . . 4 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝐹𝑥) · (𝐺𝑥)) ∈ ℂ)
140139, 53rlim0 14430 . . 3 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥) · (𝐺𝑥))) ⇝𝑟 0 ↔ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧𝑥 → (abs‘((𝐹𝑥) · (𝐺𝑥))) < 𝑦)))
141133, 140mpbird 247 . 2 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹𝑥) · (𝐺𝑥))) ⇝𝑟 0)
14221, 141eqbrtrd 4818 1 ((𝐹 ∈ 𝑂(1) ∧ 𝐺𝑟 0) → (𝐹𝑓 · 𝐺) ⇝𝑟 0)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wral 3042  wrex 3043  Vcvv 3332  cin 3706  wss 3707  ifcif 4222   class class class wbr 4796  cmpt 4873  dom cdm 5258   Fn wfn 6036  wf 6037  cfv 6041  (class class class)co 6805  𝑓 cof 7052  cc 10118  cr 10119  0cc0 10120  1c1 10121   + caddc 10123   · cmul 10125   < clt 10258  cle 10259  cmin 10450   / cdiv 10868  +crp 12017  abscabs 14165  𝑟 crli 14407  𝑂(1)co1 14408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-of 7054  df-om 7223  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-er 7903  df-pm 8018  df-en 8114  df-dom 8115  df-sdom 8116  df-sup 8505  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-n0 11477  df-z 11562  df-uz 11872  df-rp 12018  df-ico 12366  df-seq 12988  df-exp 13047  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-rlim 14411  df-o1 14412
This theorem is referenced by:  chtppilimlem2  25354  chpchtlim  25359
  Copyright terms: Public domain W3C validator