Metamath Proof Explorer


Theorem prodfrec

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

Ref Expression
Hypotheses prodfn0.1 φ N M
prodfn0.2 φ k M N F k
prodfn0.3 φ k M N F k 0
prodfrec.4 φ k M N G k = 1 F k
Assertion prodfrec φ seq M × G N = 1 seq M × F N

Proof

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