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