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 26653

Description: Lemma for aaliou 26658. (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 13117	. . . . . . 7 ⊢ 1 ∈ ℝ⁺
2		snssi 4746	. . . . . . 7 ⊢ (1 ∈ ℝ⁺ → {1} ⊆ ℝ⁺)
3	1, 2	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℝ⁺
4		ssrab2 4028	. . . . . 6 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ ℝ⁺
5	3, 4	unssi 4137	. . . . 5 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺
6		ltso 11383	. . . . . . 7 ⊢ < Or ℝ
7	6	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
8		snfi 9064	. . . . . . 7 ⊢ {1} ∈ Fin
9		aalioulem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
10		aalioulem2.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
11	10	nnne0d 12381	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
12		aalioulem2.a	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (deg‘𝐹)
13	12	eqcomi 2770	. . . . . . . . . . . . 13 ⊢ (deg‘𝐹) = 𝑁
14		dgr0 26574	. . . . . . . . . . . . 13 ⊢ (deg‘0_𝑝) = 0
15	11, 13, 14	3netr4g 3035	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐹) ≠ (deg‘0_𝑝))
16		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
17	16	necon3i 2988	. . . . . . . . . . . 12 ⊢ ((deg‘𝐹) ≠ (deg‘0_𝑝) → 𝐹 ≠ 0_𝑝)
18	15, 17	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
19		eqid 2761	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ {0}) = (^◡𝐹 “ {0})
20	19	fta1 26622	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘ℤ) ∧ 𝐹 ≠ 0_𝑝) → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
21	9, 18, 20	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
22	21	simpld 500	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 “ {0}) ∈ Fin)
23		abrexfi 9334	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
24	22, 23	syl 18	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
25		rabssab 4033	. . . . . . . 8 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}
26		ssfi 9181	. . . . . . . 8 ⊢ (({𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
27	24, 25, 26	sylancl 598	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
28		unfi 9179	. . . . . . 7 ⊢ (({1} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
29	8, 27, 28	sylancr 599	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
30		1ex 11296	. . . . . . . . 9 ⊢ 1 ∈ V
31	30	snid 4623	. . . . . . . 8 ⊢ 1 ∈ {1}
32		elun1 4128	. . . . . . . 8 ⊢ (1 ∈ {1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
33		ne0i 4287	. . . . . . . 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 13121	. . . . . . . 8 ⊢ ℝ⁺ ⊆ ℝ
37	5, 36	sstri 3940	. . . . . . 7 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ
38	37	a1i 11	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ)
39		fiinfcl 9488	. . . . . 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 1399	. . . . 5 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
41	5, 40	sselid 3929	. . . 4 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺)
42		0re 11303	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
43		rpge0 13127	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ ℝ⁺ → 0 ≤ 𝑑)
44	43	rgen 3079	. . . . . . . . . . 11 ⊢ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑
45		breq1 5106	. . . . . . . . . . . . 13 ⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑))
46	45	ralbidv 3186	. . . . . . . . . . . 12 ⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑))
47	46	rspcev 3577	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑)
48	42, 44, 47	mp2an 705	. . . . . . . . . 10 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑
49		ssralv 4000	. . . . . . . . . . . 12 ⊢ (({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑))
50	5, 49	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
51	50	reximi 3101	. . . . . . . . . 10 ⊢ (∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
52	48, 51	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑
53		eqeq1 2765	. . . . . . . . . . . 12 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
54	53	rexbidv 3187	. . . . . . . . . . 11 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
55		aalioulem2.d	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
56	55	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ)
57		simplr 781	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ)
58	56, 57	resubcld 11737	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ)
59	58	recnd 11330	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ)
60	55	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ)
61	60	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ)
62		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ)
63	62	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ)
64	61, 63	subeq0ad 11670	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟))
65	64	necon3abid 2992	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟))
66	65	biimprd 251	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0))
67	66	impr 460	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0)
68	59, 67	absrpcld 15611	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ℝ⁺)
69	57	recnd 11330	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ)
70		simprl 783	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0)
71		plyf 26509	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
72	9, 71	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
73	72	ffnd 6708	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn ℂ)
74	73	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ)
75		fniniseg 7057	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn ℂ → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
76	74, 75	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
77	69, 70, 76	mpbir2and 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (^◡𝐹 “ {0}))
78		eqid 2761	. . . . . . . . . . . 12 ⊢ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))
79		oveq2 7426	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟))
80	79	fveq2d 6887	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟)))
81	80	rspceeqv 3599	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (^◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
82	77, 78, 81	sylancl 598	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
83	54, 68, 82	elrabd 3647	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})
84		elun2 4129	. . . . . . . . . 10 ⊢ ((abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
85	83, 84	syl 18	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
86		infrelb 12295	. . . . . . . . 9 ⊢ ((({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 ∧ (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
87	37, 52, 85, 86	mp3an12i 1494	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
88	87	expr 462	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
89	88	orrd 877	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
90	89	ex 418	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
91	90	ralrimiva 3155	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
92		breq1 5106	. . . . . . . 8 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
93	92	orbi2d 929	. . . . . . 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 3186	. . . . 5 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))))
96	95	rspcev 3577	. . . 4 ⊢ ((inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
97	41, 91, 96	syl2anc 596	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
98		fveqeq2 6892	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0))
99		eqeq2 2773	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞)))
100		oveq2 7426	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞)))
101	100	fveq2d 6887	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞))))
102	101	breq2d 5115	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
103	99, 102	orbi12d 932	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
104	98, 103	imbi12d 347	. . . . . . 7 ⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
105	104	rspcv 3573	. . . . . 6 ⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
106		znq 13072	. . . . . . 7 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ)
107		qre 13073	. . . . . . 7 ⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ)
108	106, 107	syl 18	. . . . . 6 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ)
109	105, 108	syl11 34	. . . . 5 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
110	109	ralrimivv 3204	. . . 4 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
111	110	reximi 3101	. . 3 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
112	97, 111	syl 18	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
113		simplr 781	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ⁺)
114		simprr 785	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ)
115	10	nnnn0d 12660	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
116	115	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ₀)
117	114, 116	nnexpcld 14382	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ)
118	117	nnrpd 13155	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℝ⁺)
119	113, 118	rpdivcld 13174	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ⁺)
120	119	rpred 13157	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
121	120	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
122		simpllr 788	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ⁺)
123	122	rpred 13157	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ)
124	55	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈ ℝ)
125	108	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ)
126	124, 125	resubcld 11737	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ)
127	126	recnd 11330	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ)
128	127	abscld 15599	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
129	128	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
130		rpre 13122	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
131	130	ad2antlr 740	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ)
132	113	rpcnne0d 13166	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
133		divid 11997	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
134	132, 133	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1)
135	117	nnge1d 12379	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤ (𝑞↑𝑁))
136	134, 135	eqbrtrd 5127	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁))
137	131, 113, 118, 136	lediv23d 13225	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
138	137	adantr 486	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
139		simpr 490	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
140	121, 123, 129, 138, 139	letrd 11460	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
141	140	ex 418	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
142	141	orim2d 982	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
143	142	imim2d 58	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
144	143	ralimdvva 3210	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
145	144	reximdva 3176	. 2 ⊢ (𝜑 → (∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
146	112, 145	mpd 16	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 {cab 2739 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3413 ∪ cun 3897 ⊆ wss 3899 ∅c0 4279 {csn 4584 class class class wbr 5103 Or wor 5558 ^◡ccnv 5650 “ cima 5654 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 Fincfn 8966 infcinf 9426 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 < clt 11336 ≤ cle 11337 − cmin 11534 / cdiv 11966 ℕcn 12328 ℕ₀cn0 12599 ℤcz 12686 ℚcq 13068 ℝ⁺crp 13113 ↑cexp 14197 ♯chash 14467 abscabs 15394 0_𝑝c0p 25983 Polycply 26495 degcdgr 26498

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 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 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-oadd 8473 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-xnn0 12673 df-z 12687 df-uz 12959 df-q 13069 df-rp 13114 df-fz 13633 df-fzo 13782 df-fl 13925 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-rlim 15649 df-sum 15847 df-0p 25984 df-ply 26499 df-idp 26500 df-coe 26501 df-dgr 26502 df-quot 26605

This theorem is used by: aalioulem6 26657

W3C validator