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 26462

Description: Lemma for aaliou 26467. (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 13019	. . . . . . 7 ⊢ 1 ∈ ℝ⁺
2		snssi 4756	. . . . . . 7 ⊢ (1 ∈ ℝ⁺ → {1} ⊆ ℝ⁺)
3	1, 2	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℝ⁺
4		ssrab2 4042	. . . . . 6 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ ℝ⁺
5	3, 4	unssi 4152	. . . . 5 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺
6		ltso 11289	. . . . . . 7 ⊢ < Or ℝ
7	6	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
8		snfi 9039	. . . . . . 7 ⊢ {1} ∈ Fin
9		aalioulem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
10		aalioulem2.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
11	10	nnne0d 12285	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
12		aalioulem2.a	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (deg‘𝐹)
13	12	eqcomi 2778	. . . . . . . . . . . . 13 ⊢ (deg‘𝐹) = 𝑁
14		dgr0 26387	. . . . . . . . . . . . 13 ⊢ (deg‘0_𝑝) = 0
15	11, 13, 14	3netr4g 3043	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐹) ≠ (deg‘0_𝑝))
16		fveq2 6882	. . . . . . . . . . . . 13 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
17	16	necon3i 2996	. . . . . . . . . . . 12 ⊢ ((deg‘𝐹) ≠ (deg‘0_𝑝) → 𝐹 ≠ 0_𝑝)
18	15, 17	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
19		eqid 2769	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ {0}) = (^◡𝐹 “ {0})
20	19	fta1 26437	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘ℤ) ∧ 𝐹 ≠ 0_𝑝) → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
21	9, 18, 20	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
22	21	simpld 499	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 “ {0}) ∈ Fin)
23		abrexfi 9308	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
24	22, 23	syl 18	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
25		rabssab 4047	. . . . . . . 8 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}
26		ssfi 9156	. . . . . . . 8 ⊢ (({𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
27	24, 25, 26	sylancl 597	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
28		unfi 9154	. . . . . . 7 ⊢ (({1} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
29	8, 27, 28	sylancr 598	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
30		1ex 11202	. . . . . . . . 9 ⊢ 1 ∈ V
31	30	snid 4633	. . . . . . . 8 ⊢ 1 ∈ {1}
32		elun1 4143	. . . . . . . 8 ⊢ (1 ∈ {1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
33		ne0i 4302	. . . . . . . 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 13023	. . . . . . . 8 ⊢ ℝ⁺ ⊆ ℝ
37	5, 36	sstri 3954	. . . . . . 7 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ
38	37	a1i 11	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ)
39		fiinfcl 9462	. . . . . 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 1397	. . . . 5 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
41	5, 40	sselid 3943	. . . 4 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺)
42		0re 11209	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
43		rpge0 13029	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ ℝ⁺ → 0 ≤ 𝑑)
44	43	rgen 3087	. . . . . . . . . . 11 ⊢ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑
45		breq1 5116	. . . . . . . . . . . . 13 ⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑))
46	45	ralbidv 3194	. . . . . . . . . . . 12 ⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑))
47	46	rspcev 3590	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑)
48	42, 44, 47	mp2an 704	. . . . . . . . . 10 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑
49		ssralv 4014	. . . . . . . . . . . 12 ⊢ (({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑))
50	5, 49	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
51	50	reximi 3109	. . . . . . . . . 10 ⊢ (∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
52	48, 51	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑
53		eqeq1 2773	. . . . . . . . . . . 12 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
54	53	rexbidv 3195	. . . . . . . . . . 11 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
55		aalioulem2.d	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
56	55	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ)
57		simplr 780	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ)
58	56, 57	resubcld 11641	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ)
59	58	recnd 11236	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ)
60	55	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ)
61	60	recnd 11236	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ)
62		simplr 780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ)
63	62	recnd 11236	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ)
64	61, 63	subeq0ad 11578	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟))
65	64	necon3abid 3000	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟))
66	65	biimprd 251	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0))
67	66	impr 459	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0)
68	59, 67	absrpcld 15501	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ℝ⁺)
69	57	recnd 11236	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ)
70		simprl 782	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0)
71		plyf 26323	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
72	9, 71	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
73	72	ffnd 6707	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn ℂ)
74	73	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ)
75		fniniseg 7056	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn ℂ → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
76	74, 75	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
77	69, 70, 76	mpbir2and 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (^◡𝐹 “ {0}))
78		eqid 2769	. . . . . . . . . . . 12 ⊢ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))
79		oveq2 7419	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟))
80	79	fveq2d 6886	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟)))
81	80	rspceeqv 3613	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (^◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
82	77, 78, 81	sylancl 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
83	54, 68, 82	elrabd 3661	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})
84		elun2 4144	. . . . . . . . . 10 ⊢ ((abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
85	83, 84	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
86		infrelb 12199	. . . . . . . . 9 ⊢ ((({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 ∧ (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
87	37, 52, 85, 86	mp3an12i 1491	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
88	87	expr 461	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
89	88	orrd 876	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
90	89	ex 417	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
91	90	ralrimiva 3163	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
92		breq1 5116	. . . . . . . 8 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
93	92	orbi2d 928	. . . . . . 7 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
94	93	imbi2d 343	. . . . . 6 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))))
95	94	ralbidv 3194	. . . . 5 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))))
96	95	rspcev 3590	. . . 4 ⊢ ((inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
97	41, 91, 96	syl2anc 595	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
98		fveqeq2 6891	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0))
99		eqeq2 2781	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞)))
100		oveq2 7419	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞)))
101	100	fveq2d 6886	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞))))
102	101	breq2d 5125	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
103	99, 102	orbi12d 931	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
104	98, 103	imbi12d 347	. . . . . . 7 ⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
105	104	rspcv 3586	. . . . . 6 ⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
106		znq 12975	. . . . . . 7 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ)
107		qre 12976	. . . . . . 7 ⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ)
108	106, 107	syl 18	. . . . . 6 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ)
109	105, 108	syl11 34	. . . . 5 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
110	109	ralrimivv 3212	. . . 4 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
111	110	reximi 3109	. . 3 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
112	97, 111	syl 18	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
113		simplr 780	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ⁺)
114		simprr 784	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ)
115	10	nnnn0d 12564	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
116	115	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ₀)
117	114, 116	nnexpcld 14280	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ)
118	117	nnrpd 13057	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℝ⁺)
119	113, 118	rpdivcld 13076	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ⁺)
120	119	rpred 13059	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
121	120	adantr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
122		simpllr 787	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ⁺)
123	122	rpred 13059	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ)
124	55	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈ ℝ)
125	108	adantl 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ)
126	124, 125	resubcld 11641	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ)
127	126	recnd 11236	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ)
128	127	abscld 15489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
129	128	adantr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
130		rpre 13024	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
131	130	ad2antlr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ)
132	113	rpcnne0d 13068	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
133		divid 11901	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
134	132, 133	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1)
135	117	nnge1d 12283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤ (𝑞↑𝑁))
136	134, 135	eqbrtrd 5137	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁))
137	131, 113, 118, 136	lediv23d 13127	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
138	137	adantr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
139		simpr 489	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
140	121, 123, 129, 138, 139	letrd 11366	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
141	140	ex 417	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
142	141	orim2d 982	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
143	142	imim2d 58	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
144	143	ralimdvva 3218	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
145	144	reximdva 3184	. 2 ⊢ (𝜑 → (∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
146	112, 145	mpd 16	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 {cab 2747 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 {crab 3423 ∪ cun 3911 ⊆ wss 3913 ∅c0 4294 {csn 4594 class class class wbr 5113 Or wor 5569 ^◡ccnv 5661 “ cima 5665 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411 Fincfn 8942 infcinf 9400 ℂcc 11097 ℝcr 11098 0cc0 11099 1c1 11100 < clt 11242 ≤ cle 11243 − cmin 11440 / cdiv 11870 ℕcn 12232 ℕ₀cn0 12503 ℤcz 12590 ℚcq 12971 ℝ⁺crp 13015 ↑cexp 14096 ♯chash 14365 abscabs 15284 0_𝑝c0p 25796 Polycply 26309 degcdgr 26312

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9609 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-oadd 8456 df-er 8693 df-map 8825 df-pm 8826 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-sup 9401 df-inf 9402 df-oi 9471 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-q 12972 df-rp 13016 df-fz 13535 df-fzo 13682 df-fl 13824 df-seq 14037 df-exp 14097 df-hash 14366 df-cj 15149 df-re 15150 df-im 15151 df-sqrt 15285 df-abs 15286 df-clim 15538 df-rlim 15539 df-sum 15737 df-0p 25797 df-ply 26313 df-idp 26314 df-coe 26315 df-dgr 26316 df-quot 26420

This theorem is referenced by: aalioulem6 26466

W3C validator