Step |
Hyp |
Ref |
Expression |
1 |
|
aalioulem2.a |
⊢ 𝑁 = ( deg ‘ 𝐹 ) |
2 |
|
aalioulem2.b |
⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) ) |
3 |
|
aalioulem2.c |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
4 |
|
aalioulem2.d |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
5 |
|
1rp |
⊢ 1 ∈ ℝ+ |
6 |
|
snssi |
⊢ ( 1 ∈ ℝ+ → { 1 } ⊆ ℝ+ ) |
7 |
5 6
|
ax-mp |
⊢ { 1 } ⊆ ℝ+ |
8 |
|
ssrab2 |
⊢ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ⊆ ℝ+ |
9 |
7 8
|
unssi |
⊢ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ⊆ ℝ+ |
10 |
|
ltso |
⊢ < Or ℝ |
11 |
10
|
a1i |
⊢ ( 𝜑 → < Or ℝ ) |
12 |
|
snfi |
⊢ { 1 } ∈ Fin |
13 |
3
|
nnne0d |
⊢ ( 𝜑 → 𝑁 ≠ 0 ) |
14 |
1
|
eqcomi |
⊢ ( deg ‘ 𝐹 ) = 𝑁 |
15 |
|
dgr0 |
⊢ ( deg ‘ 0𝑝 ) = 0 |
16 |
13 14 15
|
3netr4g |
⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≠ ( deg ‘ 0𝑝 ) ) |
17 |
|
fveq2 |
⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) ) |
18 |
17
|
necon3i |
⊢ ( ( deg ‘ 𝐹 ) ≠ ( deg ‘ 0𝑝 ) → 𝐹 ≠ 0𝑝 ) |
19 |
16 18
|
syl |
⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 ) |
20 |
|
eqid |
⊢ ( ◡ 𝐹 “ { 0 } ) = ( ◡ 𝐹 “ { 0 } ) |
21 |
20
|
fta1 |
⊢ ( ( 𝐹 ∈ ( Poly ‘ ℤ ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( ◡ 𝐹 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝐹 “ { 0 } ) ) ≤ ( deg ‘ 𝐹 ) ) ) |
22 |
2 19 21
|
syl2anc |
⊢ ( 𝜑 → ( ( ◡ 𝐹 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝐹 “ { 0 } ) ) ≤ ( deg ‘ 𝐹 ) ) ) |
23 |
22
|
simpld |
⊢ ( 𝜑 → ( ◡ 𝐹 “ { 0 } ) ∈ Fin ) |
24 |
|
abrexfi |
⊢ ( ( ◡ 𝐹 “ { 0 } ) ∈ Fin → { 𝑎 ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ∈ Fin ) |
25 |
23 24
|
syl |
⊢ ( 𝜑 → { 𝑎 ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ∈ Fin ) |
26 |
|
rabssab |
⊢ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ⊆ { 𝑎 ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } |
27 |
|
ssfi |
⊢ ( ( { 𝑎 ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ∈ Fin ∧ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ⊆ { 𝑎 ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) → { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ∈ Fin ) |
28 |
25 26 27
|
sylancl |
⊢ ( 𝜑 → { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ∈ Fin ) |
29 |
|
unfi |
⊢ ( ( { 1 } ∈ Fin ∧ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ∈ Fin ) → ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ∈ Fin ) |
30 |
12 28 29
|
sylancr |
⊢ ( 𝜑 → ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ∈ Fin ) |
31 |
|
1ex |
⊢ 1 ∈ V |
32 |
31
|
snid |
⊢ 1 ∈ { 1 } |
33 |
|
elun1 |
⊢ ( 1 ∈ { 1 } → 1 ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ) |
34 |
|
ne0i |
⊢ ( 1 ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) → ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ≠ ∅ ) |
35 |
32 33 34
|
mp2b |
⊢ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ≠ ∅ |
36 |
35
|
a1i |
⊢ ( 𝜑 → ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ≠ ∅ ) |
37 |
|
rpssre |
⊢ ℝ+ ⊆ ℝ |
38 |
9 37
|
sstri |
⊢ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ⊆ ℝ |
39 |
38
|
a1i |
⊢ ( 𝜑 → ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ⊆ ℝ ) |
40 |
|
fiinfcl |
⊢ ( ( < Or ℝ ∧ ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ∈ Fin ∧ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ≠ ∅ ∧ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ⊆ ℝ ) ) → inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ) |
41 |
11 30 36 39 40
|
syl13anc |
⊢ ( 𝜑 → inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ) |
42 |
9 41
|
sseldi |
⊢ ( 𝜑 → inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ∈ ℝ+ ) |
43 |
|
0re |
⊢ 0 ∈ ℝ |
44 |
|
rpge0 |
⊢ ( 𝑑 ∈ ℝ+ → 0 ≤ 𝑑 ) |
45 |
44
|
rgen |
⊢ ∀ 𝑑 ∈ ℝ+ 0 ≤ 𝑑 |
46 |
|
breq1 |
⊢ ( 𝑐 = 0 → ( 𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑 ) ) |
47 |
46
|
ralbidv |
⊢ ( 𝑐 = 0 → ( ∀ 𝑑 ∈ ℝ+ 𝑐 ≤ 𝑑 ↔ ∀ 𝑑 ∈ ℝ+ 0 ≤ 𝑑 ) ) |
48 |
47
|
rspcev |
⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑑 ∈ ℝ+ 0 ≤ 𝑑 ) → ∃ 𝑐 ∈ ℝ ∀ 𝑑 ∈ ℝ+ 𝑐 ≤ 𝑑 ) |
49 |
43 45 48
|
mp2an |
⊢ ∃ 𝑐 ∈ ℝ ∀ 𝑑 ∈ ℝ+ 𝑐 ≤ 𝑑 |
50 |
|
ssralv |
⊢ ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ⊆ ℝ+ → ( ∀ 𝑑 ∈ ℝ+ 𝑐 ≤ 𝑑 → ∀ 𝑑 ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) 𝑐 ≤ 𝑑 ) ) |
51 |
9 50
|
ax-mp |
⊢ ( ∀ 𝑑 ∈ ℝ+ 𝑐 ≤ 𝑑 → ∀ 𝑑 ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) 𝑐 ≤ 𝑑 ) |
52 |
51
|
reximi |
⊢ ( ∃ 𝑐 ∈ ℝ ∀ 𝑑 ∈ ℝ+ 𝑐 ≤ 𝑑 → ∃ 𝑐 ∈ ℝ ∀ 𝑑 ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) 𝑐 ≤ 𝑑 ) |
53 |
49 52
|
ax-mp |
⊢ ∃ 𝑐 ∈ ℝ ∀ 𝑑 ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) 𝑐 ≤ 𝑑 |
54 |
|
eqeq1 |
⊢ ( 𝑎 = ( abs ‘ ( 𝐴 − 𝑟 ) ) → ( 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) ↔ ( abs ‘ ( 𝐴 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑏 ) ) ) ) |
55 |
54
|
rexbidv |
⊢ ( 𝑎 = ( abs ‘ ( 𝐴 − 𝑟 ) ) → ( ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) ↔ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) ( abs ‘ ( 𝐴 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑏 ) ) ) ) |
56 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → 𝐴 ∈ ℝ ) |
57 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → 𝑟 ∈ ℝ ) |
58 |
56 57
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( 𝐴 − 𝑟 ) ∈ ℝ ) |
59 |
58
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( 𝐴 − 𝑟 ) ∈ ℂ ) |
60 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → 𝐴 ∈ ℝ ) |
61 |
60
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → 𝐴 ∈ ℂ ) |
62 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → 𝑟 ∈ ℝ ) |
63 |
62
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → 𝑟 ∈ ℂ ) |
64 |
61 63
|
subeq0ad |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → ( ( 𝐴 − 𝑟 ) = 0 ↔ 𝐴 = 𝑟 ) ) |
65 |
64
|
necon3abid |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → ( ( 𝐴 − 𝑟 ) ≠ 0 ↔ ¬ 𝐴 = 𝑟 ) ) |
66 |
65
|
biimprd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → ( ¬ 𝐴 = 𝑟 → ( 𝐴 − 𝑟 ) ≠ 0 ) ) |
67 |
66
|
impr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( 𝐴 − 𝑟 ) ≠ 0 ) |
68 |
59 67
|
absrpcld |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ℝ+ ) |
69 |
57
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → 𝑟 ∈ ℂ ) |
70 |
|
simprl |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( 𝐹 ‘ 𝑟 ) = 0 ) |
71 |
|
plyf |
⊢ ( 𝐹 ∈ ( Poly ‘ ℤ ) → 𝐹 : ℂ ⟶ ℂ ) |
72 |
2 71
|
syl |
⊢ ( 𝜑 → 𝐹 : ℂ ⟶ ℂ ) |
73 |
72
|
ffnd |
⊢ ( 𝜑 → 𝐹 Fn ℂ ) |
74 |
73
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → 𝐹 Fn ℂ ) |
75 |
|
fniniseg |
⊢ ( 𝐹 Fn ℂ → ( 𝑟 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑟 ∈ ℂ ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) ) ) |
76 |
74 75
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( 𝑟 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑟 ∈ ℂ ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) ) ) |
77 |
69 70 76
|
mpbir2and |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → 𝑟 ∈ ( ◡ 𝐹 “ { 0 } ) ) |
78 |
|
eqid |
⊢ ( abs ‘ ( 𝐴 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) |
79 |
|
oveq2 |
⊢ ( 𝑏 = 𝑟 → ( 𝐴 − 𝑏 ) = ( 𝐴 − 𝑟 ) ) |
80 |
79
|
fveq2d |
⊢ ( 𝑏 = 𝑟 → ( abs ‘ ( 𝐴 − 𝑏 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
81 |
80
|
rspceeqv |
⊢ ( ( 𝑟 ∈ ( ◡ 𝐹 “ { 0 } ) ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑟 ) ) ) → ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) ( abs ‘ ( 𝐴 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑏 ) ) ) |
82 |
77 78 81
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) ( abs ‘ ( 𝐴 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − 𝑏 ) ) ) |
83 |
55 68 82
|
elrabd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) |
84 |
|
elun2 |
⊢ ( ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ) |
85 |
83 84
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ) |
86 |
|
infrelb |
⊢ ( ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ⊆ ℝ ∧ ∃ 𝑐 ∈ ℝ ∀ 𝑑 ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) 𝑐 ≤ 𝑑 ∧ ( abs ‘ ( 𝐴 − 𝑟 ) ) ∈ ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) ) → inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
87 |
38 53 85 86
|
mp3an12i |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( ( 𝐹 ‘ 𝑟 ) = 0 ∧ ¬ 𝐴 = 𝑟 ) ) → inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) |
88 |
87
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → ( ¬ 𝐴 = 𝑟 → inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
89 |
88
|
orrd |
⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) ∧ ( 𝐹 ‘ 𝑟 ) = 0 ) → ( 𝐴 = 𝑟 ∨ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
90 |
89
|
ex |
⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
91 |
90
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
92 |
|
breq1 |
⊢ ( 𝑥 = inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) → ( 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) |
93 |
92
|
orbi2d |
⊢ ( 𝑥 = inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) → ( ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ( 𝐴 = 𝑟 ∨ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
94 |
93
|
imbi2d |
⊢ ( 𝑥 = inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) → ( ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) |
95 |
94
|
ralbidv |
⊢ ( 𝑥 = inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) → ( ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ↔ ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) ) |
96 |
95
|
rspcev |
⊢ ( ( inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ∈ ℝ+ ∧ ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ inf ( ( { 1 } ∪ { 𝑎 ∈ ℝ+ ∣ ∃ 𝑏 ∈ ( ◡ 𝐹 “ { 0 } ) 𝑎 = ( abs ‘ ( 𝐴 − 𝑏 ) ) } ) , ℝ , < ) ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
97 |
42 91 96
|
syl2anc |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ) |
98 |
|
fveqeq2 |
⊢ ( 𝑟 = ( 𝑝 / 𝑞 ) → ( ( 𝐹 ‘ 𝑟 ) = 0 ↔ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 ) ) |
99 |
|
eqeq2 |
⊢ ( 𝑟 = ( 𝑝 / 𝑞 ) → ( 𝐴 = 𝑟 ↔ 𝐴 = ( 𝑝 / 𝑞 ) ) ) |
100 |
|
oveq2 |
⊢ ( 𝑟 = ( 𝑝 / 𝑞 ) → ( 𝐴 − 𝑟 ) = ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) |
101 |
100
|
fveq2d |
⊢ ( 𝑟 = ( 𝑝 / 𝑞 ) → ( abs ‘ ( 𝐴 − 𝑟 ) ) = ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) |
102 |
101
|
breq2d |
⊢ ( 𝑟 = ( 𝑝 / 𝑞 ) → ( 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ↔ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) |
103 |
99 102
|
orbi12d |
⊢ ( 𝑟 = ( 𝑝 / 𝑞 ) → ( ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ↔ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) |
104 |
98 103
|
imbi12d |
⊢ ( 𝑟 = ( 𝑝 / 𝑞 ) → ( ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) ↔ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) |
105 |
104
|
rspcv |
⊢ ( ( 𝑝 / 𝑞 ) ∈ ℝ → ( ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) |
106 |
|
znq |
⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℚ ) |
107 |
|
qre |
⊢ ( ( 𝑝 / 𝑞 ) ∈ ℚ → ( 𝑝 / 𝑞 ) ∈ ℝ ) |
108 |
106 107
|
syl |
⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℝ ) |
109 |
105 108
|
syl11 |
⊢ ( ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) |
110 |
109
|
ralrimivv |
⊢ ( ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) |
111 |
110
|
reximi |
⊢ ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑟 ∈ ℝ ( ( 𝐹 ‘ 𝑟 ) = 0 → ( 𝐴 = 𝑟 ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − 𝑟 ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) |
112 |
97 111
|
syl |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) |
113 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑥 ∈ ℝ+ ) |
114 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℕ ) |
115 |
3
|
nnnn0d |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
116 |
115
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ0 ) |
117 |
114 116
|
nnexpcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℕ ) |
118 |
117
|
nnrpd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℝ+ ) |
119 |
113 118
|
rpdivcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ ) |
120 |
119
|
rpred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ) |
121 |
120
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ) |
122 |
|
simpllr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → 𝑥 ∈ ℝ+ ) |
123 |
122
|
rpred |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → 𝑥 ∈ ℝ ) |
124 |
4
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝐴 ∈ ℝ ) |
125 |
108
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ ) |
126 |
124 125
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℝ ) |
127 |
126
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℂ ) |
128 |
127
|
abscld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) |
129 |
128
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) |
130 |
|
rpre |
⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ ) |
131 |
130
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑥 ∈ ℝ ) |
132 |
113
|
rpcnne0d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) |
133 |
|
divid |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 𝑥 / 𝑥 ) = 1 ) |
134 |
132 133
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑥 / 𝑥 ) = 1 ) |
135 |
117
|
nnge1d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 1 ≤ ( 𝑞 ↑ 𝑁 ) ) |
136 |
134 135
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑥 / 𝑥 ) ≤ ( 𝑞 ↑ 𝑁 ) ) |
137 |
131 113 118 136
|
lediv23d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ 𝑥 ) |
138 |
137
|
adantr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ 𝑥 ) |
139 |
|
simpr |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) |
140 |
121 123 129 138 139
|
letrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) |
141 |
140
|
ex |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) |
142 |
141
|
orim2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) |
143 |
142
|
imim2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) |
144 |
143
|
ralimdvva |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) |
145 |
144
|
reximdva |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ 𝑥 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) |
146 |
112 145
|
mpd |
⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) |