prodfn0

Description: No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-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$
Assertion	prodfn0	$⊢ φ \to seq M (\times F) (N) \neq 0$

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		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
5	1 4	syl	$⊢ φ \to N \in (M \dots N)$
6		fveq2	$⊢ m = M \to seq M (\times F) (m) = seq M (\times F) (M)$
7	6	neeq1d	$⊢ m = M \to (seq M (\times F) (m) \neq 0 \leftrightarrow seq M (\times F) (M) \neq 0)$
8	7	imbi2d	$⊢ m = M \to ((φ \to seq M (\times F) (m) \neq 0) \leftrightarrow (φ \to seq M (\times F) (M) \neq 0))$
9		fveq2	$⊢ m = n \to seq M (\times F) (m) = seq M (\times F) (n)$
10	9	neeq1d	$⊢ m = n \to (seq M (\times F) (m) \neq 0 \leftrightarrow seq M (\times F) (n) \neq 0)$
11	10	imbi2d	$⊢ m = n \to ((φ \to seq M (\times F) (m) \neq 0) \leftrightarrow (φ \to seq M (\times F) (n) \neq 0))$
12		fveq2	$⊢ m = n + 1 \to seq M (\times F) (m) = seq M (\times F) (n + 1)$
13	12	neeq1d	$⊢ m = n + 1 \to (seq M (\times F) (m) \neq 0 \leftrightarrow seq M (\times F) (n + 1) \neq 0)$
14	13	imbi2d	$⊢ m = n + 1 \to ((φ \to seq M (\times F) (m) \neq 0) \leftrightarrow (φ \to seq M (\times F) (n + 1) \neq 0))$
15		fveq2	$⊢ m = N \to seq M (\times F) (m) = seq M (\times F) (N)$
16	15	neeq1d	$⊢ m = N \to (seq M (\times F) (m) \neq 0 \leftrightarrow seq M (\times F) (N) \neq 0)$
17	16	imbi2d	$⊢ m = N \to ((φ \to seq M (\times F) (m) \neq 0) \leftrightarrow (φ \to seq M (\times F) (N) \neq 0))$
18		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
19		elfzelz	$⊢ M \in (M \dots N) \to M \in ℤ$
20	19	adantl	$⊢ (φ \land M \in (M \dots N)) \to M \in ℤ$
21		seq1	$⊢ M \in ℤ \to seq M (\times F) (M) = F (M)$
22	20 21	syl	$⊢ (φ \land M \in (M \dots N)) \to seq M (\times F) (M) = F (M)$
23		fveq2	$⊢ k = M \to F (k) = F (M)$
24	23	neeq1d	$⊢ k = M \to (F (k) \neq 0 \leftrightarrow F (M) \neq 0)$
25	24	imbi2d	$⊢ k = M \to ((φ \to F (k) \neq 0) \leftrightarrow (φ \to F (M) \neq 0))$
26	3	expcom	$⊢ k \in (M \dots N) \to (φ \to F (k) \neq 0)$
27	25 26	vtoclga	$⊢ M \in (M \dots N) \to (φ \to F (M) \neq 0)$
28	27	impcom	$⊢ (φ \land M \in (M \dots N)) \to F (M) \neq 0$
29	22 28	eqnetrd	$⊢ (φ \land M \in (M \dots N)) \to seq M (\times F) (M) \neq 0$
30	29	expcom	$⊢ M \in (M \dots N) \to (φ \to seq M (\times F) (M) \neq 0)$
31	18 30	syl	$⊢ N \in ℤ_{\geq M} \to (φ \to seq M (\times F) (M) \neq 0)$
32		elfzouz	$⊢ n \in (M ..^N) \to n \in ℤ_{\geq M}$
33	32	3ad2ant2	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to n \in ℤ_{\geq M}$
34		seqp1	$⊢ n \in ℤ_{\geq M} \to seq M (\times F) (n + 1) = seq M (\times F) (n) F (n + 1)$
35	33 34	syl	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to seq M (\times F) (n + 1) = seq M (\times F) (n) F (n + 1)$
36		elfzofz	$⊢ n \in (M ..^N) \to n \in (M \dots N)$
37		elfzuz	$⊢ n \in (M \dots N) \to n \in ℤ_{\geq M}$
38	37	adantl	$⊢ (φ \land n \in (M \dots N)) \to n \in ℤ_{\geq M}$
39		elfzuz3	$⊢ n \in (M \dots N) \to N \in ℤ_{\geq n}$
40		fzss2	$⊢ N \in ℤ_{\geq n} \to (M \dots n) \subseteq (M \dots N)$
41	39 40	syl	$⊢ n \in (M \dots N) \to (M \dots n) \subseteq (M \dots N)$
42	41	sselda	$⊢ (n \in (M \dots N) \land k \in (M \dots n)) \to k \in (M \dots N)$
43	42 2	sylan2	$⊢ (φ \land (n \in (M \dots N) \land k \in (M \dots n))) \to F (k) \in ℂ$
44	43	anassrs	$⊢ ((φ \land n \in (M \dots N)) \land k \in (M \dots n)) \to F (k) \in ℂ$
45		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
46	45	adantl	$⊢ ((φ \land n \in (M \dots N)) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
47	38 44 46	seqcl	$⊢ (φ \land n \in (M \dots N)) \to seq M (\times F) (n) \in ℂ$
48	36 47	sylan2	$⊢ (φ \land n \in (M ..^N)) \to seq M (\times F) (n) \in ℂ$
49	48	3adant3	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to seq M (\times F) (n) \in ℂ$
50		fzofzp1	$⊢ n \in (M ..^N) \to n + 1 \in (M \dots N)$
51		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
52	51	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℂ \leftrightarrow F (n + 1) \in ℂ)$
53	52	imbi2d	$⊢ k = n + 1 \to ((φ \to F (k) \in ℂ) \leftrightarrow (φ \to F (n + 1) \in ℂ))$
54	2	expcom	$⊢ k \in (M \dots N) \to (φ \to F (k) \in ℂ)$
55	53 54	vtoclga	$⊢ n + 1 \in (M \dots N) \to (φ \to F (n + 1) \in ℂ)$
56	50 55	syl	$⊢ n \in (M ..^N) \to (φ \to F (n + 1) \in ℂ)$
57	56	impcom	$⊢ (φ \land n \in (M ..^N)) \to F (n + 1) \in ℂ$
58	57	3adant3	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to F (n + 1) \in ℂ$
59		simp3	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to seq M (\times F) (n) \neq 0$
60	51	neeq1d	$⊢ k = n + 1 \to (F (k) \neq 0 \leftrightarrow F (n + 1) \neq 0)$
61	60	imbi2d	$⊢ k = n + 1 \to ((φ \to F (k) \neq 0) \leftrightarrow (φ \to F (n + 1) \neq 0))$
62	61 26	vtoclga	$⊢ n + 1 \in (M \dots N) \to (φ \to F (n + 1) \neq 0)$
63	62	impcom	$⊢ (φ \land n + 1 \in (M \dots N)) \to F (n + 1) \neq 0$
64	50 63	sylan2	$⊢ (φ \land n \in (M ..^N)) \to F (n + 1) \neq 0$
65	64	3adant3	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to F (n + 1) \neq 0$
66	49 58 59 65	mulne0d	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to seq M (\times F) (n) F (n + 1) \neq 0$
67	35 66	eqnetrd	$⊢ (φ \land n \in (M ..^N) \land seq M (\times F) (n) \neq 0) \to seq M (\times F) (n + 1) \neq 0$
68	67	3exp	$⊢ φ \to (n \in (M ..^N) \to (seq M (\times F) (n) \neq 0 \to seq M (\times F) (n + 1) \neq 0))$
69	68	com12	$⊢ n \in (M ..^N) \to (φ \to (seq M (\times F) (n) \neq 0 \to seq M (\times F) (n + 1) \neq 0))$
70	69	a2d	$⊢ n \in (M ..^N) \to ((φ \to seq M (\times F) (n) \neq 0) \to (φ \to seq M (\times F) (n + 1) \neq 0))$
71	8 11 14 17 31 70	fzind2	$⊢ N \in (M \dots N) \to (φ \to seq M (\times F) (N) \neq 0)$
72	5 71	mpcom	$⊢ φ \to seq M (\times F) (N) \neq 0$

Metamath Proof Explorer

Theorem prodfn0

Proof