Proof of Theorem mulcn2
Step | Hyp | Ref
| Expression |
1 | | rphalfcl 12686 |
. . . 4
⊢ (𝐴 ∈ ℝ+
→ (𝐴 / 2) ∈
ℝ+) |
2 | 1 | 3ad2ant1 1131 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (𝐴 / 2) ∈
ℝ+) |
3 | | abscl 14918 |
. . . . . 6
⊢ (𝐶 ∈ ℂ →
(abs‘𝐶) ∈
ℝ) |
4 | 3 | 3ad2ant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (abs‘𝐶) ∈
ℝ) |
5 | | abscl 14918 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℂ →
(abs‘𝐵) ∈
ℝ) |
6 | 5 | 3ad2ant2 1132 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ (abs‘𝐵) ∈
ℝ) |
7 | | 1re 10906 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
8 | | readdcl 10885 |
. . . . . . . . 9
⊢
(((abs‘𝐵)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝐵) + 1) ∈ ℝ) |
9 | 6, 7, 8 | sylancl 585 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ((abs‘𝐵) + 1)
∈ ℝ) |
10 | | absge0 14927 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℂ → 0 ≤
(abs‘𝐵)) |
11 | | 0lt1 11427 |
. . . . . . . . . . 11
⊢ 0 <
1 |
12 | | addgegt0 11392 |
. . . . . . . . . . . 12
⊢
((((abs‘𝐵)
∈ ℝ ∧ 1 ∈ ℝ) ∧ (0 ≤ (abs‘𝐵) ∧ 0 < 1)) → 0 <
((abs‘𝐵) +
1)) |
13 | 12 | an4s 656 |
. . . . . . . . . . 11
⊢
((((abs‘𝐵)
∈ ℝ ∧ 0 ≤ (abs‘𝐵)) ∧ (1 ∈ ℝ ∧ 0 < 1))
→ 0 < ((abs‘𝐵) + 1)) |
14 | 7, 11, 13 | mpanr12 701 |
. . . . . . . . . 10
⊢
(((abs‘𝐵)
∈ ℝ ∧ 0 ≤ (abs‘𝐵)) → 0 < ((abs‘𝐵) + 1)) |
15 | 5, 10, 14 | syl2anc 583 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ → 0 <
((abs‘𝐵) +
1)) |
16 | 15 | 3ad2ant2 1132 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ 0 < ((abs‘𝐵) + 1)) |
17 | 9, 16 | elrpd 12698 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ((abs‘𝐵) + 1)
∈ ℝ+) |
18 | 2, 17 | rpdivcld 12718 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ((𝐴 / 2) /
((abs‘𝐵) + 1)) ∈
ℝ+) |
19 | 18 | rpred 12701 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ((𝐴 / 2) /
((abs‘𝐵) + 1)) ∈
ℝ) |
20 | 4, 19 | readdcld 10935 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ((abs‘𝐶) +
((𝐴 / 2) /
((abs‘𝐵) + 1)))
∈ ℝ) |
21 | | absge0 14927 |
. . . . . 6
⊢ (𝐶 ∈ ℂ → 0 ≤
(abs‘𝐶)) |
22 | 21 | 3ad2ant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ 0 ≤ (abs‘𝐶)) |
23 | | elrp 12661 |
. . . . . 6
⊢ (((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈
ℝ+ ↔ (((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ ∧ 0 < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
24 | | addgegt0 11392 |
. . . . . . 7
⊢
((((abs‘𝐶)
∈ ℝ ∧ ((𝐴 /
2) / ((abs‘𝐵) + 1))
∈ ℝ) ∧ (0 ≤ (abs‘𝐶) ∧ 0 < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → 0 < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
25 | 24 | an4s 656 |
. . . . . 6
⊢
((((abs‘𝐶)
∈ ℝ ∧ 0 ≤ (abs‘𝐶)) ∧ (((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ ∧ 0 < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → 0 <
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
26 | 23, 25 | sylan2b 593 |
. . . . 5
⊢
((((abs‘𝐶)
∈ ℝ ∧ 0 ≤ (abs‘𝐶)) ∧ ((𝐴 / 2) / ((abs‘𝐵) + 1)) ∈ ℝ+) → 0
< ((abs‘𝐶) +
((𝐴 / 2) /
((abs‘𝐵) +
1)))) |
27 | 4, 22, 18, 26 | syl21anc 834 |
. . . 4
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ 0 < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
28 | 20, 27 | elrpd 12698 |
. . 3
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ((abs‘𝐶) +
((𝐴 / 2) /
((abs‘𝐵) + 1)))
∈ ℝ+) |
29 | 2, 28 | rpdivcld 12718 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ((𝐴 / 2) /
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∈
ℝ+) |
30 | | simprl 767 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝑢 ∈
ℂ) |
31 | | simpl2 1190 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐵 ∈
ℂ) |
32 | 30, 31 | subcld 11262 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝑢 − 𝐵) ∈
ℂ) |
33 | 32 | abscld 15076 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘(𝑢
− 𝐵)) ∈
ℝ) |
34 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐴 / 2) ∈
ℝ+) |
35 | 34 | rpred 12701 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐴 / 2) ∈
ℝ) |
36 | 28 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝐶) +
((𝐴 / 2) /
((abs‘𝐵) + 1)))
∈ ℝ+) |
37 | 33, 35, 36 | ltmuldivd 12748 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘(𝑢
− 𝐵)) ·
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) < (𝐴 / 2) ↔ (abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))) |
38 | | simprr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝑣 ∈
ℂ) |
39 | | simpl3 1191 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐶 ∈
ℂ) |
40 | 38, 39 | abs2difd 15097 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝑣)
− (abs‘𝐶)) ≤
(abs‘(𝑣 − 𝐶))) |
41 | 38 | abscld 15076 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘𝑣) ∈
ℝ) |
42 | 4 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘𝐶) ∈
ℝ) |
43 | 41, 42 | resubcld 11333 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝑣)
− (abs‘𝐶))
∈ ℝ) |
44 | 38, 39 | subcld 11262 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝑣 − 𝐶) ∈
ℂ) |
45 | 44 | abscld 15076 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘(𝑣
− 𝐶)) ∈
ℝ) |
46 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((𝐴 / 2) /
((abs‘𝐵) + 1)) ∈
ℝ) |
47 | | lelttr 10996 |
. . . . . . . . . . . . . 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 1369 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((((abs‘𝑣)
− (abs‘𝐶)) ≤
(abs‘(𝑣 − 𝐶)) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → ((abs‘𝑣) − (abs‘𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
49 | 40, 48 | mpand 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘(𝑣
− 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → ((abs‘𝑣) − (abs‘𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
50 | 41, 42, 46 | ltsubadd2d 11503 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘𝑣)
− (abs‘𝐶)) <
((𝐴 / 2) /
((abs‘𝐵) + 1)) ↔
(abs‘𝑣) <
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))) |
51 | 49, 50 | sylibd 238 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘(𝑣
− 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)) → (abs‘𝑣) < ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))) |
52 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝐶) +
((𝐴 / 2) /
((abs‘𝐵) + 1)))
∈ ℝ) |
53 | | ltle 10994 |
. . . . . . . . . . . 12
⊢
(((abs‘𝑣)
∈ ℝ ∧ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) ∈ ℝ) →
((abs‘𝑣) <
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘𝑣) ≤ ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))))) |
54 | 41, 52, 53 | syl2anc 583 |
. . . . . . . . . . 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 15084 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 0 ≤ (abs‘(𝑢
− 𝐵))) |
57 | | lemul2a 11760 |
. . . . . . . . . . . 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 1372 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝑣) ≤
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1))) →
((abs‘(𝑢 −
𝐵)) ·
(abs‘𝑣)) ≤
((abs‘(𝑢 −
𝐵)) ·
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))) |
60 | 33, 41 | remulcld 10936 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘(𝑢
− 𝐵)) ·
(abs‘𝑣)) ∈
ℝ) |
61 | 33, 52 | remulcld 10936 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘(𝑢
− 𝐵)) ·
((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∈
ℝ) |
62 | | lelttr 10996 |
. . . . . . . . . . . 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 1369 |
. . . . . . . . . . 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 259 |
. . . . . . 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 15094 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝑢
− 𝐵) · 𝑣)) = ((abs‘(𝑢 − 𝐵)) · (abs‘𝑣))) |
70 | 30, 31, 38 | subdird 11362 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((𝑢 − 𝐵) · 𝑣) = ((𝑢 · 𝑣) − (𝐵 · 𝑣))) |
71 | 70 | fveq2d 6760 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝑢
− 𝐵) · 𝑣)) = (abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣)))) |
72 | 69, 71 | eqtr3d 2780 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘(𝑢
− 𝐵)) ·
(abs‘𝑣)) =
(abs‘((𝑢 ·
𝑣) − (𝐵 · 𝑣)))) |
73 | 72 | breq1d 5080 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘(𝑢
− 𝐵)) ·
(abs‘𝑣)) < (𝐴 / 2) ↔ (abs‘((𝑢 · 𝑣) − (𝐵 · 𝑣))) < (𝐴 / 2))) |
74 | 68, 73 | sylibd 238 |
. . . . 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 12749 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((((abs‘𝐵) +
1) · (abs‘(𝑣
− 𝐶))) < (𝐴 / 2) ↔ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
77 | 31, 38, 39 | subdid 11361 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐵 · (𝑣 − 𝐶)) = ((𝐵 · 𝑣) − (𝐵 · 𝐶))) |
78 | 77 | fveq2d 6760 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘(𝐵
· (𝑣 − 𝐶))) = (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶)))) |
79 | 31, 44 | absmuld 15094 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘(𝐵
· (𝑣 − 𝐶))) = ((abs‘𝐵) · (abs‘(𝑣 − 𝐶)))) |
80 | 78, 79 | eqtr3d 2780 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝐵
· 𝑣) − (𝐵 · 𝐶))) = ((abs‘𝐵) · (abs‘(𝑣 − 𝐶)))) |
81 | 31 | abscld 15076 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘𝐵) ∈
ℝ) |
82 | 81 | lep1d 11836 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘𝐵) ≤
((abs‘𝐵) +
1)) |
83 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝐵) + 1)
∈ ℝ) |
84 | | abscl 14918 |
. . . . . . . . . . . . 13
⊢ ((𝑣 − 𝐶) ∈ ℂ → (abs‘(𝑣 − 𝐶)) ∈ ℝ) |
85 | | absge0 14927 |
. . . . . . . . . . . . 13
⊢ ((𝑣 − 𝐶) ∈ ℂ → 0 ≤
(abs‘(𝑣 − 𝐶))) |
86 | 84, 85 | jca 511 |
. . . . . . . . . . . 12
⊢ ((𝑣 − 𝐶) ∈ ℂ → ((abs‘(𝑣 − 𝐶)) ∈ ℝ ∧ 0 ≤
(abs‘(𝑣 − 𝐶)))) |
87 | | lemul1a 11759 |
. . . . . . . . . . . . 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 1163 |
. . . . . . . . . . 11
⊢
(((abs‘𝐵)
∈ ℝ ∧ ((abs‘𝐵) + 1) ∈ ℝ ∧ (𝑣 − 𝐶) ∈ ℂ) → ((abs‘𝐵) ≤ ((abs‘𝐵) + 1) → ((abs‘𝐵) · (abs‘(𝑣 − 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))))) |
90 | 81, 83, 44, 89 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝐵) ≤
((abs‘𝐵) + 1) →
((abs‘𝐵) ·
(abs‘(𝑣 − 𝐶))) ≤ (((abs‘𝐵) + 1) ·
(abs‘(𝑣 − 𝐶))))) |
91 | 82, 90 | mpd 15 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((abs‘𝐵)
· (abs‘(𝑣
− 𝐶))) ≤
(((abs‘𝐵) + 1)
· (abs‘(𝑣
− 𝐶)))) |
92 | 80, 91 | eqbrtrd 5092 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝐵
· 𝑣) − (𝐵 · 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶)))) |
93 | 31, 38 | mulcld 10926 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐵 · 𝑣) ∈
ℂ) |
94 | 31, 39 | mulcld 10926 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝐵 · 𝐶) ∈
ℂ) |
95 | 93, 94 | subcld 11262 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((𝐵 · 𝑣) − (𝐵 · 𝐶)) ∈ ℂ) |
96 | 95 | abscld 15076 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (abs‘((𝐵
· 𝑣) − (𝐵 · 𝐶))) ∈ ℝ) |
97 | 83, 45 | remulcld 10936 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘𝐵) + 1)
· (abs‘(𝑣
− 𝐶))) ∈
ℝ) |
98 | | lelttr 10996 |
. . . . . . . . 9
⊢
(((abs‘((𝐵
· 𝑣) − (𝐵 · 𝐶))) ∈ ℝ ∧ (((abs‘𝐵) + 1) ·
(abs‘(𝑣 − 𝐶))) ∈ ℝ ∧ (𝐴 / 2) ∈ ℝ) →
(((abs‘((𝐵 ·
𝑣) − (𝐵 · 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) ∧ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) < (𝐴 / 2)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2))) |
99 | 96, 97, 35, 98 | syl3anc 1369 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (((abs‘((𝐵
· 𝑣) − (𝐵 · 𝐶))) ≤ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) ∧ (((abs‘𝐵) + 1) · (abs‘(𝑣 − 𝐶))) < (𝐴 / 2)) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2))) |
100 | 92, 99 | mpand 691 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ ((((abs‘𝐵) +
1) · (abs‘(𝑣
− 𝐶))) < (𝐴 / 2) → (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2))) |
101 | 76, 100 | sylbird 259 |
. . . . . 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 10886 |
. . . . . 6
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢 · 𝑣) ∈ ℂ) |
105 | 104 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ (𝑢 · 𝑣) ∈
ℂ) |
106 | | simpl1 1189 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐴 ∈
ℝ+) |
107 | 106 | rpred 12701 |
. . . . 5
⊢ (((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
∧ (𝑢 ∈ ℂ
∧ 𝑣 ∈ ℂ))
→ 𝐴 ∈
ℝ) |
108 | | abs3lem 14978 |
. . . . 5
⊢ ((((𝑢 · 𝑣) ∈ ℂ ∧ (𝐵 · 𝐶) ∈ ℂ) ∧ ((𝐵 · 𝑣) ∈ ℂ ∧ 𝐴 ∈ ℝ)) →
(((abs‘((𝑢 ·
𝑣) − (𝐵 · 𝑣))) < (𝐴 / 2) ∧ (abs‘((𝐵 · 𝑣) − (𝐵 · 𝐶))) < (𝐴 / 2)) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴)) |
109 | 105, 94, 93, 107, 108 | syl22anc 835 |
. . . 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 3114 |
. 2
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∀𝑢 ∈
ℂ ∀𝑣 ∈
ℂ (((abs‘(𝑢
− 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1))) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴)) |
112 | | breq2 5074 |
. . . . . 6
⊢ (𝑦 = ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → ((abs‘(𝑢 − 𝐵)) < 𝑦 ↔ (abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))))) |
113 | 112 | anbi1d 629 |
. . . . 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 3122 |
. . 3
⊢ (𝑦 = ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) → (∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴) ↔ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝐵)) < ((𝐴 / 2) / ((abs‘𝐶) + ((𝐴 / 2) / ((abs‘𝐵) + 1)))) ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴))) |
116 | | breq2 5074 |
. . . . . 6
⊢ (𝑧 = ((𝐴 / 2) / ((abs‘𝐵) + 1)) → ((abs‘(𝑣 − 𝐶)) < 𝑧 ↔ (abs‘(𝑣 − 𝐶)) < ((𝐴 / 2) / ((abs‘𝐵) + 1)))) |
117 | 116 | anbi2d 628 |
. . . . 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 3122 |
. . 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 3564 |
. 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 1369 |
1
⊢ ((𝐴 ∈ ℝ+
∧ 𝐵 ∈ ℂ
∧ 𝐶 ∈ ℂ)
→ ∃𝑦 ∈
ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ
(((abs‘(𝑢 −
𝐵)) < 𝑦 ∧ (abs‘(𝑣 − 𝐶)) < 𝑧) → (abs‘((𝑢 · 𝑣) − (𝐵 · 𝐶))) < 𝐴)) |