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

Theorem aalioulem2 23805
Description: Lemma for aaliou 23810. (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 11664 . . . . . . 7 1 ∈ ℝ+
2 snssi 4275 . . . . . . 7 (1 ∈ ℝ+ → {1} ⊆ ℝ+)
31, 2ax-mp 5 . . . . . 6 {1} ⊆ ℝ+
4 ssrab2 3645 . . . . . 6 {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ⊆ ℝ+
53, 4unssi 3745 . . . . 5 ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ+
6 ltso 9965 . . . . . . 7 < Or ℝ
76a1i 11 . . . . . 6 (𝜑 → < Or ℝ)
8 snfi 7896 . . . . . . 7 {1} ∈ Fin
9 aalioulem2.b . . . . . . . . . . 11 (𝜑𝐹 ∈ (Poly‘ℤ))
10 aalioulem2.c . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ)
1110nnne0d 10908 . . . . . . . . . . . . 13 (𝜑𝑁 ≠ 0)
12 aalioulem2.a . . . . . . . . . . . . . 14 𝑁 = (deg‘𝐹)
1312eqcomi 2614 . . . . . . . . . . . . 13 (deg‘𝐹) = 𝑁
14 dgr0 23735 . . . . . . . . . . . . 13 (deg‘0𝑝) = 0
1511, 13, 143netr4g 2856 . . . . . . . . . . . 12 (𝜑 → (deg‘𝐹) ≠ (deg‘0𝑝))
16 fveq2 6084 . . . . . . . . . . . . 13 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
1716necon3i 2809 . . . . . . . . . . . 12 ((deg‘𝐹) ≠ (deg‘0𝑝) → 𝐹 ≠ 0𝑝)
1815, 17syl 17 . . . . . . . . . . 11 (𝜑𝐹 ≠ 0𝑝)
19 eqid 2605 . . . . . . . . . . . 12 (𝐹 “ {0}) = (𝐹 “ {0})
2019fta1 23780 . . . . . . . . . . 11 ((𝐹 ∈ (Poly‘ℤ) ∧ 𝐹 ≠ 0𝑝) → ((𝐹 “ {0}) ∈ Fin ∧ (#‘(𝐹 “ {0})) ≤ (deg‘𝐹)))
219, 18, 20syl2anc 690 . . . . . . . . . 10 (𝜑 → ((𝐹 “ {0}) ∈ Fin ∧ (#‘(𝐹 “ {0})) ≤ (deg‘𝐹)))
2221simpld 473 . . . . . . . . 9 (𝜑 → (𝐹 “ {0}) ∈ Fin)
23 abrexfi 8122 . . . . . . . . 9 ((𝐹 “ {0}) ∈ Fin → {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
2422, 23syl 17 . . . . . . . 8 (𝜑 → {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
25 rabssab 3647 . . . . . . . 8 {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}
26 ssfi 8038 . . . . . . . 8 (({𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin ∧ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ⊆ {𝑎 ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) → {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
2724, 25, 26sylancl 692 . . . . . . 7 (𝜑 → {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin)
28 unfi 8085 . . . . . . 7 (({1} ∈ Fin ∧ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ∈ Fin) → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ∈ Fin)
298, 27, 28sylancr 693 . . . . . 6 (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ∈ Fin)
30 1ex 9887 . . . . . . . . 9 1 ∈ V
3130snid 4150 . . . . . . . 8 1 ∈ {1}
32 elun1 3737 . . . . . . . 8 (1 ∈ {1} → 1 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
33 ne0i 3875 . . . . . . . 8 (1 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅)
3431, 32, 33mp2b 10 . . . . . . 7 ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅
3534a1i 11 . . . . . 6 (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅)
36 rpssre 11671 . . . . . . . 8 + ⊆ ℝ
375, 36sstri 3572 . . . . . . 7 ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ
3837a1i 11 . . . . . 6 (𝜑 → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ)
39 fiinfcl 8263 . . . . . 6 (( < Or ℝ ∧ (({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ∈ Fin ∧ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ≠ ∅ ∧ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ)) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
407, 29, 35, 38, 39syl13anc 1319 . . . . 5 (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
415, 40sseldi 3561 . . . 4 (𝜑 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ℝ+)
4237a1i 11 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ)
43 0re 9892 . . . . . . . . . . . 12 0 ∈ ℝ
44 rpge0 11673 . . . . . . . . . . . . 13 (𝑑 ∈ ℝ+ → 0 ≤ 𝑑)
4544rgen 2901 . . . . . . . . . . . 12 𝑑 ∈ ℝ+ 0 ≤ 𝑑
46 breq1 4576 . . . . . . . . . . . . . 14 (𝑐 = 0 → (𝑐𝑑 ↔ 0 ≤ 𝑑))
4746ralbidv 2964 . . . . . . . . . . . . 13 (𝑐 = 0 → (∀𝑑 ∈ ℝ+ 𝑐𝑑 ↔ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑))
4847rspcev 3277 . . . . . . . . . . . 12 ((0 ∈ ℝ ∧ ∀𝑑 ∈ ℝ+ 0 ≤ 𝑑) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+ 𝑐𝑑)
4943, 45, 48mp2an 703 . . . . . . . . . . 11 𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+ 𝑐𝑑
50 ssralv 3624 . . . . . . . . . . . . 13 (({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ+ → (∀𝑑 ∈ ℝ+ 𝑐𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑))
515, 50ax-mp 5 . . . . . . . . . . . 12 (∀𝑑 ∈ ℝ+ 𝑐𝑑 → ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑)
5251reximi 2989 . . . . . . . . . . 11 (∃𝑐 ∈ ℝ ∀𝑑 ∈ ℝ+ 𝑐𝑑 → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑)
5349, 52ax-mp 5 . . . . . . . . . 10 𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑
5453a1i 11 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑)
55 aalioulem2.d . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ ℝ)
5655ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐴 ∈ ℝ)
57 simplr 787 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℝ)
5856, 57resubcld 10305 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴𝑟) ∈ ℝ)
5958recnd 9920 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴𝑟) ∈ ℂ)
6055ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝐴 ∈ ℝ)
6160recnd 9920 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝐴 ∈ ℂ)
62 simplr 787 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝑟 ∈ ℝ)
6362recnd 9920 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → 𝑟 ∈ ℂ)
6461, 63subeq0ad 10249 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → ((𝐴𝑟) = 0 ↔ 𝐴 = 𝑟))
6564necon3abid 2813 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → ((𝐴𝑟) ≠ 0 ↔ ¬ 𝐴 = 𝑟))
6665biimprd 236 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → (¬ 𝐴 = 𝑟 → (𝐴𝑟) ≠ 0))
6766impr 646 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐴𝑟) ≠ 0)
6859, 67absrpcld 13977 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴𝑟)) ∈ ℝ+)
6957recnd 9920 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ ℂ)
70 simprl 789 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝐹𝑟) = 0)
71 plyf 23671 . . . . . . . . . . . . . . . . 17 (𝐹 ∈ (Poly‘ℤ) → 𝐹:ℂ⟶ℂ)
729, 71syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:ℂ⟶ℂ)
73 ffn 5940 . . . . . . . . . . . . . . . 16 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
7472, 73syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐹 Fn ℂ)
7574ad2antrr 757 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝐹 Fn ℂ)
76 fniniseg 6227 . . . . . . . . . . . . . 14 (𝐹 Fn ℂ → (𝑟 ∈ (𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹𝑟) = 0)))
7775, 76syl 17 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (𝑟 ∈ (𝐹 “ {0}) ↔ (𝑟 ∈ ℂ ∧ (𝐹𝑟) = 0)))
7869, 70, 77mpbir2and 958 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → 𝑟 ∈ (𝐹 “ {0}))
79 eqid 2605 . . . . . . . . . . . 12 (abs‘(𝐴𝑟)) = (abs‘(𝐴𝑟))
80 oveq2 6531 . . . . . . . . . . . . . . 15 (𝑏 = 𝑟 → (𝐴𝑏) = (𝐴𝑟))
8180fveq2d 6088 . . . . . . . . . . . . . 14 (𝑏 = 𝑟 → (abs‘(𝐴𝑏)) = (abs‘(𝐴𝑟)))
8281eqeq2d 2615 . . . . . . . . . . . . 13 (𝑏 = 𝑟 → ((abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏)) ↔ (abs‘(𝐴𝑟)) = (abs‘(𝐴𝑟))))
8382rspcev 3277 . . . . . . . . . . . 12 ((𝑟 ∈ (𝐹 “ {0}) ∧ (abs‘(𝐴𝑟)) = (abs‘(𝐴𝑟))) → ∃𝑏 ∈ (𝐹 “ {0})(abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏)))
8478, 79, 83sylancl 692 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → ∃𝑏 ∈ (𝐹 “ {0})(abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏)))
85 eqeq1 2609 . . . . . . . . . . . . 13 (𝑎 = (abs‘(𝐴𝑟)) → (𝑎 = (abs‘(𝐴𝑏)) ↔ (abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏))))
8685rexbidv 3029 . . . . . . . . . . . 12 (𝑎 = (abs‘(𝐴𝑟)) → (∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏)) ↔ ∃𝑏 ∈ (𝐹 “ {0})(abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏))))
8786elrab 3326 . . . . . . . . . . 11 ((abs‘(𝐴𝑟)) ∈ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} ↔ ((abs‘(𝐴𝑟)) ∈ ℝ+ ∧ ∃𝑏 ∈ (𝐹 “ {0})(abs‘(𝐴𝑟)) = (abs‘(𝐴𝑏))))
8868, 84, 87sylanbrc 694 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴𝑟)) ∈ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})
89 elun2 3738 . . . . . . . . . 10 ((abs‘(𝐴𝑟)) ∈ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))} → (abs‘(𝐴𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
9088, 89syl 17 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → (abs‘(𝐴𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}))
91 infrelb 10851 . . . . . . . . 9 ((({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}) ⊆ ℝ ∧ ∃𝑐 ∈ ℝ ∀𝑑 ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})𝑐𝑑 ∧ (abs‘(𝐴𝑟)) ∈ ({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))})) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))
9242, 54, 90, 91syl3anc 1317 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ) ∧ ((𝐹𝑟) = 0 ∧ ¬ 𝐴 = 𝑟)) → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))
9392expr 640 . . . . . . 7 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → (¬ 𝐴 = 𝑟 → inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))
9493orrd 391 . . . . . 6 (((𝜑𝑟 ∈ ℝ) ∧ (𝐹𝑟) = 0) → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))
9594ex 448 . . . . 5 ((𝜑𝑟 ∈ ℝ) → ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))))
9695ralrimiva 2944 . . . 4 (𝜑 → ∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))))
97 breq1 4576 . . . . . . . 8 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → (𝑥 ≤ (abs‘(𝐴𝑟)) ↔ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))
9897orbi2d 733 . . . . . . 7 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → ((𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟))) ↔ (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟)))))
9998imbi2d 328 . . . . . 6 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → (((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) ↔ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))))
10099ralbidv 2964 . . . . 5 (𝑥 = inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) → (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) ↔ ∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))))
101100rspcev 3277 . . . 4 ((inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ∈ ℝ+ ∧ ∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟 ∨ inf(({1} ∪ {𝑎 ∈ ℝ+ ∣ ∃𝑏 ∈ (𝐹 “ {0})𝑎 = (abs‘(𝐴𝑏))}), ℝ, < ) ≤ (abs‘(𝐴𝑟))))) → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))))
10241, 96, 101syl2anc 690 . . 3 (𝜑 → ∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))))
103 znq 11620 . . . . . . . 8 ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℚ)
104 qre 11621 . . . . . . . 8 ((𝑝 / 𝑞) ∈ ℚ → (𝑝 / 𝑞) ∈ ℝ)
105103, 104syl 17 . . . . . . 7 ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (𝑝 / 𝑞) ∈ ℝ)
106 fveq2 6084 . . . . . . . . . 10 (𝑟 = (𝑝 / 𝑞) → (𝐹𝑟) = (𝐹‘(𝑝 / 𝑞)))
107106eqeq1d 2607 . . . . . . . . 9 (𝑟 = (𝑝 / 𝑞) → ((𝐹𝑟) = 0 ↔ (𝐹‘(𝑝 / 𝑞)) = 0))
108 eqeq2 2616 . . . . . . . . . 10 (𝑟 = (𝑝 / 𝑞) → (𝐴 = 𝑟𝐴 = (𝑝 / 𝑞)))
109 oveq2 6531 . . . . . . . . . . . 12 (𝑟 = (𝑝 / 𝑞) → (𝐴𝑟) = (𝐴 − (𝑝 / 𝑞)))
110109fveq2d 6088 . . . . . . . . . . 11 (𝑟 = (𝑝 / 𝑞) → (abs‘(𝐴𝑟)) = (abs‘(𝐴 − (𝑝 / 𝑞))))
111110breq2d 4585 . . . . . . . . . 10 (𝑟 = (𝑝 / 𝑞) → (𝑥 ≤ (abs‘(𝐴𝑟)) ↔ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
112108, 111orbi12d 741 . . . . . . . . 9 (𝑟 = (𝑝 / 𝑞) → ((𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟))) ↔ (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
113107, 112imbi12d 332 . . . . . . . 8 (𝑟 = (𝑝 / 𝑞) → (((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) ↔ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
114113rspcv 3273 . . . . . . 7 ((𝑝 / 𝑞) ∈ ℝ → (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
115105, 114syl 17 . . . . . 6 ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
116115com12 32 . . . . 5 (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ((𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
117116ralrimivv 2948 . . . 4 (∀𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
118117reximi 2989 . . 3 (∃𝑥 ∈ ℝ+𝑟 ∈ ℝ ((𝐹𝑟) = 0 → (𝐴 = 𝑟𝑥 ≤ (abs‘(𝐴𝑟)))) → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
119102, 118syl 17 . 2 (𝜑 → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
120 simplr 787 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ+)
121 simprr 791 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑞 ∈ ℕ)
12210nnnn0d 11194 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℕ0)
123122ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑁 ∈ ℕ0)
124121, 123nnexpcld 12843 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞𝑁) ∈ ℕ)
125124nnrpd 11698 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑞𝑁) ∈ ℝ+)
126120, 125rpdivcld 11717 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞𝑁)) ∈ ℝ+)
127126rpred 11700 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞𝑁)) ∈ ℝ)
128127adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞𝑁)) ∈ ℝ)
129 simpllr 794 . . . . . . . . 9 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ+)
130129rpred 11700 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ∈ ℝ)
13155ad2antrr 757 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝐴 ∈ ℝ)
132105adantl 480 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑝 / 𝑞) ∈ ℝ)
133131, 132resubcld 10305 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℝ)
134133recnd 9920 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝐴 − (𝑝 / 𝑞)) ∈ ℂ)
135134abscld 13965 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
136135adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (abs‘(𝐴 − (𝑝 / 𝑞))) ∈ ℝ)
137 rpre 11667 . . . . . . . . . . 11 (𝑥 ∈ ℝ+𝑥 ∈ ℝ)
138137ad2antlr 758 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 𝑥 ∈ ℝ)
139120rpcnne0d 11709 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
140 divid 10559 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥 / 𝑥) = 1)
141139, 140syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) = 1)
142124nnge1d 10906 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → 1 ≤ (𝑞𝑁))
143141, 142eqbrtrd 4595 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / 𝑥) ≤ (𝑞𝑁))
144138, 120, 125, 143lediv23d 11766 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 / (𝑞𝑁)) ≤ 𝑥)
145144adantr 479 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞𝑁)) ≤ 𝑥)
146 simpr 475 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
147128, 130, 136, 145, 146letrd 10041 . . . . . . 7 ((((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) ∧ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))
148147ex 448 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))) → (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))
149148orim2d 880 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → ((𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))) → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
150149imim2d 54 . . . 4 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ)) → (((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
151150ralimdvva 2942 . . 3 ((𝜑𝑥 ∈ ℝ+) → (∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∀𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
152151reximdva 2995 . 2 (𝜑 → (∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ 𝑥 ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))) → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞)))))))
153119, 152mpd 15 1 (𝜑 → ∃𝑥 ∈ ℝ+𝑝 ∈ ℤ ∀𝑞 ∈ ℕ ((𝐹‘(𝑝 / 𝑞)) = 0 → (𝐴 = (𝑝 / 𝑞) ∨ (𝑥 / (𝑞𝑁)) ≤ (abs‘(𝐴 − (𝑝 / 𝑞))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382   = wceq 1474  wcel 1975  {cab 2591  wne 2775  wral 2891  wrex 2892  {crab 2895  cun 3533  wss 3535  c0 3869  {csn 4120   class class class wbr 4573   Or wor 4944  ccnv 5023  cima 5027   Fn wfn 5781  wf 5782  cfv 5786  (class class class)co 6523  Fincfn 7814  infcinf 8203  cc 9786  cr 9787  0cc0 9788  1c1 9789   < clt 9926  cle 9927  cmin 10113   / cdiv 10529  cn 10863  0cn0 11135  cz 11206  cq 11616  +crp 11660  cexp 12673  #chash 12930  abscabs 13764  0𝑝c0p 23155  Polycply 23657  degcdgr 23660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-inf2 8394  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865  ax-pre-sup 9866  ax-addf 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rmo 2899  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-se 4984  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-isom 5795  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-of 6768  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-oadd 7424  df-er 7602  df-map 7719  df-pm 7720  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-sup 8204  df-inf 8205  df-oi 8271  df-card 8621  df-cda 8846  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-div 10530  df-nn 10864  df-2 10922  df-3 10923  df-n0 11136  df-z 11207  df-uz 11516  df-q 11617  df-rp 11661  df-fz 12149  df-fzo 12286  df-fl 12406  df-seq 12615  df-exp 12674  df-hash 12931  df-cj 13629  df-re 13630  df-im 13631  df-sqrt 13765  df-abs 13766  df-clim 14009  df-rlim 14010  df-sum 14207  df-0p 23156  df-ply 23661  df-idp 23662  df-coe 23663  df-dgr 23664  df-quot 23763
This theorem is referenced by:  aalioulem6  23809
  Copyright terms: Public domain W3C validator