Metamath Proof Explorer

Theorem prodfrec

Description: The reciprocal of an infinite product. (Contributed by Scott Fenton, 15-Jan-2018)

Ref Expression
Hypotheses prodfn0.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
prodfn0.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
prodfn0.3 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )
prodfrec.4 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( 1 / ( F ` k ) ) )
Assertion prodfrec 
|- ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 prodfn0.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 prodfn0.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
3 prodfn0.3 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )
4 prodfrec.4 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( 1 / ( F ` k ) ) )
5 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
6 1 5 syl 
 |-  ( ph -> N e. ( M ... N ) )
7 fveq2 
 |-  ( m = M -> ( seq M ( x. , G ) ` m ) = ( seq M ( x. , G ) ` M ) )
8 fveq2 
 |-  ( m = M -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` M ) )
9 8 oveq2d 
 |-  ( m = M -> ( 1 / ( seq M ( x. , F ) ` m ) ) = ( 1 / ( seq M ( x. , F ) ` M ) ) )
10 7 9 eqeq12d 
 |-  ( m = M -> ( ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) <-> ( seq M ( x. , G ) ` M ) = ( 1 / ( seq M ( x. , F ) ` M ) ) ) )
11 10 imbi2d 
 |-  ( m = M -> ( ( ph -> ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) ) <-> ( ph -> ( seq M ( x. , G ) ` M ) = ( 1 / ( seq M ( x. , F ) ` M ) ) ) ) )
12 fveq2 
 |-  ( m = n -> ( seq M ( x. , G ) ` m ) = ( seq M ( x. , G ) ` n ) )
13 fveq2 
 |-  ( m = n -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` n ) )
14 13 oveq2d 
 |-  ( m = n -> ( 1 / ( seq M ( x. , F ) ` m ) ) = ( 1 / ( seq M ( x. , F ) ` n ) ) )
15 12 14 eqeq12d 
 |-  ( m = n -> ( ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) <-> ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) )
16 15 imbi2d 
 |-  ( m = n -> ( ( ph -> ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) ) <-> ( ph -> ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) ) )
17 fveq2 
 |-  ( m = ( n + 1 ) -> ( seq M ( x. , G ) ` m ) = ( seq M ( x. , G ) ` ( n + 1 ) ) )
18 fveq2 
 |-  ( m = ( n + 1 ) -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` ( n + 1 ) ) )
19 18 oveq2d 
 |-  ( m = ( n + 1 ) -> ( 1 / ( seq M ( x. , F ) ` m ) ) = ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) )
20 17 19 eqeq12d 
 |-  ( m = ( n + 1 ) -> ( ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) <-> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) ) )
21 20 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( ph -> ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) ) <-> ( ph -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) ) ) )
22 fveq2 
 |-  ( m = N -> ( seq M ( x. , G ) ` m ) = ( seq M ( x. , G ) ` N ) )
