Metamath Proof Explorer

Theorem coprmproddvds

Description: If a positive integer is divisible by each element of a set of pairwise coprime positive integers, then it is divisible by their product. (Contributed by AV, 19-Aug-2020)

Ref Expression
Assertion coprmproddvds 
|- ( ( ( M C_ NN /\ M e. Fin ) /\ ( K e. NN /\ F : NN --> NN ) /\ ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) ) -> prod_ m e. M ( F ` m ) || K )

Proof

Step Hyp Ref Expression
1 cleq1lem 
 |-  ( x = (/) -> ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) <-> ( (/) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) )
2 difeq1 
 |-  ( x = (/) -> ( x \ { m } ) = ( (/) \ { m } ) )
3 2 raleqdv 
 |-  ( x = (/) -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
4 3 raleqbi1dv 
 |-  ( x = (/) -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
5 raleq 
 |-  ( x = (/) -> ( A. m e. x ( F ` m ) || K <-> A. m e. (/) ( F ` m ) || K ) )
6 4 5 anbi12d 
 |-  ( x = (/) -> ( ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) <-> ( A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. (/) ( F ` m ) || K ) ) )
7 1 6 anbi12d 
 |-  ( x = (/) -> ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) <-> ( ( (/) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. (/) ( F ` m ) || K ) ) ) )
8 prodeq1 
 |-  ( x = (/) -> prod_ m e. x ( F ` m ) = prod_ m e. (/) ( F ` m ) )
9 8 breq1d 
 |-  ( x = (/) -> ( prod_ m e. x ( F ` m ) || K <-> prod_ m e. (/) ( F ` m ) || K ) )
10 7 9 imbi12d 
 |-  ( x = (/) -> ( ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) -> prod_ m e. x ( F ` m ) || K ) <-> ( ( ( (/) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. (/) ( F ` m ) || K ) ) -> prod_ m e. (/) ( F ` m ) || K ) ) )
11 cleq1lem 
 |-  ( x = y -> ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) <-> ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) )
12 difeq1 
 |-  ( x = y -> ( x \ { m } ) = ( y \ { m } ) )
13 12 raleqdv 
 |-  ( x = y -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
14 13 raleqbi1dv 
 |-  ( x = y -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
15 raleq 
 |-  ( x = y -> ( A. m e. x ( F ` m ) || K <-> A. m e. y ( F ` m ) || K ) )
16 14 15 anbi12d 
 |-  ( x = y -> ( ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) <-> ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) )
17 11 16 anbi12d 
 |-  ( x = y -> ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) <-> ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) ) )
18 prodeq1 
 |-  ( x = y -> prod_ m e. x ( F ` m ) = prod_ m e. y ( F ` m ) )
19 18 breq1d 
 |-  ( x = y -> ( prod_ m e. x ( F ` m ) || K <-> prod_ m e. y ( F ` m ) || K ) )
20 17 19 imbi12d 
 |-  ( x = y -> ( ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) -> prod_ m e. x ( F ` m ) || K ) <-> ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) ) )
21 cleq1lem 
 |-  ( x = ( y u. { z } ) -> ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) <-> ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) )
22 difeq1 
 |-  ( x = ( y u. { z } ) -> ( x \ { m } ) = ( ( y u. { z } ) \ { m } ) )
23 22 raleqdv 
 |-  ( x = ( y u. { z } ) -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
24 23 raleqbi1dv 
 |-  ( x = ( y u. { z } ) -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
25 raleq 
 |-  ( x = ( y u. { z } ) -> ( A. m e. x ( F ` m ) || K <-> A. m e. ( y u. { z } ) ( F ` m ) || K ) )
26 24 25 anbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) <-> ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) )
27 21 26 anbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) <-> ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) ) )
28 prodeq1 
 |-  ( x = ( y u. { z } ) -> prod_ m e. x ( F ` m ) = prod_ m e. ( y u. { z } ) ( F ` m ) )
29 28 breq1d 
 |-  ( x = ( y u. { z } ) -> ( prod_ m e. x ( F ` m ) || K <-> prod_ m e. ( y u. { z } ) ( F ` m ) || K ) )
30 27 29 imbi12d 
 |-  ( x = ( y u. { z } ) -> ( ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) -> prod_ m e. x ( F ` m ) || K ) <-> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) || K ) ) )
