Metamath Proof Explorer

Theorem dvdsprime

Description: If M divides a prime, then M is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014)

Ref Expression
Assertion dvdsprime 
|- ( ( P e. Prime /\ M e. NN ) -> ( M || P <-> ( M = P \/ M = 1 ) ) )

Proof

Step Hyp Ref Expression
1 isprm2 
 |-  ( P e. Prime <-> ( P e. ( ZZ>= ` 2 ) /\ A. m e. NN ( m || P -> ( m = 1 \/ m = P ) ) ) )
2 breq1 
 |-  ( m = M -> ( m || P <-> M || P ) )
3 eqeq1 
 |-  ( m = M -> ( m = 1 <-> M = 1 ) )
4 eqeq1 
 |-  ( m = M -> ( m = P <-> M = P ) )
5 3 4 orbi12d 
 |-  ( m = M -> ( ( m = 1 \/ m = P ) <-> ( M = 1 \/ M = P ) ) )
6 orcom 
 |-  ( ( M = 1 \/ M = P ) <-> ( M = P \/ M = 1 ) )
7 5 6 bitrdi 
 |-  ( m = M -> ( ( m = 1 \/ m = P ) <-> ( M = P \/ M = 1 ) ) )
8 2 7 imbi12d 
 |-  ( m = M -> ( ( m || P -> ( m = 1 \/ m = P ) ) <-> ( M || P -> ( M = P \/ M = 1 ) ) ) )
9 8 rspccva 
 |-  ( ( A. m e. NN ( m || P -> ( m = 1 \/ m = P ) ) /\ M e. NN ) -> ( M || P -> ( M = P \/ M = 1 ) ) )
10 9 adantll 
 |-  ( ( ( P e. ( ZZ>= ` 2 ) /\ A. m e. NN ( m || P -> ( m = 1 \/ m = P ) ) ) /\ M e. NN ) -> ( M || P -> ( M = P \/ M = 1 ) ) )
11 1 10 sylanb 
 |-  ( ( P e. Prime /\ M e. NN ) -> ( M || P -> ( M = P \/ M = 1 ) ) )
12 prmz 
 |-  ( P e. Prime -> P e. ZZ )
13 iddvds 
 |-  ( P e. ZZ -> P || P )
14 12 13 syl 
 |-  ( P e. Prime -> P || P )
15 14 adantr 
 |-  ( ( P e. Prime /\ M e. NN ) -> P || P )
16 breq1 
 |-  ( M = P -> ( M || P <-> P || P ) )
17 15 16 syl5ibrcom 
 |-  ( ( P e. Prime /\ M e. NN ) -> ( M = P -> M || P ) )
18 1dvds 
 |-  ( P e. ZZ -> 1 || P )
19 12 18 syl 
 |-  ( P e. Prime -> 1 || P )
20 19 adantr 
 |-  ( ( P e. Prime /\ M e. NN ) -> 1 || P )
21 breq1 
 |-  ( M = 1 -> ( M || P <-> 1 || P ) )
22 20 21 syl5ibrcom 
 |-  ( ( P e. Prime /\ M e. NN ) -> ( M = 1 -> M || P ) )
23 17 22 jaod 
 |-  ( ( P e. Prime /\ M e. NN ) -> ( ( M = P \/ M = 1 ) -> M || P ) )
24 11 23 impbid 
 |-  ( ( P e. Prime /\ M e. NN ) -> ( M || P <-> ( M = P \/ M = 1 ) ) )