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 MMFinKF:mMnMmFmgcdFn=1mMFmKmMFmK

Proof

Step Hyp Ref Expression
1 cleq1lem x=xKF:KF:
2 difeq1 x=xm=m
3 2 raleqdv x=nxmFmgcdFn=1nmFmgcdFn=1
4 3 raleqbi1dv x=mxnxmFmgcdFn=1mnmFmgcdFn=1
5 raleq x=mxFmKmFmK
6 4 5 anbi12d x=mxnxmFmgcdFn=1mxFmKmnmFmgcdFn=1mFmK
7 1 6 anbi12d x=xKF:mxnxmFmgcdFn=1mxFmKKF:mnmFmgcdFn=1mFmK
8 prodeq1 x=mxFm=mFm
9 8 breq1d x=mxFmKmFmK
10 7 9 imbi12d x=xKF:mxnxmFmgcdFn=1mxFmKmxFmKKF:mnmFmgcdFn=1mFmKmFmK
11 cleq1lem x=yxKF:yKF:
12 difeq1 x=yxm=ym
13 12 raleqdv x=ynxmFmgcdFn=1nymFmgcdFn=1
14 13 raleqbi1dv x=ymxnxmFmgcdFn=1mynymFmgcdFn=1
15 raleq x=ymxFmKmyFmK
16 14 15 anbi12d x=ymxnxmFmgcdFn=1mxFmKmynymFmgcdFn=1myFmK
17 11 16 anbi12d x=yxKF:mxnxmFmgcdFn=1mxFmKyKF:mynymFmgcdFn=1myFmK
18 prodeq1 x=ymxFm=myFm
19 18 breq1d x=ymxFmKmyFmK
20 17 19 imbi12d x=yxKF:mxnxmFmgcdFn=1mxFmKmxFmKyKF:mynymFmgcdFn=1myFmKmyFmK
21 cleq1lem x=yzxKF:yzKF:
22 difeq1 x=yzxm=yzm
23 22 raleqdv x=yznxmFmgcdFn=1nyzmFmgcdFn=1
24 23 raleqbi1dv x=yzmxnxmFmgcdFn=1myznyzmFmgcdFn=1
25 raleq x=yzmxFmKmyzFmK
26 24 25 anbi12d x=yzmxnxmFmgcdFn=1mxFmKmyznyzmFmgcdFn=1myzFmK
27 21 26 anbi12d x=yzxKF:mxnxmFmgcdFn=1mxFmKyzKF:myznyzmFmgcdFn=1myzFmK
28 prodeq1 x=yzmxFm=myzFm
29 28 breq1d x=yzmxFmKmyzFmK
30 27 29 imbi12d x=yzxKF:mxnxmFmgcdFn=1mxFmKmxFmKyzKF:myznyzmFmgcdFn=1myzFmKmyzFmK
31 cleq1lem x=MxKF:MKF:
32 difeq1 x=Mxm=Mm
33 32 raleqdv x=MnxmFmgcdFn=1nMmFmgcdFn=1
34 33 raleqbi1dv x=MmxnxmFmgcdFn=1mMnMmFmgcdFn=1
35 raleq x=MmxFmKmMFmK
36 34 35 anbi12d x=MmxnxmFmgcdFn=1mxFmKmMnMmFmgcdFn=1mMFmK
37 31 36 anbi12d x=MxKF:mxnxmFmgcdFn=1mxFmKMKF:mMnMmFmgcdFn=1mMFmK
38 prodeq1 x=MmxFm=mMFm
39 38 breq1d x=MmxFmKmMFmK
40 37 39 imbi12d x=MxKF:mxnxmFmgcdFn=1mxFmKmxFmKMKF:mMnMmFmgcdFn=1mMFmKmMFmK
41 prod0 mFm=1
42 nnz KK
43 1dvds K1K
44 42 43 syl K1K
45 41 44 eqbrtrid KmFmK
46 45 adantr KF:mFmK
47 46 ad2antlr KF:mnmFmgcdFn=1mFmKmFmK
48 coprmproddvdslem yFin¬zyyKF:mynymFmgcdFn=1myFmKmyFmKyzKF:myznyzmFmgcdFn=1myzFmKmyzFmK
49 10 20 30 40 47 48 findcard2s MFinMKF:mMnMmFmgcdFn=1mMFmKmMFmK
50 49 exp4c MFinMKF:mMnMmFmgcdFn=1mMFmKmMFmK
51 50 impcom MMFinKF:mMnMmFmgcdFn=1mMFmKmMFmK
52 51 3imp MMFinKF:mMnMmFmgcdFn=1mMFmKmMFmK