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 25693

Description: Lemma for aaliou 25698. (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 12919	. . . . . . 7 ⊢ 1 ∈ ℝ⁺
2		snssi 4768	. . . . . . 7 ⊢ (1 ∈ ℝ⁺ → {1} ⊆ ℝ⁺)
3	1, 2	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℝ⁺
4		ssrab2 4037	. . . . . 6 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ ℝ⁺
5	3, 4	unssi 4145	. . . . 5 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺
6		ltso 11235	. . . . . . 7 ⊢ < Or ℝ
7	6	a1i 11	. . . . . 6 ⊢ (𝜑 → < Or ℝ)
8		snfi 8988	. . . . . . 7 ⊢ {1} ∈ Fin
9		aalioulem2.b	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ (Poly‘ℤ))
10		aalioulem2.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ)
11	10	nnne0d 12203	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ≠ 0)
12		aalioulem2.a	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (deg‘𝐹)
13	12	eqcomi 2745	. . . . . . . . . . . . 13 ⊢ (deg‘𝐹) = 𝑁
14		dgr0 25623	. . . . . . . . . . . . 13 ⊢ (deg‘0_𝑝) = 0
15	11, 13, 14	3netr4g 3023	. . . . . . . . . . . 12 ⊢ (𝜑 → (deg‘𝐹) ≠ (deg‘0_𝑝))
16		fveq2 6842	. . . . . . . . . . . . 13 ⊢ (𝐹 = 0_𝑝 → (deg‘𝐹) = (deg‘0_𝑝))
17	16	necon3i 2976	. . . . . . . . . . . 12 ⊢ ((deg‘𝐹) ≠ (deg‘0_𝑝) → 𝐹 ≠ 0_𝑝)
18	15, 17	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ≠ 0_𝑝)
19		eqid 2736	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ {0}) = (^◡𝐹 “ {0})
20	19	fta1 25668	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ (Poly‘ℤ) ∧ 𝐹 ≠ 0_𝑝) → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
21	9, 18, 20	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((^◡𝐹 “ {0}) ∈ Fin ∧ (♯‘(^◡𝐹 “ {0})) ≤ (deg‘𝐹)))
22	21	simpld 495	. . . . . . . . 9 ⊢ (𝜑 → (^◡𝐹 “ {0}) ∈ Fin)
23		abrexfi 9296	. . . . . . . . 9 ⊢ ((^◡𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
24	22, 23	syl 17	. . . . . . . 8 ⊢ (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
25		rabssab 4043	. . . . . . . 8 ⊢ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}
26		ssfi 9117	. . . . . . . 8 ⊢ (({𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
27	24, 25, 26	sylancl 586	. . . . . . 7 ⊢ (𝜑 → {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin)
28		unfi 9116	. . . . . . 7 ⊢ (({1} ∈ Fin ∧ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
29	8, 27, 28	sylancr 587	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ∈ Fin)
30		1ex 11151	. . . . . . . . 9 ⊢ 1 ∈ V
31	30	snid 4622	. . . . . . . 8 ⊢ 1 ∈ {1}
32		elun1 4136	. . . . . . . 8 ⊢ (1 ∈ {1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
33		ne0i 4294	. . . . . . . 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 12922	. . . . . . . 8 ⊢ ℝ⁺ ⊆ ℝ
37	5, 36	sstri 3953	. . . . . . 7 ⊢ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ
38	37	a1i 11	. . . . . 6 ⊢ (𝜑 → ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ)
39		fiinfcl 9437	. . . . . 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 1372	. . . . 5 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
41	5, 40	sselid 3942	. . . 4 ⊢ (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺)
42		0re 11157	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
43		rpge0 12928	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ ℝ⁺ → 0 ≤ 𝑑)
44	43	rgen 3066	. . . . . . . . . . 11 ⊢ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑
45		breq1 5108	. . . . . . . . . . . . 13 ⊢ (𝑐 = 0 → (𝑐 ≤ 𝑑 ↔ 0 ≤ 𝑑))
46	45	ralbidv 3174	. . . . . . . . . . . 12 ⊢ (𝑐 = 0 → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 ↔ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑))
47	46	rspcev 3581	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ ∧ ∀𝑑 ∈ ℝ⁺ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑)
48	42, 44, 47	mp2an 690	. . . . . . . . . 10 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑
49		ssralv 4010	. . . . . . . . . . . 12 ⊢ (({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ⁺ → (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑))
50	5, 49	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
51	50	reximi 3087	. . . . . . . . . 10 ⊢ (∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ⁺ 𝑐 ≤ 𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑)
52	48, 51	ax-mp 5	. . . . . . . . 9 ⊢ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑
53		eqeq1 2740	. . . . . . . . . . . 12 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (𝑎 = (abs‘(𝐴 − 𝑏)) ↔ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
54	53	rexbidv 3175	. . . . . . . . . . 11 ⊢ (𝑎 = (abs‘(𝐴 − 𝑟)) → (∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏)) ↔ ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏))))
55		aalioulem2.d	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ∈ ℝ)
56	55	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ)
57		simplr 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ)
58	56, 57	resubcld 11583	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℝ)
59	58	recnd 11183	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ∈ ℂ)
60	55	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℝ)
61	60	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝐴 ∈ ℂ)
62		simplr 767	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℝ)
63	62	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → 𝑟 ∈ ℂ)
64	61, 63	subeq0ad 11522	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) = 0 ↔ 𝐴 = 𝑟))
65	64	necon3abid 2980	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → ((𝐴 − 𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟))
66	65	biimprd 247	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴 − 𝑟) ≠ 0))
67	66	impr 455	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴 − 𝑟) ≠ 0)
68	59, 67	absrpcld 15333	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ℝ⁺)
69	57	recnd 11183	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ)
70		simprl 769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹‘𝑟) = 0)
71		plyf 25559	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
72	9, 71	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:ℂ⟶ℂ)
73	72	ffnd 6669	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn ℂ)
74	73	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ)
75		fniniseg 7010	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn ℂ → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
76	74, 75	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (^◡𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹‘𝑟) = 0)))
77	69, 70, 76	mpbir2and 711	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (^◡𝐹 “ {0}))
78		eqid 2736	. . . . . . . . . . . 12 ⊢ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))
79		oveq2 7365	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑟 → (𝐴 − 𝑏) = (𝐴 − 𝑟))
80	79	fveq2d 6846	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑟 → (abs‘(𝐴 − 𝑏)) = (abs‘(𝐴 − 𝑟)))
81	80	rspceeqv 3595	. . . . . . . . . . . 12 ⊢ ((𝑟 ∈ (^◡𝐹 “ {0}) ∧ (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑟))) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
82	77, 78, 81	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (^◡𝐹 “ {0})(abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − 𝑏)))
83	54, 68, 82	elrabd 3647	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})
84		elun2 4137	. . . . . . . . . 10 ⊢ ((abs‘(𝐴 − 𝑟)) ∈ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))} → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
85	83, 84	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}))
86		infrelb 12140	. . . . . . . . 9 ⊢ ((({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})𝑐 ≤ 𝑑 ∧ (abs‘(𝐴 − 𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
87	37, 52, 85, 86	mp3an12i 1465	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ ((𝐹‘𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))
88	87	expr 457	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
89	88	orrd 861	. . . . . 6 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ) ∧ (𝐹‘𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
90	89	ex 413	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ) → ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
91	90	ralrimiva 3143	. . . 4 ⊢ (𝜑 → ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟)))))
92		breq1 5108	. . . . . . . 8 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))
93	92	orbi2d 914	. . . . . . 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 3174	. . . . 5 ⊢ (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))))
96	95	rspcev 3581	. . . 4 ⊢ ((inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ∈ ℝ⁺ ∧ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ⁺ ∣ ∃𝑏 ∈ (^◡𝐹 “ {0})𝑎 = (abs‘(𝐴 − 𝑏))}), ℝ, < ) ≤ (abs‘(𝐴 − 𝑟))))) → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
97	41, 91, 96	syl2anc 584	. . 3 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))))
98		fveqeq2 6851	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐹‘𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0))
99		eqeq2 2748	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟 ↔ 𝐴 = (𝑝 / 𝑞)))
100		oveq2 7365	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝐴 − 𝑟) = (𝐴 − (𝑝 / 𝑞)))
101	100	fveq2d 6846	. . . . . . . . . 10 ⊢ (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴 − 𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞))))
102	101	breq2d 5117	. . . . . . . . 9 ⊢ (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴 − 𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
103	99, 102	orbi12d 917	. . . . . . . 8 ⊢ (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
104	98, 103	imbi12d 344	. . . . . . 7 ⊢ (𝑟 = (𝑝 / 𝑞) → (((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
105	104	rspcv 3577	. . . . . 6 ⊢ ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
106		znq 12877	. . . . . . 7 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ)
107		qre 12878	. . . . . . 7 ⊢ ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ)
108	106, 107	syl 17	. . . . . 6 ⊢ ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ)
109	105, 108	syl11 33	. . . . 5 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
110	109	ralrimivv 3195	. . . 4 ⊢ (∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
111	110	reximi 3087	. . 3 ⊢ (∃𝑥 ∈ ℝ⁺ ∀𝑟 ∈ ℝ ((𝐹‘𝑟) = 0 → (𝐴 = 𝑟 ∨ 𝑥 ≤ (abs‘(𝐴 − 𝑟)))) → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
112	97, 111	syl 17	. 2 ⊢ (𝜑 → ∃𝑥 ∈ ℝ⁺ ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
113		simplr 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ⁺)
114		simprr 771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ)
115	10	nnnn0d 12473	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
116	115	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ₀)
117	114, 116	nnexpcld 14148	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℕ)
118	117	nnrpd 12955	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞↑𝑁) ∈ ℝ⁺)
119	113, 118	rpdivcld 12974	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ⁺)
120	119	rpred 12957	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
121	120	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ∈ ℝ)
122		simpllr 774	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ⁺)
123	122	rpred 12957	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ)
124	55	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈ ℝ)
125	108	adantl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ)
126	124, 125	resubcld 11583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ)
127	126	recnd 11183	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ)
128	127	abscld 15321	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
129	128	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
130		rpre 12923	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℝ)
131	130	ad2antlr 725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ)
132	113	rpcnne0d 12966	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
133		divid 11842	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
134	132, 133	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1)
135	117	nnge1d 12201	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤ (𝑞↑𝑁))
136	134, 135	eqbrtrd 5127	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞↑𝑁))
137	131, 113, 118, 136	lediv23d 13025	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
138	137	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ 𝑥)
139		simpr 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
140	121, 123, 129, 138, 139	letrd 11312	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
141	140	ex 413	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
142	141	orim2d 965	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
143	142	imim2d 57	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ⁺) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
144	143	ralimdvva 3201	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ⁺) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞↑𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
145	144	reximdva 3165	. 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 205 ∧ wa 396 ∨ wo 845 = wceq 1541 ∈ wcel 2106 {cab 2713 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 {crab 3407 ∪ cun 3908 ⊆ wss 3910 ∅c0 4282 {csn 4586 class class class wbr 5105 Or wor 5544 ^◡ccnv 5632 “ cima 5636 Fn wfn 6491 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 Fincfn 8883 infcinf 9377 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 < clt 11189 ≤ cle 11190 − cmin 11385 / cdiv 11812 ℕcn 12153 ℕ₀cn0 12413 ℤcz 12499 ℚcq 12873 ℝ⁺crp 12915 ↑cexp 13967 ♯chash 14230 abscabs 15119 0_𝑝c0p 25033 Polycply 25545 degcdgr 25548

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-oadd 8416 df-er 8648 df-map 8767 df-pm 8768 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9378 df-inf 9379 df-oi 9446 df-dju 9837 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-xnn0 12486 df-z 12500 df-uz 12764 df-q 12874 df-rp 12916 df-fz 13425 df-fzo 13568 df-fl 13697 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-clim 15370 df-rlim 15371 df-sum 15571 df-0p 25034 df-ply 25549 df-idp 25550 df-coe 25551 df-dgr 25552 df-quot 25651

This theorem is referenced by: aalioulem6 25697

W3C validator