This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )