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 
|- F/ k ph
fprodn0f.a 
|- ( ph -> A e. Fin )
fprodn0f.b 
|- ( ( ph /\ k e. A ) -> B e. CC )
fprodn0f.bne0 
|- ( ( ph /\ k e. A ) -> B =/= 0 )
Assertion fprodn0f 
|- ( ph -> prod_ k e. A B =/= 0 )

Proof

Step Hyp Ref Expression
1 fprodn0f.kph 
 |-  F/ k ph
2 fprodn0f.a 
 |-  ( ph -> A e. Fin )
3 fprodn0f.b 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 fprodn0f.bne0 
 |-  ( ( ph /\ k e. A ) -> B =/= 0 )
5 difssd 
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
6 eldifi 
 |-  ( x e. ( CC \ { 0 } ) -> x e. CC )
7 6 adantr 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> x e. CC )
8 eldifi 
 |-  ( y e. ( CC \ { 0 } ) -> y e. CC )
9 8 adantl 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> y e. CC )
10 7 9 mulcld 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) e. CC )
11 eldifsni 
 |-  ( x e. ( CC \ { 0 } ) -> x =/= 0 )
12 11 adantr 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> x =/= 0 )
13 eldifsni 
 |-  ( y e. ( CC \ { 0 } ) -> y =/= 0 )
14 13 adantl 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> y =/= 0 )
15 7 9 12 14 mulne0d 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) =/= 0 )
16 15 neneqd 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> -. ( x x. y ) = 0 )
17 ovex 
 |-  ( x x. y ) e. _V
18 17 elsn 
 |-  ( ( x x. y ) e. { 0 } <-> ( x x. y ) = 0 )
19 16 18 sylnibr 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> -. ( x x. y ) e. { 0 } )
20 10 19 eldifd 
 |-  ( ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) -> ( x x. y ) e. ( CC \ { 0 } ) )
21 20 adantl 
 |-  ( ( ph /\ ( x e. ( CC \ { 0 } ) /\ y e. ( CC \ { 0 } ) ) ) -> ( x x. y ) e. ( CC \ { 0 } ) )
22 4 neneqd 
 |-  ( ( ph /\ k e. A ) -> -. B = 0 )
23 elsng 
 |-  ( B e. CC -> ( B e. { 0 } <-> B = 0 ) )
24 3 23 syl 
 |-  ( ( ph /\ k e. A ) -> ( B e. { 0 } <-> B = 0 ) )
25 22 24 mtbird 
 |-  ( ( ph /\ k e. A ) -> -. B e. { 0 } )
26 3 25 eldifd 
 |-  ( ( ph /\ k e. A ) -> B e. ( CC \ { 0 } ) )
27 ax-1cn 
 |-  1 e. CC
28 ax-1ne0 
 |-  1 =/= 0
29 1ex 
 |-  1 e. _V
30 29 elsn 
 |-  ( 1 e. { 0 } <-> 1 = 0 )
31 28 30 nemtbir 
 |-  -. 1 e. { 0 }
32 eldif 
 |-  ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ -. 1 e. { 0 } ) )
33 27 31 32 mpbir2an 
 |-  1 e. ( CC \ { 0 } )
34 33 a1i 
 |-  ( ph -> 1 e. ( CC \ { 0 } ) )
35 1 5 21 2 26 34 fprodcllemf 
 |-  ( ph -> prod_ k e. A B e. ( CC \ { 0 } ) )
36 eldifsni 
 |-  ( prod_ k e. A B e. ( CC \ { 0 } ) -> prod_ k e. A B =/= 0 )
37 35 36 syl 
 |-  ( ph -> prod_ k e. A B =/= 0 )