mulcn2

Description: Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (Contributed by Mario Carneiro, 31-Jan-2014)

		Ref	Expression
	Assertion	mulcn2	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u v - B C\| < A)$

Proof

Step	Hyp	Ref	Expression
1		rphalfcl	$⊢ A \in ℝ^{+} \to \frac{A}{2} \in ℝ^{+}$
2	1	3ad2ant1	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \frac{A}{2} \in ℝ^{+}$
3		abscl	$⊢ C \in ℂ \to \|C\| \in ℝ$
4	3	3ad2ant3	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \|C\| \in ℝ$
5		abscl	$⊢ B \in ℂ \to \|B\| \in ℝ$
6	5	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \|B\| \in ℝ$
7		1re	$⊢ 1 \in ℝ$
8		readdcl	$⊢ (\|B\| \in ℝ \land 1 \in ℝ) \to \|B\| + 1 \in ℝ$
9	6 7 8	sylancl	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \|B\| + 1 \in ℝ$
10		absge0	$⊢ B \in ℂ \to 0 \leq \|B\|$
11		0lt1	$⊢ 0 < 1$
12		addgegt0	$⊢ ((\|B\| \in ℝ \land 1 \in ℝ) \land (0 \leq \|B\| \land 0 < 1)) \to 0 < \|B\| + 1$
13	12	an4s	$⊢ ((\|B\| \in ℝ \land 0 \leq \|B\|) \land (1 \in ℝ \land 0 < 1)) \to 0 < \|B\| + 1$
14	7 11 13	mpanr12	$⊢ (\|B\| \in ℝ \land 0 \leq \|B\|) \to 0 < \|B\| + 1$
15	5 10 14	syl2anc	$⊢ B \in ℂ \to 0 < \|B\| + 1$
16	15	3ad2ant2	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to 0 < \|B\| + 1$
17	9 16	elrpd	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \|B\| + 1 \in ℝ^{+}$
18	2 17	rpdivcld	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ^{+}$
19	18	rpred	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ$
20	4 19	readdcld	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \in ℝ$
21		absge0	$⊢ C \in ℂ \to 0 \leq \|C\|$
22	21	3ad2ant3	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to 0 \leq \|C\|$
23		elrp	$⊢ \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ^{+} \leftrightarrow (\frac{\frac{A}{2}}{\|B\| + 1} \in ℝ \land 0 < \frac{\frac{A}{2}}{\|B\| + 1})$
24		addgegt0	$⊢ ((\|C\| \in ℝ \land \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ) \land (0 \leq \|C\| \land 0 < \frac{\frac{A}{2}}{\|B\| + 1})) \to 0 < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})$
25	24	an4s	$⊢ ((\|C\| \in ℝ \land 0 \leq \|C\|) \land (\frac{\frac{A}{2}}{\|B\| + 1} \in ℝ \land 0 < \frac{\frac{A}{2}}{\|B\| + 1})) \to 0 < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})$
26	23 25	sylan2b	$⊢ ((\|C\| \in ℝ \land 0 \leq \|C\|) \land \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ^{+}) \to 0 < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})$
27	4 22 18 26	syl21anc	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to 0 < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})$
28	20 27	elrpd	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \in ℝ^{+}$
29	2 28	rpdivcld	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \in ℝ^{+}$
30		simprl	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to u \in ℂ$
31		simpl2	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B \in ℂ$
32	30 31	subcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to u - B \in ℂ$
33	32	abscld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|u - B\| \in ℝ$
34	2	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \frac{A}{2} \in ℝ^{+}$
35	34	rpred	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \frac{A}{2} \in ℝ$
36	28	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \in ℝ^{+}$
37	33 35 36	ltmuldivd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) < \frac{A}{2} \leftrightarrow \|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})})$
38		simprr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to v \in ℂ$
39		simpl3	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to C \in ℂ$
40	38 39	abs2difd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|v\| - \|C\| \leq \|v - C\|$
41	38	abscld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|v\| \in ℝ$
42	4	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|C\| \in ℝ$
43	41 42	resubcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|v\| - \|C\| \in ℝ$
44	38 39	subcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to v - C \in ℂ$
45	44	abscld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|v - C\| \in ℝ$
46	19	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ$
47		lelttr	$⊢ (\|v\| - \|C\| \in ℝ \land \|v - C\| \in ℝ \land \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ) \to ((\|v\| - \|C\| \leq \|v - C\| \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|v\| - \|C\| < \frac{\frac{A}{2}}{\|B\| + 1})$
48	43 45 46 47	syl3anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|v\| - \|C\| \leq \|v - C\| \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|v\| - \|C\| < \frac{\frac{A}{2}}{\|B\| + 1})$
49	40 48	mpand	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1} \to \|v\| - \|C\| < \frac{\frac{A}{2}}{\|B\| + 1})$
50	41 42 46	ltsubadd2d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v\| - \|C\| < \frac{\frac{A}{2}}{\|B\| + 1} \leftrightarrow \|v\| < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}))$
51	49 50	sylibd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1} \to \|v\| < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}))$
52	20	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \in ℝ$
53		ltle	$⊢ (\|v\| \in ℝ \land \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \in ℝ) \to (\|v\| < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \to \|v\| \leq \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}))$
54	41 52 53	syl2anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v\| < \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \to \|v\| \leq \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}))$
55	51 54	syld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1} \to \|v\| \leq \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}))$
56	32	absge0d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to 0 \leq \|u - B\|$
57		lemul2a	$⊢ ((\|v\| \in ℝ \land \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \in ℝ \land (\|u - B\| \in ℝ \land 0 \leq \|u - B\|)) \land \|v\| \leq \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) \to \|u - B\| \|v\| \leq \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}))$
58	57	ex	$⊢ (\|v\| \in ℝ \land \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \in ℝ \land (\|u - B\| \in ℝ \land 0 \leq \|u - B\|)) \to (\|v\| \leq \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \to \|u - B\| \|v\| \leq \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})))$
59	41 52 33 56 58	syl112anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v\| \leq \|C\| + (\frac{\frac{A}{2}}{\|B\| + 1}) \to \|u - B\| \|v\| \leq \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})))$
60	33 41	remulcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|u - B\| \|v\| \in ℝ$
61	33 52	remulcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) \in ℝ$
62		lelttr	$⊢ (\|u - B\| \|v\| \in ℝ \land \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) \in ℝ \land \frac{A}{2} \in ℝ) \to ((\|u - B\| \|v\| \leq \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) \land \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) < \frac{A}{2}) \to \|u - B\| \|v\| < \frac{A}{2})$
63	60 61 35 62	syl3anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u - B\| \|v\| \leq \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) \land \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) < \frac{A}{2}) \to \|u - B\| \|v\| < \frac{A}{2})$
64	63	expd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|u - B\| \|v\| \leq \|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) \to (\|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) < \frac{A}{2} \to \|u - B\| \|v\| < \frac{A}{2}))$
65	55 59 64	3syld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1} \to (\|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) < \frac{A}{2} \to \|u - B\| \|v\| < \frac{A}{2}))$
66	65	com23	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|u - B\| (\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})) < \frac{A}{2} \to (\|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1} \to \|u - B\| \|v\| < \frac{A}{2}))$
67	37 66	sylbird	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \to (\|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1} \to \|u - B\| \|v\| < \frac{A}{2}))$
68	67	impd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|u - B\| \|v\| < \frac{A}{2})$
69	32 38	absmuld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|(u - B) v\| = \|u - B\| \|v\|$
70	30 31 38	subdird	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (u - B) v = u v - B v$
71	70	fveq2d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|(u - B) v\| = \|u v - B v\|$
72	69 71	eqtr3d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|u - B\| \|v\| = \|u v - B v\|$
73	72	breq1d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|u - B\| \|v\| < \frac{A}{2} \leftrightarrow \|u v - B v\| < \frac{A}{2})$
74	68 73	sylibd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|u v - B v\| < \frac{A}{2})$
75	17	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B\| + 1 \in ℝ^{+}$
76	45 35 75	ltmuldiv2d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|B\| + 1) \|v - C\| < \frac{A}{2} \leftrightarrow \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1})$
77	31 38 39	subdid	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B (v - C) = B v - B C$
78	77	fveq2d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B (v - C)\| = \|B v - B C\|$
79	31 44	absmuld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B (v - C)\| = \|B\| \|v - C\|$
80	78 79	eqtr3d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B v - B C\| = \|B\| \|v - C\|$
81	31	abscld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B\| \in ℝ$
82	81	lep1d	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B\| \leq \|B\| + 1$
83	9	adantr	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B\| + 1 \in ℝ$
84		abscl	$⊢ v - C \in ℂ \to \|v - C\| \in ℝ$
85		absge0	$⊢ v - C \in ℂ \to 0 \leq \|v - C\|$
86	84 85	jca	$⊢ v - C \in ℂ \to (\|v - C\| \in ℝ \land 0 \leq \|v - C\|)$
87		lemul1a	$⊢ ((\|B\| \in ℝ \land \|B\| + 1 \in ℝ \land (\|v - C\| \in ℝ \land 0 \leq \|v - C\|)) \land \|B\| \leq \|B\| + 1) \to \|B\| \|v - C\| \leq (\|B\| + 1) \|v - C\|$
88	87	ex	$⊢ (\|B\| \in ℝ \land \|B\| + 1 \in ℝ \land (\|v - C\| \in ℝ \land 0 \leq \|v - C\|)) \to (\|B\| \leq \|B\| + 1 \to \|B\| \|v - C\| \leq (\|B\| + 1) \|v - C\|)$
89	86 88	syl3an3	$⊢ (\|B\| \in ℝ \land \|B\| + 1 \in ℝ \land v - C \in ℂ) \to (\|B\| \leq \|B\| + 1 \to \|B\| \|v - C\| \leq (\|B\| + 1) \|v - C\|)$
90	81 83 44 89	syl3anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|B\| \leq \|B\| + 1 \to \|B\| \|v - C\| \leq (\|B\| + 1) \|v - C\|)$
91	82 90	mpd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B\| \|v - C\| \leq (\|B\| + 1) \|v - C\|$
92	80 91	eqbrtrd	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B v - B C\| \leq (\|B\| + 1) \|v - C\|$
93	31 38	mulcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B v \in ℂ$
94	31 39	mulcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B C \in ℂ$
95	93 94	subcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to B v - B C \in ℂ$
96	95	abscld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to \|B v - B C\| \in ℝ$
97	83 45	remulcld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|B\| + 1) \|v - C\| \in ℝ$
98		lelttr	$⊢ (\|B v - B C\| \in ℝ \land (\|B\| + 1) \|v - C\| \in ℝ \land \frac{A}{2} \in ℝ) \to ((\|B v - B C\| \leq (\|B\| + 1) \|v - C\| \land (\|B\| + 1) \|v - C\| < \frac{A}{2}) \to \|B v - B C\| < \frac{A}{2})$
99	96 97 35 98	syl3anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|B v - B C\| \leq (\|B\| + 1) \|v - C\| \land (\|B\| + 1) \|v - C\| < \frac{A}{2}) \to \|B v - B C\| < \frac{A}{2})$
100	92 99	mpand	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|B\| + 1) \|v - C\| < \frac{A}{2} \to \|B v - B C\| < \frac{A}{2})$
101	76 100	sylbird	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to (\|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1} \to \|B v - B C\| < \frac{A}{2})$
102	101	adantld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|B v - B C\| < \frac{A}{2})$
103	74 102	jcad	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to (\|u v - B v\| < \frac{A}{2} \land \|B v - B C\| < \frac{A}{2}))$
104		mulcl	$⊢ (u \in ℂ \land v \in ℂ) \to u v \in ℂ$
105	104	adantl	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to u v \in ℂ$
106		simpl1	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to A \in ℝ^{+}$
107	106	rpred	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to A \in ℝ$
108		abs3lem	$⊢ ((u v \in ℂ \land B C \in ℂ) \land (B v \in ℂ \land A \in ℝ)) \to ((\|u v - B v\| < \frac{A}{2} \land \|B v - B C\| < \frac{A}{2}) \to \|u v - B C\| < A)$
109	105 94 93 107 108	syl22anc	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u v - B v\| < \frac{A}{2} \land \|B v - B C\| < \frac{A}{2}) \to \|u v - B C\| < A)$
110	103 109	syld	$⊢ ((A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \land (u \in ℂ \land v \in ℂ)) \to ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|u v - B C\| < A)$
111	110	ralrimivva	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|u v - B C\| < A)$
112		breq2	$⊢ y = \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \to (\|u - B\| < y \leftrightarrow \|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})})$
113	112	anbi1d	$⊢ y = \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \to ((\|u - B\| < y \land \|v - C\| < z) \leftrightarrow (\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < z))$
114	113	imbi1d	$⊢ y = \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \to (((\|u - B\| < y \land \|v - C\| < z) \to \|u v - B C\| < A) \leftrightarrow ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < z) \to \|u v - B C\| < A))$
115	114	2ralbidv	$⊢ y = \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \to (\forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u v - B C\| < A) \leftrightarrow \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < z) \to \|u v - B C\| < A))$
116		breq2	$⊢ z = \frac{\frac{A}{2}}{\|B\| + 1} \to (\|v - C\| < z \leftrightarrow \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1})$
117	116	anbi2d	$⊢ z = \frac{\frac{A}{2}}{\|B\| + 1} \to ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < z) \leftrightarrow (\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}))$
118	117	imbi1d	$⊢ z = \frac{\frac{A}{2}}{\|B\| + 1} \to (((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < z) \to \|u v - B C\| < A) \leftrightarrow ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|u v - B C\| < A))$
119	118	2ralbidv	$⊢ z = \frac{\frac{A}{2}}{\|B\| + 1} \to (\forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < z) \to \|u v - B C\| < A) \leftrightarrow \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|u v - B C\| < A))$
120	115 119	rspc2ev	$⊢ (\frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \in ℝ^{+} \land \frac{\frac{A}{2}}{\|B\| + 1} \in ℝ^{+} \land \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < \frac{\frac{A}{2}}{\|C\| + (\frac{\frac{A}{2}}{\|B\| + 1})} \land \|v - C\| < \frac{\frac{A}{2}}{\|B\| + 1}) \to \|u v - B C\| < A)) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u v - B C\| < A)$
121	29 18 111 120	syl3anc	$⊢ (A \in ℝ^{+} \land B \in ℂ \land C \in ℂ) \to \exists y \in ℝ^{+} \exists z \in ℝ^{+} \forall u \in ℂ \forall v \in ℂ ((\|u - B\| < y \land \|v - C\| < z) \to \|u v - B C\| < A)$

Metamath Proof Explorer

Theorem mulcn2

Proof