Metamath Proof Explorer

Theorem iprodefisumlem

Description: Lemma for iprodefisum . (Contributed by Scott Fenton, 11-Feb-2018)

Ref Expression
Hypotheses iprodefisumlem.1 
|- Z = ( ZZ>= ` M )
iprodefisumlem.2 
|- ( ph -> M e. ZZ )
iprodefisumlem.3 
|- ( ph -> F : Z --> CC )
Assertion iprodefisumlem 
|- ( ph -> seq M ( x. , ( exp o. F ) ) = ( exp o. seq M ( + , F ) ) )

Proof

Step Hyp Ref Expression
1 iprodefisumlem.1 
 |-  Z = ( ZZ>= ` M )
2 iprodefisumlem.2 
 |-  ( ph -> M e. ZZ )
3 iprodefisumlem.3 
 |-  ( ph -> F : Z --> CC )
4 fvco3 
 |-  ( ( F : Z --> CC /\ k e. Z ) -> ( ( exp o. F ) ` k ) = ( exp ` ( F ` k ) ) )
5 3 4 sylan 
 |-  ( ( ph /\ k e. Z ) -> ( ( exp o. F ) ` k ) = ( exp ` ( F ` k ) ) )
6 3 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
7 efcl 
 |-  ( ( F ` k ) e. CC -> ( exp ` ( F ` k ) ) e. CC )
8 6 7 syl 
 |-  ( ( ph /\ k e. Z ) -> ( exp ` ( F ` k ) ) e. CC )
9 5 8 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( exp o. F ) ` k ) e. CC )
10 1 2 9 prodf 
 |-  ( ph -> seq M ( x. , ( exp o. F ) ) : Z --> CC )
11 10 ffnd 
 |-  ( ph -> seq M ( x. , ( exp o. F ) ) Fn Z )
12 eff 
 |-  exp : CC --> CC
13 ffn 
 |-  ( exp : CC --> CC -> exp Fn CC )
14 12 13 ax-mp 
 |-  exp Fn CC
15 1 2 6 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
16 fnfco 
 |-  ( ( exp Fn CC /\ seq M ( + , F ) : Z --> CC ) -> ( exp o. seq M ( + , F ) ) Fn Z )
17 14 15 16 sylancr 
 |-  ( ph -> ( exp o. seq M ( + , F ) ) Fn Z )
18 fveq2 
 |-  ( j = M -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( seq M ( x. , ( exp o. F ) ) ` M ) )
19 2fveq3 
 |-  ( j = M -> ( exp ` ( seq M ( + , F ) ` j ) ) = ( exp ` ( seq M ( + , F ) ` M ) ) )
20 18 19 eqeq12d 
 |-  ( j = M -> ( ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) <-> ( seq M ( x. , ( exp o. F ) ) ` M ) = ( exp ` ( seq M ( + , F ) ` M ) ) ) )
21 20 imbi2d 
 |-  ( j = M -> ( ( ph -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) ) <-> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` M ) = ( exp ` ( seq M ( + , F ) ` M ) ) ) ) )
22 fveq2 
 |-  ( j = n -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( seq M ( x. , ( exp o. F ) ) ` n ) )
23 2fveq3 
 |-  ( j = n -> ( exp ` ( seq M ( + , F ) ` j ) ) = ( exp ` ( seq M ( + , F ) ` n ) ) )
24 22 23 eqeq12d 
 |-  ( j = n -> ( ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) <-> ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) )
25 24 imbi2d 
 |-  ( j = n -> ( ( ph -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) ) <-> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) ) )
26 fveq2 
 |-  ( j = ( n + 1 ) -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) )
27 2fveq3 
 |-  ( j = ( n + 1 ) -> ( exp ` ( seq M ( + , F ) ` j ) ) = ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) )
28 26 27 eqeq12d 
 |-  ( j = ( n + 1 ) -> ( ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) <-> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) ) )
29 28 imbi2d 
 |-  ( j = ( n + 1 ) -> ( ( ph -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) ) <-> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) ) ) )
