Metamath Proof Explorer


Theorem prodfrec

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

Ref Expression
Hypotheses prodfn0.1 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
prodfn0.2 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
prodfn0.3 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑘 ) ≠ 0 )
prodfrec.4 ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺𝑘 ) = ( 1 / ( 𝐹𝑘 ) ) )
Assertion prodfrec ( 𝜑 → ( seq 𝑀 ( · , 𝐺 ) ‘ 𝑁 ) = ( 1 / ( seq 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) )

Proof

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