| Step | Hyp | Ref
| Expression |
| 1 | | 1rp 13038 |
. . . . . . 7
⊢ 1 ∈
ℝ+ |
| 2 | | snssi 4808 |
. . . . . . 7
⊢ (1 ∈
ℝ+ → {1} ⊆ ℝ+) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ {1}
⊆ ℝ+ |
| 4 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆
ℝ+ |
| 5 | 3, 4 | unssi 4191 |
. . . . 5
⊢ ({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆
ℝ+ |
| 6 | | ltso 11341 |
. . . . . . 7
⊢ < Or
ℝ |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
| 8 | | snfi 9083 |
. . . . . . 7
⊢ {1}
∈ Fin |
| 9 | | aalioulem2.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈
(Poly‘ℤ)) |
| 10 | | aalioulem2.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 11 | 10 | nnne0d 12316 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≠ 0) |
| 12 | | aalioulem2.a |
. . . . . . . . . . . . . 14
⊢ 𝑁 = (deg‘𝐹) |
| 13 | 12 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢
(deg‘𝐹) =
𝑁 |
| 14 | | dgr0 26302 |
. . . . . . . . . . . . 13
⊢
(deg‘0𝑝) = 0 |
| 15 | 11, 13, 14 | 3netr4g 3020 |
. . . . . . . . . . . 12
⊢ (𝜑 → (deg‘𝐹) ≠
(deg‘0𝑝)) |
| 16 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝐹 = 0𝑝 →
(deg‘𝐹) =
(deg‘0𝑝)) |
| 17 | 16 | necon3i 2973 |
. . . . . . . . . . . 12
⊢
((deg‘𝐹) ≠
(deg‘0𝑝) → 𝐹 ≠
0𝑝) |
| 18 | 15, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ≠
0𝑝) |
| 19 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (◡𝐹 “ {0}) = (◡𝐹 “ {0}) |
| 20 | 19 | fta1 26350 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (Poly‘ℤ)
∧ 𝐹 ≠
0𝑝) → ((◡𝐹 “ {0}) ∈ Fin ∧
(♯‘(◡𝐹 “ {0})) ≤ (deg‘𝐹))) |
| 21 | 9, 18, 20 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((◡𝐹 “ {0}) ∈ Fin ∧
(♯‘(◡𝐹 “ {0})) ≤ (deg‘𝐹))) |
| 22 | 21 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → (◡𝐹 “ {0}) ∈ Fin) |
| 23 | | abrexfi 9392 |
. . . . . . . . 9
⊢ ((◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
| 24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
| 25 | | rabssab 4085 |
. . . . . . . 8
⊢ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} |
| 26 | | ssfi 9213 |
. . . . . . . 8
⊢ (({𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
| 27 | 24, 25, 26 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 → {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) |
| 28 | | unfi 9211 |
. . . . . . 7
⊢ (({1}
∈ Fin ∧ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin) |
| 29 | 8, 27, 28 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin) |
| 30 | | 1ex 11257 |
. . . . . . . . 9
⊢ 1 ∈
V |
| 31 | 30 | snid 4662 |
. . . . . . . 8
⊢ 1 ∈
{1} |
| 32 | | elun1 4182 |
. . . . . . . 8
⊢ (1 ∈
{1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
| 33 | | ne0i 4341 |
. . . . . . . 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 13042 |
. . . . . . . 8
⊢
ℝ+ ⊆ ℝ |
| 37 | 5, 36 | sstri 3993 |
. . . . . . 7
⊢ ({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ |
| 38 | 37 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ) |
| 39 | | fiinfcl 9541 |
. . . . . 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 1374 |
. . . . 5
⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪
{𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
| 41 | 5, 40 | sselid 3981 |
. . . 4
⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈
ℝ+) |
| 42 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 43 | | rpge0 13048 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ℝ+
→ 0 ≤ 𝑑) |
| 44 | 43 | rgen 3063 |
. . . . . . . . . . 11
⊢
∀𝑑 ∈
ℝ+ 0 ≤ 𝑑 |
| 45 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑)) |
| 46 | 45 | ralbidv 3178 |
. . . . . . . . . . . 12
⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ+
𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑)) |
| 47 | 46 | rspcev 3622 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+
𝑐 ≤ 𝑑) |
| 48 | 42, 44, 47 | mp2an 692 |
. . . . . . . . . 10
⊢
∃𝑐 ∈
ℝ ∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 |
| 49 | | ssralv 4052 |
. . . . . . . . . . . 12
⊢ (({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ+ →
(∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)) |
| 50 | 5, 49 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑) |
| 51 | 50 | reximi 3084 |
. . . . . . . . . 10
⊢
(∃𝑐 ∈
ℝ ∀𝑑 ∈
ℝ+ 𝑐 ≤
𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑) |
| 52 | 48, 51 | ax-mp 5 |
. . . . . . . . 9
⊢
∃𝑐 ∈
ℝ ∀𝑑 ∈
({1} ∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 |
| 53 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
| 54 | 53 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))) |
| 55 | | aalioulem2.d |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 56 | 55 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ) |
| 57 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ) |
| 58 | 56, 57 | resubcld 11691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ) |
| 59 | 58 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ) |
| 60 | 55 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ) |
| 61 | 60 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ) |
| 62 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ) |
| 63 | 62 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ) |
| 64 | 61, 63 | subeq0ad 11630 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟)) |
| 65 | 64 | necon3abid 2977 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟)) |
| 66 | 65 | biimprd 248 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0)) |
| 67 | 66 | impr 454 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0) |
| 68 | 59, 67 | absrpcld 15487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈
ℝ+) |
| 69 | 57 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ) |
| 70 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0) |
| 71 | | plyf 26237 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 ∈ (Poly‘ℤ)
→ 𝐹:ℂ⟶ℂ) |
| 72 | 9, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐹:ℂ⟶ℂ) |
| 73 | 72 | ffnd 6737 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn ℂ) |
| 74 | 73 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ) |
| 75 | | fniniseg 7080 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn ℂ → (𝑟 ∈ (◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0))) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0))) |
| 77 | 69, 70, 76 | mpbir2and 713 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (◡𝐹 “ {0})) |
| 78 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(abs‘(𝐴
− 𝑟)) =
(abs‘(𝐴 − 𝑟)) |
| 79 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟)) |
| 80 | 79 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟))) |
| 81 | 80 | rspceeqv 3645 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ (◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))) |
| 82 | 77, 78, 81 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))) |
| 83 | 54, 68, 82 | elrabd 3694 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) |
| 84 | | elun2 4183 |
. . . . . . . . . 10
⊢
((abs‘(𝐴
− 𝑟)) ∈ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
| 85 | 83, 84 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) |
| 86 | | infrelb 12253 |
. . . . . . . . 9
⊢ ((({1}
∪ {𝑎 ∈
ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 ∧ (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))) |
| 87 | 37, 52, 85, 86 | mp3an12i 1467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))) |
| 88 | 87 | expr 456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
| 89 | 88 | orrd 864 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
| 90 | 89 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
| 91 | 90 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
| 92 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))) |
| 93 | 92 | orbi2d 916 |
. . . . . . 7
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) |
| 94 | 93 | imbi2d 340 |
. . . . . 6
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))) |
| 95 | 94 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+
∣ ∃𝑏 ∈
(◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))) |
| 96 | 95 | rspcev 3622 |
. . . 4
⊢
((inf(({1} ∪ {𝑎
∈ ℝ+ ∣ ∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈
ℝ+ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣
∃𝑏 ∈ (◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))))) |
| 97 | 41, 91, 96 | syl2anc 584 |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))))) |
| 98 | | fveqeq2 6915 |
. . . . . . . 8
⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0)) |
| 99 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞))) |
| 100 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞))) |
| 101 | 100 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞)))) |
| 102 | 101 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| 103 | 99, 102 | orbi12d 919 |
. . . . . . . 8
⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 104 | 98, 103 | imbi12d 344 |
. . . . . . 7
⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
| 105 | 104 | rspcv 3618 |
. . . . . 6
⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
| 106 | | znq 12994 |
. . . . . . 7
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ) |
| 107 | | qre 12995 |
. . . . . . 7
⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ) |
| 108 | 106, 107 | syl 17 |
. . . . . 6
⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ) |
| 109 | 105, 108 | syl11 33 |
. . . . 5
⊢
(∀𝑟 ∈
ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
| 110 | 109 | ralrimivv 3200 |
. . . 4
⊢
(∀𝑟 ∈
ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 111 | 110 | reximi 3084 |
. . 3
⊢
(∃𝑥 ∈
ℝ+ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 112 | 97, 111 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 113 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈
ℝ+) |
| 114 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈
ℕ) |
| 115 | 10 | nnnn0d 12587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 116 | 115 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈
ℕ0) |
| 117 | 114, 116 | nnexpcld 14284 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ) |
| 118 | 117 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈
ℝ+) |
| 119 | 113, 118 | rpdivcld 13094 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈
ℝ+) |
| 120 | 119 | rpred 13077 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ) |
| 121 | 120 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ) |
| 122 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ+) |
| 123 | 122 | rpred 13077 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ) |
| 124 | 55 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈
ℝ) |
| 125 | 108 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ) |
| 126 | 124, 125 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ) |
| 127 | 126 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ) |
| 128 | 127 | abscld 15475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) →
(abs‘(𝐴 −
(𝑝 / 𝑞))) ∈ ℝ) |
| 129 | 128 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ) |
| 130 | | rpre 13043 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 131 | 130 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈
ℝ) |
| 132 | 113 | rpcnne0d 13086 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
| 133 | | divid 11953 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1) |
| 134 | 132, 133 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1) |
| 135 | 117 | nnge1d 12314 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤
(𝑞↑𝑁)) |
| 136 | 134, 135 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁)) |
| 137 | 131, 113,
118, 136 | lediv23d 13145 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥) |
| 138 | 137 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥) |
| 139 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
| 140 | 121, 123,
129, 138, 139 | letrd 11418 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) |
| 141 | 140 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) |
| 142 | 141 | orim2d 969 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |
| 143 | 142 | imim2d 57 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) →
(((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
| 144 | 143 | ralimdvva 3206 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∀𝑝 ∈ ℤ
∀𝑞 ∈ ℕ
((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
| 145 | 144 | reximdva 3168 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))) |
| 146 | 112, 145 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ+ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))) |