fprodn0

Description: A finite product of nonzero terms is nonzero. (Contributed by Scott Fenton, 15-Jan-2018)

	Ref	Expression
Hypotheses	fprodn0.1	$⊢ φ \to A \in Fin$
	fprodn0.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	fprodn0.3	$⊢ (φ \land k \in A) \to B \neq 0$
Assertion	fprodn0	$⊢ φ \to \prod_{k \in A} B \neq 0$

Proof

Step	Hyp	Ref	Expression
1		fprodn0.1	$⊢ φ \to A \in Fin$
2		fprodn0.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		fprodn0.3	$⊢ (φ \land k \in A) \to B \neq 0$
4		prodeq1	$⊢ A = \emptyset \to \prod_{k \in A} B = \prod_{k \in \emptyset} B$
5		prod0	$⊢ \prod_{k \in \emptyset} B = 1$
6	4 5	eqtrdi	$⊢ A = \emptyset \to \prod_{k \in A} B = 1$
7		ax-1ne0	$⊢ 1 \neq 0$
8	7	a1i	$⊢ A = \emptyset \to 1 \neq 0$
9	6 8	eqnetrd	$⊢ A = \emptyset \to \prod_{k \in A} B \neq 0$
10	9	a1i	$⊢ φ \to (A = \emptyset \to \prod_{k \in A} B \neq 0)$
11		prodfc	$⊢ \prod_{m \in A} (k \in A ⟼ B) (m) = \prod_{k \in A} B$
12		fveq2	$⊢ m = f (n) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (n))$
13		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
14		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
15	2	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
16	15	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : A ⟶ ℂ$
17	16	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
18		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
19	14 18	syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
20		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
21	19 20	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
22	12 13 14 17 21	fprod	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{m \in A} (k \in A ⟼ B) (m) = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)$
23	11 22	eqtr3id	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} B = seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|)$
24		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
25	13 24	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
26		fco	$⊢ ((k \in A ⟼ B) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
27	16 19 26	syl2anc	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
28	27	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (m) \in ℂ$
29		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land m \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (m) = (k \in A ⟼ B) (f (m))$
30	19 29	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (m) = (k \in A ⟼ B) (f (m))$
31	18	ffvelcdmda	$⊢ (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \land m \in (1 \dots \|A\|)) \to f (m) \in A$
32	31	adantll	$⊢ ((\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land m \in (1 \dots \|A\|)) \to f (m) \in A$
33		simpr	$⊢ (φ \land f (m) \in A) \to f (m) \in A$
34		nfcv	$⊢ \underline{Ⅎ} k f (m)$
35		nfv	$⊢ Ⅎ k φ$
36		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ f (m) / k ⦌ B$
37	36	nfel1	$⊢ Ⅎ k ⦋ f (m) / k ⦌ B \in ℂ$
38	35 37	nfim	$⊢ Ⅎ k (φ \to ⦋ f (m) / k ⦌ B \in ℂ)$
39		csbeq1a	$⊢ k = f (m) \to B = ⦋ f (m) / k ⦌ B$
40	39	eleq1d	$⊢ k = f (m) \to (B \in ℂ \leftrightarrow ⦋ f (m) / k ⦌ B \in ℂ)$
41	40	imbi2d	$⊢ k = f (m) \to ((φ \to B \in ℂ) \leftrightarrow (φ \to ⦋ f (m) / k ⦌ B \in ℂ))$
42	2	expcom	$⊢ k \in A \to (φ \to B \in ℂ)$
43	34 38 41 42	vtoclgaf	$⊢ f (m) \in A \to (φ \to ⦋ f (m) / k ⦌ B \in ℂ)$
44	43	impcom	$⊢ (φ \land f (m) \in A) \to ⦋ f (m) / k ⦌ B \in ℂ$
45		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
46	45	fvmpts	$⊢ (f (m) \in A \land ⦋ f (m) / k ⦌ B \in ℂ) \to (k \in A ⟼ B) (f (m)) = ⦋ f (m) / k ⦌ B$
47	33 44 46	syl2anc	$⊢ (φ \land f (m) \in A) \to (k \in A ⟼ B) (f (m)) = ⦋ f (m) / k ⦌ B$
48		nfcv	$⊢ \underline{Ⅎ} k 0$
49	36 48	nfne	$⊢ Ⅎ k ⦋ f (m) / k ⦌ B \neq 0$
50	35 49	nfim	$⊢ Ⅎ k (φ \to ⦋ f (m) / k ⦌ B \neq 0)$
51	39	neeq1d	$⊢ k = f (m) \to (B \neq 0 \leftrightarrow ⦋ f (m) / k ⦌ B \neq 0)$
52	51	imbi2d	$⊢ k = f (m) \to ((φ \to B \neq 0) \leftrightarrow (φ \to ⦋ f (m) / k ⦌ B \neq 0))$
53	3	expcom	$⊢ k \in A \to (φ \to B \neq 0)$
54	34 50 52 53	vtoclgaf	$⊢ f (m) \in A \to (φ \to ⦋ f (m) / k ⦌ B \neq 0)$
55	54	impcom	$⊢ (φ \land f (m) \in A) \to ⦋ f (m) / k ⦌ B \neq 0$
56	47 55	eqnetrd	$⊢ (φ \land f (m) \in A) \to (k \in A ⟼ B) (f (m)) \neq 0$
57	32 56	sylan2	$⊢ (φ \land ((\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land m \in (1 \dots \|A\|))) \to (k \in A ⟼ B) (f (m)) \neq 0$
58	57	anassrs	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in (1 \dots \|A\|)) \to (k \in A ⟼ B) (f (m)) \neq 0$
59	30 58	eqnetrd	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (m) \neq 0$
60	25 28 59	prodfn0	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (\times ((k \in A ⟼ B) \circ f)) (\|A\|) \neq 0$
61	23 60	eqnetrd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \prod_{k \in A} B \neq 0$
62	61	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B \neq 0)$
63	62	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \prod_{k \in A} B \neq 0)$
64	63	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \prod_{k \in A} B \neq 0)$
65		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
66	1 65	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
67	10 64 66	mpjaod	$⊢ φ \to \prod_{k \in A} B \neq 0$

Metamath Proof Explorer

Theorem fprodn0

Proof