o1rlimmul - Metamath Proof Explorer

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

Theorem o1rlimmul 14393

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.

Step	Hyp	Ref	Expression
1		o1f 14304	. . . . 5 ⊢ (𝐹 ∈ 𝑂(1) → 𝐹:dom 𝐹⟶ℂ)
2	1	adantr 480	. . . 4 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → 𝐹:dom 𝐹⟶ℂ)
3		ffn 6083	. . . 4 ⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹)
4	2, 3	syl 17	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → 𝐹 Fn dom 𝐹)
5		rlimf 14276	. . . . 5 ⊢ (𝐺 ⇝_𝑟 0 → 𝐺:dom 𝐺⟶ℂ)
6	5	adantl 481	. . . 4 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → 𝐺:dom 𝐺⟶ℂ)
7		ffn 6083	. . . 4 ⊢ (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺)
8	6, 7	syl 17	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → 𝐺 Fn dom 𝐺)
9		o1dm 14305	. . . . 5 ⊢ (𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ)
10	9	adantr 480	. . . 4 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → dom 𝐹 ⊆ ℝ)
11		reex 10065	. . . 4 ⊢ ℝ ∈ V
12		ssexg 4837	. . . 4 ⊢ ((dom 𝐹 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐹 ∈ V)
13	10, 11, 12	sylancl 695	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → dom 𝐹 ∈ V)
14		rlimss 14277	. . . . 5 ⊢ (𝐺 ⇝_𝑟 0 → dom 𝐺 ⊆ ℝ)
15	14	adantl 481	. . . 4 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → dom 𝐺 ⊆ ℝ)
16		ssexg 4837	. . . 4 ⊢ ((dom 𝐺 ⊆ ℝ ∧ ℝ ∈ V) → dom 𝐺 ∈ V)
17	15, 11, 16	sylancl 695	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → dom 𝐺 ∈ V)
18		eqid 2651	. . 3 ⊢ (dom 𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺)
19		eqidd 2652	. . 3 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥))
20		eqidd 2652	. . 3 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥))
21	4, 8, 13, 17, 18, 19, 20	offval 6946	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → (𝐹 ∘_𝑓 · 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))))
22		o1bdd 14306	. . . . . . 7 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐹:dom 𝐹⟶ℂ) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚))
23	1, 22	mpdan 703	. . . . . 6 ⊢ (𝐹 ∈ 𝑂(1) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚))
24	23	ad2antrr 762	. . . . 5 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) → ∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚))
25		fvexd 6241	. . . . . . . . 9 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ V)
26	25	ralrimiva 2995	. . . . . . . 8 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∀𝑥 ∈ dom 𝐺(𝐺‘𝑥) ∈ V)
27		simplr 807	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑦 ∈ ℝ⁺)
28		recn 10064	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ℝ → 𝑚 ∈ ℂ)
29	28	ad2antll 765	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 𝑚 ∈ ℂ)
30	29	abscld 14219	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (abs‘𝑚) ∈ ℝ)
31	29	absge0d 14227	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → 0 ≤ (abs‘𝑚))
32	30, 31	ge0p1rpd 11940	. . . . . . . . 9 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈ ℝ⁺)
33	27, 32	rpdivcld 11927	. . . . . . . 8 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ⁺)
34	6	feqmptd 6288	. . . . . . . . . 10 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)))
35		simpr 476	. . . . . . . . . 10 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → 𝐺 ⇝_𝑟 0)
36	34, 35	eqbrtrrd 4709	. . . . . . . . 9 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ⇝_𝑟 0)
37	36	ad2antrr 762	. . . . . . . 8 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ⇝_𝑟 0)
38	26, 33, 37	rlimi 14288	. . . . . . 7 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))
39		inss1 3866	. . . . . . . . . . . . . 14 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹
40		ssralv 3699	. . . . . . . . . . . . . 14 ⊢ ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚)))
41	39, 40	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚))
42		inss2 3867	. . . . . . . . . . . . . 14 ⊢ (dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺
43		ssralv 3699	. . . . . . . . . . . . . 14 ⊢ ((dom 𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → (∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
44	42, 43	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))))
45	41, 44	anim12i 589	. . . . . . . . . . . 12 ⊢ ((∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
46		r19.26 3093	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) ↔ (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
47	45, 46	sylibr 224	. . . . . . . . . . 11 ⊢ ((∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
48		prth 594	. . . . . . . . . . . 12 ⊢ (((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
49	48	ralimi 2981	. . . . . . . . . . 11 ⊢ (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ (𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
50	47, 49	syl 17	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))))
51		simplrl 817	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑎 ∈ ℝ)
52		simprl 809	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑏 ∈ ℝ)
53	39, 10	syl5ss 3647	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
54	53	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (dom 𝐹 ∩ dom 𝐺) ⊆ ℝ)
55		simprr 811	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))
56	54, 55	sseldd 3637	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ ℝ)
57		maxle 12060	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥)))
58	51, 52, 56, 57	syl3anc 1366	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 ↔ (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥)))
59	58	biimpd 219	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥)))
60	6	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐺:dom 𝐺⟶ℂ)
61	42	sseli 3632	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺)
62	61	ad2antll 765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐺)
63	60, 62	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐺‘𝑥) ∈ ℂ)
64	63	subid1d 10419	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐺‘𝑥) − 0) = (𝐺‘𝑥))
65	64	fveq2d 6233	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐺‘𝑥) − 0)) = (abs‘(𝐺‘𝑥)))
66	65	breq1d 4695	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) ↔ (abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1))))
67	63	abscld 14219	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐺‘𝑥)) ∈ ℝ)
68	33	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ⁺)
69	68	rpred 11910	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ)
70		ltle 10164	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ) → ((abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))
71	67, 69, 70	syl2anc 694	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺‘𝑥)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))
72	66, 71	sylbid 230	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)) → (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))))
73	72	anim2d 588	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1)))))
74	2	ad3antrrr 766	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝐹:dom 𝐹⟶ℂ)
75	39	sseli 3632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹)
76	75	ad2antll 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑥 ∈ dom 𝐹)
77	74, 76	ffvelrnd 6400	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝐹‘𝑥) ∈ ℂ)
78	77	abscld 14219	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘(𝐹‘𝑥)) ∈ ℝ)
79	77	absge0d 14227	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐹‘𝑥)))
80	78, 79	jca 553	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐹‘𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐹‘𝑥))))
81		simplrr 818	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℝ)
82	63	absge0d 14227	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 0 ≤ (abs‘(𝐺‘𝑥)))
83	67, 82	jca 553	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐺‘𝑥))))
84		lemul12a 10919	. . . . . . . . . . . . . . . 16 ⊢ (((((abs‘(𝐹‘𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐹‘𝑥))) ∧ 𝑚 ∈ ℝ) ∧ (((abs‘(𝐺‘𝑥)) ∈ ℝ ∧ 0 ≤ (abs‘(𝐺‘𝑥))) ∧ (𝑦 / ((abs‘𝑚) + 1)) ∈ ℝ)) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))))
85	80, 81, 83, 69, 84	syl22anc 1367	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘(𝐺‘𝑥)) ≤ (𝑦 / ((abs‘𝑚) + 1))) → ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))))
86	77, 63	absmuld 14237	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) = ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))))
87	86	breq1d 4695	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ↔ ((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1)))))
88	81	recnd 10106	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ∈ ℂ)
89	27	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ⁺)
90	89	rpcnd 11912	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℂ)
91	32	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℝ⁺)
92	91	rpcnd 11912	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℂ)
93	91	rpne0d 11915	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ≠ 0)
94	88, 90, 92, 93	divassd 10874	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) = (𝑚 · (𝑦 / ((abs‘𝑚) + 1))))
95		peano2re 10247	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘𝑚) ∈ ℝ → ((abs‘𝑚) + 1) ∈ ℝ)
96	30, 95	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → ((abs‘𝑚) + 1) ∈ ℝ)
97	96	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘𝑚) + 1) ∈ ℝ)
98	30	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) ∈ ℝ)
99	81	leabsd 14197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 ≤ (abs‘𝑚))
100	98	ltp1d 10992	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘𝑚) < ((abs‘𝑚) + 1))
101	81, 98, 97, 99, 100	lelttrd 10233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑚 < ((abs‘𝑚) + 1))
102	81, 97, 89, 101	ltmul1dd 11965	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦))
103	89	rpred 11910	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → 𝑦 ∈ ℝ)
104	81, 103	remulcld 10108	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · 𝑦) ∈ ℝ)
105	104, 103, 91	ltdivmuld 11961	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦 ↔ (𝑚 · 𝑦) < (((abs‘𝑚) + 1) · 𝑦)))
106	102, 105	mpbird 247	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝑚 · 𝑦) / ((abs‘𝑚) + 1)) < 𝑦)
107	94, 106	eqbrtrrd 4709	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦)
108	77, 63	mulcld 10098	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
109	108	abscld 14219	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ ℝ)
110	81, 69	remulcld 10108	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ)
111		lelttr 10166	. . . . . . . . . . . . . . . . . 18 ⊢ (((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ ℝ ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∈ ℝ ∧ 𝑦 ∈ ℝ) → (((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
112	109, 110, 103, 111	syl3anc 1366	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) ∧ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) < 𝑦) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
113	107, 112	mpan2d 710	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → ((abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
114	87, 113	sylbird 250	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) · (abs‘(𝐺‘𝑥))) ≤ (𝑚 · (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
115	73, 85, 114	3syld 60	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
116	59, 115	imim12d 81	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ (𝑏 ∈ ℝ ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺))) → (((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
117	116	anassrs 681	. . . . . . . . . . . 12 ⊢ ((((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
118	117	ralimdva 2991	. . . . . . . . . . 11 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
119		simpr 476	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑏 ∈ ℝ)
120		simplrl 817	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → 𝑎 ∈ ℝ)
121	119, 120	ifcld 4164	. . . . . . . . . . 11 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ)
122	118, 121	jctild 565	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝑎 ≤ 𝑥 ∧ 𝑏 ≤ 𝑥) → ((abs‘(𝐹‘𝑥)) ≤ 𝑚 ∧ (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))))
123		breq1 4688	. . . . . . . . . . . . 13 ⊢ (𝑧 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → (𝑧 ≤ 𝑥 ↔ if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥))
124	123	imbi1d 330	. . . . . . . . . . . 12 ⊢ (𝑧 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → ((𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦) ↔ (if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
125	124	ralbidv 3015	. . . . . . . . . . 11 ⊢ (𝑧 = if(𝑎 ≤ 𝑏, 𝑏, 𝑎) → (∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦) ↔ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
126	125	rspcev 3340	. . . . . . . . . 10 ⊢ ((if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ∈ ℝ ∧ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(if(𝑎 ≤ 𝑏, 𝑏, 𝑎) ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
127	50, 122, 126	syl56 36	. . . . . . . . 9 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → ((∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) ∧ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1)))) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
128	127	expcomd 453	. . . . . . . 8 ⊢ (((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) ∧ 𝑏 ∈ ℝ) → (∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))))
129	128	rexlimdva 3060	. . . . . . 7 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∃𝑏 ∈ ℝ ∀𝑥 ∈ dom 𝐺(𝑏 ≤ 𝑥 → (abs‘((𝐺‘𝑥) − 0)) < (𝑦 / ((abs‘𝑚) + 1))) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))))
130	38, 129	mpd 15	. . . . . 6 ⊢ ((((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) ∧ (𝑎 ∈ ℝ ∧ 𝑚 ∈ ℝ)) → (∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
131	130	rexlimdvva 3067	. . . . 5 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) → (∃𝑎 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑥 ∈ dom 𝐹(𝑎 ≤ 𝑥 → (abs‘(𝐹‘𝑥)) ≤ 𝑚) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
132	24, 131	mpd 15	. . . 4 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑦 ∈ ℝ⁺) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
133	132	ralrimiva 2995	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦))
134		ffvelrn 6397	. . . . . . 7 ⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ)
135	2, 75, 134	syl2an 493	. . . . . 6 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ)
136		ffvelrn 6397	. . . . . . 7 ⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ)
137	6, 61, 136	syl2an 493	. . . . . 6 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ)
138	135, 137	mulcld 10098	. . . . 5 ⊢ (((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
139	138	ralrimiva 2995	. . . 4 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ)
140	139, 53	rlim0 14283	. . 3 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ⇝_𝑟 0 ↔ ∀𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ ∀𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)(𝑧 ≤ 𝑥 → (abs‘((𝐹‘𝑥) · (𝐺‘𝑥))) < 𝑦)))
141	133, 140	mpbird 247	. 2 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ⇝_𝑟 0)
142	21, 141	eqbrtrd 4707	1 ⊢ ((𝐹 ∈ 𝑂(1) ∧ 𝐺 ⇝_𝑟 0) → (𝐹 ∘_𝑓 · 𝐺) ⇝_𝑟 0)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ∀wral 2941 ∃wrex 2942 Vcvv 3231 ∩ cin 3606 ⊆ wss 3607 ifcif 4119 class class class wbr 4685 ↦ cmpt 4762 dom cdm 5143 Fn wfn 5921 ⟶wf 5922 ‘cfv 5926 (class class class)co 6690 ∘_𝑓 cof 6937 ℂcc 9972 ℝcr 9973 0cc0 9974 1c1 9975 + caddc 9977 · cmul 9979 < clt 10112 ≤ cle 10113 − cmin 10304 / cdiv 10722 ℝ⁺crp 11870 abscabs 14018 ⇝_𝑟 crli 14260 𝑂(1)co1 14261

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-rep 4804 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-cnex 10030 ax-resscn 10031 ax-1cn 10032 ax-icn 10033 ax-addcl 10034 ax-addrcl 10035 ax-mulcl 10036 ax-mulrcl 10037 ax-mulcom 10038 ax-addass 10039 ax-mulass 10040 ax-distr 10041 ax-i2m1 10042 ax-1ne0 10043 ax-1rid 10044 ax-rnegex 10045 ax-rrecex 10046 ax-cnre 10047 ax-pre-lttri 10048 ax-pre-lttrn 10049 ax-pre-ltadd 10050 ax-pre-mulgt0 10051 ax-pre-sup 10052

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-nel 2927 df-ral 2946 df-rex 2947 df-reu 2948 df-rmo 2949 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-riota 6651 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-of 6939 df-om 7108 df-2nd 7211 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-er 7787 df-pm 7902 df-en 7998 df-dom 7999 df-sdom 8000 df-sup 8389 df-pnf 10114 df-mnf 10115 df-xr 10116 df-ltxr 10117 df-le 10118 df-sub 10306 df-neg 10307 df-div 10723 df-nn 11059 df-2 11117 df-3 11118 df-n0 11331 df-z 11416 df-uz 11726 df-rp 11871 df-ico 12219 df-seq 12842 df-exp 12901 df-cj 13883 df-re 13884 df-im 13885 df-sqrt 14019 df-abs 14020 df-rlim 14264 df-o1 14265

This theorem is referenced by: chtppilimlem2 25208 chpchtlim 25213

W3C validator