Step | Hyp | Ref
| Expression |
1 | | abscl 14988 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
2 | | rerpdivcl 12759 |
. . . . 5
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑥
∈ ℝ+) → ((abs‘𝐴) / 𝑥) ∈ ℝ) |
3 | 1, 2 | sylan 580 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ ((abs‘𝐴) /
𝑥) ∈
ℝ) |
4 | | simpll 764 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 𝐴 ∈ ℂ) |
5 | | rpcn 12739 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℂ) |
6 | 5 | ad2antrl 725 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 𝑛 ∈ ℂ) |
7 | | rpne0 12745 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ≠
0) |
8 | 7 | ad2antrl 725 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 𝑛 ≠ 0) |
9 | 4, 6, 8 | absdivd 15165 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → (abs‘(𝐴 / 𝑛)) = ((abs‘𝐴) / (abs‘𝑛))) |
10 | | rpre 12737 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ) |
11 | 10 | ad2antrl 725 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 𝑛 ∈ ℝ) |
12 | | rpge0 12742 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℝ+
→ 0 ≤ 𝑛) |
13 | 12 | ad2antrl 725 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 0 ≤ 𝑛) |
14 | 11, 13 | absidd 15132 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → (abs‘𝑛) = 𝑛) |
15 | 14 | oveq2d 7287 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → ((abs‘𝐴) / (abs‘𝑛)) = ((abs‘𝐴) / 𝑛)) |
16 | 9, 15 | eqtrd 2780 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → (abs‘(𝐴 / 𝑛)) = ((abs‘𝐴) / 𝑛)) |
17 | | simprr 770 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → ((abs‘𝐴) / 𝑥) < 𝑛) |
18 | 4 | abscld 15146 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → (abs‘𝐴) ∈ ℝ) |
19 | | rpre 12737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
20 | 19 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 𝑥 ∈ ℝ) |
21 | | rpgt0 12741 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ 0 < 𝑥) |
22 | 21 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 0 < 𝑥) |
23 | | rpgt0 12741 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ+
→ 0 < 𝑛) |
24 | 23 | ad2antrl 725 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → 0 < 𝑛) |
25 | | ltdiv23 11866 |
. . . . . . . . 9
⊢
(((abs‘𝐴)
∈ ℝ ∧ (𝑥
∈ ℝ ∧ 0 < 𝑥) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → (((abs‘𝐴) / 𝑥) < 𝑛 ↔ ((abs‘𝐴) / 𝑛) < 𝑥)) |
26 | 18, 20, 22, 11, 24, 25 | syl122anc 1378 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → (((abs‘𝐴) / 𝑥) < 𝑛 ↔ ((abs‘𝐴) / 𝑛) < 𝑥)) |
27 | 17, 26 | mpbid 231 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → ((abs‘𝐴) / 𝑛) < 𝑥) |
28 | 16, 27 | eqbrtrd 5101 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ (𝑛 ∈
ℝ+ ∧ ((abs‘𝐴) / 𝑥) < 𝑛)) → (abs‘(𝐴 / 𝑛)) < 𝑥) |
29 | 28 | expr 457 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
ℝ+) → (((abs‘𝐴) / 𝑥) < 𝑛 → (abs‘(𝐴 / 𝑛)) < 𝑥)) |
30 | 29 | ralrimiva 3110 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ ∀𝑛 ∈
ℝ+ (((abs‘𝐴) / 𝑥) < 𝑛 → (abs‘(𝐴 / 𝑛)) < 𝑥)) |
31 | | breq1 5082 |
. . . . 5
⊢ (𝑦 = ((abs‘𝐴) / 𝑥) → (𝑦 < 𝑛 ↔ ((abs‘𝐴) / 𝑥) < 𝑛)) |
32 | 31 | rspceaimv 3566 |
. . . 4
⊢
((((abs‘𝐴) /
𝑥) ∈ ℝ ∧
∀𝑛 ∈
ℝ+ (((abs‘𝐴) / 𝑥) < 𝑛 → (abs‘(𝐴 / 𝑛)) < 𝑥)) → ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘(𝐴 / 𝑛)) < 𝑥)) |
33 | 3, 30, 32 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+)
→ ∃𝑦 ∈
ℝ ∀𝑛 ∈
ℝ+ (𝑦 <
𝑛 → (abs‘(𝐴 / 𝑛)) < 𝑥)) |
34 | 33 | ralrimiva 3110 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘(𝐴 / 𝑛)) < 𝑥)) |
35 | | simpl 483 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+)
→ 𝐴 ∈
ℂ) |
36 | 5 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+)
→ 𝑛 ∈
ℂ) |
37 | 7 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+)
→ 𝑛 ≠
0) |
38 | 35, 36, 37 | divcld 11751 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑛 ∈ ℝ+)
→ (𝐴 / 𝑛) ∈
ℂ) |
39 | 38 | ralrimiva 3110 |
. . 3
⊢ (𝐴 ∈ ℂ →
∀𝑛 ∈
ℝ+ (𝐴 /
𝑛) ∈
ℂ) |
40 | | rpssre 12736 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
41 | 40 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ →
ℝ+ ⊆ ℝ) |
42 | 39, 41 | rlim0lt 15216 |
. 2
⊢ (𝐴 ∈ ℂ → ((𝑛 ∈ ℝ+
↦ (𝐴 / 𝑛)) ⇝𝑟 0
↔ ∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ℝ ∀𝑛 ∈ ℝ+ (𝑦 < 𝑛 → (abs‘(𝐴 / 𝑛)) < 𝑥))) |
43 | 34, 42 | mpbird 256 |
1
⊢ (𝐴 ∈ ℂ → (𝑛 ∈ ℝ+
↦ (𝐴 / 𝑛)) ⇝𝑟
0) |