30 fveq2 
 |-  ( j = k -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( seq M ( x. , ( exp o. F ) ) ` k ) )
31 2fveq3 
 |-  ( j = k -> ( exp ` ( seq M ( + , F ) ` j ) ) = ( exp ` ( seq M ( + , F ) ` k ) ) )
32 30 31 eqeq12d 
 |-  ( j = k -> ( ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) <-> ( seq M ( x. , ( exp o. F ) ) ` k ) = ( exp ` ( seq M ( + , F ) ` k ) ) ) )
33 32 imbi2d 
 |-  ( j = k -> ( ( ph -> ( seq M ( x. , ( exp o. F ) ) ` j ) = ( exp ` ( seq M ( + , F ) ` j ) ) ) <-> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` k ) = ( exp ` ( seq M ( + , F ) ` k ) ) ) ) )
34 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
35 2 34 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
36 35 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
37 fvco3 
 |-  ( ( F : Z --> CC /\ M e. Z ) -> ( ( exp o. F ) ` M ) = ( exp ` ( F ` M ) ) )
38 3 36 37 syl2anc 
 |-  ( ph -> ( ( exp o. F ) ` M ) = ( exp ` ( F ` M ) ) )
39 seq1 
 |-  ( M e. ZZ -> ( seq M ( x. , ( exp o. F ) ) ` M ) = ( ( exp o. F ) ` M ) )
40 2 39 syl 
 |-  ( ph -> ( seq M ( x. , ( exp o. F ) ) ` M ) = ( ( exp o. F ) ` M ) )
41 seq1 
 |-  ( M e. ZZ -> ( seq M ( + , F ) ` M ) = ( F ` M ) )
42 2 41 syl 
 |-  ( ph -> ( seq M ( + , F ) ` M ) = ( F ` M ) )
43 42 fveq2d 
 |-  ( ph -> ( exp ` ( seq M ( + , F ) ` M ) ) = ( exp ` ( F ` M ) ) )
44 38 40 43 3eqtr4d 
 |-  ( ph -> ( seq M ( x. , ( exp o. F ) ) ` M ) = ( exp ` ( seq M ( + , F ) ` M ) ) )
45 44 a1i 
 |-  ( M e. ZZ -> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` M ) = ( exp ` ( seq M ( + , F ) ` M ) ) ) )
46 oveq1 
 |-  ( ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) -> ( ( seq M ( x. , ( exp o. F ) ) ` n ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) = ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) )
47 46 3ad2ant3 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph /\ ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) -> ( ( seq M ( x. , ( exp o. F ) ) ` n ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) = ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) )
48 3 adantl 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> F : Z --> CC )
49 peano2uz 
 |-  ( n e. ( ZZ>= ` M ) -> ( n + 1 ) e. ( ZZ>= ` M ) )
50 49 1 eleqtrrdi 
 |-  ( n e. ( ZZ>= ` M ) -> ( n + 1 ) e. Z )
51 50 adantr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( n + 1 ) e. Z )
52 fvco3 
 |-  ( ( F : Z --> CC /\ ( n + 1 ) e. Z ) -> ( ( exp o. F ) ` ( n + 1 ) ) = ( exp ` ( F ` ( n + 1 ) ) ) )
