Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isermulc2 Unicode version

Theorem isermulc2 12406
 Description: Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)
Hypotheses
Ref Expression
clim2ser.1
isermulc2.2
isermulc2.4
isermulc2.5
isermulc2.6
isermulc2.7
Assertion
Ref Expression
isermulc2
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem isermulc2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 clim2ser.1 . 2
2 isermulc2.2 . 2
3 isermulc2.5 . 2
4 isermulc2.4 . 2
5 seqex 11280 . . 3
65a1i 11 . 2
7 isermulc2.6 . . . 4
81, 2, 7serf 11306 . . 3
98ffvelrnda 5829 . 2
10 addcl 9028 . . . 4
124adantr 452 . . . 4
13 adddi 9035 . . . . 5
14133expb 1154 . . . 4
1512, 14sylan 458 . . 3
16 simpr 448 . . . 4
1716, 1syl6eleq 2494 . . 3
18 elfzuz 11011 . . . . . 6
1918, 1syl6eleqr 2495 . . . . 5
2019, 7sylan2 461 . . . 4