23 fveq2 
 |-  ( m = N -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` N ) )
24 23 oveq2d 
 |-  ( m = N -> ( 1 / ( seq M ( x. , F ) ` m ) ) = ( 1 / ( seq M ( x. , F ) ` N ) ) )
25 22 24 eqeq12d 
 |-  ( m = N -> ( ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) <-> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) ) )
26 25 imbi2d 
 |-  ( m = N -> ( ( ph -> ( seq M ( x. , G ) ` m ) = ( 1 / ( seq M ( x. , F ) ` m ) ) ) <-> ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) ) ) )
27 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
28 1 27 syl 
 |-  ( ph -> M e. ( M ... N ) )
29 fveq2 
 |-  ( k = M -> ( G ` k ) = ( G ` M ) )
30 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
31 30 oveq2d 
 |-  ( k = M -> ( 1 / ( F ` k ) ) = ( 1 / ( F ` M ) ) )
32 29 31 eqeq12d 
 |-  ( k = M -> ( ( G ` k ) = ( 1 / ( F ` k ) ) <-> ( G ` M ) = ( 1 / ( F ` M ) ) ) )
33 32 imbi2d 
 |-  ( k = M -> ( ( ph -> ( G ` k ) = ( 1 / ( F ` k ) ) ) <-> ( ph -> ( G ` M ) = ( 1 / ( F ` M ) ) ) ) )
34 4 expcom 
 |-  ( k e. ( M ... N ) -> ( ph -> ( G ` k ) = ( 1 / ( F ` k ) ) ) )
35 33 34 vtoclga 
 |-  ( M e. ( M ... N ) -> ( ph -> ( G ` M ) = ( 1 / ( F ` M ) ) ) )
36 28 35 mpcom 
 |-  ( ph -> ( G ` M ) = ( 1 / ( F ` M ) ) )
37 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
38 1 37 syl 
 |-  ( ph -> M e. ZZ )
39 seq1 
 |-  ( M e. ZZ -> ( seq M ( x. , G ) ` M ) = ( G ` M ) )
40 38 39 syl 
 |-  ( ph -> ( seq M ( x. , G ) ` M ) = ( G ` M ) )
41 seq1 
 |-  ( M e. ZZ -> ( seq M ( x. , F ) ` M ) = ( F ` M ) )
42 38 41 syl 
 |-  ( ph -> ( seq M ( x. , F ) ` M ) = ( F ` M ) )
43 42 oveq2d 
 |-  ( ph -> ( 1 / ( seq M ( x. , F ) ` M ) ) = ( 1 / ( F ` M ) ) )
44 36 40 43 3eqtr4d 
 |-  ( ph -> ( seq M ( x. , G ) ` M ) = ( 1 / ( seq M ( x. , F ) ` M ) ) )
45 44 a1i 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( seq M ( x. , G ) ` M ) = ( 1 / ( seq M ( x. , F ) ` M ) ) ) )
46 oveq1 
 |-  ( ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) -> ( ( seq M ( x. , G ) ` n ) x. ( G ` ( n + 1 ) ) ) = ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( G ` ( n + 1 ) ) ) )
47 46 3ad2ant3 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) -> ( ( seq M ( x. , G ) ` n ) x. ( G ` ( n + 1 ) ) ) = ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( G ` ( n + 1 ) ) ) )
48 fzofzp1 
 |-  ( n e. ( M ..^ N ) -> ( n + 1 ) e. ( M ... N ) )
49 fveq2 
 |-  ( k = ( n + 1 ) -> ( G ` k ) = ( G ` ( n + 1 ) ) )
50 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
51 50 oveq2d 
 |-  ( k = ( n + 1 ) -> ( 1 / ( F ` k ) ) = ( 1 / ( F ` ( n + 1 ) ) ) )
52 49 51 eqeq12d 
 |-  ( k = ( n + 1 ) -> ( ( G ` k ) = ( 1 / ( F ` k ) ) <-> ( G ` ( n + 1 ) ) = ( 1 / ( F ` ( n + 1 ) ) ) ) )
53 52 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( G ` k ) = ( 1 / ( F ` k ) ) ) <-> ( ph -> ( G ` ( n + 1 ) ) = ( 1 / ( F ` ( n + 1 ) ) ) ) ) )
54 53 34 vtoclga 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( ph -> ( G ` ( n + 1 ) ) = ( 1 / ( F ` ( n + 1 ) ) ) ) )
55 48 54 syl 
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( G ` ( n + 1 ) ) = ( 1 / ( F ` ( n + 1 ) ) ) ) )
56 55 impcom 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( G ` ( n + 1 ) ) = ( 1 / ( F ` ( n + 1 ) ) ) )
57 56 oveq2d 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( G ` ( n + 1 ) ) ) = ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( 1 / ( F ` ( n + 1 ) ) ) ) )
58 1cnd 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> 1 e. CC )
59 elfzouz 
 |-  ( n e. ( M ..^ N ) -> n e. ( ZZ>= ` M ) )
60 59 adantl 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> n e. ( ZZ>= ` M ) )
61 elfzouz2 
 |-  ( n e. ( M ..^ N ) -> N e. ( ZZ>= ` n ) )
62 fzss2 
 |-  ( N e. ( ZZ>= ` n ) -> ( M ... n ) C_ ( M ... N ) )
63 61 62 syl 
 |-  ( n e. ( M ..^ N ) -> ( M ... n ) C_ ( M ... N ) )
64 63 sselda 
 |-  ( ( n e. ( M ..^ N ) /\ k e. ( M ... n ) ) -> k e. ( M ... N ) )
65 64 2 sylan2 
 |-  ( ( ph /\ ( n e. ( M ..^ N ) /\ k e. ( M ... n ) ) ) -> ( F ` k ) e. CC )
66 65 anassrs 
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ k e. ( M ... n ) ) -> ( F ` k ) e. CC )
67 mulcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
68 67 adantl 
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
69 60 66 68 seqcl 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( seq M ( x. , F ) ` n ) e. CC )
70 50 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. CC <-> ( F ` ( n + 1 ) ) e. CC ) )
71 70 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( F ` k ) e. CC ) <-> ( ph -> ( F ` ( n + 1 ) ) e. CC ) ) )
72 2 expcom 
 |-  ( k e. ( M ... N ) -> ( ph -> ( F ` k ) e. CC ) )
73 71 72 vtoclga 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( ph -> ( F ` ( n + 1 ) ) e. CC ) )
74 48 73 syl 
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( F ` ( n + 1 ) ) e. CC ) )
75 74 impcom 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( F ` ( n + 1 ) ) e. CC )
76 64 3 sylan2 
 |-  ( ( ph /\ ( n e. ( M ..^ N ) /\ k e. ( M ... n ) ) ) -> ( F ` k ) =/= 0 )
77 76 anassrs 
 |-  ( ( ( ph /\ n e. ( M ..^ N ) ) /\ k e. ( M ... n ) ) -> ( F ` k ) =/= 0 )
78 60 66 77 prodfn0 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( seq M ( x. , F ) ` n ) =/= 0 )
79 50 neeq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) =/= 0 <-> ( F ` ( n + 1 ) ) =/= 0 ) )
80 79 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( F ` k ) =/= 0 ) <-> ( ph -> ( F ` ( n + 1 ) ) =/= 0 ) ) )
81 3 expcom 
 |-  ( k e. ( M ... N ) -> ( ph -> ( F ` k ) =/= 0 ) )
82 80 81 vtoclga 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( ph -> ( F ` ( n + 1 ) ) =/= 0 ) )
83 48 82 syl 
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( F ` ( n + 1 ) ) =/= 0 ) )
84 83 impcom 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( F ` ( n + 1 ) ) =/= 0 )
85 58 69 58 75 78 84 divmuldivd 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( 1 / ( F ` ( n + 1 ) ) ) ) = ( ( 1 x. 1 ) / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
86 1t1e1 
 |-  ( 1 x. 1 ) = 1
87 86 oveq1i 
 |-  ( ( 1 x. 1 ) / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) = ( 1 / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
88 85 87 eqtrdi 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( 1 / ( F ` ( n + 1 ) ) ) ) = ( 1 / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
89 57 88 eqtrd 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( G ` ( n + 1 ) ) ) = ( 1 / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
90 89 3adant3 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) -> ( ( 1 / ( seq M ( x. , F ) ` n ) ) x. ( G ` ( n + 1 ) ) ) = ( 1 / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
91 47 90 eqtrd 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) -> ( ( seq M ( x. , G ) ` n ) x. ( G ` ( n + 1 ) ) ) = ( 1 / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
92 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( ( seq M ( x. , G ) ` n ) x. ( G ` ( n + 1 ) ) ) )
93 59 92 syl 
 |-  ( n e. ( M ..^ N ) -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( ( seq M ( x. , G ) ` n ) x. ( G ` ( n + 1 ) ) ) )
94 93 3ad2ant2 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( ( seq M ( x. , G ) ` n ) x. ( G ` ( n + 1 ) ) ) )
95 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
96 59 95 syl 
 |-  ( n e. ( M ..^ N ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
97 96 oveq2d 
 |-  ( n e. ( M ..^ N ) -> ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) = ( 1 / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
98 97 3ad2ant2 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) -> ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) = ( 1 / ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) ) )
99 91 94 98 3eqtr4d 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) )
100 99 3exp 
 |-  ( ph -> ( n e. ( M ..^ N ) -> ( ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) ) ) )
101 100 com12 
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) ) ) )
102 101 a2d 
 |-  ( n e. ( M ..^ N ) -> ( ( ph -> ( seq M ( x. , G ) ` n ) = ( 1 / ( seq M ( x. , F ) ` n ) ) ) -> ( ph -> ( seq M ( x. , G ) ` ( n + 1 ) ) = ( 1 / ( seq M ( x. , F ) ` ( n + 1 ) ) ) ) ) )
103 11 16 21 26 45 102 fzind2 
 |-  ( N e. ( M ... N ) -> ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) ) )
104 6 103 mpcom 
 |-  ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) )