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 ⊢ Ⅎ k φ
fprodn0f.a ⊢ φ → A ∈ Fin
fprodn0f.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
fprodn0f.bne0 ⊢ φ ∧ k ∈ A → B ≠ 0
Assertion fprodn0f ⊢ φ → ∏ k ∈ A B ≠ 0

Proof

Step Hyp Ref Expression
1 fprodn0f.kph ⊢ Ⅎ k φ
2 fprodn0f.a ⊢ φ → A ∈ Fin
3 fprodn0f.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 fprodn0f.bne0 ⊢ φ ∧ k ∈ A → B ≠ 0
5 difssd ⊢ φ → ℂ ∖ 0 ⊆ ℂ
6 eldifi ⊢ x ∈ ℂ ∖ 0 → x ∈ ℂ
7 6 adantr ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → x ∈ ℂ
8 eldifi ⊢ y ∈ ℂ ∖ 0 → y ∈ ℂ
9 8 adantl ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → y ∈ ℂ
10 7 9 mulcld ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → x ⁢ y ∈ ℂ
11 eldifsni ⊢ x ∈ ℂ ∖ 0 → x ≠ 0
12 11 adantr ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → x ≠ 0
13 eldifsni ⊢ y ∈ ℂ ∖ 0 → y ≠ 0
14 13 adantl ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → y ≠ 0
15 7 9 12 14 mulne0d ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → x ⁢ y ≠ 0
16 15 neneqd ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → ¬ x ⁢ y = 0
17 ovex ⊢ x ⁢ y ∈ V
18 17 elsn ⊢ x ⁢ y ∈ 0 ↔ x ⁢ y = 0
19 16 18 sylnibr ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → ¬ x ⁢ y ∈ 0
20 10 19 eldifd ⊢ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → x ⁢ y ∈ ℂ ∖ 0
21 20 adantl ⊢ φ ∧ x ∈ ℂ ∖ 0 ∧ y ∈ ℂ ∖ 0 → x ⁢ y ∈ ℂ ∖ 0
22 4 neneqd ⊢ φ ∧ k ∈ A → ¬ B = 0
23 elsng ⊢ B ∈ ℂ → B ∈ 0 ↔ B = 0
24 3 23 syl ⊢ φ ∧ k ∈ A → B ∈ 0 ↔ B = 0
25 22 24 mtbird ⊢ φ ∧ k ∈ A → ¬ B ∈ 0
26 3 25 eldifd ⊢ φ ∧ k ∈ A → B ∈ ℂ ∖ 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 ⊢ φ → ∏ k ∈ A B ∈ ℂ ∖ 0
36 eldifsni ⊢ ∏ k ∈ A B ∈ ℂ ∖ 0 → ∏ k ∈ A B ≠ 0
37 35 36 syl ⊢ φ → ∏ k ∈ A B ≠ 0