mulcn2 - Metamath Proof Explorer

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

Theorem mulcn2 15610

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.)

**Assertion**
Ref	Expression
mulcn2	⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))

Distinct variable groups: 𝑣,𝑢,𝑦,𝑧,𝐴 𝑢,𝐵,𝑣,𝑦,𝑧 𝑢,𝐶,𝑣,𝑦,𝑧

**Proof of Theorem mulcn2**
Step	Hyp	Ref	Expression
1		rphalfcl 13034	. . . 4 ⊢ (𝐴 ∈ ℝ⁺ → (𝐴 / 2) ∈ ℝ⁺)
2	1	3ad2ant1 1133	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 / 2) ∈ ℝ⁺)
3		abscl 15295	. . . . . 6 ⊢ (𝐶 ∈ ℂ → (abs‘𝐶) ∈ ℝ)
4	3	3ad2ant3 1135	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘𝐶) ∈ ℝ)
5		abscl 15295	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℂ → (abs‘𝐵) ∈ ℝ)
6	5	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (abs‘𝐵) ∈ ℝ)
7		1re 11233	. . . . . . . . 9 ⊢ 1 ∈ ℝ
8		readdcl 11210	. . . . . . . . 9 ⊢ (((abs‘𝐵) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝐵) + 1) ∈ ℝ)
9	6, 7, 8	sylancl 586	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((abs‘𝐵) + 1) ∈ ℝ)
10		absge0 15304	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℂ → 0 ≤ (abs‘𝐵))
11		0lt1 11757	. . . . . . . . . . 11 ⊢ 0 < 1
12		addgegt0 11722	. . . . . . . . . . . 12 ⊢ ((((abs‘𝐵) ∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ (abs‘𝐵) ∧ 0 < 1)) → 0 < ((abs‘𝐵) + 1))
13	12	an4s 660	. . . . . . . . . . 11 ⊢ ((((abs‘𝐵) ∈ ℝ ∧ 0 ≤ (abs‘𝐵)) ∧ (1 ∈ ℝ ∧ 0 < 1)) → 0 < ((abs‘𝐵) + 1))
14	7, 11, 13	mpanr12 705	. . . . . . . . . 10 ⊢ (((abs‘𝐵) ∈ ℝ ∧ 0 ≤ (abs‘𝐵)) → 0 < ((abs‘𝐵) + 1))
15	5, 10, 14	syl2anc 584	. . . . . . . . 9 ⊢ (𝐵 ∈ ℂ → 0 < ((abs‘𝐵) + 1))
16	15	3ad2ant2 1134	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 0 < ((abs‘𝐵) + 1))
17	9, 16	elrpd 13046	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((abs‘𝐵) + 1) ∈ ℝ⁺)
18	2, 17	rpdivcld 13066	. . . . . 6 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ⁺)
19	18	rpred 13049	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ)
20	4, 19	readdcld 11262	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) ∈ ℝ)
21		absge0 15304	. . . . . 6 ⊢ (𝐶 ∈ ℂ → 0 ≤ (abs‘𝐶))
22	21	3ad2ant3 1135	. . . . 5 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 0 ≤ (abs‘𝐶))
23		elrp 13008	. . . . . 6 ⊢ (((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ⁺ ↔ (((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ ∧ 0 < ((𝐴 / 2) / ((abs‘𝐵) + 1))))
24		addgegt0 11722	. . . . . . 7 ⊢ ((((abs‘𝐶) ∈ ℝ ∧ ((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ) ∧ (0 ≤ (abs‘𝐶) ∧ 0 < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → 0 < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))
25	24	an4s 660	. . . . . 6 ⊢ ((((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶)) ∧ (((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ ∧ 0 < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → 0 < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))
26	23, 25	sylan2b 594	. . . . 5 ⊢ ((((abs‘𝐶) ∈ ℝ ∧ 0 ≤ (abs‘𝐶)) ∧ ((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ⁺) → 0 < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))
27	4, 22, 18, 26	syl21anc 837	. . . 4 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → 0 < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))
28	20, 27	elrpd 13046	. . 3 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) ∈ ℝ⁺)
29	2, 28	rpdivcld 13066	. 2 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∈ ℝ⁺)
30		simprl 770	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑢 ∈ ℂ)
31		simpl2 1193	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝐵 ∈ ℂ)
32	30, 31	subcld 11592	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑢 − 𝐵) ∈ ℂ)
33	32	abscld 15453	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘(𝑢 − 𝐵)) ∈ ℝ)
34	2	adantr 480	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝐴 / 2) ∈ ℝ⁺)
35	34	rpred 13049	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝐴 / 2) ∈ ℝ)
36	28	adantr 480	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) ∈ ℝ⁺)
37	33, 35, 36	ltmuldivd 13096	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) < (𝐴 / 2) ↔ (abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))))
38		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝑣 ∈ ℂ)
39		simpl3 1194	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝐶 ∈ ℂ)
40	38, 39	abs2difd 15474	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝑣) − (abs‘𝐶)) ≤ (abs‘(𝑣 − 𝐶)))
41	38	abscld 15453	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘𝑣) ∈ ℝ)
42	4	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘𝐶) ∈ ℝ)
43	41, 42	resubcld 11663	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝑣) − (abs‘𝐶)) ∈ ℝ)
44	38, 39	subcld 11592	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑣 − 𝐶) ∈ ℂ)
45	44	abscld 15453	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘(𝑣 − 𝐶)) ∈ ℝ)
46	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ)
47		lelttr 11323	. . . . . . . . . . . . . 14 ⊢ ((((abs‘𝑣) − (abs‘𝐶)) ∈ ℝ ∧ (abs‘(𝑣 − 𝐶)) ∈ ℝ ∧ ((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ) → ((((abs‘𝑣) − (abs‘𝐶)) ≤ (abs‘(𝑣 − 𝐶)) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → ((abs‘𝑣) − (abs‘𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))))
48	43, 45, 46, 47	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((((abs‘𝑣) − (abs‘𝐶)) ≤ (abs‘(𝑣 − 𝐶)) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → ((abs‘𝑣) − (abs‘𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))))
49	40, 48	mpand 695	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → ((abs‘𝑣) − (abs‘𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))))
50	41, 42, 46	ltsubadd2d 11833	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘𝑣) − (abs‘𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) ↔ (abs‘𝑣) < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))
51	49, 50	sylibd 239	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → (abs‘𝑣) < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))
52	20	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) ∈ ℝ)
53		ltle 11321	. . . . . . . . . . . 12 ⊢ (((abs‘𝑣) ∈ ℝ ∧ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) ∈ ℝ) → ((abs‘𝑣) < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘𝑣) ≤ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))
54	41, 52, 53	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝑣) < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘𝑣) ≤ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))
55	51, 54	syld 47	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → (abs‘𝑣) ≤ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))
56	32	absge0d 15461	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 0 ≤ (abs‘(𝑢 − 𝐵)))
57		lemul2a 12094	. . . . . . . . . . . 12 ⊢ ((((abs‘𝑣) ∈ ℝ ∧ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) ∈ ℝ ∧ ((abs‘(𝑢 − 𝐵)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑢 − 𝐵)))) ∧ (abs‘𝑣) ≤ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) ≤ ((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))
58	57	ex 412	. . . . . . . . . . 11 ⊢ (((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 1376	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝑣) ≤ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) ≤ ((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))))
60	33, 41	remulcld 11263	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) ∈ ℝ)
61	33, 52	remulcld 11263	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∈ ℝ)
62		lelttr 11323	. . . . . . . . . . . 12 ⊢ ((((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 1373	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) ≤ ((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ ((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) < (𝐴 / 2)) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) < (𝐴 / 2)))
64	63	expd 415	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) ≤ ((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → (((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) < (𝐴 / 2) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) < (𝐴 / 2))))
65	55, 59, 64	3syld 60	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → (((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) < (𝐴 / 2) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) < (𝐴 / 2))))
66	65	com23 86	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) · ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) < (𝐴 / 2) → ((abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) < (𝐴 / 2))))
67	37, 66	sylbird 260	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → ((abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) < (𝐴 / 2))))
68	67	impd 410	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) < (𝐴 / 2)))
69	32, 38	absmuld 15471	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘((𝑢 − 𝐵) · 𝑣)) = ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)))
70	30, 31, 38	subdird 11692	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝑢 − 𝐵) · 𝑣) = ((𝑢 · 𝑣) − (𝐵 · 𝑣)))
71	70	fveq2d 6879	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘((𝑢 − 𝐵) · 𝑣)) = (abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))))
72	69, 71	eqtr3d 2772	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) = (abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))))
73	72	breq1d 5129	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) · (abs‘𝑣)) < (𝐴 / 2) ↔ (abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))) < (𝐴 / 2)))
74	68, 73	sylibd 239	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))) < (𝐴 / 2)))
75	17	adantr 480	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝐵) + 1) ∈ ℝ⁺)
76	45, 35, 75	ltmuldiv2d 13097	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) < (𝐴 / 2) ↔ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))))
77	31, 38, 39	subdid 11691	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝐵 · (𝑣 − 𝐶)) = ((𝐵 · 𝑣) − (𝐵 · 𝐶)))
78	77	fveq2d 6879	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘(𝐵 · (𝑣 − 𝐶))) = (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))))
79	31, 44	absmuld 15471	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘(𝐵 · (𝑣 − 𝐶))) = ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))))
80	78, 79	eqtr3d 2772	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) = ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))))
81	31	abscld 15453	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘𝐵) ∈ ℝ)
82	81	lep1d 12171	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘𝐵) ≤ ((abs‘𝐵) + 1))
83	9	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝐵) + 1) ∈ ℝ)
84		abscl 15295	. . . . . . . . . . . . 13 ⊢ ((𝑣 − 𝐶) ∈ ℂ → (abs‘(𝑣 − 𝐶)) ∈ ℝ)
85		absge0 15304	. . . . . . . . . . . . 13 ⊢ ((𝑣 − 𝐶) ∈ ℂ → 0 ≤ (abs‘(𝑣 − 𝐶)))
86	84, 85	jca 511	. . . . . . . . . . . 12 ⊢ ((𝑣 − 𝐶) ∈ ℂ → ((abs‘(𝑣 − 𝐶)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑣 − 𝐶))))
87		lemul1a 12093	. . . . . . . . . . . . 13 ⊢ ((((abs‘𝐵) ∈ ℝ ∧ ((abs‘𝐵) + 1) ∈ ℝ ∧ ((abs‘(𝑣 − 𝐶)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑣 − 𝐶)))) ∧ (abs‘𝐵) ≤ ((abs‘𝐵) + 1)) → ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))))
88	87	ex 412	. . . . . . . . . . . 12 ⊢ (((abs‘𝐵) ∈ ℝ ∧ ((abs‘𝐵) + 1) ∈ ℝ ∧ ((abs‘(𝑣 − 𝐶)) ∈ ℝ ∧ 0 ≤ (abs‘(𝑣 − 𝐶)))) → ((abs‘𝐵) ≤ ((abs‘𝐵) + 1) → ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶)))))
89	86, 88	syl3an3 1165	. . . . . . . . . . 11 ⊢ (((abs‘𝐵) ∈ ℝ ∧ ((abs‘𝐵) + 1) ∈ ℝ ∧ (𝑣 − 𝐶) ∈ ℂ) → ((abs‘𝐵) ≤ ((abs‘𝐵) + 1) → ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶)))))
90	81, 83, 44, 89	syl3anc 1373	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝐵) ≤ ((abs‘𝐵) + 1) → ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶)))))
91	82, 90	mpd 15	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))))
92	80, 91	eqbrtrd 5141	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))))
93	31, 38	mulcld 11253	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝐵 · 𝑣) ∈ ℂ)
94	31, 39	mulcld 11253	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝐵 · 𝐶) ∈ ℂ)
95	93, 94	subcld 11592	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((𝐵 · 𝑣) − (𝐵 · 𝐶)) ∈ ℂ)
96	95	abscld 15453	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) ∈ ℝ)
97	83, 45	remulcld 11263	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) ∈ ℝ)
98		lelttr 11323	. . . . . . . . 9 ⊢ (((abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) ∈ ℝ ∧ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) ∈ ℝ ∧ (𝐴 / 2) ∈ ℝ) → (((abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) ∧ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) < (𝐴 / 2)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)))
99	96, 97, 35, 98	syl3anc 1373	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) ∧ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) < (𝐴 / 2)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)))
100	92, 99	mpand 695	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) < (𝐴 / 2) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)))
101	76, 100	sylbird 260	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → ((abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)))
102	101	adantld 490	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)))
103	74, 102	jcad 512	. . . 4 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → ((abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2))))
104		mulcl 11211	. . . . . 6 ⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 · 𝑣) ∈ ℂ)
105	104	adantl 481	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (𝑢 · 𝑣) ∈ ℂ)
106		simpl1 1192	. . . . . 6 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝐴 ∈ ℝ⁺)
107	106	rpred 13049	. . . . 5 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → 𝐴 ∈ ℝ)
108		abs3lem 15355	. . . . 5 ⊢ ((((𝑢 · 𝑣) ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) ∧ ((𝐵 · 𝑣) ∈ ℂ ∧ 𝐴 ∈ ℝ)) → (((abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))
109	105, 94, 93, 107, 108	syl22anc 838	. . . 4 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))
110	103, 109	syld 47	. . 3 ⊢ (((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ)) → (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))
111	110	ralrimivva 3187	. 2 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))
112		breq2 5123	. . . . . 6 ⊢ (𝑦 = ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → ((abs‘(𝑢 − 𝐵)) < 𝑦 ↔ (abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))))
113	112	anbi1d 631	. . . . 5 ⊢ (𝑦 = ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧)))
114	113	imbi1d 341	. . . 4 ⊢ (𝑦 = ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → ((((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴) ↔ (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴)))
115	114	2ralbidv 3205	. . 3 ⊢ (𝑦 = ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴) ↔ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴)))
116		breq2 5123	. . . . . 6 ⊢ (𝑧 = ((𝐴 / 2) / ((abs‘𝐵) + 1)) → ((abs‘(𝑣 − 𝐶)) < 𝑧 ↔ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))))
117	116	anbi2d 630	. . . . 5 ⊢ (𝑧 = ((𝐴 / 2) / ((abs‘𝐵) + 1)) → (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) ↔ ((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)))))
118	117	imbi1d 341	. . . 4 ⊢ (𝑧 = ((𝐴 / 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 3205	. . 3 ⊢ (𝑧 = ((𝐴 / 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 3614	. 2 ⊢ ((((𝐴 / 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 1373	1 ⊢ ((𝐴 ∈ ℝ⁺ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑦 ∈ ℝ⁺ ∃𝑧 ∈ ℝ⁺ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3051 ∃wrex 3060 class class class wbr 5119 ‘cfv 6530 (class class class)co 7403 ℂcc 11125 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 < clt 11267 ≤ cle 11268 − cmin 11464 / cdiv 11892 2c2 12293 ℝ⁺crp 13006 abscabs 15251

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7727 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-pre-sup 11205

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6483 df-fun 6532 df-fn 6533 df-f 6534 df-f1 6535 df-fo 6536 df-f1o 6537 df-fv 6538 df-riota 7360 df-ov 7406 df-oprab 7407 df-mpo 7408 df-om 7860 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8383 df-rdg 8422 df-er 8717 df-en 8958 df-dom 8959 df-sdom 8960 df-sup 9452 df-pnf 11269 df-mnf 11270 df-xr 11271 df-ltxr 11272 df-le 11273 df-sub 11466 df-neg 11467 df-div 11893 df-nn 12239 df-2 12301 df-3 12302 df-n0 12500 df-z 12587 df-uz 12851 df-rp 13007 df-seq 14018 df-exp 14078 df-cj 15116 df-re 15117 df-im 15118 df-sqrt 15252 df-abs 15253

This theorem is referenced by: climmul 15647 rlimmul 15659 mulcn 24805 mpomulcn 24807 mulc1cncf 24847 mullimc 45593 mullimcf 45600

W3C validator