Step | Hyp | Ref
| Expression |
1 | | 1rp 11712 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
2 | | snssi 4280 |
. . . . . . 7
⊢ (1 ∈
ℝ+ → {1} ⊆ ℝ+) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ {1}
⊆ ℝ+ |
4 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆
ℝ+ |
5 | 3, 4 | unssi 3750 |
. . . . 5
⊢ ({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆
ℝ+ |
6 | | ltso 9997 |
. . . . . . 7
⊢ < Or
ℝ |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
8 | | snfi 7923 |
. . . . . . 7
⊢ {1}
∈ Fin |
9 | | aalioulem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
10 | | aalioulem2.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
11 | 10 | nnne0d 10942 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
12 | | aalioulem2.a |
. . . . . . . . . . . . . 14
⊢ 𝑁 = (deg‘𝐹) |
13 | 12 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢
(deg‘𝐹) =
𝑁 |
14 | | dgr0 23822 |
. . . . . . . . . . . . 13
⊢
(deg‘0𝑝) = 0 |
15 | 11, 13, 14 | 3netr4g 2861 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐹) ≠
(deg‘0𝑝)) |
16 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
17 | 16 | necon3i 2814 |
. . . . . . . . . . . 12
⊢
((deg‘𝐹) ≠
(deg‘0𝑝) → 𝐹 ≠
0𝑝) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
19 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ {0}) = (◡𝐹 “ {0}) |
20 | 19 | fta1 23867 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ 𝐹 ≠
0𝑝) → ((◡𝐹 “ {0}) ∈ Fin ∧
(#‘(◡𝐹 “ {0})) ≤ (deg‘𝐹))) |
21 | 9, 18, 20 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((◡𝐹 “ {0}) ∈ Fin ∧
(#‘(◡𝐹 “ {0})) ≤ (deg‘𝐹))) |
22 | 21 | simpld 474 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ {0}) ∈ Fin) |
23 | | abrexfi 8149 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
25 | | rabssab 3652 |
. . . . . . . 8
⊢ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} |
26 | | ssfi 8065 |
. . . . . . . 8
⊢ (({𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
27 | 24, 25, 26 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
28 | | unfi 8112 |
. . . . . . 7
⊢ (({1}
∈ Fin ∧ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin) |
29 | 8, 27, 28 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin) |
30 | | 1ex 9914 |
. . . . . . . . 9
⊢ 1 ∈
V |
31 | 30 | snid 4155 |
. . . . . . . 8
⊢ 1 ∈
{1} |
32 | | elun1 3742 |
. . . . . . . 8
⊢ (1 ∈
{1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
33 | | ne0i 3880 |
. . . . . . . 8
⊢ (1 ∈
({1} ∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅) |
34 | 31, 32, 33 | mp2b 10 |
. . . . . . 7
⊢ ({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅ |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅) |
36 | | rpssre 11719 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
37 | 5, 36 | sstri 3577 |
. . . . . . 7
⊢ ({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ |
38 | 37 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ) |
39 | | fiinfcl 8290 |
. . . . . 6
⊢ (( <
Or ℝ ∧ (({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin ∧ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅ ∧ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ)) → inf(({1} ∪
{𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪
{𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
40 | 7, 29, 35, 38, 39 | syl13anc 1320 |
. . . . 5
⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪
{𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
41 | 5, 40 | sseldi 3566 |
. . . 4
⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈
ℝ+) |
42 | 37 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ) |
43 | | 0re 9919 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
44 | | rpge0 11721 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℝ+
→ 0 ≤ 𝑑) |
45 | 44 | rgen 2906 |
. . . . . . . . . . . 12
⊢
∀𝑑 ∈
ℝ+ 0 ≤ 𝑑 |
46 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑)) |
47 | 46 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ+
𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑)) |
48 | 47 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+
𝑐 ≤ 𝑑) |
49 | 43, 45, 48 | mp2an 704 |
. . . . . . . . . . 11
⊢
∃𝑐 ∈
ℝ ∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 |
50 | | ssralv 3629 |
. . . . . . . . . . . . 13
⊢ (({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ+ →
(∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)) |
51 | 5, 50 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑) |
52 | 51 | reximi 2994 |
. . . . . . . . . . 11
⊢
(∃𝑐 ∈
ℝ ∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑) |
53 | 49, 52 | ax-mp 5 |
. . . . . . . . . 10
⊢
∃𝑐 ∈
ℝ ∀𝑑 ∈
({1} ∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 |
54 | 53 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑) |
55 | | aalioulem2.d |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
56 | 55 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ) |
57 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ) |
58 | 56, 57 | resubcld 10337 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ) |
59 | 58 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ) |
60 | 55 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ) |
61 | 60 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ) |
62 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ) |
63 | 62 | recnd 9947 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ) |
64 | 61, 63 | subeq0ad 10281 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟)) |
65 | 64 | necon3abid 2818 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟)) |
66 | 65 | biimprd 237 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0)) |
67 | 66 | impr 647 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0) |
68 | 59, 67 | absrpcld 14035 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈
ℝ+) |
69 | 57 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ) |
70 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0) |
71 | | plyf 23758 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹:ℂ⟶ℂ) |
72 | 9, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
73 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn ℂ) |
75 | 74 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ) |
76 | | fniniseg 6246 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn ℂ → (𝑟 ∈ (◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0))) |
78 | 69, 70, 77 | mpbir2and 959 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (◡𝐹 “ {0})) |
79 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(abs‘(𝐴
− 𝑟)) =
(abs‘(𝐴 − 𝑟)) |
80 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟)) |
81 | 80 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟))) |
82 | 81 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → ((abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟)))) |
83 | 82 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ (◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))) |
84 | 78, 79, 83 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))) |
85 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
86 | 85 | rexbidv 3034 |
. . . . . . . . . . . 12
⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
87 | 86 | elrab 3331 |
. . . . . . . . . . 11
⊢
((abs‘(𝐴
− 𝑟)) ∈ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ↔ ((abs‘(𝐴 − 𝑟)) ∈ ℝ+ ∧
∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
88 | 68, 84, 87 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) |
89 | | elun2 3743 |
. . . . . . . . . 10
⊢
((abs‘(𝐴
− 𝑟)) ∈ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
90 | 88, 89 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
91 | | infrelb 10885 |
. . . . . . . . 9
⊢ ((({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 ∧ (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))) |
92 | 42, 54, 90, 91 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))) |
93 | 92 | expr 641 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
94 | 93 | orrd 392 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
95 | 94 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
96 | 95 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
97 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
98 | 97 | orbi2d 734 |
. . . . . . 7
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
99 | 98 | imbi2d 329 |
. . . . . 6
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))) |
100 | 99 | ralbidv 2969 |
. . . . 5
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))) |
101 | 100 | rspcev 3282 |
. . . 4
⊢
((inf(({1} ∪ {𝑎
∈ ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈
ℝ+ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))))) |
102 | 41, 96, 101 | syl2anc 691 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))))) |
103 | | znq 11668 |
. . . . . . . 8
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ) |
104 | | qre 11669 |
. . . . . . . 8
⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ) |
105 | 103, 104 | syl 17 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ) |
106 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐹‘𝑟) = (𝐹‘(𝑝 / 𝑞))) |
107 | 106 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0)) |
108 | | eqeq2 2621 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞))) |
109 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞))) |
110 | 109 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞)))) |
111 | 110 | breq2d 4595 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
112 | 108, 111 | orbi12d 742 |
. . . . . . . . 9
⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
113 | 107, 112 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
114 | 113 | rspcv 3278 |
. . . . . . 7
⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
115 | 105, 114 | syl 17 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) →
(∀𝑟 ∈ ℝ
((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
116 | 115 | com12 32 |
. . . . 5
⊢
(∀𝑟 ∈
ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
117 | 116 | ralrimivv 2953 |
. . . 4
⊢
(∀𝑟 ∈
ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
118 | 117 | reximi 2994 |
. . 3
⊢
(∃𝑥 ∈
ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
119 | 102, 118 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
120 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈
ℝ+) |
121 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈
ℕ) |
122 | 10 | nnnn0d 11228 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
123 | 122 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
ℕ0) |
124 | 121, 123 | nnexpcld 12892 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ) |
125 | 124 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈
ℝ+) |
126 | 120, 125 | rpdivcld 11765 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈
ℝ+) |
127 | 126 | rpred 11748 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ) |
128 | 127 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ) |
129 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ+) |
130 | 129 | rpred 11748 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ) |
131 | 55 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈
ℝ) |
132 | 105 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ) |
133 | 131, 132 | resubcld 10337 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ) |
134 | 133 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ) |
135 | 134 | abscld 14023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) →
(abs‘(𝐴 −
(𝑝 / 𝑞))) ∈ ℝ) |
136 | 135 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ) |
137 | | rpre 11715 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
138 | 137 | ad2antlr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈
ℝ) |
139 | 120 | rpcnne0d 11757 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
140 | | divid 10593 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1) |
142 | 124 | nnge1d 10940 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤
(𝑞↑𝑁)) |
143 | 141, 142 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁)) |
144 | 138, 120,
125, 143 | lediv23d 11814 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥) |
145 | 144 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥) |
146 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
147 | 128, 130,
136, 145, 146 | letrd 10073 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
148 | 147 | ex 449 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
149 | 148 | orim2d 881 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
150 | 149 | imim2d 55 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) →
(((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
151 | 150 | ralimdvva 2947 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∀𝑝 ∈ ℤ
∀𝑞 ∈ ℕ
((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
152 | 151 | reximdva 3000 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
153 | 119, 152 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |