prodfrec

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

	Ref	Expression
Hypotheses	prodfn0.1	$⊢ φ \to N \in ℤ_{\geq M}$
	prodfn0.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℂ$
	prodfn0.3	$⊢ (φ \land k \in (M \dots N)) \to F (k) \neq 0$
	prodfrec.4	$⊢ (φ \land k \in (M \dots N)) \to G (k) = \frac{1}{F (k)}$
Assertion	prodfrec	$⊢ φ \to seq M (\times G) (N) = \frac{1}{seq M (\times F) (N)}$

Proof

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

Metamath Proof Explorer

Theorem prodfrec

Proof