Metamath Proof Explorer

Theorem aalioulem4

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses aalioulem2.a ⊢ 𝑁 = ( deg ‘ 𝐹 )
aalioulem2.b ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
aalioulem2.c ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aalioulem2.d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
aalioulem3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
Assertion aalioulem4 ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aalioulem2.a ⊢ 𝑁 = ( deg ‘ 𝐹 )
2 aalioulem2.b ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℤ ) )
3 aalioulem2.c ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 aalioulem2.d ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
5 aalioulem3.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = 0 )
6 1 2 3 4 5 aalioulem3 ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) )
7 simp2l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑝 ∈ ℤ )
8 simp2r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑞 ∈ ℕ )
9 znq ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℚ )
10 7 8 9 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑝 / 𝑞 ) ∈ ℚ )
11 qre ⊢ ( ( 𝑝 / 𝑞 ) ∈ ℚ → ( 𝑝 / 𝑞 ) ∈ ℝ )
12 10 11 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
13 simp3r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 )
14 oveq2 ⊢ ( 𝑎 = ( 𝑝 / 𝑞 ) → ( 𝐴 − 𝑎 ) = ( 𝐴 − ( 𝑝 / 𝑞 ) ) )
15 14 fveq2d ⊢ ( 𝑎 = ( 𝑝 / 𝑞 ) → ( abs ‘ ( 𝐴 − 𝑎 ) ) = ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
16 15 breq1d ⊢ ( 𝑎 = ( 𝑝 / 𝑞 ) → ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 ↔ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) )
17 2fveq3 ⊢ ( 𝑎 = ( 𝑝 / 𝑞 ) → ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) = ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) )
18 17 oveq2d ⊢ ( 𝑎 = ( 𝑝 / 𝑞 ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) = ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
19 18 15 breq12d ⊢ ( 𝑎 = ( 𝑝 / 𝑞 ) → ( ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ↔ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
20 16 19 imbi12d ⊢ ( 𝑎 = ( 𝑝 / 𝑞 ) → ( ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) ↔ ( ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
21 20 rspcv ⊢ ( ( 𝑝 / 𝑞 ) ∈ ℝ → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ( ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
22 21 com23 ⊢ ( ( 𝑝 / 𝑞 ) ∈ ℝ → ( ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
23 12 13 22 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
24 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑥 ∈ ℝ+ )
25 8 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑞 ∈ ℝ+ )
26 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝜑 )
27 26 3 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑁 ∈ ℕ )
28 27 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑁 ∈ ℤ )
29 25 28 rpexpcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℝ+ )
30 24 29 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
31 30 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
32 31 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) ∧ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
33 24 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑥 ∈ ℝ )
34 26 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝐹 ∈ ( Poly ‘ ℤ ) )
35 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ ℤ ) → 𝐹 : ℂ ⟶ ℂ )
36 34 35 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝐹 : ℂ ⟶ ℂ )
37 12 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑝 / 𝑞 ) ∈ ℂ )
38 36 37 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ∈ ℂ )
39 38 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ∈ ℝ )
40 33 39 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ∈ ℝ )
41 40 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) ∧ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ∈ ℝ )
42 26 4 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝐴 ∈ ℝ )
43 42 12 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℝ )
44 43 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℂ )
45 44 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ )
46 45 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) ∧ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ )
47 24 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 𝑥 ∈ ℂ )
48 29 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℂ )
49 29 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑞 ↑ 𝑁 ) ≠ 0 )
50 47 48 49 divrecd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) = ( 𝑥 · ( 1 / ( 𝑞 ↑ 𝑁 ) ) ) )
51 48 38 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( abs ‘ ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) = ( ( abs ‘ ( 𝑞 ↑ 𝑁 ) ) · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
52 29 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℝ )
53 29 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 0 ≤ ( 𝑞 ↑ 𝑁 ) )
54 52 53 absidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( abs ‘ ( 𝑞 ↑ 𝑁 ) ) = ( 𝑞 ↑ 𝑁 ) )
55 54 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( abs ‘ ( 𝑞 ↑ 𝑁 ) ) · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) = ( ( 𝑞 ↑ 𝑁 ) · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
56 51 55 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( abs ‘ ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) = ( ( 𝑞 ↑ 𝑁 ) · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
57 48 38 mulcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) = ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) · ( 𝑞 ↑ 𝑁 ) ) )
58 1 oveq2i ⊢ ( 𝑞 ↑ 𝑁 ) = ( 𝑞 ↑ ( deg ‘ 𝐹 ) )
59 58 oveq2i ⊢ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) · ( 𝑞 ↑ 𝑁 ) ) = ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) · ( 𝑞 ↑ ( deg ‘ 𝐹 ) ) )
60 57 59 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) = ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) · ( 𝑞 ↑ ( deg ‘ 𝐹 ) ) ) )
61 34 7 8 aalioulem1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) · ( 𝑞 ↑ ( deg ‘ 𝐹 ) ) ) ∈ ℤ )
62 60 61 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ∈ ℤ )
63 simp3l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 )
64 48 38 49 63 mulne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ≠ 0 )
65 nnabscl ⊢ ( ( ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ∈ ℤ ∧ ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ≠ 0 ) → ( abs ‘ ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ∈ ℕ )
66 62 64 65 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( abs ‘ ( ( 𝑞 ↑ 𝑁 ) · ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ∈ ℕ )
67 56 66 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 𝑞 ↑ 𝑁 ) · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ∈ ℕ )
68 67 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 1 ≤ ( ( 𝑞 ↑ 𝑁 ) · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
69 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → 1 ∈ ℝ )
70 69 39 29 ledivmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 1 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ↔ 1 ≤ ( ( 𝑞 ↑ 𝑁 ) · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ) )
71 68 70 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 1 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) )
72 29 rprecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 1 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
73 72 39 24 lemul2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 1 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ↔ ( 𝑥 · ( 1 / ( 𝑞 ↑ 𝑁 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ) )
74 71 73 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑥 · ( 1 / ( 𝑞 ↑ 𝑁 ) ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
75 50 74 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
76 75 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) ∧ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) )
77 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) ∧ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
78 32 41 46 76 77 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) ∧ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
79 78 olcd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) ∧ ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
80 79 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ( 𝑥 · ( abs ‘ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
81 23 80 syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
82 81 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) )
83 82 com34 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) )
84 83 com23 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ) )
85 84 ralrimdvv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
86 85 reximdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ+ ∀ 𝑎 ∈ ℝ ( ( abs ‘ ( 𝐴 − 𝑎 ) ) ≤ 1 → ( 𝑥 · ( abs ‘ ( 𝐹 ‘ 𝑎 ) ) ) ≤ ( abs ‘ ( 𝐴 − 𝑎 ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
87 6 86 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )