Metamath Proof Explorer

Theorem aalioulem5

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 aalioulem5 ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 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 aalioulem4 ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → 𝑎 ∈ ℝ+ )
8 1rp ⊢ 1 ∈ ℝ+
9 ifcl ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 1 ∈ ℝ+ ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ∈ ℝ+ )
10 7 8 9 sylancl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ∈ ℝ+ )
11 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ∈ ℝ+ )
12 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℕ )
13 12 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℝ+ )
14 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ )
15 14 nnzd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℤ )
16 13 15 rpexpcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℝ+ )
17 11 16 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
18 17 rpred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
19 1re ⊢ 1 ∈ ℝ
20 19 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 1 ∈ ℝ )
21 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝐴 ∈ ℝ )
22 znq ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℚ )
23 qre ⊢ ( ( 𝑝 / 𝑞 ) ∈ ℚ → ( 𝑝 / 𝑞 ) ∈ ℝ )
24 22 23 syl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
26 21 25 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℝ )
27 26 recnd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℂ )
28 27 abscld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ )
29 18 20 28 3jca ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
30 29 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
31 16 rprecred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
32 11 rpred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ∈ ℝ )
33 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑎 ∈ ℝ+ )
34 33 rpred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑎 ∈ ℝ )
35 min2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ≤ 1 )
36 34 19 35 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ≤ 1 )
37 32 20 16 36 lediv1dd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 1 / ( 𝑞 ↑ 𝑁 ) ) )
38 14 nnnn0d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ0 )
39 12 38 nnexpcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℕ )
40 1nn ⊢ 1 ∈ ℕ
41 40 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 1 ∈ ℕ )
42 39 41 nnmulcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑞 ↑ 𝑁 ) · 1 ) ∈ ℕ )
43 42 nnge1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 1 ≤ ( ( 𝑞 ↑ 𝑁 ) · 1 ) )
44 20 20 16 ledivmuld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 1 / ( 𝑞 ↑ 𝑁 ) ) ≤ 1 ↔ 1 ≤ ( ( 𝑞 ↑ 𝑁 ) · 1 ) ) )
45 43 44 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 1 / ( 𝑞 ↑ 𝑁 ) ) ≤ 1 )
46 18 31 20 37 45 letrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ 1 )
47 46 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ 1 )
48 ltle ⊢ ( ( 1 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) → ( 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → 1 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
49 19 28 48 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → 1 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
50 49 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → 1 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
51 47 50 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ 1 ∧ 1 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
52 letr ⊢ ( ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) → ( ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ 1 ∧ 1 ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
53 30 51 52 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
54 53 olcd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
55 54 2a1d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ 1 < ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
56 pm3.21 ⊢ ( ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) )
57 56 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) ) )
58 33 16 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
59 58 rpred ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
60 18 59 28 3jca ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
61 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
62 min1 ⊢ ( ( 𝑎 ∈ ℝ ∧ 1 ∈ ℝ ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ≤ 𝑎 )
63 34 19 62 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ≤ 𝑎 )
64 32 34 16 63 lediv1dd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) )
65 64 anim1i ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
66 letr ⊢ ( ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) → ( ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
67 61 65 66 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
68 67 ex ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
69 68 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
70 69 orim2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
71 57 70 imim12d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
72 55 71 20 28 ltlecasei ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
73 72 ralimdvva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
74 oveq1 ⊢ ( 𝑥 = if ( 𝑎 ≤ 1 , 𝑎 , 1 ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) = ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) )
75 74 breq1d ⊢ ( 𝑥 = if ( 𝑎 ≤ 1 , 𝑎 , 1 ) → ( ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ↔ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
76 75 orbi2d ⊢ ( 𝑥 = if ( 𝑎 ≤ 1 , 𝑎 , 1 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
77 76 imbi2d ⊢ ( 𝑥 = if ( 𝑎 ≤ 1 , 𝑎 , 1 ) → ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ↔ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
78 77 2ralbidv ⊢ ( 𝑥 = if ( 𝑎 ≤ 1 , 𝑎 , 1 ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ↔ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
79 78 rspcev ⊢ ( ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) ∈ ℝ+ ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 1 , 𝑎 , 1 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
80 10 73 79 syl6an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ+ ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
81 80 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ≤ 1 ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
82 6 81 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )