This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ‘ ( ( 𝑢 · 𝑣 ) − ( 𝐵 · 𝐶 ) ) ) < 𝐴 ) )