Metamath Proof Explorer

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 )