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