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	⊢ ( ( 𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑢 ∈ ℂ ∀ 𝑣 ∈ ℂ ( ( ( abs ‘ ( 𝑢 − 𝐵 ) ) < 𝑦 ∧ ( abs ‘ ( 𝑣 − 𝐶 ) ) < 𝑧 ) → ( abs ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐵 · 𝐶 ) ) ) < 𝐴 ) )

Proof

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

Metamath Proof Explorer

Theorem mulcn2

Proof