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