Theorem 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	⊢ Ⅎ 𝑘 𝜑
	fprodn0f.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodn0f.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fprodn0f.bne0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≠ 0 )
Assertion	fprodn0f	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		fprodn0f.kph	⊢ Ⅎ 𝑘 𝜑
2		fprodn0f.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fprodn0f.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
4		fprodn0f.bne0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≠ 0 )
5		difssd	⊢ ( 𝜑 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
6		eldifi	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ∈ ℂ )
7	6	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
8		eldifi	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ∈ ℂ )
9	8	adantl	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
10	7 9	mulcld	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
11		eldifsni	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ≠ 0 )
12	11	adantr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ≠ 0 )
13		eldifsni	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
14	13	adantl	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
15	7 9 12 14	mulne0d	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
16	15	neneqd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ¬ ( 𝑥 · 𝑦 ) = 0 )
17		ovex	⊢ ( 𝑥 · 𝑦 ) ∈ V
18	17	elsn	⊢ ( ( 𝑥 · 𝑦 ) ∈ { 0 } ↔ ( 𝑥 · 𝑦 ) = 0 )
19	16 18	sylnibr	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ¬ ( 𝑥 · 𝑦 ) ∈ { 0 } )
20	10 19	eldifd	⊢ ( ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) ) → ( 𝑥 · 𝑦 ) ∈ ( ℂ ∖ { 0 } ) )
22	4	neneqd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝐵 = 0 )
23		elsng	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ { 0 } ↔ 𝐵 = 0 ) )
24	3 23	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 ∈ { 0 } ↔ 𝐵 = 0 ) )
25	22 24	mtbird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ 𝐵 ∈ { 0 } )
26	3 25	eldifd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( ℂ ∖ { 0 } ) )
27		ax-1cn	⊢ 1 ∈ ℂ
28		ax-1ne0	⊢ 1 ≠ 0
29		1ex	⊢ 1 ∈ V
30	29	elsn	⊢ ( 1 ∈ { 0 } ↔ 1 = 0 )
31	28 30	nemtbir	⊢ ¬ 1 ∈ { 0 }
32		eldif	⊢ ( 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( 1 ∈ ℂ ∧ ¬ 1 ∈ { 0 } ) )
33	27 31 32	mpbir2an	⊢ 1 ∈ ( ℂ ∖ { 0 } )
34	33	a1i	⊢ ( 𝜑 → 1 ∈ ( ℂ ∖ { 0 } ) )
35	1 5 21 2 26 34	fprodcllemf	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ( ℂ ∖ { 0 } ) )
36		eldifsni	⊢ ( ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ( ℂ ∖ { 0 } ) → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )
37	35 36	syl	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )