Metamath Proof Explorer


Theorem coprmdvds2

Description: If an integer is divisible by two coprime integers, then it is divisible by their product. (Contributed by Mario Carneiro, 24-Feb-2014)

Ref Expression
Assertion coprmdvds2 ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โ†’ ( ( ๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ ) โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) )

Proof

Step Hyp Ref Expression
1 divides โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โ†’ ( ๐‘ โˆฅ ๐พ โ†” โˆƒ ๐‘ฅ โˆˆ โ„ค ( ๐‘ฅ ยท ๐‘ ) = ๐พ ) )
2 1 3adant1 โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โ†’ ( ๐‘ โˆฅ ๐พ โ†” โˆƒ ๐‘ฅ โˆˆ โ„ค ( ๐‘ฅ ยท ๐‘ ) = ๐พ ) )
3 2 adantr โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โ†’ ( ๐‘ โˆฅ ๐พ โ†” โˆƒ ๐‘ฅ โˆˆ โ„ค ( ๐‘ฅ ยท ๐‘ ) = ๐พ ) )
4 simprr โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ๐‘ฅ โˆˆ โ„ค )
5 simpl2 โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ๐‘ โˆˆ โ„ค )
6 zcn โŠข ( ๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„‚ )
7 zcn โŠข ( ๐‘ โˆˆ โ„ค โ†’ ๐‘ โˆˆ โ„‚ )
8 mulcom โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ ) โ†’ ( ๐‘ฅ ยท ๐‘ ) = ( ๐‘ ยท ๐‘ฅ ) )
9 6 7 8 syl2an โŠข ( ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ ยท ๐‘ ) = ( ๐‘ ยท ๐‘ฅ ) )
10 4 5 9 syl2anc โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ๐‘ฅ ยท ๐‘ ) = ( ๐‘ ยท ๐‘ฅ ) )
11 10 breq2d โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ๐‘€ โˆฅ ( ๐‘ฅ ยท ๐‘ ) โ†” ๐‘€ โˆฅ ( ๐‘ ยท ๐‘ฅ ) ) )
12 simprl โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ๐‘€ gcd ๐‘ ) = 1 )
13 simpl1 โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ๐‘€ โˆˆ โ„ค )
14 coprmdvds โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ๐‘€ โˆฅ ( ๐‘ ยท ๐‘ฅ ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โ†’ ๐‘€ โˆฅ ๐‘ฅ ) )
15 13 5 4 14 syl3anc โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘€ โˆฅ ( ๐‘ ยท ๐‘ฅ ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โ†’ ๐‘€ โˆฅ ๐‘ฅ ) )
16 12 15 mpan2d โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ๐‘€ โˆฅ ( ๐‘ ยท ๐‘ฅ ) โ†’ ๐‘€ โˆฅ ๐‘ฅ ) )
17 11 16 sylbid โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ๐‘€ โˆฅ ( ๐‘ฅ ยท ๐‘ ) โ†’ ๐‘€ โˆฅ ๐‘ฅ ) )
18 dvdsmulc โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘€ โˆฅ ๐‘ฅ โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ( ๐‘ฅ ยท ๐‘ ) ) )
19 13 4 5 18 syl3anc โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ๐‘€ โˆฅ ๐‘ฅ โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ( ๐‘ฅ ยท ๐‘ ) ) )
20 17 19 syld โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ๐‘€ โˆฅ ( ๐‘ฅ ยท ๐‘ ) โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ( ๐‘ฅ ยท ๐‘ ) ) )
21 breq2 โŠข ( ( ๐‘ฅ ยท ๐‘ ) = ๐พ โ†’ ( ๐‘€ โˆฅ ( ๐‘ฅ ยท ๐‘ ) โ†” ๐‘€ โˆฅ ๐พ ) )
22 breq2 โŠข ( ( ๐‘ฅ ยท ๐‘ ) = ๐พ โ†’ ( ( ๐‘€ ยท ๐‘ ) โˆฅ ( ๐‘ฅ ยท ๐‘ ) โ†” ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) )
23 21 22 imbi12d โŠข ( ( ๐‘ฅ ยท ๐‘ ) = ๐พ โ†’ ( ( ๐‘€ โˆฅ ( ๐‘ฅ ยท ๐‘ ) โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ( ๐‘ฅ ยท ๐‘ ) ) โ†” ( ๐‘€ โˆฅ ๐พ โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) ) )
24 20 23 syl5ibcom โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ( ๐‘€ gcd ๐‘ ) = 1 โˆง ๐‘ฅ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘ฅ ยท ๐‘ ) = ๐พ โ†’ ( ๐‘€ โˆฅ ๐พ โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) ) )
25 24 anassrs โŠข ( ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โˆง ๐‘ฅ โˆˆ โ„ค ) โ†’ ( ( ๐‘ฅ ยท ๐‘ ) = ๐พ โ†’ ( ๐‘€ โˆฅ ๐พ โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) ) )
26 25 rexlimdva โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โ†’ ( โˆƒ ๐‘ฅ โˆˆ โ„ค ( ๐‘ฅ ยท ๐‘ ) = ๐พ โ†’ ( ๐‘€ โˆฅ ๐พ โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) ) )
27 3 26 sylbid โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โ†’ ( ๐‘ โˆฅ ๐พ โ†’ ( ๐‘€ โˆฅ ๐พ โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) ) )
28 27 impcomd โŠข ( ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โˆง ( ๐‘€ gcd ๐‘ ) = 1 ) โ†’ ( ( ๐‘€ โˆฅ ๐พ โˆง ๐‘ โˆฅ ๐พ ) โ†’ ( ๐‘€ ยท ๐‘ ) โˆฅ ๐พ ) )