Metamath Proof Explorer

Theorem aalioulem6

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 aalioulem6 ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 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 aalioulem2 ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
7 1 2 3 4 5 aalioulem5 ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
8 reeanv ⊢ ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ↔ ( ∃ 𝑎 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ∃ 𝑏 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
9 6 7 8 sylanbrc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
10 r19.26-2 ⊢ ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) ↔ ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) )
11 ifcl ⊢ ( ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ )
12 11 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ )
13 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 ) → ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 )
14 11 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ )
15 nnrp ⊢ ( 𝑞 ∈ ℕ → 𝑞 ∈ ℝ+ )
16 15 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑞 ∈ ℝ+ )
17 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℕ )
18 17 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑁 ∈ ℤ )
19 16 18 rpexpcld ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑞 ↑ 𝑁 ) ∈ ℝ+ )
20 14 19 rpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
21 20 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
22 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑎 ∈ ℝ+ )
23 22 19 rpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
24 23 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
25 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝐴 ∈ ℝ )
26 znq ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℚ )
27 qre ⊢ ( ( 𝑝 / 𝑞 ) ∈ ℚ → ( 𝑝 / 𝑞 ) ∈ ℝ )
28 26 27 syl ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
29 28 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑝 / 𝑞 ) ∈ ℝ )
30 25 29 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℝ )
31 30 recnd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐴 − ( 𝑝 / 𝑞 ) ) ∈ ℂ )
32 31 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ )
33 21 24 32 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
34 33 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
35 14 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ )
36 22 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑎 ∈ ℝ )
37 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑏 ∈ ℝ+ )
38 37 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → 𝑏 ∈ ℝ )
39 min1 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
40 36 38 39 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑎 )
41 35 36 19 40 lediv1dd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) )
42 41 anim1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
43 letr ⊢ ( ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) → ( ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
44 34 42 43 sylc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
45 44 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
46 45 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 ) → ( ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
47 46 orim2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
48 13 47 embantd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 ) → ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
49 48 adantrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 ) → ( ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
50 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ) → ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 )
51 37 19 rpdivcld ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ+ )
52 51 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ )
53 21 52 32 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
54 53 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) )
55 min2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
56 36 38 55 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ≤ 𝑏 )
57 35 38 19 56 lediv1dd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) )
58 57 anim1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
59 letr ⊢ ( ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ∈ ℝ ∧ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ∈ ℝ ) → ( ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
60 54 58 59 sylc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) )
61 60 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
62 61 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ) → ( ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) → ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
63 62 orim2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
64 50 63 embantd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ) → ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
65 64 adantld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) ∧ ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 ) → ( ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
66 49 65 pm2.61dane ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) ∧ ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ) → ( ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
67 66 ralimdvva ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
68 oveq1 ⊢ ( 𝑥 = if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) → ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) = ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) )
69 68 breq1d ⊢ ( 𝑥 = if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) → ( ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ↔ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
70 69 orbi2d ⊢ ( 𝑥 = if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) → ( ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
71 70 2ralbidv ⊢ ( 𝑥 = if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ↔ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
72 71 rspcev ⊢ ( ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) ∈ ℝ+ ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( if ( 𝑎 ≤ 𝑏 , 𝑎 , 𝑏 ) / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )
73 12 67 72 syl6an ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
74 10 73 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℝ+ ) ) → ( ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
75 74 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℝ+ ∃ 𝑏 ∈ ℝ+ ( ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) = 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑎 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ∧ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( ( 𝐹 ‘ ( 𝑝 / 𝑞 ) ) ≠ 0 → ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑏 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) ) → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) ) )
76 9 75 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ+ ∀ 𝑝 ∈ ℤ ∀ 𝑞 ∈ ℕ ( 𝐴 = ( 𝑝 / 𝑞 ) ∨ ( 𝑥 / ( 𝑞 ↑ 𝑁 ) ) ≤ ( abs ‘ ( 𝐴 − ( 𝑝 / 𝑞 ) ) ) ) )