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 
|- ( ph -> A e. Fin )
fprodn0.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
fprodn0.3 
|- ( ( ph /\ k e. A ) -> B =/= 0 )
Assertion fprodn0 
|- ( ph -> prod_ k e. A B =/= 0 )

Proof

Step Hyp Ref Expression
1 fprodn0.1 
 |-  ( ph -> A e. Fin )
2 fprodn0.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 fprodn0.3 
 |-  ( ( ph /\ k e. A ) -> B =/= 0 )
4 prodeq1 
 |-  ( A = (/) -> prod_ k e. A B = prod_ k e. (/) B )
5 prod0 
 |-  prod_ k e. (/) B = 1
6 4 5 eqtrdi 
 |-  ( A = (/) -> prod_ k e. A B = 1 )
7 ax-1ne0 
 |-  1 =/= 0
8 7 a1i 
 |-  ( A = (/) -> 1 =/= 0 )
9 6 8 eqnetrd 
 |-  ( A = (/) -> prod_ k e. A B =/= 0 )
10 9 a1i 
 |-  ( ph -> ( A = (/) -> prod_ k e. A B =/= 0 ) )
11 prodfc 
 |-  prod_ m e. A ( ( k e. A |-> B ) ` m ) = prod_ k e. A B
12 fveq2 
 |-  ( m = ( f ` n ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
13 simprl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. NN )
14 simprr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
15 2 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
16 15 adantr 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( k e. A |-> B ) : A --> CC )
17 16 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
18 f1of 
 |-  ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> f : ( 1 ... ( # ` A ) ) --> A )
19 14 18 syl 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> f : ( 1 ... ( # ` A ) ) --> A )
20 fvco3 
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
21 19 20 sylan 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` n ) = ( ( k e. A |-> B ) ` ( f ` n ) ) )
22 12 13 14 17 21 fprod 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
23 11 22 eqtr3id 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B = ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) )
24 nnuz 
 |-  NN = ( ZZ>= ` 1 )
25 13 24 eleqtrdi 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( # ` A ) e. ( ZZ>= ` 1 ) )
26 fco 
 |-  ( ( ( k e. A |-> B ) : A --> CC /\ f : ( 1 ... ( # ` A ) ) --> A ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
27 16 19 26 syl2anc 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( ( k e. A |-> B ) o. f ) : ( 1 ... ( # ` A ) ) --> CC )
28 27 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` m ) e. CC )
29 fvco3 
 |-  ( ( f : ( 1 ... ( # ` A ) ) --> A /\ m e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` m ) = ( ( k e. A |-> B ) ` ( f ` m ) ) )
30 19 29 sylan 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` m ) = ( ( k e. A |-> B ) ` ( f ` m ) ) )
31 18 ffvelrnda 
 |-  ( ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ m e. ( 1 ... ( # ` A ) ) ) -> ( f ` m ) e. A )
32 31 adantll 
 |-  ( ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ m e. ( 1 ... ( # ` A ) ) ) -> ( f ` m ) e. A )
33 simpr 
 |-  ( ( ph /\ ( f ` m ) e. A ) -> ( f ` m ) e. A )
34 nfcv 
 |-  F/_ k ( f ` m )
35 nfv 
 |-  F/ k ph
36 nfcsb1v 
 |-  F/_ k [_ ( f ` m ) / k ]_ B
37 36 nfel1 
 |-  F/ k [_ ( f ` m ) / k ]_ B e. CC
38 35 37 nfim 
 |-  F/ k ( ph -> [_ ( f ` m ) / k ]_ B e. CC )
39 csbeq1a 
 |-  ( k = ( f ` m ) -> B = [_ ( f ` m ) / k ]_ B )
40 39 eleq1d 
 |-  ( k = ( f ` m ) -> ( B e. CC <-> [_ ( f ` m ) / k ]_ B e. CC ) )
41 40 imbi2d 
 |-  ( k = ( f ` m ) -> ( ( ph -> B e. CC ) <-> ( ph -> [_ ( f ` m ) / k ]_ B e. CC ) ) )
42 2 expcom 
 |-  ( k e. A -> ( ph -> B e. CC ) )
43 34 38 41 42 vtoclgaf 
 |-  ( ( f ` m ) e. A -> ( ph -> [_ ( f ` m ) / k ]_ B e. CC ) )
44 43 impcom 
 |-  ( ( ph /\ ( f ` m ) e. A ) -> [_ ( f ` m ) / k ]_ B e. CC )
45 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
46 45 fvmpts 
 |-  ( ( ( f ` m ) e. A /\ [_ ( f ` m ) / k ]_ B e. CC ) -> ( ( k e. A |-> B ) ` ( f ` m ) ) = [_ ( f ` m ) / k ]_ B )
47 33 44 46 syl2anc 
 |-  ( ( ph /\ ( f ` m ) e. A ) -> ( ( k e. A |-> B ) ` ( f ` m ) ) = [_ ( f ` m ) / k ]_ B )
48 nfcv 
 |-  F/_ k 0
49 36 48 nfne 
 |-  F/ k [_ ( f ` m ) / k ]_ B =/= 0
50 35 49 nfim 
 |-  F/ k ( ph -> [_ ( f ` m ) / k ]_ B =/= 0 )
51 39 neeq1d 
 |-  ( k = ( f ` m ) -> ( B =/= 0 <-> [_ ( f ` m ) / k ]_ B =/= 0 ) )
52 51 imbi2d 
 |-  ( k = ( f ` m ) -> ( ( ph -> B =/= 0 ) <-> ( ph -> [_ ( f ` m ) / k ]_ B =/= 0 ) ) )
53 3 expcom 
 |-  ( k e. A -> ( ph -> B =/= 0 ) )
54 34 50 52 53 vtoclgaf 
 |-  ( ( f ` m ) e. A -> ( ph -> [_ ( f ` m ) / k ]_ B =/= 0 ) )
55 54 impcom 
 |-  ( ( ph /\ ( f ` m ) e. A ) -> [_ ( f ` m ) / k ]_ B =/= 0 )
56 47 55 eqnetrd 
 |-  ( ( ph /\ ( f ` m ) e. A ) -> ( ( k e. A |-> B ) ` ( f ` m ) ) =/= 0 )
57 32 56 sylan2 
 |-  ( ( ph /\ ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ m e. ( 1 ... ( # ` A ) ) ) ) -> ( ( k e. A |-> B ) ` ( f ` m ) ) =/= 0 )
58 57 anassrs 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. ( 1 ... ( # ` A ) ) ) -> ( ( k e. A |-> B ) ` ( f ` m ) ) =/= 0 )
59 30 58 eqnetrd 
 |-  ( ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) /\ m e. ( 1 ... ( # ` A ) ) ) -> ( ( ( k e. A |-> B ) o. f ) ` m ) =/= 0 )
60 25 28 59 prodfn0 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> ( seq 1 ( x. , ( ( k e. A |-> B ) o. f ) ) ` ( # ` A ) ) =/= 0 )
61 23 60 eqnetrd 
 |-  ( ( ph /\ ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> prod_ k e. A B =/= 0 )
62 61 expr 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B =/= 0 ) )
63 62 exlimdv 
 |-  ( ( ph /\ ( # ` A ) e. NN ) -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> prod_ k e. A B =/= 0 ) )
64 63 expimpd 
 |-  ( ph -> ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> prod_ k e. A B =/= 0 ) )
65 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
66 1 65 syl 
 |-  ( ph -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
67 10 64 66 mpjaod 
 |-  ( ph -> prod_ k e. A B =/= 0 )