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 ) )