Metamath Proof Explorer


Theorem coprm

Description: A prime number either divides an integer or is coprime to it, but not both. Theorem 1.8 in ApostolNT p. 17. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion coprm ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑃𝑁 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 prmz ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
2 gcddvds ( ( 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 gcd 𝑁 ) ∥ 𝑃 ∧ ( 𝑃 gcd 𝑁 ) ∥ 𝑁 ) )
3 1 2 sylan ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 gcd 𝑁 ) ∥ 𝑃 ∧ ( 𝑃 gcd 𝑁 ) ∥ 𝑁 ) )
4 3 simprd ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 gcd 𝑁 ) ∥ 𝑁 )
5 breq1 ( ( 𝑃 gcd 𝑁 ) = 𝑃 → ( ( 𝑃 gcd 𝑁 ) ∥ 𝑁𝑃𝑁 ) )
6 4 5 syl5ibcom ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 gcd 𝑁 ) = 𝑃𝑃𝑁 ) )
7 6 con3d ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑃𝑁 → ¬ ( 𝑃 gcd 𝑁 ) = 𝑃 ) )
8 0nnn ¬ 0 ∈ ℕ
9 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
10 eleq1 ( 𝑃 = 0 → ( 𝑃 ∈ ℕ ↔ 0 ∈ ℕ ) )
11 9 10 syl5ibcom ( 𝑃 ∈ ℙ → ( 𝑃 = 0 → 0 ∈ ℕ ) )
12 8 11 mtoi ( 𝑃 ∈ ℙ → ¬ 𝑃 = 0 )
13 12 intnanrd ( 𝑃 ∈ ℙ → ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) )
14 13 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) )
15 gcdn0cl ( ( ( 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑃 gcd 𝑁 ) ∈ ℕ )
16 15 ex ( ( 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) → ( 𝑃 gcd 𝑁 ) ∈ ℕ ) )
17 1 16 sylan ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) → ( 𝑃 gcd 𝑁 ) ∈ ℕ ) )
18 14 17 mpd ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 gcd 𝑁 ) ∈ ℕ )
19 3 simpld ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 gcd 𝑁 ) ∥ 𝑃 )
20 isprm2 ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
21 20 simprbi ( 𝑃 ∈ ℙ → ∀ 𝑧 ∈ ℕ ( 𝑧𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
22 breq1 ( 𝑧 = ( 𝑃 gcd 𝑁 ) → ( 𝑧𝑃 ↔ ( 𝑃 gcd 𝑁 ) ∥ 𝑃 ) )
23 eqeq1 ( 𝑧 = ( 𝑃 gcd 𝑁 ) → ( 𝑧 = 1 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) )
24 eqeq1 ( 𝑧 = ( 𝑃 gcd 𝑁 ) → ( 𝑧 = 𝑃 ↔ ( 𝑃 gcd 𝑁 ) = 𝑃 ) )
25 23 24 orbi12d ( 𝑧 = ( 𝑃 gcd 𝑁 ) → ( ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ↔ ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) ) )
26 22 25 imbi12d ( 𝑧 = ( 𝑃 gcd 𝑁 ) → ( ( 𝑧𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ( ( 𝑃 gcd 𝑁 ) ∥ 𝑃 → ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) ) ) )
27 26 rspcv ( ( 𝑃 gcd 𝑁 ) ∈ ℕ → ( ∀ 𝑧 ∈ ℕ ( 𝑧𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) → ( ( 𝑃 gcd 𝑁 ) ∥ 𝑃 → ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) ) ) )
28 21 27 syl5com ( 𝑃 ∈ ℙ → ( ( 𝑃 gcd 𝑁 ) ∈ ℕ → ( ( 𝑃 gcd 𝑁 ) ∥ 𝑃 → ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) ) ) )
29 28 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 gcd 𝑁 ) ∈ ℕ → ( ( 𝑃 gcd 𝑁 ) ∥ 𝑃 → ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) ) ) )
30 18 19 29 mp2d ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) )
31 biorf ( ¬ ( 𝑃 gcd 𝑁 ) = 𝑃 → ( ( 𝑃 gcd 𝑁 ) = 1 ↔ ( ( 𝑃 gcd 𝑁 ) = 𝑃 ∨ ( 𝑃 gcd 𝑁 ) = 1 ) ) )
32 orcom ( ( ( 𝑃 gcd 𝑁 ) = 𝑃 ∨ ( 𝑃 gcd 𝑁 ) = 1 ) ↔ ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) )
33 31 32 bitrdi ( ¬ ( 𝑃 gcd 𝑁 ) = 𝑃 → ( ( 𝑃 gcd 𝑁 ) = 1 ↔ ( ( 𝑃 gcd 𝑁 ) = 1 ∨ ( 𝑃 gcd 𝑁 ) = 𝑃 ) ) )
34 30 33 syl5ibrcom ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑃 gcd 𝑁 ) = 𝑃 → ( 𝑃 gcd 𝑁 ) = 1 ) )
35 7 34 syld ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑃𝑁 → ( 𝑃 gcd 𝑁 ) = 1 ) )
36 iddvds ( 𝑃 ∈ ℤ → 𝑃𝑃 )
37 1 36 syl ( 𝑃 ∈ ℙ → 𝑃𝑃 )
38 37 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → 𝑃𝑃 )
39 dvdslegcd ( ( ( 𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑃𝑃𝑃𝑁 ) → 𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) )
40 39 ex ( ( 𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑃𝑃𝑃𝑁 ) → 𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) ) )
41 40 3anidm12 ( ( 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑃𝑃𝑃𝑁 ) → 𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) ) )
42 1 41 sylan ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑃 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑃𝑃𝑃𝑁 ) → 𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) ) )
43 14 42 mpd ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃𝑃𝑃𝑁 ) → 𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) )
44 38 43 mpand ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃𝑁𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) )
45 prmgt1 ( 𝑃 ∈ ℙ → 1 < 𝑃 )
46 45 adantr ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → 1 < 𝑃 )
47 1re 1 ∈ ℝ
48 1 zred ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
49 18 nnred ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 gcd 𝑁 ) ∈ ℝ )
50 ltletr ( ( 1 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ ( 𝑃 gcd 𝑁 ) ∈ ℝ ) → ( ( 1 < 𝑃𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) → 1 < ( 𝑃 gcd 𝑁 ) ) )
51 47 48 49 50 mp3an2ani ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ( 1 < 𝑃𝑃 ≤ ( 𝑃 gcd 𝑁 ) ) → 1 < ( 𝑃 gcd 𝑁 ) ) )
52 46 51 mpand ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ≤ ( 𝑃 gcd 𝑁 ) → 1 < ( 𝑃 gcd 𝑁 ) ) )
53 ltne ( ( 1 ∈ ℝ ∧ 1 < ( 𝑃 gcd 𝑁 ) ) → ( 𝑃 gcd 𝑁 ) ≠ 1 )
54 47 53 mpan ( 1 < ( 𝑃 gcd 𝑁 ) → ( 𝑃 gcd 𝑁 ) ≠ 1 )
55 54 a1i ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 1 < ( 𝑃 gcd 𝑁 ) → ( 𝑃 gcd 𝑁 ) ≠ 1 ) )
56 44 52 55 3syld ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( 𝑃𝑁 → ( 𝑃 gcd 𝑁 ) ≠ 1 ) )
57 56 necon2bd ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 gcd 𝑁 ) = 1 → ¬ 𝑃𝑁 ) )
58 35 57 impbid ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ) → ( ¬ 𝑃𝑁 ↔ ( 𝑃 gcd 𝑁 ) = 1 ) )