Theorem fprodn0

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

	Ref	Expression
Hypotheses	fprodn0.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fprodn0.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	fprodn0.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≠ 0 )
Assertion	fprodn0	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		fprodn0.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		fprodn0.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		fprodn0.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≠ 0 )
4		prodeq1	⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ ∅ 𝐵 )
5		prod0	⊢ ∏ 𝑘 ∈ ∅ 𝐵 = 1
6	4 5	eqtrdi	⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐵 = 1 )
7		ax-1ne0	⊢ 1 ≠ 0
8	7	a1i	⊢ ( 𝐴 = ∅ → 1 ≠ 0 )
9	6 8	eqnetrd	⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )
10	9	a1i	⊢ ( 𝜑 → ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) )
11		prodfc	⊢ ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝐴 𝐵
12		fveq2	⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
13		simprl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
14		simprr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
15	2	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
17	16	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
18		f1of	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
19	14 18	syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
20		fvco3	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
21	19 20	sylan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
22	12 13 14 17 21	fprod	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
23	11 22	eqtr3id	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
24		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
25	13 24	eleqtrdi	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
26		fco	⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
27	16 19 26	syl2anc	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
28	27	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑚 ) ∈ ℂ )
29		fvco3	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑚 ) ) )
30	19 29	sylan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑚 ) ) )
31	18	ffvelcdmda	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 )
32	31	adantll	⊢ ( ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 )
33		simpr	⊢ ( ( 𝜑 ∧ ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 ) → ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 )
34		nfcv	⊢ Ⅎ 𝑘 ( 𝑓 ‘ 𝑚 )
35		nfv	⊢ Ⅎ 𝑘 𝜑
36		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵
37	36	nfel1	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ
38	35 37	nfim	⊢ Ⅎ 𝑘 ( 𝜑 → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ )
39		csbeq1a	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → 𝐵 = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 )
40	39	eleq1d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → ( 𝐵 ∈ ℂ ↔ ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
41	40	imbi2d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → ( ( 𝜑 → 𝐵 ∈ ℂ ) ↔ ( 𝜑 → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
42	2	expcom	⊢ ( 𝑘 ∈ 𝐴 → ( 𝜑 → 𝐵 ∈ ℂ ) )
43	34 38 41 42	vtoclgaf	⊢ ( ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 → ( 𝜑 → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
44	43	impcom	⊢ ( ( 𝜑 ∧ ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 ) → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ )
45		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
46	45	fvmpts	⊢ ( ( ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 ∧ ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑚 ) ) = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 )
47	33 44 46	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑚 ) ) = ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 )
48		nfcv	⊢ Ⅎ 𝑘 0
49	36 48	nfne	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ≠ 0
50	35 49	nfim	⊢ Ⅎ 𝑘 ( 𝜑 → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ≠ 0 )
51	39	neeq1d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → ( 𝐵 ≠ 0 ↔ ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ≠ 0 ) )
52	51	imbi2d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑚 ) → ( ( 𝜑 → 𝐵 ≠ 0 ) ↔ ( 𝜑 → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ≠ 0 ) ) )
53	3	expcom	⊢ ( 𝑘 ∈ 𝐴 → ( 𝜑 → 𝐵 ≠ 0 ) )
54	34 50 52 53	vtoclgaf	⊢ ( ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 → ( 𝜑 → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ≠ 0 ) )
55	54	impcom	⊢ ( ( 𝜑 ∧ ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 ) → ⦋ ( 𝑓 ‘ 𝑚 ) / 𝑘 ⦌ 𝐵 ≠ 0 )
56	47 55	eqnetrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ‘ 𝑚 ) ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑚 ) ) ≠ 0 )
57	32 56	sylan2	⊢ ( ( 𝜑 ∧ ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑚 ) ) ≠ 0 )
58	57	anassrs	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑚 ) ) ≠ 0 )
59	30 58	eqnetrd	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑚 ) ≠ 0 )
60	25 28 59	prodfn0	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( · , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ≠ 0 )
61	23 60	eqnetrd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )
62	61	expr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) )
63	62	exlimdv	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) )
64	63	expimpd	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 ) )
65		fz1f1o	⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
66	1 65	syl	⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
67	10 64 66	mpjaod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ≠ 0 )