31 cleq1lem 
 |-  ( x = M -> ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) <-> ( M C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) ) )
32 difeq1 
 |-  ( x = M -> ( x \ { m } ) = ( M \ { m } ) )
33 32 raleqdv 
 |-  ( x = M -> ( A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
34 33 raleqbi1dv 
 |-  ( x = M -> ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 <-> A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 ) )
35 raleq 
 |-  ( x = M -> ( A. m e. x ( F ` m ) || K <-> A. m e. M ( F ` m ) || K ) )
36 34 35 anbi12d 
 |-  ( x = M -> ( ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) <-> ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) ) )
37 31 36 anbi12d 
 |-  ( x = M -> ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) <-> ( ( M C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) ) ) )
38 prodeq1 
 |-  ( x = M -> prod_ m e. x ( F ` m ) = prod_ m e. M ( F ` m ) )
39 38 breq1d 
 |-  ( x = M -> ( prod_ m e. x ( F ` m ) || K <-> prod_ m e. M ( F ` m ) || K ) )
40 37 39 imbi12d 
 |-  ( x = M -> ( ( ( ( x C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. x A. n e. ( x \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. x ( F ` m ) || K ) ) -> prod_ m e. x ( F ` m ) || K ) <-> ( ( ( M C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) ) -> prod_ m e. M ( F ` m ) || K ) ) )
41 prod0 
 |-  prod_ m e. (/) ( F ` m ) = 1
42 nnz 
 |-  ( K e. NN -> K e. ZZ )
43 1dvds 
 |-  ( K e. ZZ -> 1 || K )
44 42 43 syl 
 |-  ( K e. NN -> 1 || K )
45 41 44 eqbrtrid 
 |-  ( K e. NN -> prod_ m e. (/) ( F ` m ) || K )
46 45 adantr 
 |-  ( ( K e. NN /\ F : NN --> NN ) -> prod_ m e. (/) ( F ` m ) || K )
47 46 ad2antlr 
 |-  ( ( ( (/) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. (/) A. n e. ( (/) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. (/) ( F ` m ) || K ) ) -> prod_ m e. (/) ( F ` m ) || K )
48 coprmproddvdslem 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( ( ( y C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. y A. n e. ( y \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. y ( F ` m ) || K ) ) -> prod_ m e. y ( F ` m ) || K ) -> ( ( ( ( y u. { z } ) C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. ( y u. { z } ) A. n e. ( ( y u. { z } ) \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. ( y u. { z } ) ( F ` m ) || K ) ) -> prod_ m e. ( y u. { z } ) ( F ` m ) || K ) ) )
49 10 20 30 40 47 48 findcard2s 
 |-  ( M e. Fin -> ( ( ( M C_ NN /\ ( K e. NN /\ F : NN --> NN ) ) /\ ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) ) -> prod_ m e. M ( F ` m ) || K ) )
50 49 exp4c 
 |-  ( M e. Fin -> ( M C_ NN -> ( ( K e. NN /\ F : NN --> NN ) -> ( ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) -> prod_ m e. M ( F ` m ) || K ) ) ) )
51 50 impcom 
 |-  ( ( M C_ NN /\ M e. Fin ) -> ( ( K e. NN /\ F : NN --> NN ) -> ( ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) -> prod_ m e. M ( F ` m ) || K ) ) )
52 51 3imp 
 |-  ( ( ( M C_ NN /\ M e. Fin ) /\ ( K e. NN /\ F : NN --> NN ) /\ ( A. m e. M A. n e. ( M \ { m } ) ( ( F ` m ) gcd ( F ` n ) ) = 1 /\ A. m e. M ( F ` m ) || K ) ) -> prod_ m e. M ( F ` m ) || K )