Step | Hyp | Ref
| Expression |
1 | | 1rp 11836 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
2 | | snssi 4339 |
. . . . . . 7
⊢ (1 ∈
ℝ+ → {1} ⊆ ℝ+) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ {1}
⊆ ℝ+ |
4 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆
ℝ+ |
5 | 3, 4 | unssi 3788 |
. . . . 5
⊢ ({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆
ℝ+ |
6 | | ltso 10118 |
. . . . . . 7
⊢ < Or
ℝ |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
8 | | snfi 8038 |
. . . . . . 7
⊢ {1}
∈ Fin |
9 | | aalioulem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
10 | | aalioulem2.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
11 | 10 | nnne0d 11065 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
12 | | aalioulem2.a |
. . . . . . . . . . . . . 14
⊢ 𝑁 = (deg‘𝐹) |
13 | 12 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢
(deg‘𝐹) =
𝑁 |
14 | | dgr0 24018 |
. . . . . . . . . . . . 13
⊢
(deg‘0𝑝) = 0 |
15 | 11, 13, 14 | 3netr4g 2873 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐹) ≠
(deg‘0𝑝)) |
16 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
17 | 16 | necon3i 2826 |
. . . . . . . . . . . 12
⊢
((deg‘𝐹) ≠
(deg‘0𝑝) → 𝐹 ≠
0𝑝) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
19 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ {0}) = (◡𝐹 “ {0}) |
20 | 19 | fta1 24063 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ 𝐹 ≠
0𝑝) → ((◡𝐹 “ {0}) ∈ Fin ∧
(#‘(◡𝐹 “ {0})) ≤ (deg‘𝐹))) |
21 | 9, 18, 20 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((◡𝐹 “ {0}) ∈ Fin ∧
(#‘(◡𝐹 “ {0})) ≤ (deg‘𝐹))) |
22 | 21 | simpld 475 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ {0}) ∈ Fin) |
23 | | abrexfi 8266 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
25 | | rabssab 3690 |
. . . . . . . 8
⊢ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} |
26 | | ssfi 8180 |
. . . . . . . 8
⊢ (({𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
27 | 24, 25, 26 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
28 | | unfi 8227 |
. . . . . . 7
⊢ (({1}
∈ Fin ∧ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin) |
29 | 8, 27, 28 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin) |
30 | | 1ex 10035 |
. . . . . . . . 9
⊢ 1 ∈
V |
31 | 30 | snid 4208 |
. . . . . . . 8
⊢ 1 ∈
{1} |
32 | | elun1 3780 |
. . . . . . . 8
⊢ (1 ∈
{1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
33 | | ne0i 3921 |
. . . . . . . 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 11843 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
37 | 5, 36 | sstri 3612 |
. . . . . . 7
⊢ ({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ |
38 | 37 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ) |
39 | | fiinfcl 8407 |
. . . . . 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 1328 |
. . . . 5
⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪
{𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
41 | 5, 40 | sseldi 3601 |
. . . 4
⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈
ℝ+) |
42 | 37 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ) |
43 | | 0re 10040 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
44 | | rpge0 11845 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℝ+
→ 0 ≤ 𝑑) |
45 | 44 | rgen 2922 |
. . . . . . . . . . . 12
⊢
∀𝑑 ∈
ℝ+ 0 ≤ 𝑑 |
46 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑)) |
47 | 46 | ralbidv 2986 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ+
𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑)) |
48 | 47 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+
𝑐 ≤ 𝑑) |
49 | 43, 45, 48 | mp2an 708 |
. . . . . . . . . . 11
⊢
∃𝑐 ∈
ℝ ∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 |
50 | | ssralv 3666 |
. . . . . . . . . . . . 13
⊢ (({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ+ →
(∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)) |
51 | 5, 50 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑) |
52 | 51 | reximi 3011 |
. . . . . . . . . . 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 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ) |
57 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ) |
58 | 56, 57 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ) |
59 | 58 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ) |
60 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ) |
61 | 60 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ) |
62 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ) |
63 | 62 | recnd 10068 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ) |
64 | 61, 63 | subeq0ad 10402 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟)) |
65 | 64 | necon3abid 2830 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟)) |
66 | 65 | biimprd 238 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0)) |
67 | 66 | impr 649 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0) |
68 | 59, 67 | absrpcld 14187 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈
ℝ+) |
69 | 57 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ) |
70 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0) |
71 | | plyf 23954 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹:ℂ⟶ℂ) |
72 | 9, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
73 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:ℂ⟶ℂ →
𝐹 Fn
ℂ) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn ℂ) |
75 | 74 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ) |
76 | | fniniseg 6338 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn ℂ → (𝑟 ∈ (◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0))) |
78 | 69, 70, 77 | mpbir2and 957 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (◡𝐹 “ {0})) |
79 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(abs‘(𝐴
− 𝑟)) =
(abs‘(𝐴 − 𝑟)) |
80 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟)) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟))) |
82 | 81 | eqeq2d 2632 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → ((abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟)))) |
83 | 82 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ (◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))) |
84 | 78, 79, 83 | sylancl 694 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))) |
85 | | eqeq1 2626 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
86 | 85 | rexbidv 3052 |
. . . . . . . . . . . 12
⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
87 | 86 | elrab 3363 |
. . . . . . . . . . 11
⊢
((abs‘(𝐴
− 𝑟)) ∈ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ↔ ((abs‘(𝐴 − 𝑟)) ∈ ℝ+ ∧
∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
88 | 68, 84, 87 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) |
89 | | elun2 3781 |
. . . . . . . . . 10
⊢
((abs‘(𝐴
− 𝑟)) ∈ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
90 | 88, 89 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
91 | | infrelb 11008 |
. . . . . . . . 9
⊢ ((({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 ∧ (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))) |
92 | 42, 54, 90, 91 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))) |
93 | 92 | expr 643 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
94 | 93 | orrd 393 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
95 | 94 | ex 450 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
96 | 95 | ralrimiva 2966 |
. . . 4
⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
97 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
98 | 97 | orbi2d 738 |
. . . . . . 7
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
99 | 98 | imbi2d 330 |
. . . . . 6
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))) |
100 | 99 | ralbidv 2986 |
. . . . 5
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))) |
101 | 100 | rspcev 3309 |
. . . 4
⊢
((inf(({1} ∪ {𝑎
∈ ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈
ℝ+ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))))) |
102 | 41, 96, 101 | syl2anc 693 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))))) |
103 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐹‘𝑟) = (𝐹‘(𝑝 / 𝑞))) |
104 | 103 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0)) |
105 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞))) |
106 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞))) |
107 | 106 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞)))) |
108 | 107 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
109 | 105, 108 | orbi12d 746 |
. . . . . . . 8
⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
110 | 104, 109 | imbi12d 334 |
. . . . . . 7
⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
111 | 110 | rspcv 3305 |
. . . . . 6
⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
112 | | znq 11792 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ) |
113 | | qre 11793 |
. . . . . . 7
⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ) |
114 | 112, 113 | syl 17 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ) |
115 | 111, 114 | syl11 33 |
. . . . 5
⊢
(∀𝑟 ∈
ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
116 | 115 | ralrimivv 2970 |
. . . 4
⊢
(∀𝑟 ∈
ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
117 | 116 | reximi 3011 |
. . 3
⊢
(∃𝑥 ∈
ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
118 | 102, 117 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
119 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈
ℝ+) |
120 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈
ℕ) |
121 | 10 | nnnn0d 11351 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
122 | 121 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
ℕ0) |
123 | 120, 122 | nnexpcld 13030 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ) |
124 | 123 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈
ℝ+) |
125 | 119, 124 | rpdivcld 11889 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈
ℝ+) |
126 | 125 | rpred 11872 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ) |
127 | 126 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ) |
128 | | simpllr 799 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ+) |
129 | 128 | rpred 11872 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ) |
130 | 55 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈
ℝ) |
131 | 114 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ) |
132 | 130, 131 | resubcld 10458 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ) |
133 | 132 | recnd 10068 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ) |
134 | 133 | abscld 14175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) →
(abs‘(𝐴 −
(𝑝 / 𝑞))) ∈ ℝ) |
135 | 134 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ) |
136 | | rpre 11839 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
137 | 136 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈
ℝ) |
138 | 119 | rpcnne0d 11881 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
139 | | divid 10714 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1) |
140 | 138, 139 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1) |
141 | 123 | nnge1d 11063 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤
(𝑞↑𝑁)) |
142 | 140, 141 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁)) |
143 | 137, 119,
124, 142 | lediv23d 11938 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥) |
144 | 143 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥) |
145 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
146 | 127, 129,
135, 144, 145 | letrd 10194 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
147 | 146 | ex 450 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
148 | 147 | orim2d 885 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
149 | 148 | imim2d 57 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) →
(((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
150 | 149 | ralimdvva 2964 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∀𝑝 ∈ ℤ
∀𝑞 ∈ ℕ
((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
151 | 150 | reximdva 3017 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
152 | 118, 151 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |