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	$⊢ (F \in 𝑂 (1) \land G \underset{ℝ}{⇝} 0) \to (F \times_{f} G) \underset{ℝ}{⇝} 0$

Proof

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

Metamath Proof Explorer

Theorem o1rlimmul

Proof