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

Theorem cvgrat 15022
 Description: Ratio test for convergence of a complex infinite series. If the ratio 𝐴 of the absolute values of successive terms in an infinite sequence 𝐹 is less than 1 for all terms beyond some index 𝐵, then the infinite sum of the terms of 𝐹 converges to a complex number. Equivalent to first part of Exercise 4 of [Gleason] p. 182. (Contributed by NM, 26-Apr-2005.) (Proof shortened by Mario Carneiro, 27-Apr-2014.)
Hypotheses
Ref Expression
cvgrat.1 𝑍 = (ℤ𝑀)
cvgrat.2 𝑊 = (ℤ𝑁)
cvgrat.3 (𝜑𝐴 ∈ ℝ)
cvgrat.4 (𝜑𝐴 < 1)
cvgrat.5 (𝜑𝑁𝑍)
cvgrat.6 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
cvgrat.7 ((𝜑𝑘𝑊) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
Assertion
Ref Expression
cvgrat (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
Distinct variable groups:   𝐴,𝑘   𝑘,𝐹   𝑘,𝑀   𝑘,𝑁   𝜑,𝑘   𝑘,𝑊   𝑘,𝑍

Proof of Theorem cvgrat
Dummy variable 𝑛 is distinct from all other variables.
StepHypRef Expression
1 cvgrat.2 . . 3 𝑊 = (ℤ𝑁)
2 cvgrat.5 . . . . . . 7 (𝜑𝑁𝑍)
3 cvgrat.1 . . . . . . 7 𝑍 = (ℤ𝑀)
42, 3syl6eleq 2869 . . . . . 6 (𝜑𝑁 ∈ (ℤ𝑀))
5 eluzelz 12006 . . . . . 6 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
64, 5syl 17 . . . . 5 (𝜑𝑁 ∈ ℤ)
7 uzid 12011 . . . . 5 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
86, 7syl 17 . . . 4 (𝜑𝑁 ∈ (ℤ𝑁))
98, 1syl6eleqr 2870 . . 3 (𝜑𝑁𝑊)
10 oveq1 6931 . . . . . . 7 (𝑛 = 𝑘 → (𝑛𝑁) = (𝑘𝑁))
1110oveq2d 6940 . . . . . 6 (𝑛 = 𝑘 → (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))
12 eqid 2778 . . . . . 6 (𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁))) = (𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))
13 ovex 6956 . . . . . 6 (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)) ∈ V
1411, 12, 13fvmpt 6544 . . . . 5 (𝑘𝑊 → ((𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))‘𝑘) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))
1514adantl 475 . . . 4 ((𝜑𝑘𝑊) → ((𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))‘𝑘) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))
16 0re 10380 . . . . . . 7 0 ∈ ℝ
17 cvgrat.3 . . . . . . 7 (𝜑𝐴 ∈ ℝ)
18 ifcl 4351 . . . . . . 7 ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → if(𝐴 ≤ 0, 0, 𝐴) ∈ ℝ)
1916, 17, 18sylancr 581 . . . . . 6 (𝜑 → if(𝐴 ≤ 0, 0, 𝐴) ∈ ℝ)
2019adantr 474 . . . . 5 ((𝜑𝑘𝑊) → if(𝐴 ≤ 0, 0, 𝐴) ∈ ℝ)
21 simpr 479 . . . . . . 7 ((𝜑𝑘𝑊) → 𝑘𝑊)
2221, 1syl6eleq 2869 . . . . . 6 ((𝜑𝑘𝑊) → 𝑘 ∈ (ℤ𝑁))
23 uznn0sub 12029 . . . . . 6 (𝑘 ∈ (ℤ𝑁) → (𝑘𝑁) ∈ ℕ0)
2422, 23syl 17 . . . . 5 ((𝜑𝑘𝑊) → (𝑘𝑁) ∈ ℕ0)
2520, 24reexpcld 13348 . . . 4 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)) ∈ ℝ)
2615, 25eqeltrd 2859 . . 3 ((𝜑𝑘𝑊) → ((𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))‘𝑘) ∈ ℝ)
27 uzss 12017 . . . . . . 7 (𝑁 ∈ (ℤ𝑀) → (ℤ𝑁) ⊆ (ℤ𝑀))
284, 27syl 17 . . . . . 6 (𝜑 → (ℤ𝑁) ⊆ (ℤ𝑀))
2928, 1, 33sstr4g 3865 . . . . 5 (𝜑𝑊𝑍)
3029sselda 3821 . . . 4 ((𝜑𝑘𝑊) → 𝑘𝑍)
31 cvgrat.6 . . . 4 ((𝜑𝑘𝑍) → (𝐹𝑘) ∈ ℂ)
3230, 31syldan 585 . . 3 ((𝜑𝑘𝑊) → (𝐹𝑘) ∈ ℂ)
3323adantl 475 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑁)) → (𝑘𝑁) ∈ ℕ0)
34 oveq2 6932 . . . . . . . . 9 (𝑛 = (𝑘𝑁) → (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))
35 eqid 2778 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))
3634, 35, 13fvmpt 6544 . . . . . . . 8 ((𝑘𝑁) ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))‘(𝑘𝑁)) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))
3733, 36syl 17 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑁)) → ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))‘(𝑘𝑁)) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))
386zcnd 11839 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
39 eluzelz 12006 . . . . . . . . 9 (𝑘 ∈ (ℤ𝑁) → 𝑘 ∈ ℤ)
4039zcnd 11839 . . . . . . . 8 (𝑘 ∈ (ℤ𝑁) → 𝑘 ∈ ℂ)
41 nn0ex 11653 . . . . . . . . . 10 0 ∈ V
4241mptex 6760 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) ∈ V
4342shftval 14225 . . . . . . . 8 ((𝑁 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) shift 𝑁)‘𝑘) = ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))‘(𝑘𝑁)))
4438, 40, 43syl2an 589 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑁)) → (((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) shift 𝑁)‘𝑘) = ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))‘(𝑘𝑁)))
45 simpr 479 . . . . . . . . 9 ((𝜑𝑘 ∈ (ℤ𝑁)) → 𝑘 ∈ (ℤ𝑁))
4645, 1syl6eleqr 2870 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑁)) → 𝑘𝑊)
4746, 14syl 17 . . . . . . 7 ((𝜑𝑘 ∈ (ℤ𝑁)) → ((𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))‘𝑘) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))
4837, 44, 473eqtr4rd 2825 . . . . . 6 ((𝜑𝑘 ∈ (ℤ𝑁)) → ((𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))‘𝑘) = (((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) shift 𝑁)‘𝑘))
496, 48seqfeq 13148 . . . . 5 (𝜑 → seq𝑁( + , (𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))) = seq𝑁( + , ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) shift 𝑁)))
5042seqshft 14236 . . . . . 6 ((𝑁 ∈ ℤ ∧ 𝑁 ∈ ℤ) → seq𝑁( + , ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) shift 𝑁)) = (seq(𝑁𝑁)( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁))
516, 6, 50syl2anc 579 . . . . 5 (𝜑 → seq𝑁( + , ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛)) shift 𝑁)) = (seq(𝑁𝑁)( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁))
5238subidd 10724 . . . . . . 7 (𝜑 → (𝑁𝑁) = 0)
5352seqeq1d 13129 . . . . . 6 (𝜑 → seq(𝑁𝑁)( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) = seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))))
5453oveq1d 6939 . . . . 5 (𝜑 → (seq(𝑁𝑁)( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) = (seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁))
5549, 51, 543eqtrd 2818 . . . 4 (𝜑 → seq𝑁( + , (𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))) = (seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁))
5619recnd 10407 . . . . . . 7 (𝜑 → if(𝐴 ≤ 0, 0, 𝐴) ∈ ℂ)
57 max2 12334 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → 0 ≤ if(𝐴 ≤ 0, 0, 𝐴))
5817, 16, 57sylancl 580 . . . . . . . . 9 (𝜑 → 0 ≤ if(𝐴 ≤ 0, 0, 𝐴))
5919, 58absidd 14573 . . . . . . . 8 (𝜑 → (abs‘if(𝐴 ≤ 0, 0, 𝐴)) = if(𝐴 ≤ 0, 0, 𝐴))
60 0lt1 10899 . . . . . . . . 9 0 < 1
61 cvgrat.4 . . . . . . . . 9 (𝜑𝐴 < 1)
62 breq1 4891 . . . . . . . . . 10 (0 = if(𝐴 ≤ 0, 0, 𝐴) → (0 < 1 ↔ if(𝐴 ≤ 0, 0, 𝐴) < 1))
63 breq1 4891 . . . . . . . . . 10 (𝐴 = if(𝐴 ≤ 0, 0, 𝐴) → (𝐴 < 1 ↔ if(𝐴 ≤ 0, 0, 𝐴) < 1))
6462, 63ifboth 4345 . . . . . . . . 9 ((0 < 1 ∧ 𝐴 < 1) → if(𝐴 ≤ 0, 0, 𝐴) < 1)
6560, 61, 64sylancr 581 . . . . . . . 8 (𝜑 → if(𝐴 ≤ 0, 0, 𝐴) < 1)
6659, 65eqbrtrd 4910 . . . . . . 7 (𝜑 → (abs‘if(𝐴 ≤ 0, 0, 𝐴)) < 1)
67 oveq2 6932 . . . . . . . . 9 (𝑛 = 𝑘 → (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛) = (if(𝐴 ≤ 0, 0, 𝐴)↑𝑘))
68 ovex 6956 . . . . . . . . 9 (if(𝐴 ≤ 0, 0, 𝐴)↑𝑘) ∈ V
6967, 35, 68fvmpt 6544 . . . . . . . 8 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))‘𝑘) = (if(𝐴 ≤ 0, 0, 𝐴)↑𝑘))
7069adantl 475 . . . . . . 7 ((𝜑𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))‘𝑘) = (if(𝐴 ≤ 0, 0, 𝐴)↑𝑘))
7156, 66, 70geolim 15009 . . . . . 6 (𝜑 → seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) ⇝ (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴))))
72 seqex 13125 . . . . . . 7 seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) ∈ V
73 climshft 14719 . . . . . . 7 ((𝑁 ∈ ℤ ∧ seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) ∈ V) → ((seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) ⇝ (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴))) ↔ seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) ⇝ (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴)))))
746, 72, 73sylancl 580 . . . . . 6 (𝜑 → ((seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) ⇝ (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴))) ↔ seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) ⇝ (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴)))))
7571, 74mpbird 249 . . . . 5 (𝜑 → (seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) ⇝ (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴))))
76 ovex 6956 . . . . . 6 (seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) ∈ V
77 ovex 6956 . . . . . 6 (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴))) ∈ V
7876, 77breldm 5576 . . . . 5 ((seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) ⇝ (1 / (1 − if(𝐴 ≤ 0, 0, 𝐴))) → (seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) ∈ dom ⇝ )
7975, 78syl 17 . . . 4 (𝜑 → (seq0( + , (𝑛 ∈ ℕ0 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑𝑛))) shift 𝑁) ∈ dom ⇝ )
8055, 79eqeltrd 2859 . . 3 (𝜑 → seq𝑁( + , (𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))) ∈ dom ⇝ )
81 fveq2 6448 . . . . . 6 (𝑘 = 𝑁 → (𝐹𝑘) = (𝐹𝑁))
8281eleq1d 2844 . . . . 5 (𝑘 = 𝑁 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑁) ∈ ℂ))
8331ralrimiva 3148 . . . . 5 (𝜑 → ∀𝑘𝑍 (𝐹𝑘) ∈ ℂ)
8482, 83, 2rspcdva 3517 . . . 4 (𝜑 → (𝐹𝑁) ∈ ℂ)
8584abscld 14587 . . 3 (𝜑 → (abs‘(𝐹𝑁)) ∈ ℝ)
86 2fveq3 6453 . . . . . . . 8 (𝑛 = 𝑁 → (abs‘(𝐹𝑛)) = (abs‘(𝐹𝑁)))
87 oveq1 6931 . . . . . . . . . 10 (𝑛 = 𝑁 → (𝑛𝑁) = (𝑁𝑁))
8887oveq2d 6940 . . . . . . . . 9 (𝑛 = 𝑁 → (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)) = (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁)))
8988oveq2d 6940 . . . . . . . 8 (𝑛 = 𝑁 → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁))) = ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁))))
9086, 89breq12d 4901 . . . . . . 7 (𝑛 = 𝑁 → ((abs‘(𝐹𝑛)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁))) ↔ (abs‘(𝐹𝑁)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁)))))
9190imbi2d 332 . . . . . 6 (𝑛 = 𝑁 → ((𝜑 → (abs‘(𝐹𝑛)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))) ↔ (𝜑 → (abs‘(𝐹𝑁)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁))))))
92 2fveq3 6453 . . . . . . . 8 (𝑛 = 𝑘 → (abs‘(𝐹𝑛)) = (abs‘(𝐹𝑘)))
9311oveq2d 6940 . . . . . . . 8 (𝑛 = 𝑘 → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁))) = ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))))
9492, 93breq12d 4901 . . . . . . 7 (𝑛 = 𝑘 → ((abs‘(𝐹𝑛)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁))) ↔ (abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))))
9594imbi2d 332 . . . . . 6 (𝑛 = 𝑘 → ((𝜑 → (abs‘(𝐹𝑛)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))) ↔ (𝜑 → (abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))))))
96 2fveq3 6453 . . . . . . . 8 (𝑛 = (𝑘 + 1) → (abs‘(𝐹𝑛)) = (abs‘(𝐹‘(𝑘 + 1))))
97 oveq1 6931 . . . . . . . . . 10 (𝑛 = (𝑘 + 1) → (𝑛𝑁) = ((𝑘 + 1) − 𝑁))
9897oveq2d 6940 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)) = (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))
9998oveq2d 6940 . . . . . . . 8 (𝑛 = (𝑘 + 1) → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁))) = ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))))
10096, 99breq12d 4901 . . . . . . 7 (𝑛 = (𝑘 + 1) → ((abs‘(𝐹𝑛)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁))) ↔ (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
101100imbi2d 332 . . . . . 6 (𝑛 = (𝑘 + 1) → ((𝜑 → (abs‘(𝐹𝑛)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))) ↔ (𝜑 → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))))))
10285leidd 10943 . . . . . . 7 (𝜑 → (abs‘(𝐹𝑁)) ≤ (abs‘(𝐹𝑁)))
10352oveq2d 6940 . . . . . . . . . 10 (𝜑 → (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁)) = (if(𝐴 ≤ 0, 0, 𝐴)↑0))
10456exp0d 13325 . . . . . . . . . 10 (𝜑 → (if(𝐴 ≤ 0, 0, 𝐴)↑0) = 1)
105103, 104eqtrd 2814 . . . . . . . . 9 (𝜑 → (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁)) = 1)
106105oveq2d 6940 . . . . . . . 8 (𝜑 → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁))) = ((abs‘(𝐹𝑁)) · 1))
10785recnd 10407 . . . . . . . . 9 (𝜑 → (abs‘(𝐹𝑁)) ∈ ℂ)
108107mulid1d 10396 . . . . . . . 8 (𝜑 → ((abs‘(𝐹𝑁)) · 1) = (abs‘(𝐹𝑁)))
109106, 108eqtrd 2814 . . . . . . 7 (𝜑 → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁))) = (abs‘(𝐹𝑁)))
110102, 109breqtrrd 4916 . . . . . 6 (𝜑 → (abs‘(𝐹𝑁)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑁𝑁))))
11132abscld 14587 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → (abs‘(𝐹𝑘)) ∈ ℝ)
11285adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → (abs‘(𝐹𝑁)) ∈ ℝ)
113112, 25remulcld 10409 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) ∈ ℝ)
11458adantr 474 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → 0 ≤ if(𝐴 ≤ 0, 0, 𝐴))
115 lemul2a 11234 . . . . . . . . . . . . 13 ((((abs‘(𝐹𝑘)) ∈ ℝ ∧ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) ∈ ℝ ∧ (if(𝐴 ≤ 0, 0, 𝐴) ∈ ℝ ∧ 0 ≤ if(𝐴 ≤ 0, 0, 𝐴))) ∧ (abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))) → (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))))
116115ex 403 . . . . . . . . . . . 12 (((abs‘(𝐹𝑘)) ∈ ℝ ∧ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) ∈ ℝ ∧ (if(𝐴 ≤ 0, 0, 𝐴) ∈ ℝ ∧ 0 ≤ if(𝐴 ≤ 0, 0, 𝐴))) → ((abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) → (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))))))
117111, 113, 20, 114, 116syl112anc 1442 . . . . . . . . . . 11 ((𝜑𝑘𝑊) → ((abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) → (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))))))
11856adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑊) → if(𝐴 ≤ 0, 0, 𝐴) ∈ ℂ)
119107adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑊) → (abs‘(𝐹𝑁)) ∈ ℂ)
12025recnd 10407 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)) ∈ ℂ)
121118, 119, 120mul12d 10587 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴) · ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))) = ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))))
122118, 24expp1d 13332 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘𝑁) + 1)) = ((if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)) · if(𝐴 ≤ 0, 0, 𝐴)))
12340, 1eleq2s 2877 . . . . . . . . . . . . . . . . 17 (𝑘𝑊𝑘 ∈ ℂ)
124 ax-1cn 10332 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
125 addsub 10636 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑘 + 1) − 𝑁) = ((𝑘𝑁) + 1))
126124, 125mp3an2 1522 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑘 + 1) − 𝑁) = ((𝑘𝑁) + 1))
127123, 38, 126syl2anr 590 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝑊) → ((𝑘 + 1) − 𝑁) = ((𝑘𝑁) + 1))
128127oveq2d 6940 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)) = (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘𝑁) + 1)))
129118, 120mulcomd 10400 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) = ((if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)) · if(𝐴 ≤ 0, 0, 𝐴)))
130122, 128, 1293eqtr4rd 2825 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) = (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))
131130oveq2d 6940 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))) = ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))))
132121, 131eqtrd 2814 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴) · ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))) = ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))))
133132breq2d 4900 . . . . . . . . . . 11 ((𝜑𝑘𝑊) → ((if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))) ↔ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
134117, 133sylibd 231 . . . . . . . . . 10 ((𝜑𝑘𝑊) → ((abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) → (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
135 fveq2 6448 . . . . . . . . . . . . . . 15 (𝑛 = (𝑘 + 1) → (𝐹𝑛) = (𝐹‘(𝑘 + 1)))
136135eleq1d 2844 . . . . . . . . . . . . . 14 (𝑛 = (𝑘 + 1) → ((𝐹𝑛) ∈ ℂ ↔ (𝐹‘(𝑘 + 1)) ∈ ℂ))
137 fveq2 6448 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
138137eleq1d 2844 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑛 → ((𝐹𝑘) ∈ ℂ ↔ (𝐹𝑛) ∈ ℂ))
139138cbvralv 3367 . . . . . . . . . . . . . . . 16 (∀𝑘𝑍 (𝐹𝑘) ∈ ℂ ↔ ∀𝑛𝑍 (𝐹𝑛) ∈ ℂ)
14083, 139sylib 210 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑛𝑍 (𝐹𝑛) ∈ ℂ)
141140adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑊) → ∀𝑛𝑍 (𝐹𝑛) ∈ ℂ)
1421peano2uzs 12052 . . . . . . . . . . . . . . 15 (𝑘𝑊 → (𝑘 + 1) ∈ 𝑊)
14329sselda 3821 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑘 + 1) ∈ 𝑊) → (𝑘 + 1) ∈ 𝑍)
144142, 143sylan2 586 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑊) → (𝑘 + 1) ∈ 𝑍)
145136, 141, 144rspcdva 3517 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → (𝐹‘(𝑘 + 1)) ∈ ℂ)
146145abscld 14587 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → (abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ)
14717adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → 𝐴 ∈ ℝ)
148147, 111remulcld 10409 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → (𝐴 · (abs‘(𝐹𝑘))) ∈ ℝ)
14920, 111remulcld 10409 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ∈ ℝ)
150 cvgrat.7 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹𝑘))))
15132absge0d 14595 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → 0 ≤ (abs‘(𝐹𝑘)))
152 max1 12332 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 0 ∈ ℝ) → 𝐴 ≤ if(𝐴 ≤ 0, 0, 𝐴))
15317, 16, 152sylancl 580 . . . . . . . . . . . . . 14 (𝜑𝐴 ≤ if(𝐴 ≤ 0, 0, 𝐴))
154153adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → 𝐴 ≤ if(𝐴 ≤ 0, 0, 𝐴))
155147, 20, 111, 151, 154lemul1ad 11319 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → (𝐴 · (abs‘(𝐹𝑘))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))))
156146, 148, 149, 150, 155letrd 10535 . . . . . . . . . . 11 ((𝜑𝑘𝑊) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))))
157 peano2uz 12051 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (ℤ𝑁) → (𝑘 + 1) ∈ (ℤ𝑁))
15822, 157syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝑊) → (𝑘 + 1) ∈ (ℤ𝑁))
159 uznn0sub 12029 . . . . . . . . . . . . . . 15 ((𝑘 + 1) ∈ (ℤ𝑁) → ((𝑘 + 1) − 𝑁) ∈ ℕ0)
160158, 159syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑘𝑊) → ((𝑘 + 1) − 𝑁) ∈ ℕ0)
16120, 160reexpcld 13348 . . . . . . . . . . . . 13 ((𝜑𝑘𝑊) → (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)) ∈ ℝ)
162112, 161remulcld 10409 . . . . . . . . . . . 12 ((𝜑𝑘𝑊) → ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))) ∈ ℝ)
163 letr 10472 . . . . . . . . . . . 12 (((abs‘(𝐹‘(𝑘 + 1))) ∈ ℝ ∧ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ∈ ℝ ∧ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))) ∈ ℝ) → (((abs‘(𝐹‘(𝑘 + 1))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ∧ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
164146, 149, 162, 163syl3anc 1439 . . . . . . . . . . 11 ((𝜑𝑘𝑊) → (((abs‘(𝐹‘(𝑘 + 1))) ≤ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ∧ (if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
165156, 164mpand 685 . . . . . . . . . 10 ((𝜑𝑘𝑊) → ((if(𝐴 ≤ 0, 0, 𝐴) · (abs‘(𝐹𝑘))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
166134, 165syld 47 . . . . . . . . 9 ((𝜑𝑘𝑊) → ((abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
16746, 166syldan 585 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ𝑁)) → ((abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁)))))
168167expcom 404 . . . . . . 7 (𝑘 ∈ (ℤ𝑁) → (𝜑 → ((abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))) → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))))))
169168a2d 29 . . . . . 6 (𝑘 ∈ (ℤ𝑁) → ((𝜑 → (abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))) → (𝜑 → (abs‘(𝐹‘(𝑘 + 1))) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑((𝑘 + 1) − 𝑁))))))
17091, 95, 101, 95, 110, 169uzind4i 12060 . . . . 5 (𝑘 ∈ (ℤ𝑁) → (𝜑 → (abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁)))))
171170impcom 398 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑁)) → (abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))))
17247oveq2d 6940 . . . 4 ((𝜑𝑘 ∈ (ℤ𝑁)) → ((abs‘(𝐹𝑁)) · ((𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))‘𝑘)) = ((abs‘(𝐹𝑁)) · (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑘𝑁))))
173171, 172breqtrrd 4916 . . 3 ((𝜑𝑘 ∈ (ℤ𝑁)) → (abs‘(𝐹𝑘)) ≤ ((abs‘(𝐹𝑁)) · ((𝑛𝑊 ↦ (if(𝐴 ≤ 0, 0, 𝐴)↑(𝑛𝑁)))‘𝑘)))
1741, 9, 26, 32, 80, 85, 173cvgcmpce 14958 . 2 (𝜑 → seq𝑁( + , 𝐹) ∈ dom ⇝ )
1753, 2, 31iserex 14799 . 2 (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ seq𝑁( + , 𝐹) ∈ dom ⇝ ))
176174, 175mpbird 249 1 (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107  ∀wral 3090  Vcvv 3398   ⊆ wss 3792  ifcif 4307   class class class wbr 4888   ↦ cmpt 4967  dom cdm 5357  ‘cfv 6137  (class class class)co 6924  ℂcc 10272  ℝcr 10273  0cc0 10274  1c1 10275   + caddc 10277   · cmul 10279   < clt 10413   ≤ cle 10414   − cmin 10608   / cdiv 11034  ℕ0cn0 11646  ℤcz 11732  ℤ≥cuz 11996  seqcseq 13123  ↑cexp 13182   shift cshi 14217  abscabs 14385   ⇝ cli 14627 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-inf2 8837  ax-cnex 10330  ax-resscn 10331  ax-1cn 10332  ax-icn 10333  ax-addcl 10334  ax-addrcl 10335  ax-mulcl 10336  ax-mulrcl 10337  ax-mulcom 10338  ax-addass 10339  ax-mulass 10340  ax-distr 10341  ax-i2m1 10342  ax-1ne0 10343  ax-1rid 10344  ax-rnegex 10345  ax-rrecex 10346  ax-cnre 10347  ax-pre-lttri 10348  ax-pre-lttrn 10349  ax-pre-ltadd 10350  ax-pre-mulgt0 10351  ax-pre-sup 10352  ax-addf 10353  ax-mulf 10354 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4674  df-int 4713  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-tr 4990  df-id 5263  df-eprel 5268  df-po 5276  df-so 5277  df-fr 5316  df-se 5317  df-we 5318  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-pred 5935  df-ord 5981  df-on 5982  df-lim 5983  df-suc 5984  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-isom 6146  df-riota 6885  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-om 7346  df-1st 7447  df-2nd 7448  df-wrecs 7691  df-recs 7753  df-rdg 7791  df-1o 7845  df-oadd 7849  df-er 8028  df-pm 8145  df-en 8244  df-dom 8245  df-sdom 8246  df-fin 8247  df-sup 8638  df-inf 8639  df-oi 8706  df-card 9100  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419  df-sub 10610  df-neg 10611  df-div 11035  df-nn 11379  df-2 11442  df-3 11443  df-n0 11647  df-z 11733  df-uz 11997  df-rp 12142  df-ico 12497  df-fz 12648  df-fzo 12789  df-fl 12916  df-seq 13124  df-exp 13183  df-hash 13440  df-shft 14218  df-cj 14250  df-re 14251  df-im 14252  df-sqrt 14386  df-abs 14387  df-limsup 14614  df-clim 14631  df-rlim 14632  df-sum 14829 This theorem is referenced by:  efcllem  15214  cvgdvgrat  39478
 Copyright terms: Public domain W3C validator