53 48 51 52 syl2anc 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( ( exp o. F ) ` ( n + 1 ) ) = ( exp ` ( F ` ( n + 1 ) ) ) )
54 53 oveq2d 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) = ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( exp ` ( F ` ( n + 1 ) ) ) ) )
55 15 ffvelrnda 
 |-  ( ( ph /\ n e. Z ) -> ( seq M ( + , F ) ` n ) e. CC )
56 55 expcom 
 |-  ( n e. Z -> ( ph -> ( seq M ( + , F ) ` n ) e. CC ) )
57 1 eqcomi 
 |-  ( ZZ>= ` M ) = Z
58 56 57 eleq2s 
 |-  ( n e. ( ZZ>= ` M ) -> ( ph -> ( seq M ( + , F ) ` n ) e. CC ) )
59 58 imp 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( seq M ( + , F ) ` n ) e. CC )
60 48 51 ffvelrnd 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( F ` ( n + 1 ) ) e. CC )
61 efadd 
 |-  ( ( ( seq M ( + , F ) ` n ) e. CC /\ ( F ` ( n + 1 ) ) e. CC ) -> ( exp ` ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) ) = ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( exp ` ( F ` ( n + 1 ) ) ) ) )
62 59 60 61 syl2anc 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( exp ` ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) ) = ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( exp ` ( F ` ( n + 1 ) ) ) ) )
63 54 62 eqtr4d 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) = ( exp ` ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) ) )
64 63 3adant3 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph /\ ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) -> ( ( exp ` ( seq M ( + , F ) ` n ) ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) = ( exp ` ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) ) )
65 47 64 eqtrd 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph /\ ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) -> ( ( seq M ( x. , ( exp o. F ) ) ` n ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) = ( exp ` ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) ) )
66 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( ( seq M ( x. , ( exp o. F ) ) ` n ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) )
67 66 adantr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( ( seq M ( x. , ( exp o. F ) ) ` n ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) )
68 67 3adant3 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph /\ ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) -> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( ( seq M ( x. , ( exp o. F ) ) ` n ) x. ( ( exp o. F ) ` ( n + 1 ) ) ) )
69 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( + , F ) ` ( n + 1 ) ) = ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) )
70 69 adantr 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( seq M ( + , F ) ` ( n + 1 ) ) = ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) )
71 70 fveq2d 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph ) -> ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) = ( exp ` ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) ) )
72 71 3adant3 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph /\ ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) -> ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) = ( exp ` ( ( seq M ( + , F ) ` n ) + ( F ` ( n + 1 ) ) ) ) )
73 65 68 72 3eqtr4d 
 |-  ( ( n e. ( ZZ>= ` M ) /\ ph /\ ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) -> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) )
74 73 3exp 
 |-  ( n e. ( ZZ>= ` M ) -> ( ph -> ( ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) -> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) ) ) )
75 74 a2d 
 |-  ( n e. ( ZZ>= ` M ) -> ( ( ph -> ( seq M ( x. , ( exp o. F ) ) ` n ) = ( exp ` ( seq M ( + , F ) ` n ) ) ) -> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` ( n + 1 ) ) = ( exp ` ( seq M ( + , F ) ` ( n + 1 ) ) ) ) ) )
76 21 25 29 33 45 75 uzind4 
 |-  ( k e. ( ZZ>= ` M ) -> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` k ) = ( exp ` ( seq M ( + , F ) ` k ) ) ) )
77 76 1 eleq2s 
 |-  ( k e. Z -> ( ph -> ( seq M ( x. , ( exp o. F ) ) ` k ) = ( exp ` ( seq M ( + , F ) ` k ) ) ) )
78 77 impcom 
 |-  ( ( ph /\ k e. Z ) -> ( seq M ( x. , ( exp o. F ) ) ` k ) = ( exp ` ( seq M ( + , F ) ` k ) ) )
79 fvco3 
 |-  ( ( seq M ( + , F ) : Z --> CC /\ k e. Z ) -> ( ( exp o. seq M ( + , F ) ) ` k ) = ( exp ` ( seq M ( + , F ) ` k ) ) )
80 15 79 sylan 
 |-  ( ( ph /\ k e. Z ) -> ( ( exp o. seq M ( + , F ) ) ` k ) = ( exp ` ( seq M ( + , F ) ` k ) ) )
81 78 80 eqtr4d 
 |-  ( ( ph /\ k e. Z ) -> ( seq M ( x. , ( exp o. F ) ) ` k ) = ( ( exp o. seq M ( + , F ) ) ` k ) )
82 11 17 81 eqfnfvd 
 |-  ( ph -> seq M ( x. , ( exp o. F ) ) = ( exp o. seq M ( + , F ) ) )