Proof of Theorem aaliou2b
Step | Hyp | Ref
| Expression |
1 | | elin 3758 |
. . 3
⊢ (𝐴 ∈ (𝔸 ∩
ℝ) ↔ (𝐴 ∈
𝔸 ∧ 𝐴 ∈
ℝ)) |
2 | | aaliou2 23899 |
. . 3
⊢ (𝐴 ∈ (𝔸 ∩
ℝ) → ∃𝑘
∈ ℕ ∃𝑥
∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
3 | 1, 2 | sylbir 224 |
. 2
⊢ ((𝐴 ∈ 𝔸 ∧ 𝐴 ∈ ℝ) →
∃𝑘 ∈ ℕ
∃𝑥 ∈
ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
4 | | 1nn 10908 |
. . . 4
⊢ 1 ∈
ℕ |
5 | 4 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) → 1
∈ ℕ) |
6 | | aacn 23876 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝔸 → 𝐴 ∈
ℂ) |
7 | 6 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
𝐴 ∈
ℂ) |
8 | 7 | imcld 13783 |
. . . . . 6
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
(ℑ‘𝐴) ∈
ℝ) |
9 | 8 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
(ℑ‘𝐴) ∈
ℂ) |
10 | | reim0b 13707 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
11 | 6, 10 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ 𝔸 → (𝐴 ∈ ℝ ↔
(ℑ‘𝐴) =
0)) |
12 | 11 | necon3bbid 2819 |
. . . . . 6
⊢ (𝐴 ∈ 𝔸 → (¬
𝐴 ∈ ℝ ↔
(ℑ‘𝐴) ≠
0)) |
13 | 12 | biimpa 500 |
. . . . 5
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
(ℑ‘𝐴) ≠
0) |
14 | 9, 13 | absrpcld 14035 |
. . . 4
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
15 | 14 | rphalfcld 11760 |
. . 3
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
((abs‘(ℑ‘𝐴)) / 2) ∈
ℝ+) |
16 | 15 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((abs‘(ℑ‘𝐴)) / 2) ∈
ℝ+) |
17 | | 1nn0 11185 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
18 | | nnexpcl 12735 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ ℕ ∧ 1 ∈
ℕ0) → (𝑞↑1) ∈ ℕ) |
19 | 17, 18 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℕ → (𝑞↑1) ∈
ℕ) |
20 | 19 | ad2antll 761 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(𝑞↑1) ∈
ℕ) |
21 | 20 | nnrpd 11746 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(𝑞↑1) ∈
ℝ+) |
22 | 16, 21 | rpdivcld 11765 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) ∈
ℝ+) |
23 | 22 | rpred 11748 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) ∈ ℝ) |
24 | 16 | rpred 11748 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ) |
25 | 7 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
𝐴 ∈
ℂ) |
26 | | znq 11668 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ) |
27 | 26 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(𝑝 / 𝑞) ∈ ℚ) |
28 | | qre 11669 |
. . . . . . . . . 10
⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ) |
29 | 27, 28 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(𝑝 / 𝑞) ∈ ℝ) |
30 | 29 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(𝑝 / 𝑞) ∈ ℂ) |
31 | 25, 30 | subcld 10271 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(𝐴 − (𝑝 / 𝑞)) ∈ ℂ) |
32 | 31 | abscld 14023 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(abs‘(𝐴 −
(𝑝 / 𝑞))) ∈ ℝ) |
33 | 20 | nnge1d 10940 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) → 1
≤ (𝑞↑1)) |
34 | | 1rp 11712 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ+ |
35 | | rpregt0 11722 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ+ → (1 ∈ ℝ ∧ 0 < 1)) |
36 | 34, 35 | mp1i 13 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(1 ∈ ℝ ∧ 0 < 1)) |
37 | 21 | rpregt0d 11754 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((𝑞↑1) ∈ ℝ
∧ 0 < (𝑞↑1))) |
38 | 16 | rpregt0d 11754 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ ∧ 0 <
((abs‘(ℑ‘𝐴)) / 2))) |
39 | | lediv2 10792 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ ((𝑞↑1) ∈ ℝ ∧ 0 < (𝑞↑1)) ∧
(((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ ∧ 0 <
((abs‘(ℑ‘𝐴)) / 2))) → (1 ≤ (𝑞↑1) ↔
(((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) ≤
(((abs‘(ℑ‘𝐴)) / 2) / 1))) |
40 | 36, 37, 38, 39 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(1 ≤ (𝑞↑1) ↔
(((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) ≤
(((abs‘(ℑ‘𝐴)) / 2) / 1))) |
41 | 33, 40 | mpbid 221 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) ≤
(((abs‘(ℑ‘𝐴)) / 2) / 1)) |
42 | 16 | rpcnd 11750 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((abs‘(ℑ‘𝐴)) / 2) ∈ ℂ) |
43 | 42 | div1d 10672 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(((abs‘(ℑ‘𝐴)) / 2) / 1) =
((abs‘(ℑ‘𝐴)) / 2)) |
44 | 41, 43 | breqtrd 4609 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) ≤
((abs‘(ℑ‘𝐴)) / 2)) |
45 | 14 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(abs‘(ℑ‘𝐴)) ∈
ℝ+) |
46 | 45 | rpred 11748 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(abs‘(ℑ‘𝐴)) ∈ ℝ) |
47 | | rphalflt 11736 |
. . . . . . . 8
⊢
((abs‘(ℑ‘𝐴)) ∈ ℝ+ →
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(ℑ‘𝐴))) |
48 | 45, 47 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(ℑ‘𝐴))) |
49 | 25, 30 | imsubd 13805 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(ℑ‘(𝐴 −
(𝑝 / 𝑞))) = ((ℑ‘𝐴) − (ℑ‘(𝑝 / 𝑞)))) |
50 | 29 | reim0d 13813 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(ℑ‘(𝑝 / 𝑞)) = 0) |
51 | 50 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((ℑ‘𝐴) −
(ℑ‘(𝑝 / 𝑞))) = ((ℑ‘𝐴) − 0)) |
52 | 9 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(ℑ‘𝐴) ∈
ℂ) |
53 | 52 | subid1d 10260 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((ℑ‘𝐴) −
0) = (ℑ‘𝐴)) |
54 | 49, 51, 53 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(ℑ‘(𝐴 −
(𝑝 / 𝑞))) = (ℑ‘𝐴)) |
55 | 54 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(abs‘(ℑ‘(𝐴 − (𝑝 / 𝑞)))) = (abs‘(ℑ‘𝐴))) |
56 | | absimle 13897 |
. . . . . . . . 9
⊢ ((𝐴 − (𝑝 / 𝑞)) ∈ ℂ →
(abs‘(ℑ‘(𝐴 − (𝑝 / 𝑞)))) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
57 | 31, 56 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(abs‘(ℑ‘(𝐴 − (𝑝 / 𝑞)))) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
58 | 55, 57 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(abs‘(ℑ‘𝐴)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
59 | 24, 46, 32, 48, 58 | ltletrd 10076 |
. . . . . 6
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
((abs‘(ℑ‘𝐴)) / 2) < (abs‘(𝐴 − (𝑝 / 𝑞)))) |
60 | 23, 24, 32, 44, 59 | lelttrd 10074 |
. . . . 5
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞)))) |
61 | 60 | olcd 407 |
. . . 4
⊢ (((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) ∧
(𝑝 ∈ ℤ ∧
𝑞 ∈ ℕ)) →
(𝐴 = (𝑝 / 𝑞) ∨ (((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
62 | 61 | ralrimivva 2954 |
. . 3
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
∀𝑝 ∈ ℤ
∀𝑞 ∈ ℕ
(𝐴 = (𝑝 / 𝑞) ∨ (((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
63 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 1 → (𝑞↑𝑘) = (𝑞↑1)) |
64 | 63 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑘 = 1 → (𝑥 / (𝑞↑𝑘)) = (𝑥 / (𝑞↑1))) |
65 | 64 | breq1d 4593 |
. . . . . 6
⊢ (𝑘 = 1 → ((𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))) ↔ (𝑥 / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
66 | 65 | orbi2d 734 |
. . . . 5
⊢ (𝑘 = 1 → ((𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞)))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
67 | 66 | 2ralbidv 2972 |
. . . 4
⊢ (𝑘 = 1 → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞)))) ↔ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
68 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → (𝑥 / (𝑞↑1)) = (((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1))) |
69 | 68 | breq1d 4593 |
. . . . . 6
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → ((𝑥 / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞))) ↔ (((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
70 | 69 | orbi2d 734 |
. . . . 5
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → ((𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞)))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ (((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
71 | 70 | 2ralbidv 2972 |
. . . 4
⊢ (𝑥 =
((abs‘(ℑ‘𝐴)) / 2) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞)))) ↔ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
72 | 67, 71 | rspc2ev 3295 |
. . 3
⊢ ((1
∈ ℕ ∧ ((abs‘(ℑ‘𝐴)) / 2) ∈ ℝ+ ∧
∀𝑝 ∈ ℤ
∀𝑞 ∈ ℕ
(𝐴 = (𝑝 / 𝑞) ∨ (((abs‘(ℑ‘𝐴)) / 2) / (𝑞↑1)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑘 ∈ ℕ ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
73 | 5, 15, 62, 72 | syl3anc 1318 |
. 2
⊢ ((𝐴 ∈ 𝔸 ∧ ¬
𝐴 ∈ ℝ) →
∃𝑘 ∈ ℕ
∃𝑥 ∈
ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |
74 | 3, 73 | pm2.61dan 828 |
1
⊢ (𝐴 ∈ 𝔸 →
∃𝑘 ∈ ℕ
∃𝑥 ∈
ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑘)) < (abs‘(𝐴 − (𝑝 / 𝑞))))) |