Metamath Proof Explorer


Theorem euclemma

Description: Euclid's lemma. A prime number divides the product of two integers iff it divides at least one of them. Theorem 1.9 in ApostolNT p. 17. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Assertion euclemma ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โ†” ( ๐‘ƒ โˆฅ ๐‘€ โˆจ ๐‘ƒ โˆฅ ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 coprm โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค ) โ†’ ( ยฌ ๐‘ƒ โˆฅ ๐‘€ โ†” ( ๐‘ƒ gcd ๐‘€ ) = 1 ) )
2 1 3adant3 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ยฌ ๐‘ƒ โˆฅ ๐‘€ โ†” ( ๐‘ƒ gcd ๐‘€ ) = 1 ) )
3 2 anbi2d โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โˆง ยฌ ๐‘ƒ โˆฅ ๐‘€ ) โ†” ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โˆง ( ๐‘ƒ gcd ๐‘€ ) = 1 ) ) )
4 prmz โŠข ( ๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค )
5 coprmdvds โŠข ( ( ๐‘ƒ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โˆง ( ๐‘ƒ gcd ๐‘€ ) = 1 ) โ†’ ๐‘ƒ โˆฅ ๐‘ ) )
6 4 5 syl3an1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โˆง ( ๐‘ƒ gcd ๐‘€ ) = 1 ) โ†’ ๐‘ƒ โˆฅ ๐‘ ) )
7 3 6 sylbid โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โˆง ยฌ ๐‘ƒ โˆฅ ๐‘€ ) โ†’ ๐‘ƒ โˆฅ ๐‘ ) )
8 7 expd โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โ†’ ( ยฌ ๐‘ƒ โˆฅ ๐‘€ โ†’ ๐‘ƒ โˆฅ ๐‘ ) ) )
9 df-or โŠข ( ( ๐‘ƒ โˆฅ ๐‘€ โˆจ ๐‘ƒ โˆฅ ๐‘ ) โ†” ( ยฌ ๐‘ƒ โˆฅ ๐‘€ โ†’ ๐‘ƒ โˆฅ ๐‘ ) )
10 8 9 imbitrrdi โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โ†’ ( ๐‘ƒ โˆฅ ๐‘€ โˆจ ๐‘ƒ โˆฅ ๐‘ ) ) )
11 ordvdsmul โŠข ( ( ๐‘ƒ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โˆฅ ๐‘€ โˆจ ๐‘ƒ โˆฅ ๐‘ ) โ†’ ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )
12 4 11 syl3an1 โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ƒ โˆฅ ๐‘€ โˆจ ๐‘ƒ โˆฅ ๐‘ ) โ†’ ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )
13 10 12 impbid โŠข ( ( ๐‘ƒ โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ƒ โˆฅ ( ๐‘€ ยท ๐‘ ) โ†” ( ๐‘ƒ โˆฅ ๐‘€ โˆจ ๐‘ƒ โˆฅ ๐‘ ) ) )