Metamath Proof Explorer

Theorem aalioulem2

Description: Lemma for aaliou . (Contributed by Stefan O'Rear, 15-Nov-2014) (Proof shortened by AV, 28-Sep-2020)

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

Proof

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 sselid ⊢ ( 𝜑 → 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 ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )