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 26248

Description: Lemma for aaliou 26253. (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 12962	. . . . . . 7 ⊢ 1 ∈ ℝ⁺
2		snssi 4775	. . . . . . 7 ⊢ (1 ∈ ℝ⁺ → {1} ⊆ ℝ⁺)
3	1, 2	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℝ⁺
4		ssrab2 4046	. . . . . 6 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ ℝ⁺
5	3, 4	unssi 4157	. . . . 5 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺
6		ltso 11261	. . . . . . 7 ⊢ < Or ℝ
7	6	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
8		snfi 9017	. . . . . . 7 ⊢ {1} ∈ Fin
9		aalioulem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
10		aalioulem2.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
11	10	nnne0d 12243	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
12		aalioulem2.a	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (deg‘𝐹)
13	12	eqcomi 2739	. . . . . . . . . . . . 13 ⊢ (deg‘𝐹) = 𝑁
14		dgr0 26175	. . . . . . . . . . . . 13 ⊢ (deg‘0_𝑝) = 0
15	11, 13, 14	3netr4g 3005	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐹) ≠ (deg‘0_𝑝))
16		fveq2 6861	. . . . . . . . . . . . 13 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
17	16	necon3i 2958	. . . . . . . . . . . 12 ⊢ ((deg‘𝐹) ≠ (deg‘0_𝑝) → 𝐹 ≠ 0_𝑝)
18	15, 17	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
19		eqid 2730	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ {0}) = (^◡𝐹 “ {0})
20	19	fta1 26223	. . . . . . . . . . 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 9310	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
24	22, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
25		rabssab 4051	. . . . . . . 8 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}
26		ssfi 9143	. . . . . . . 8 ⊢ (({𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
27	24, 25, 26	sylancl 586	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
28		unfi 9141	. . . . . . 7 ⊢ (({1} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
29	8, 27, 28	sylancr 587	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
30		1ex 11177	. . . . . . . . 9 ⊢ 1 ∈ V
31	30	snid 4629	. . . . . . . 8 ⊢ 1 ∈ {1}
32		elun1 4148	. . . . . . . 8 ⊢ (1 ∈ {1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
33		ne0i 4307	. . . . . . . 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 12966	. . . . . . . 8 ⊢ ℝ⁺ ⊆ ℝ
37	5, 36	sstri 3959	. . . . . . 7 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ
38	37	a1i 11	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ)
39		fiinfcl 9461	. . . . . 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 3947	. . . 4 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺)
42		0re 11183	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
43		rpge0 12972	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ ℝ⁺ → 0 ≤ 𝑑)
44	43	rgen 3047	. . . . . . . . . . 11 ⊢ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑
45		breq1 5113	. . . . . . . . . . . . 13 ⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑))
46	45	ralbidv 3157	. . . . . . . . . . . 12 ⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑))
47	46	rspcev 3591	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑)
48	42, 44, 47	mp2an 692	. . . . . . . . . 10 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑
49		ssralv 4018	. . . . . . . . . . . 12 ⊢ (({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑))
50	5, 49	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
51	50	reximi 3068	. . . . . . . . . 10 ⊢ (∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
52	48, 51	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑
53		eqeq1 2734	. . . . . . . . . . . 12 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
54	53	rexbidv 3158	. . . . . . . . . . 11 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
55		aalioulem2.d	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
56	55	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ)
57		simplr 768	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ)
58	56, 57	resubcld 11613	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ)
59	58	recnd 11209	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ)
60	55	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ)
61	60	recnd 11209	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ)
62		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ)
63	62	recnd 11209	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ)
64	61, 63	subeq0ad 11550	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟))
65	64	necon3abid 2962	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟))
66	65	biimprd 248	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0))
67	66	impr 454	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0)
68	59, 67	absrpcld 15424	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ℝ⁺)
69	57	recnd 11209	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ)
70		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0)
71		plyf 26110	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
72	9, 71	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
73	72	ffnd 6692	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn ℂ)
74	73	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ)
75		fniniseg 7035	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn ℂ → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
77	69, 70, 76	mpbir2and 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (^◡𝐹 “ {0}))
78		eqid 2730	. . . . . . . . . . . 12 ⊢ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))
79		oveq2 7398	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟))
80	79	fveq2d 6865	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟)))
81	80	rspceeqv 3614	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (^◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
82	77, 78, 81	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
83	54, 68, 82	elrabd 3664	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})
84		elun2 4149	. . . . . . . . . 10 ⊢ ((abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
85	83, 84	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
86		infrelb 12175	. . . . . . . . 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 863	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
90	89	ex 412	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
91	90	ralrimiva 3126	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
92		breq1 5113	. . . . . . . 8 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
93	92	orbi2d 915	. . . . . . 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 3157	. . . . 5 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))))
96	95	rspcev 3591	. . . 4 ⊢ ((inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
97	41, 91, 96	syl2anc 584	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
98		fveqeq2 6870	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0))
99		eqeq2 2742	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞)))
100		oveq2 7398	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞)))
101	100	fveq2d 6865	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞))))
102	101	breq2d 5122	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
103	99, 102	orbi12d 918	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
104	98, 103	imbi12d 344	. . . . . . 7 ⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
105	104	rspcv 3587	. . . . . 6 ⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
106		znq 12918	. . . . . . 7 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ)
107		qre 12919	. . . . . . 7 ⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ)
108	106, 107	syl 17	. . . . . 6 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ)
109	105, 108	syl11 33	. . . . 5 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
110	109	ralrimivv 3179	. . . 4 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
111	110	reximi 3068	. . 3 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
112	97, 111	syl 17	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
113		simplr 768	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ⁺)
114		simprr 772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ)
115	10	nnnn0d 12510	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
116	115	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ₀)
117	114, 116	nnexpcld 14217	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ)
118	117	nnrpd 13000	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℝ⁺)
119	113, 118	rpdivcld 13019	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ⁺)
120	119	rpred 13002	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
121	120	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
122		simpllr 775	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ⁺)
123	122	rpred 13002	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ)
124	55	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈ ℝ)
125	108	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ)
126	124, 125	resubcld 11613	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ)
127	126	recnd 11209	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ)
128	127	abscld 15412	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
129	128	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
130		rpre 12967	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
131	130	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ)
132	113	rpcnne0d 13011	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
133		divid 11875	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
134	132, 133	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1)
135	117	nnge1d 12241	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤ (𝑞↑𝑁))
136	134, 135	eqbrtrd 5132	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁))
137	131, 113, 118, 136	lediv23d 13070	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
138	137	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
139		simpr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
140	121, 123, 129, 138, 139	letrd 11338	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
141	140	ex 412	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
142	141	orim2d 968	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
143	142	imim2d 57	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
144	143	ralimdvva 3185	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
145	144	reximdva 3147	. 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 847 = wceq 1540 ∈ wcel 2109 {cab 2708 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3408 ∪ cun 3915 ⊆ wss 3917 ∅c0 4299 {csn 4592 class class class wbr 5110 Or wor 5548 ^◡ccnv 5640 “ cima 5644 Fn wfn 6509 ⟶wf 6510 ‘cfv 6514 (class class class)co 7390 Fincfn 8921 infcinf 9399 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 < clt 11215 ≤ cle 11216 − cmin 11412 / cdiv 11842 ℕcn 12193 ℕ₀cn0 12449 ℤcz 12536 ℚcq 12914 ℝ⁺crp 12958 ↑cexp 14033 ♯chash 14302 abscabs 15207 0_𝑝c0p 25577 Polycply 26096 degcdgr 26099

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-oadd 8441 df-er 8674 df-map 8804 df-pm 8805 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9861 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-n0 12450 df-xnn0 12523 df-z 12537 df-uz 12801 df-q 12915 df-rp 12959 df-fz 13476 df-fzo 13623 df-fl 13761 df-seq 13974 df-exp 14034 df-hash 14303 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-clim 15461 df-rlim 15462 df-sum 15660 df-0p 25578 df-ply 26100 df-idp 26101 df-coe 26102 df-dgr 26103 df-quot 26206

This theorem is referenced by: aalioulem6 26252

W3C validator