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

Theorem isermulc2 12452
 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 11326 . . 3
65a1i 11 . 2
7 isermulc2.6 . . . 4
81, 2, 7serf 11352 . . 3
98ffvelrnda 5871 . 2
10 addcl 9073 . . . 4
124adantr 453 . . . 4
13 adddi 9080 . . . . 5
14133expb 1155 . . . 4
1512, 14sylan 459 . . 3
16 simpr 449 . . . 4
1716, 1syl6eleq 2527 . . 3
18 elfzuz 11056 . . . . . 6
1918, 1syl6eleqr 2528 . . . . 5
2019, 7sylan2 462 . . . 4