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

Theorem isermulc2 12131
 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 11048 . . 3
65a1i 10 . 2
7 isermulc2.6 . . . 4
81, 2, 7serf 11074 . . 3
9 ffvelrn 5663 . . 3
108, 9sylan 457 . 2
11 addcl 8819 . . . 4
134adantr 451 . . . 4
14 adddi 8826 . . . . 5
15143expb 1152 . . . 4
1613, 15sylan 457 . . 3
17 simpr 447 . . . 4
1817, 1syl6eleq 2373 . . 3
19 elfzuz 10794 . . . . . 6
2019, 1syl6eleqr 2374 . . . . 5
2120, 7sylan2 460 . . . 4