Users' Mathboxes Mathbox for Steve Rodriguez < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvgrat Structured version   Visualization version   GIF version

Theorem dvgrat 43780
Description: Ratio test for divergence of a complex infinite series. See e.g. remark "if (abs‘((𝑎‘(𝑛 + 1)) / (𝑎𝑛))) ≥ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test. (Contributed by Steve Rodriguez, 28-Feb-2020.)
Hypotheses
Ref Expression
dvgrat.z 𝑍 = (ℤ𝑀)
dvgrat.w 𝑊 = (ℤ𝑁)
dvgrat.n (𝜑𝑁𝑍)
dvgrat.f (𝜑𝐹𝑉)
dvgrat.c ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
dvgrat.n0 ((𝜑𝑘𝑊) → (𝐹𝑘) ≠ 0)
dvgrat.le ((𝜑𝑘𝑊) → (abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
Assertion
Ref Expression
dvgrat (𝜑 → seq𝑀( + , 𝐹) ∉ dom ⇝ )
Distinct variable groups:   𝜑,𝑘   𝑘,𝐹   𝑘,𝑁   𝑘,𝑊   𝑘,𝑀   𝑘,𝑉   𝑘,𝑍

Proof of Theorem dvgrat
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 dvgrat.n . . . . . . . . 9 (𝜑𝑁𝑍)
2 dvgrat.z . . . . . . . . 9 𝑍 = (ℤ𝑀)
31, 2eleqtrdi 2839 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ𝑀))
4 eluzelz 12870 . . . . . . . 8 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
53, 4syl 17 . . . . . . 7 (𝜑𝑁 ∈ ℤ)
6 uzid 12875 . . . . . . . 8 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
7 dvgrat.w . . . . . . . 8 𝑊 = (ℤ𝑁)
86, 7eleqtrrdi 2840 . . . . . . 7 (𝑁 ∈ ℤ → 𝑁𝑊)
95, 8syl 17 . . . . . 6 (𝜑𝑁𝑊)
10 simpr 483 . . . . . . . . 9 ((𝜑𝑘 = 𝑁) → 𝑘 = 𝑁)
1110eleq1d 2814 . . . . . . . 8 ((𝜑𝑘 = 𝑁) → (𝑘𝑊𝑁𝑊))
1210fveq2d 6906 . . . . . . . . . 10 ((𝜑𝑘 = 𝑁) → (𝐹𝑘) = (𝐹𝑁))
1312fveq2d 6906 . . . . . . . . 9 ((𝜑𝑘 = 𝑁) → (abs‘(𝐹𝑘)) = (abs‘(𝐹𝑁)))
1413breq2d 5164 . . . . . . . 8 ((𝜑𝑘 = 𝑁) → (0 < (abs‘(𝐹𝑘)) ↔ 0 < (abs‘(𝐹𝑁))))
1511, 14imbi12d 343 . . . . . . 7 ((𝜑𝑘 = 𝑁) → ((𝑘𝑊 → 0 < (abs‘(𝐹𝑘))) ↔ (𝑁𝑊 → 0 < (abs‘(𝐹𝑁)))))
16 dvgrat.n0 . . . . . . . . 9 ((𝜑𝑘𝑊) → (𝐹𝑘) ≠ 0)
177eleq2i 2821 . . . . . . . . . . . . 13 (𝑘𝑊𝑘 ∈ (ℤ𝑁))
182uztrn2 12879 . . . . . . . . . . . . 13 ((𝑁𝑍𝑘 ∈ (ℤ𝑁)) → 𝑘𝑍)
1917, 18sylan2b 592 . . . . . . . . . . . 12 ((𝑁𝑍𝑘𝑊) → 𝑘𝑍)
201, 19sylan 578 . . . . . . . . . . 11 ((𝜑𝑘𝑊) → 𝑘𝑍)
21 dvgrat.c . . . . . . . . . . 11 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
2220, 21syldan 589 . . . . . . . . . 10 ((𝜑𝑘𝑊) → (𝐹𝑘) ∈ ℂ)
23 absgt0 15311 . . . . . . . . . 10 ((𝐹𝑘) ∈ ℂ → ((𝐹𝑘) ≠ 0 ↔ 0 < (abs‘(𝐹𝑘))))
2422, 23syl 17 . . . . . . . . 9 ((𝜑𝑘𝑊) → ((𝐹𝑘) ≠ 0 ↔ 0 < (abs‘(𝐹𝑘))))
2516, 24mpbid 231 . . . . . . . 8 ((𝜑𝑘𝑊) → 0 < (abs‘(𝐹𝑘)))
2625ex 411 . . . . . . 7 (𝜑 → (𝑘𝑊 → 0 < (abs‘(𝐹𝑘))))
271, 15, 26vtocld 3547 . . . . . 6 (𝜑 → (𝑁𝑊 → 0 < (abs‘(𝐹𝑁))))
289, 27mpd 15 . . . . 5 (𝜑 → 0 < (abs‘(𝐹𝑁)))
29 0red 11255 . . . . . 6 (𝜑 → 0 ∈ ℝ)
3010eleq1d 2814 . . . . . . . . . 10 ((𝜑𝑘 = 𝑁) → (𝑘𝑍𝑁𝑍))
3112eleq1d 2814 . . . . . . . . . 10 ((𝜑𝑘 = 𝑁) → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑁) ∈ ℂ))
3230, 31imbi12d 343 . . . . . . . . 9 ((𝜑𝑘 = 𝑁) → ((𝑘𝑍 → (𝐹𝑘) ∈ ℂ) ↔ (𝑁𝑍 → (𝐹𝑁) ∈ ℂ)))
3321ex 411 . . . . . . . . 9 (𝜑 → (𝑘𝑍 → (𝐹𝑘) ∈ ℂ))
341, 32, 33vtocld 3547 . . . . . . . 8 (𝜑 → (𝑁𝑍 → (𝐹𝑁) ∈ ℂ))
351, 34mpd 15 . . . . . . 7 (𝜑 → (𝐹𝑁) ∈ ℂ)
3635abscld 15423 . . . . . 6 (𝜑 → (abs‘(𝐹𝑁)) ∈ ℝ)
3729, 36ltnled 11399 . . . . 5 (𝜑 → (0 < (abs‘(𝐹𝑁)) ↔ ¬ (abs‘(𝐹𝑁)) ≤ 0))
3828, 37mpbid 231 . . . 4 (𝜑 → ¬ (abs‘(𝐹𝑁)) ≤ 0)
395adantr 479 . . . . 5 ((𝜑𝐹 ⇝ 0) → 𝑁 ∈ ℤ)
4036adantr 479 . . . . 5 ((𝜑𝐹 ⇝ 0) → (abs‘(𝐹𝑁)) ∈ ℝ)
41 simpr 483 . . . . . . 7 ((𝜑𝐹 ⇝ 0) → 𝐹 ⇝ 0)
427fvexi 6916 . . . . . . . . 9 𝑊 ∈ V
4342mptex 7241 . . . . . . . 8 (𝑖𝑊 ↦ (abs‘(𝐹𝑖))) ∈ V
4443a1i 11 . . . . . . 7 ((𝜑𝐹 ⇝ 0) → (𝑖𝑊 ↦ (abs‘(𝐹𝑖))) ∈ V)
4522adantlr 713 . . . . . . 7 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → (𝐹𝑘) ∈ ℂ)
46 eqidd 2729 . . . . . . . 8 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → (𝑖𝑊 ↦ (abs‘(𝐹𝑖))) = (𝑖𝑊 ↦ (abs‘(𝐹𝑖))))
47 simpr 483 . . . . . . . . . 10 ((((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) ∧ 𝑖 = 𝑘) → 𝑖 = 𝑘)
4847fveq2d 6906 . . . . . . . . 9 ((((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) ∧ 𝑖 = 𝑘) → (𝐹𝑖) = (𝐹𝑘))
4948fveq2d 6906 . . . . . . . 8 ((((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) ∧ 𝑖 = 𝑘) → (abs‘(𝐹𝑖)) = (abs‘(𝐹𝑘)))
50 simpr 483 . . . . . . . 8 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → 𝑘𝑊)
51 fvex 6915 . . . . . . . . 9 (abs‘(𝐹𝑘)) ∈ V
5251a1i 11 . . . . . . . 8 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → (abs‘(𝐹𝑘)) ∈ V)
5346, 49, 50, 52fvmptd 7017 . . . . . . 7 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → ((𝑖𝑊 ↦ (abs‘(𝐹𝑖)))‘𝑘) = (abs‘(𝐹𝑘)))
547, 41, 44, 39, 45, 53climabs 15588 . . . . . 6 ((𝜑𝐹 ⇝ 0) → (𝑖𝑊 ↦ (abs‘(𝐹𝑖))) ⇝ (abs‘0))
55 abs0 15272 . . . . . 6 (abs‘0) = 0
5654, 55breqtrdi 5193 . . . . 5 ((𝜑𝐹 ⇝ 0) → (𝑖𝑊 ↦ (abs‘(𝐹𝑖))) ⇝ 0)
5745abscld 15423 . . . . . 6 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → (abs‘(𝐹𝑘)) ∈ ℝ)
5853, 57eqeltrd 2829 . . . . 5 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → ((𝑖𝑊 ↦ (abs‘(𝐹𝑖)))‘𝑘) ∈ ℝ)
59 2fveq3 6907 . . . . . . . . . . . 12 (𝑖 = 𝑁 → (abs‘(𝐹𝑖)) = (abs‘(𝐹𝑁)))
6059breq2d 5164 . . . . . . . . . . 11 (𝑖 = 𝑁 → ((abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑖)) ↔ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑁))))
6160imbi2d 339 . . . . . . . . . 10 (𝑖 = 𝑁 → ((𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑖))) ↔ (𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑁)))))
62 2fveq3 6907 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (abs‘(𝐹𝑖)) = (abs‘(𝐹𝑘)))
6362breq2d 5164 . . . . . . . . . . 11 (𝑖 = 𝑘 → ((abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑖)) ↔ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))))
6463imbi2d 339 . . . . . . . . . 10 (𝑖 = 𝑘 → ((𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑖))) ↔ (𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)))))
65 2fveq3 6907 . . . . . . . . . . . 12 (𝑖 = (𝑘 + 1) → (abs‘(𝐹𝑖)) = (abs‘(𝐹‘(𝑘 + 1))))
6665breq2d 5164 . . . . . . . . . . 11 (𝑖 = (𝑘 + 1) → ((abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑖)) ↔ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
6766imbi2d 339 . . . . . . . . . 10 (𝑖 = (𝑘 + 1) → ((𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑖))) ↔ (𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹‘(𝑘 + 1))))))
6836adantr 479 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ ℤ) → (abs‘(𝐹𝑁)) ∈ ℝ)
6968leidd 11818 . . . . . . . . . . 11 ((𝜑𝑁 ∈ ℤ) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑁)))
7069expcom 412 . . . . . . . . . 10 (𝑁 ∈ ℤ → (𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑁))))
7136ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (abs‘(𝐹𝑁)) ∈ ℝ)
7222adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (𝐹𝑘) ∈ ℂ)
7372abscld 15423 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (abs‘(𝐹𝑘)) ∈ ℝ)
747peano2uzs 12924 . . . . . . . . . . . . . . . . . 18 (𝑘𝑊 → (𝑘 + 1) ∈ 𝑊)
75 ovex 7459 . . . . . . . . . . . . . . . . . . 19 (𝑘 + 1) ∈ V
76 eleq1 2817 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑘 + 1) → (𝑖𝑊 ↔ (𝑘 + 1) ∈ 𝑊))
7776anbi2d 628 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = (𝑘 + 1) → ((𝜑𝑖𝑊) ↔ (𝜑 ∧ (𝑘 + 1) ∈ 𝑊)))
78 fveq2 6902 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = (𝑘 + 1) → (𝐹𝑖) = (𝐹‘(𝑘 + 1)))
7978eleq1d 2814 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = (𝑘 + 1) → ((𝐹𝑖) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
8077, 79imbi12d 343 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑘 + 1) → (((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)))
81 eleq1 2817 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → (𝑘𝑊𝑖𝑊))
8281anbi2d 628 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → ((𝜑𝑘𝑊) ↔ (𝜑𝑖𝑊)))
83 fveq2 6902 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
8483eleq1d 2814 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑖) ∈ ℂ))
8582, 84imbi12d 343 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (((𝜑𝑘𝑊) → (𝐹𝑘) ∈ ℂ) ↔ ((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ)))
8685, 22chvarvv 1994 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖𝑊) → (𝐹𝑖) ∈ ℂ)
8775, 80, 86vtocl 3545 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
8874, 87sylan2 591 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
8988adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
9089abscld 15423 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
91 simpr 483 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)))
92 dvgrat.le . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑊) → (abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
9392adantr 479 . . . . . . . . . . . . . . 15 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (abs‘(𝐹𝑘)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
9471, 73, 90, 91, 93letrd 11409 . . . . . . . . . . . . . 14 (((𝜑𝑘𝑊) ∧ (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹‘(𝑘 + 1))))
9594ex 411 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → ((abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
9617, 95sylan2br 593 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (ℤ𝑁)) → ((abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹‘(𝑘 + 1)))))
9796expcom 412 . . . . . . . . . . 11 (𝑘 ∈ (ℤ𝑁) → (𝜑 → ((abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹‘(𝑘 + 1))))))
9897a2d 29 . . . . . . . . . 10 (𝑘 ∈ (ℤ𝑁) → ((𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))) → (𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹‘(𝑘 + 1))))))
9961, 64, 67, 64, 70, 98uzind4 12928 . . . . . . . . 9 (𝑘 ∈ (ℤ𝑁) → (𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘))))
10099impcom 406 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑁)) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)))
10117, 100sylan2b 592 . . . . . . 7 ((𝜑𝑘𝑊) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)))
102101adantlr 713 . . . . . 6 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑘)))
103102, 53breqtrrd 5180 . . . . 5 (((𝜑𝐹 ⇝ 0) ∧ 𝑘𝑊) → (abs‘(𝐹𝑁)) ≤ ((𝑖𝑊 ↦ (abs‘(𝐹𝑖)))‘𝑘))
1047, 39, 40, 56, 58, 103climlec2 15645 . . . 4 ((𝜑𝐹 ⇝ 0) → (abs‘(𝐹𝑁)) ≤ 0)
10538, 104mtand 814 . . 3 (𝜑 → ¬ 𝐹 ⇝ 0)
106 eluzel2 12865 . . . . . 6 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
1073, 106syl 17 . . . . 5 (𝜑𝑀 ∈ ℤ)
108107adantr 479 . . . 4 ((𝜑 ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → 𝑀 ∈ ℤ)
109 dvgrat.f . . . . 5 (𝜑𝐹𝑉)
110109adantr 479 . . . 4 ((𝜑 ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → 𝐹𝑉)
111 simpr 483 . . . 4 ((𝜑 ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → seq𝑀( + , 𝐹) ∈ dom ⇝ )
11221adantlr 713 . . . 4 (((𝜑 ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) ∧ 𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
1132, 108, 110, 111, 112serf0 15667 . . 3 ((𝜑 ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → 𝐹 ⇝ 0)
114105, 113mtand 814 . 2 (𝜑 → ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
115 df-nel 3044 . 2 (seq𝑀( + , 𝐹) ∉ dom ⇝ ↔ ¬ seq𝑀( + , 𝐹) ∈ dom ⇝ )
116114, 115sylibr 233 1 (𝜑 → seq𝑀( + , 𝐹) ∉ dom ⇝ )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  wne 2937  wnel 3043  Vcvv 3473   class class class wbr 5152  cmpt 5235  dom cdm 5682  cfv 6553  (class class class)co 7426  cc 11144  cr 11145  0cc0 11146  1c1 11147   + caddc 11149   < clt 11286  cle 11287  cz 12596  cuz 12860  seqcseq 14006  abscabs 15221  cli 15468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11202  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222  ax-pre-mulgt0 11223  ax-pre-sup 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7877  df-1st 7999  df-2nd 8000  df-frecs 8293  df-wrecs 8324  df-recs 8398  df-rdg 8437  df-er 8731  df-pm 8854  df-en 8971  df-dom 8972  df-sdom 8973  df-sup 9473  df-inf 9474  df-pnf 11288  df-mnf 11289  df-xr 11290  df-ltxr 11291  df-le 11292  df-sub 11484  df-neg 11485  df-div 11910  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-z 12597  df-uz 12861  df-rp 13015  df-ico 13370  df-fz 13525  df-fl 13797  df-seq 14007  df-exp 14067  df-cj 15086  df-re 15087  df-im 15088  df-sqrt 15222  df-abs 15223  df-limsup 15455  df-clim 15472  df-rlim 15473
This theorem is referenced by:  cvgdvgrat  43781
  Copyright terms: Public domain W3C validator