fprodn0f

Description: A finite product of nonzero terms is nonzero. A version of fprodn0 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodn0f.kph	$⊢ Ⅎ k φ$
	fprodn0f.a	$⊢ φ \to A \in Fin$
	fprodn0f.b	$⊢ (φ \land k \in A) \to B \in ℂ$
	fprodn0f.bne0	$⊢ (φ \land k \in A) \to B \neq 0$
Assertion	fprodn0f	$⊢ φ \to \prod_{k \in A} B \neq 0$

Proof

Step	Hyp	Ref	Expression
1		fprodn0f.kph	$⊢ Ⅎ k φ$
2		fprodn0f.a	$⊢ φ \to A \in Fin$
3		fprodn0f.b	$⊢ (φ \land k \in A) \to B \in ℂ$
4		fprodn0f.bne0	$⊢ (φ \land k \in A) \to B \neq 0$
5		difssd	$⊢ φ \to ℂ ∖ \{0\} \subseteq ℂ$
6		eldifi	$⊢ x \in (ℂ ∖ \{0\}) \to x \in ℂ$
7	6	adantr	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x \in ℂ$
8		eldifi	$⊢ y \in (ℂ ∖ \{0\}) \to y \in ℂ$
9	8	adantl	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to y \in ℂ$
10	7 9	mulcld	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \in ℂ$
11		eldifsni	$⊢ x \in (ℂ ∖ \{0\}) \to x \neq 0$
12	11	adantr	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x \neq 0$
13		eldifsni	$⊢ y \in (ℂ ∖ \{0\}) \to y \neq 0$
14	13	adantl	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to y \neq 0$
15	7 9 12 14	mulne0d	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \neq 0$
16	15	neneqd	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to \neg x y = 0$
17		ovex	$⊢ x y \in V$
18	17	elsn	$⊢ x y \in \{0\} \leftrightarrow x y = 0$
19	16 18	sylnibr	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to \neg x y \in \{0\}$
20	10 19	eldifd	$⊢ (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\})) \to x y \in (ℂ ∖ \{0\})$
21	20	adantl	$⊢ (φ \land (x \in (ℂ ∖ \{0\}) \land y \in (ℂ ∖ \{0\}))) \to x y \in (ℂ ∖ \{0\})$
22	4	neneqd	$⊢ (φ \land k \in A) \to \neg B = 0$
23		elsng	$⊢ B \in ℂ \to (B \in \{0\} \leftrightarrow B = 0)$
24	3 23	syl	$⊢ (φ \land k \in A) \to (B \in \{0\} \leftrightarrow B = 0)$
25	22 24	mtbird	$⊢ (φ \land k \in A) \to \neg B \in \{0\}$
26	3 25	eldifd	$⊢ (φ \land k \in A) \to B \in (ℂ ∖ \{0\})$
27		ax-1cn	$⊢ 1 \in ℂ$
28		ax-1ne0	$⊢ 1 \neq 0$
29		1ex	$⊢ 1 \in V$
30	29	elsn	$⊢ 1 \in \{0\} \leftrightarrow 1 = 0$
31	28 30	nemtbir	$⊢ \neg 1 \in \{0\}$
32		eldif	$⊢ 1 \in (ℂ ∖ \{0\}) \leftrightarrow (1 \in ℂ \land \neg 1 \in \{0\})$
33	27 31 32	mpbir2an	$⊢ 1 \in (ℂ ∖ \{0\})$
34	33	a1i	$⊢ φ \to 1 \in (ℂ ∖ \{0\})$
35	1 5 21 2 26 34	fprodcllemf	$⊢ φ \to \prod_{k \in A} B \in (ℂ ∖ \{0\})$
36		eldifsni	$⊢ \prod_{k \in A} B \in (ℂ ∖ \{0\}) \to \prod_{k \in A} B \neq 0$
37	35 36	syl	$⊢ φ \to \prod_{k \in A} B \neq 0$

Metamath Proof Explorer

Theorem fprodn0f

Proof