Metamath Proof Explorer

Theorem aaliou2b

Description: Liouville's approximation theorem extended to complex A . (Contributed by Stefan O'Rear, 20-Nov-2014)

Ref Expression
Assertion aaliou2b ( 𝐴 ∈ 𝔸 → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝐴 ∈ ( 𝔸 ∩ ℝ ) ↔ ( 𝐴 ∈ 𝔸 ∧ 𝐴 ∈ ℝ ) )
2 aaliou2 ⊢ ( 𝐴 ∈ ( 𝔸 ∩ ℝ ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
3 1 2 sylbir ⊢ ( ( 𝐴 ∈ 𝔸 ∧ 𝐴 ∈ ℝ ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
4 1nn ⊢ 1 ∈ ℕ
5 aacn ⊢ ( 𝐴 ∈ 𝔸 → 𝐴 ∈ ℂ )
6 5 adantr ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℂ )
7 6 imcld ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
9 reim0b ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
10 5 9 syl ⊢ ( 𝐴 ∈ 𝔸 → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
11 10 necon3bbid ⊢ ( 𝐴 ∈ 𝔸 → ( ¬ 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) ≠ 0 ) )
12 11 biimpa ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
13 8 12 absrpcld ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )
14 13 rphalfcld ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ+ )
15 14 adantr ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ+ )
16 1nn0 ⊢ 1 ∈ ℕ0
17 nnexpcl ⊢ ( ( 𝑞 ∈ ℕ ∧ 1 ∈ ℕ0 ) → ( 𝑞 ↑ 1 ) ∈ ℕ )
18 16 17 mpan2 ⊢ ( 𝑞 ∈ ℕ → ( 𝑞 ↑ 1 ) ∈ ℕ )
19 18 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 1 ) ∈ ℕ )
20 19 nnrpd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 1 ) ∈ ℝ+ )
21 15 20 rpdivcld ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) ∈ ℝ+ )
22 21 rpred ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) ∈ ℝ )
23 15 rpred ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ )
24 6 adantr ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝐴 ∈ ℂ )
25 znq ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℚ )
26 25 adantl ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℚ )
27 qre ⊢ ( ( 𝑝 / 𝑞 ) ∈ ℚ → ( 𝑝 / 𝑞 ) ∈ ℝ )
28 26 27 syl ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
29 28 recnd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℂ )
30 24 29 subcld ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℂ )
31 30 abscld ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ )
32 19 nnge1d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 1 ≤ ( 𝑞 ↑ 1 ) )
33 1rp ⊢ 1 ∈ ℝ+
34 rpregt0 ⊢ ( 1 ∈ ℝ+ → ( 1 ∈ ℝ ∧ 0 < 1 ) )
35 33 34 mp1i ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 1 ∈ ℝ ∧ 0 < 1 ) )
36 20 rpregt0d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑞 ↑ 1 ) ∈ ℝ ∧ 0 < ( 𝑞 ↑ 1 ) ) )
37 15 rpregt0d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ ∧ 0 < ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ) )
38 lediv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( 𝑞 ↑ 1 ) ∈ ℝ ∧ 0 < ( 𝑞 ↑ 1 ) ) ∧ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ ∧ 0 < ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ) ) → ( 1 ≤ ( 𝑞 ↑ 1 ) ↔ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) ≤ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / 1 ) ) )
39 35 36 37 38 syl3anc ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 1 ≤ ( 𝑞 ↑ 1 ) ↔ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) ≤ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / 1 ) ) )
40 32 39 mpbid ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) ≤ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / 1 ) )
41 15 rpcnd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℂ )
42 41 div1d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / 1 ) = ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) )
43 40 42 breqtrd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) ≤ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) )
44 13 adantr ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )
45 44 rpred ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ )
46 rphalflt ⊢ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
47 44 46 syl ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
48 24 29 imsubd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ℑ ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) = ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ ( 𝑝 / 𝑞 ) ) ) )
49 28 reim0d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ℑ ‘ ( 𝑝 / 𝑞 ) ) = 0 )
50 49 oveq2d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ ( 𝑝 / 𝑞 ) ) ) = ( ( ℑ ‘ 𝐴 ) − 0 ) )
51 8 adantr ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
52 51 subid1d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ℑ ‘ 𝐴 ) − 0 ) = ( ℑ ‘ 𝐴 ) )
53 48 50 52 3eqtrd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ℑ ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) = ( ℑ ‘ 𝐴 ) )
54 53 fveq2d ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( ℑ ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) = ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
55 absimle ⊢ ( ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
56 30 55 syl ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( ℑ ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
57 54 56 eqbrtrrd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
58 23 45 31 47 57 ltletrd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
59 22 23 31 43 58 lelttrd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
60 59 olcd ⊢ ( ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
61 60 ralrimivva ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
62 oveq2 ⊢ ( 𝑘 = 1 → ( 𝑞 ↑ 𝑘 ) = ( 𝑞 ↑ 1 ) )
63 62 oveq2d ⊢ ( 𝑘 = 1 → ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) = ( 𝑥 / ( 𝑞 ↑ 1 ) ) )
64 63 breq1d ⊢ ( 𝑘 = 1 → ( ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ↔ ( 𝑥 / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
65 64 orbi2d ⊢ ( 𝑘 = 1 → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
66 65 2ralbidv ⊢ ( 𝑘 = 1 → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
67 oveq1 ⊢ ( 𝑥 = ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) → ( 𝑥 / ( 𝑞 ↑ 1 ) ) = ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) )
68 67 breq1d ⊢ ( 𝑥 = ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) → ( ( 𝑥 / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ↔ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
69 68 orbi2d ⊢ ( 𝑥 = ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
70 69 2ralbidv ⊢ ( 𝑥 = ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
71 66 70 rspc2ev ⊢ ( ( 1 ∈ ℕ ∧ ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) ∈ ℝ+ ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( ( ( abs ‘ ( ℑ ‘ 𝐴 ) ) / 2 ) / ( 𝑞 ↑ 1 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
72 4 14 61 71 mp3an2i ⊢ ( ( 𝐴 ∈ 𝔸 ∧ ¬ 𝐴 ∈ ℝ ) → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
73 3 72 pm2.61dan ⊢ ( 𝐴 ∈ 𝔸 → ∃ 𝑘 ∈ ℕ ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑘 ) ) < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )