aalioulem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > aalioulem2		Structured version Visualization version GIF version

Theorem aalioulem2 26375

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

**Hypotheses**
Ref	Expression
aalioulem2.a	⊢ 𝑁 = (deg‘𝐹)
aalioulem2.b	⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
aalioulem2.c	⊢ (𝜑 → 𝑁 ∈ ℕ)
aalioulem2.d	⊢ (𝜑 → 𝐴 ∈ ℝ)

**Assertion**
Ref	Expression
aalioulem2	⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))

Distinct variable groups: 𝜑,𝑥,𝑝,𝑞 𝑥,𝐴,𝑝,𝑞 𝑥,𝐹,𝑝,𝑞 Allowed substitution hints: 𝑁(𝑥,𝑞,𝑝)

Proof of Theorem aalioulem2 Dummy variables 𝑟 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1rp 13038	. . . . . . 7 ⊢ 1 ∈ ℝ⁺
2		snssi 4808	. . . . . . 7 ⊢ (1 ∈ ℝ⁺ → {1} ⊆ ℝ⁺)
3	1, 2	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℝ⁺
4		ssrab2 4080	. . . . . 6 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ ℝ⁺
5	3, 4	unssi 4191	. . . . 5 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺
6		ltso 11341	. . . . . . 7 ⊢ < Or ℝ
7	6	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
8		snfi 9083	. . . . . . 7 ⊢ {1} ∈ Fin
9		aalioulem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
10		aalioulem2.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
11	10	nnne0d 12316	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
12		aalioulem2.a	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (deg‘𝐹)
13	12	eqcomi 2746	. . . . . . . . . . . . 13 ⊢ (deg‘𝐹) = 𝑁
14		dgr0 26302	. . . . . . . . . . . . 13 ⊢ (deg‘0_𝑝) = 0
15	11, 13, 14	3netr4g 3020	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐹) ≠ (deg‘0_𝑝))
16		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
17	16	necon3i 2973	. . . . . . . . . . . 12 ⊢ ((deg‘𝐹) ≠ (deg‘0_𝑝) → 𝐹 ≠ 0_𝑝)
18	15, 17	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
19		eqid 2737	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ {0}) = (^◡𝐹 “ {0})
20	19	fta1 26350	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘ℤ) ∧ 𝐹 ≠ 0_𝑝) → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
21	9, 18, 20	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
22	21	simpld 494	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 “ {0}) ∈ Fin)
23		abrexfi 9392	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
24	22, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
25		rabssab 4085	. . . . . . . 8 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}
26		ssfi 9213	. . . . . . . 8 ⊢ (({𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
27	24, 25, 26	sylancl 586	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
28		unfi 9211	. . . . . . 7 ⊢ (({1} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
29	8, 27, 28	sylancr 587	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
30		1ex 11257	. . . . . . . . 9 ⊢ 1 ∈ V
31	30	snid 4662	. . . . . . . 8 ⊢ 1 ∈ {1}
32		elun1 4182	. . . . . . . 8 ⊢ (1 ∈ {1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
33		ne0i 4341	. . . . . . . 8 ⊢ (1 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅)
34	31, 32, 33	mp2b 10	. . . . . . 7 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅
35	34	a1i 11	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅)
36		rpssre 13042	. . . . . . . 8 ⊢ ℝ⁺ ⊆ ℝ
37	5, 36	sstri 3993	. . . . . . 7 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ
38	37	a1i 11	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ)
39		fiinfcl 9541	. . . . . 6 ⊢ (( < Or ℝ ∧ (({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin ∧ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ≠ ∅ ∧ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ)) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
40	7, 29, 35, 38, 39	syl13anc 1374	. . . . 5 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
41	5, 40	sselid 3981	. . . 4 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺)
42		0re 11263	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
43		rpge0 13048	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ ℝ⁺ → 0 ≤ 𝑑)
44	43	rgen 3063	. . . . . . . . . . 11 ⊢ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑
45		breq1 5146	. . . . . . . . . . . . 13 ⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑))
46	45	ralbidv 3178	. . . . . . . . . . . 12 ⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑))
47	46	rspcev 3622	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑)
48	42, 44, 47	mp2an 692	. . . . . . . . . 10 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑
49		ssralv 4052	. . . . . . . . . . . 12 ⊢ (({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑))
50	5, 49	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
51	50	reximi 3084	. . . . . . . . . 10 ⊢ (∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
52	48, 51	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑
53		eqeq1 2741	. . . . . . . . . . . 12 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
54	53	rexbidv 3179	. . . . . . . . . . 11 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
55		aalioulem2.d	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
56	55	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ)
57		simplr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ)
58	56, 57	resubcld 11691	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ)
59	58	recnd 11289	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ)
60	55	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ)
61	60	recnd 11289	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ)
62		simplr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ)
63	62	recnd 11289	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ)
64	61, 63	subeq0ad 11630	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟))
65	64	necon3abid 2977	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟))
66	65	biimprd 248	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0))
67	66	impr 454	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0)
68	59, 67	absrpcld 15487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ℝ⁺)
69	57	recnd 11289	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ)
70		simprl 771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0)
71		plyf 26237	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
72	9, 71	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
73	72	ffnd 6737	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn ℂ)
74	73	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ)
75		fniniseg 7080	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn ℂ → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
77	69, 70, 76	mpbir2and 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (^◡𝐹 “ {0}))
78		eqid 2737	. . . . . . . . . . . 12 ⊢ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))
79		oveq2 7439	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟))
80	79	fveq2d 6910	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟)))
81	80	rspceeqv 3645	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (^◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
82	77, 78, 81	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
83	54, 68, 82	elrabd 3694	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})
84		elun2 4183	. . . . . . . . . 10 ⊢ ((abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
85	83, 84	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
86		infrelb 12253	. . . . . . . . 9 ⊢ ((({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 ∧ (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
87	37, 52, 85, 86	mp3an12i 1467	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
88	87	expr 456	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
89	88	orrd 864	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
90	89	ex 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
91	90	ralrimiva 3146	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
92		breq1 5146	. . . . . . . 8 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
93	92	orbi2d 916	. . . . . . 7 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
94	93	imbi2d 340	. . . . . 6 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))))
95	94	ralbidv 3178	. . . . 5 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))))
96	95	rspcev 3622	. . . 4 ⊢ ((inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
97	41, 91, 96	syl2anc 584	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
98		fveqeq2 6915	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0))
99		eqeq2 2749	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞)))
100		oveq2 7439	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞)))
101	100	fveq2d 6910	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞))))
102	101	breq2d 5155	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
103	99, 102	orbi12d 919	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
104	98, 103	imbi12d 344	. . . . . . 7 ⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
105	104	rspcv 3618	. . . . . 6 ⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
106		znq 12994	. . . . . . 7 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ)
107		qre 12995	. . . . . . 7 ⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ)
108	106, 107	syl 17	. . . . . 6 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ)
109	105, 108	syl11 33	. . . . 5 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
110	109	ralrimivv 3200	. . . 4 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
111	110	reximi 3084	. . 3 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
112	97, 111	syl 17	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
113		simplr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ⁺)
114		simprr 773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ)
115	10	nnnn0d 12587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
116	115	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ₀)
117	114, 116	nnexpcld 14284	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ)
118	117	nnrpd 13075	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℝ⁺)
119	113, 118	rpdivcld 13094	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ⁺)
120	119	rpred 13077	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
121	120	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
122		simpllr 776	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ⁺)
123	122	rpred 13077	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ)
124	55	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈ ℝ)
125	108	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ)
126	124, 125	resubcld 11691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ)
127	126	recnd 11289	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ)
128	127	abscld 15475	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
129	128	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
130		rpre 13043	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
131	130	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ)
132	113	rpcnne0d 13086	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
133		divid 11953	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
134	132, 133	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1)
135	117	nnge1d 12314	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤ (𝑞↑𝑁))
136	134, 135	eqbrtrd 5165	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁))
137	131, 113, 118, 136	lediv23d 13145	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
138	137	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
139		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
140	121, 123, 129, 138, 139	letrd 11418	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
141	140	ex 412	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
142	141	orim2d 969	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
143	142	imim2d 57	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
144	143	ralimdvva 3206	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
145	144	reximdva 3168	. 2 ⊢ (𝜑 → (∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
146	112, 145	mpd 15	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 {cab 2714 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3436 ∪ cun 3949 ⊆ wss 3951 ∅c0 4333 {csn 4626 class class class wbr 5143 Or wor 5591 ^◡ccnv 5684 “ cima 5688 Fn wfn 6556 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 Fincfn 8985 infcinf 9481 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 < clt 11295 ≤ cle 11296 − cmin 11492 / cdiv 11920 ℕcn 12266 ℕ₀cn0 12526 ℤcz 12613 ℚcq 12990 ℝ⁺crp 13034 ↑cexp 14102 ♯chash 14369 abscabs 15273 0_𝑝c0p 25704 Polycply 26223 degcdgr 26226

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-oadd 8510 df-er 8745 df-map 8868 df-pm 8869 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-q 12991 df-rp 13035 df-fz 13548 df-fzo 13695 df-fl 13832 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-clim 15524 df-rlim 15525 df-sum 15723 df-0p 25705 df-ply 26227 df-idp 26228 df-coe 26229 df-dgr 26230 df-quot 26333

This theorem is referenced by: aalioulem6 26379

W3C validator