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

Theorem aalioulem2 25033
 Description: Lemma for aaliou 25038. (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.
StepHypRef Expression
1 1rp 12439 . . . . . . 7 1 ∈ ℝ+
2 snssi 4701 . . . . . . 7 (1 ∈ ℝ+ → {1} ⊆ ℝ+)
31, 2ax-mp 5 . . . . . 6 {1} ⊆ ℝ+
4 ssrab2 3986 . . . . . 6 {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ⊆ ℝ+
53, 4unssi 4092 . . . . 5 ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ+
6 ltso 10764 . . . . . . 7 < Or ℝ
76a1i 11 . . . . . 6 (𝜑 → < Or ℝ)
8 snfi 8619 . . . . . . 7 {1} ∈ Fin
9 aalioulem2.b . . . . . . . . . . 11 (𝜑𝐹 ∈ (Poly‘ℤ))
10 aalioulem2.c . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
1110nnne0d 11729 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
12 aalioulem2.a . . . . . . . . . . . . . 14 𝑁 = (deg‘𝐹)
1312eqcomi 2767 . . . . . . . . . . . . 13 (deg‘𝐹) = 𝑁
14 dgr0 24963 . . . . . . . . . . . . 13 (deg‘0𝑝) = 0
1511, 13, 143netr4g 3030 . . . . . . . . . . . 12 (𝜑 → (deg‘𝐹) ≠ (deg‘0𝑝))
16 fveq2 6662 . . . . . . . . . . . . 13 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
1716necon3i 2983 . . . . . . . . . . . 12 ((deg‘𝐹) ≠ (deg‘0𝑝) → 𝐹 ≠ 0𝑝)
1815, 17syl 17 . . . . . . . . . . 11 (𝜑𝐹 ≠ 0𝑝)
19 eqid 2758 . . . . . . . . . . . 12 (𝐹 “ {0}) = (𝐹 “ {0})
2019fta1 25008 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℤ) ∧ 𝐹 ≠ 0𝑝) → ((𝐹 “ {0}) ∈ Fin ∧ (♯‘(𝐹 “ {0})) ≤ (deg‘𝐹)))
219, 18, 20syl2anc 587 . . . . . . . . . 10 (𝜑 → ((𝐹 “ {0}) ∈ Fin ∧ (♯‘(𝐹 “ {0})) ≤ (deg‘𝐹)))
2221simpld 498 . . . . . . . . 9 (𝜑 → (𝐹 “ {0}) ∈ Fin)
23 abrexfi 8862 . . . . . . . . 9 ((𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
2422, 23syl 17 . . . . . . . 8 (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
25 rabssab 3991 . . . . . . . 8 {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}
26 ssfi 8747 . . . . . . . 8 (({𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) → {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
2724, 25, 26sylancl 589 . . . . . . 7 (𝜑 → {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
28 unfi 8746 . . . . . . 7 (({1} ∈ Fin ∧ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ∈ Fin)
298, 27, 28sylancr 590 . . . . . 6 (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ∈ Fin)
30 1ex 10680 . . . . . . . . 9 1 ∈ V
3130snid 4561 . . . . . . . 8 1 ∈ {1}
32 elun1 4083 . . . . . . . 8 (1 ∈ {1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
33 ne0i 4235 . . . . . . . 8 (1 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅)
3431, 32, 33mp2b 10 . . . . . . 7 ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅
3534a1i 11 . . . . . 6 (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅)
36 rpssre 12442 . . . . . . . 8 + ⊆ ℝ
375, 36sstri 3903 . . . . . . 7 ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ
3837a1i 11 . . . . . 6 (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ)
39 fiinfcl 9003 . . . . . 6 (( < Or ℝ ∧ (({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ∈ Fin ∧ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅ ∧ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ)) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
407, 29, 35, 38, 39syl13anc 1369 . . . . 5 (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
415, 40sseldi 3892 . . . 4 (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ℝ+)
42 0re 10686 . . . . . . . . . . 11 0 ∈ ℝ
43 rpge0 12448 . . . . . . . . . . . 12 (𝑑 ∈ ℝ+ → 0 ≤ 𝑑)
4443rgen 3080 . . . . . . . . . . 11 𝑑 ∈ ℝ+ 0 ≤ 𝑑
45 breq1 5038 . . . . . . . . . . . . 13 (𝑐 = 0 → (𝑐𝑑 ↔ 0 ≤ 𝑑))
4645ralbidv 3126 . . . . . . . . . . . 12 (𝑐 = 0 → (∀𝑑 ∈ ℝ+ 𝑐𝑑 ↔ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑))
4746rspcev 3543 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+ 𝑐𝑑)
4842, 44, 47mp2an 691 . . . . . . . . . 10 𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+ 𝑐𝑑
49 ssralv 3960 . . . . . . . . . . . 12 (({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ+ → (∀𝑑 ∈ ℝ+ 𝑐𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑))
505, 49ax-mp 5 . . . . . . . . . . 11 (∀𝑑 ∈ ℝ+ 𝑐𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑)
5150reximi 3171 . . . . . . . . . 10 (∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+ 𝑐𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑)
5248, 51ax-mp 5 . . . . . . . . 9 𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑
53 eqeq1 2762 . . . . . . . . . . . 12 (𝑎 = (abs‘(𝐴𝑟)) → (𝑎 = (abs‘(𝐴𝑏)) ↔ (abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏))))
5453rexbidv 3221 . . . . . . . . . . 11 (𝑎 = (abs‘(𝐴𝑟)) → (∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏)) ↔ ∃𝑏 ∈ (𝐹 “ {0})(abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏))))
55 aalioulem2.d . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
5655ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ)
57 simplr 768 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ)
5856, 57resubcld 11111 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴𝑟) ∈ ℝ)
5958recnd 10712 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴𝑟) ∈ ℂ)
6055ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝐴 ∈ ℝ)
6160recnd 10712 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝐴 ∈ ℂ)
62 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝑟 ∈ ℝ)
6362recnd 10712 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝑟 ∈ ℂ)
6461, 63subeq0ad 11050 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → ((𝐴𝑟) = 0 ↔ 𝐴 = 𝑟))
6564necon3abid 2987 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → ((𝐴𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟))
6665biimprd 251 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴𝑟) ≠ 0))
6766impr 458 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴𝑟) ≠ 0)
6859, 67absrpcld 14861 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴𝑟)) ∈ ℝ+)
6957recnd 10712 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ)
70 simprl 770 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹𝑟) = 0)
71 plyf 24899 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
729, 71syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:ℂ⟶ℂ)
7372ffnd 6503 . . . . . . . . . . . . . . 15 (𝜑𝐹 Fn ℂ)
7473ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ)
75 fniniseg 6825 . . . . . . . . . . . . . 14 (𝐹 Fn ℂ → (𝑟 ∈ (𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹𝑟) = 0)))
7674, 75syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹𝑟) = 0)))
7769, 70, 76mpbir2and 712 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (𝐹 “ {0}))
78 eqid 2758 . . . . . . . . . . . 12 (abs‘(𝐴𝑟)) = (abs‘(𝐴𝑟))
79 oveq2 7163 . . . . . . . . . . . . . 14 (𝑏 = 𝑟 → (𝐴𝑏) = (𝐴𝑟))
8079fveq2d 6666 . . . . . . . . . . . . 13 (𝑏 = 𝑟 → (abs‘(𝐴𝑏)) = (abs‘(𝐴𝑟)))
8180rspceeqv 3558 . . . . . . . . . . . 12 ((𝑟 ∈ (𝐹 “ {0}) ∧ (abs‘(𝐴𝑟)) = (abs‘(𝐴𝑟))) → ∃𝑏 ∈ (𝐹 “ {0})(abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏)))
8277, 78, 81sylancl 589 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (𝐹 “ {0})(abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏)))
8354, 68, 82elrabd 3606 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴𝑟)) ∈ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})
84 elun2 4084 . . . . . . . . . 10 ((abs‘(𝐴𝑟)) ∈ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} → (abs‘(𝐴𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
8583, 84syl 17 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
86 infrelb 11667 . . . . . . . . 9 ((({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑 ∧ (abs‘(𝐴𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))
8737, 52, 85, 86mp3an12i 1462 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))
8887expr 460 . . . . . . 7 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))
8988orrd 860 . . . . . 6 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))
9089ex 416 . . . . 5 ((𝜑𝑟 ∈ ℝ) → ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))))
9190ralrimiva 3113 . . . 4 (𝜑 → ∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))))
92 breq1 5038 . . . . . . . 8 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))
9392orbi2d 913 . . . . . . 7 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → ((𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟))) ↔ (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))))
9493imbi2d 344 . . . . . 6 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → (((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) ↔ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))))
9594ralbidv 3126 . . . . 5 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))))
9695rspcev 3543 . . . 4 ((inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ℝ+ ∧ ∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))) → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))))
9741, 91, 96syl2anc 587 . . 3 (𝜑 → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))))
98 fveqeq2 6671 . . . . . . . 8 (𝑟 = (𝑝 / 𝑞) → ((𝐹𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0))
99 eqeq2 2770 . . . . . . . . 9 (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟𝐴 = (𝑝 / 𝑞)))
100 oveq2 7163 . . . . . . . . . . 11 (𝑟 = (𝑝 / 𝑞) → (𝐴𝑟) = (𝐴 − (𝑝 / 𝑞)))
101100fveq2d 6666 . . . . . . . . . 10 (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞))))
102101breq2d 5047 . . . . . . . . 9 (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
10399, 102orbi12d 916 . . . . . . . 8 (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
10498, 103imbi12d 348 . . . . . . 7 (𝑟 = (𝑝 / 𝑞) → (((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
105104rspcv 3538 . . . . . 6 ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
106 znq 12397 . . . . . . 7 ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ)
107 qre 12398 . . . . . . 7 ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ)
108106, 107syl 17 . . . . . 6 ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ)
109105, 108syl11 33 . . . . 5 (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
110109ralrimivv 3119 . . . 4 (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
111110reximi 3171 . . 3 (∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
11297, 111syl 17 . 2 (𝜑 → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
113 simplr 768 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ+)
114 simprr 772 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ)
11510nnnn0d 11999 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ0)
116115ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ0)
117114, 116nnexpcld 13661 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞𝑁) ∈ ℕ)
118117nnrpd 12475 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞𝑁) ∈ ℝ+)
119113, 118rpdivcld 12494 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞𝑁)) ∈ ℝ+)
120119rpred 12477 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞𝑁)) ∈ ℝ)
121120adantr 484 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞𝑁)) ∈ ℝ)
122 simpllr 775 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ+)
123122rpred 12477 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ)
12455ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈ ℝ)
125108adantl 485 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ)
126124, 125resubcld 11111 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ)
127126recnd 10712 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ)
128127abscld 14849 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
129128adantr 484 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
130 rpre 12443 . . . . . . . . . . 11 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
131130ad2antlr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ)
132113rpcnne0d 12486 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
133 divid 11370 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
134132, 133syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1)
135117nnge1d 11727 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤ (𝑞𝑁))
136134, 135eqbrtrd 5057 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞𝑁))
137131, 113, 118, 136lediv23d 12545 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞𝑁)) ≤ 𝑥)
138137adantr 484 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞𝑁)) ≤ 𝑥)
139 simpr 488 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
140121, 123, 129, 138, 139letrd 10840 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
141140ex 416 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
142141orim2d 964 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
143142imim2d 57 . . . 4 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
144143ralimdvva 3110 . . 3 ((𝜑𝑥 ∈ ℝ+) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
145144reximdva 3198 . 2 (𝜑 → (∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
146112, 145mpd 15 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cab 2735   ≠ wne 2951  ∀wral 3070  ∃wrex 3071  {crab 3074   ∪ cun 3858   ⊆ wss 3860  ∅c0 4227  {csn 4525   class class class wbr 5035   Or wor 5445  ◡ccnv 5526   “ cima 5530   Fn wfn 6334  ⟶wf 6335  ‘cfv 6339  (class class class)co 7155  Fincfn 8532  infcinf 8943  ℂcc 10578  ℝcr 10579  0cc0 10580  1c1 10581   < clt 10718   ≤ cle 10719   − cmin 10913   / cdiv 11340  ℕcn 11679  ℕ0cn0 11939  ℤcz 12025  ℚcq 12393  ℝ+crp 12435  ↑cexp 13484  ♯chash 13745  abscabs 14646  0𝑝c0p 24374  Polycply 24885  degcdgr 24888 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464  ax-inf2 9142  ax-cnex 10636  ax-resscn 10637  ax-1cn 10638  ax-icn 10639  ax-addcl 10640  ax-addrcl 10641  ax-mulcl 10642  ax-mulrcl 10643  ax-mulcom 10644  ax-addass 10645  ax-mulass 10646  ax-distr 10647  ax-i2m1 10648  ax-1ne0 10649  ax-1rid 10650  ax-rnegex 10651  ax-rrecex 10652  ax-cnre 10653  ax-pre-lttri 10654  ax-pre-lttrn 10655  ax-pre-ltadd 10656  ax-pre-mulgt0 10657  ax-pre-sup 10658  ax-addf 10659 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-se 5487  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-of 7410  df-om 7585  df-1st 7698  df-2nd 7699  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-1o 8117  df-oadd 8121  df-er 8304  df-map 8423  df-pm 8424  df-en 8533  df-dom 8534  df-sdom 8535  df-fin 8536  df-sup 8944  df-inf 8945  df-oi 9012  df-dju 9368  df-card 9406  df-pnf 10720  df-mnf 10721  df-xr 10722  df-ltxr 10723  df-le 10724  df-sub 10915  df-neg 10916  df-div 11341  df-nn 11680  df-2 11742  df-3 11743  df-n0 11940  df-xnn0 12012  df-z 12026  df-uz 12288  df-q 12394  df-rp 12436  df-fz 12945  df-fzo 13088  df-fl 13216  df-seq 13424  df-exp 13485  df-hash 13746  df-cj 14511  df-re 14512  df-im 14513  df-sqrt 14647  df-abs 14648  df-clim 14898  df-rlim 14899  df-sum 15096  df-0p 24375  df-ply 24889  df-idp 24890  df-coe 24891  df-dgr 24892  df-quot 24991 This theorem is referenced by:  aalioulem6  25037
 Copyright terms: Public domain W3C validator