This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑀 ( · , 𝐹 ) ‘ 𝑁 ) ) )