Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  coprm GIF version

Theorem coprm 11998
 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.)
Assertion
Ref Expression
coprm ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃𝑁 ↔ (𝑃 gcd 𝑁) = 1))

Proof of Theorem coprm
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 prmz 11968 . . . . . . 7 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
2 gcddvds 11827 . . . . . . 7 ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) ∥ 𝑃 ∧ (𝑃 gcd 𝑁) ∥ 𝑁))
31, 2sylan 281 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) ∥ 𝑃 ∧ (𝑃 gcd 𝑁) ∥ 𝑁))
43simprd 113 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∥ 𝑁)
5 breq1 3968 . . . . 5 ((𝑃 gcd 𝑁) = 𝑃 → ((𝑃 gcd 𝑁) ∥ 𝑁𝑃𝑁))
64, 5syl5ibcom 154 . . . 4 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) = 𝑃𝑃𝑁))
76con3d 621 . . 3 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃𝑁 → ¬ (𝑃 gcd 𝑁) = 𝑃))
8 0nnn 8843 . . . . . . . . 9 ¬ 0 ∈ ℕ
9 prmnn 11967 . . . . . . . . . 10 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
10 eleq1 2220 . . . . . . . . . 10 (𝑃 = 0 → (𝑃 ∈ ℕ ↔ 0 ∈ ℕ))
119, 10syl5ibcom 154 . . . . . . . . 9 (𝑃 ∈ ℙ → (𝑃 = 0 → 0 ∈ ℕ))
128, 11mtoi 654 . . . . . . . 8 (𝑃 ∈ ℙ → ¬ 𝑃 = 0)
1312intnanrd 918 . . . . . . 7 (𝑃 ∈ ℙ → ¬ (𝑃 = 0 ∧ 𝑁 = 0))
1413adantr 274 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ¬ (𝑃 = 0 ∧ 𝑁 = 0))
15 gcdn0cl 11826 . . . . . . . 8 (((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑃 = 0 ∧ 𝑁 = 0)) → (𝑃 gcd 𝑁) ∈ ℕ)
1615ex 114 . . . . . . 7 ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → (𝑃 gcd 𝑁) ∈ ℕ))
171, 16sylan 281 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → (𝑃 gcd 𝑁) ∈ ℕ))
1814, 17mpd 13 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∈ ℕ)
193simpld 111 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∥ 𝑃)
20 isprm2 11974 . . . . . . . 8 (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ‘2) ∧ ∀𝑧 ∈ ℕ (𝑧𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
2120simprbi 273 . . . . . . 7 (𝑃 ∈ ℙ → ∀𝑧 ∈ ℕ (𝑧𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))
22 breq1 3968 . . . . . . . . 9 (𝑧 = (𝑃 gcd 𝑁) → (𝑧𝑃 ↔ (𝑃 gcd 𝑁) ∥ 𝑃))
23 eqeq1 2164 . . . . . . . . . 10 (𝑧 = (𝑃 gcd 𝑁) → (𝑧 = 1 ↔ (𝑃 gcd 𝑁) = 1))
24 eqeq1 2164 . . . . . . . . . 10 (𝑧 = (𝑃 gcd 𝑁) → (𝑧 = 𝑃 ↔ (𝑃 gcd 𝑁) = 𝑃))
2523, 24orbi12d 783 . . . . . . . . 9 (𝑧 = (𝑃 gcd 𝑁) → ((𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃)))
2622, 25imbi12d 233 . . . . . . . 8 (𝑧 = (𝑃 gcd 𝑁) → ((𝑧𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
2726rspcv 2812 . . . . . . 7 ((𝑃 gcd 𝑁) ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)) → ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
2821, 27syl5com 29 . . . . . 6 (𝑃 ∈ ℙ → ((𝑃 gcd 𝑁) ∈ ℕ → ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
2928adantr 274 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) ∈ ℕ → ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
3018, 19, 29mp2d 47 . . . 4 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))
31 biorf 734 . . . . 5 (¬ (𝑃 gcd 𝑁) = 𝑃 → ((𝑃 gcd 𝑁) = 1 ↔ ((𝑃 gcd 𝑁) = 𝑃 ∨ (𝑃 gcd 𝑁) = 1)))
32 orcom 718 . . . . 5 (((𝑃 gcd 𝑁) = 𝑃 ∨ (𝑃 gcd 𝑁) = 1) ↔ ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))
3331, 32bitrdi 195 . . . 4 (¬ (𝑃 gcd 𝑁) = 𝑃 → ((𝑃 gcd 𝑁) = 1 ↔ ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃)))
3430, 33syl5ibrcom 156 . . 3 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 gcd 𝑁) = 𝑃 → (𝑃 gcd 𝑁) = 1))
357, 34syld 45 . 2 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃𝑁 → (𝑃 gcd 𝑁) = 1))
36 iddvds 11681 . . . . . . 7 (𝑃 ∈ ℤ → 𝑃𝑃)
371, 36syl 14 . . . . . 6 (𝑃 ∈ ℙ → 𝑃𝑃)
3837adantr 274 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 𝑃𝑃)
39 dvdslegcd 11828 . . . . . . . . 9 (((𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑃 = 0 ∧ 𝑁 = 0)) → ((𝑃𝑃𝑃𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁)))
4039ex 114 . . . . . . . 8 ((𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → ((𝑃𝑃𝑃𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁))))
41403anidm12 1277 . . . . . . 7 ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → ((𝑃𝑃𝑃𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁))))
421, 41sylan 281 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → ((𝑃𝑃𝑃𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁))))
4314, 42mpd 13 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃𝑃𝑃𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁)))
4438, 43mpand 426 . . . 4 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃𝑁𝑃 ≤ (𝑃 gcd 𝑁)))
45 prmgt1 11988 . . . . . 6 (𝑃 ∈ ℙ → 1 < 𝑃)
4645adantr 274 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 1 < 𝑃)
471zred 9269 . . . . . . 7 (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
4847adantr 274 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 𝑃 ∈ ℝ)
4918nnred 8829 . . . . . 6 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∈ ℝ)
50 1re 7860 . . . . . . 7 1 ∈ ℝ
51 ltletr 7949 . . . . . . 7 ((1 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑃 gcd 𝑁) ∈ ℝ) → ((1 < 𝑃𝑃 ≤ (𝑃 gcd 𝑁)) → 1 < (𝑃 gcd 𝑁)))
5250, 51mp3an1 1306 . . . . . 6 ((𝑃 ∈ ℝ ∧ (𝑃 gcd 𝑁) ∈ ℝ) → ((1 < 𝑃𝑃 ≤ (𝑃 gcd 𝑁)) → 1 < (𝑃 gcd 𝑁)))
5348, 49, 52syl2anc 409 . . . . 5 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((1 < 𝑃𝑃 ≤ (𝑃 gcd 𝑁)) → 1 < (𝑃 gcd 𝑁)))
5446, 53mpand 426 . . . 4 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 ≤ (𝑃 gcd 𝑁) → 1 < (𝑃 gcd 𝑁)))
55 ltne 7945 . . . . . 6 ((1 ∈ ℝ ∧ 1 < (𝑃 gcd 𝑁)) → (𝑃 gcd 𝑁) ≠ 1)
5650, 55mpan 421 . . . . 5 (1 < (𝑃 gcd 𝑁) → (𝑃 gcd 𝑁) ≠ 1)
5756a1i 9 . . . 4 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (1 < (𝑃 gcd 𝑁) → (𝑃 gcd 𝑁) ≠ 1))
5844, 54, 573syld 57 . . 3 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃𝑁 → (𝑃 gcd 𝑁) ≠ 1))
5958necon2bd 2385 . 2 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) = 1 → ¬ 𝑃𝑁))
6035, 59impbid 128 1 ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃𝑁 ↔ (𝑃 gcd 𝑁) = 1))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 963   = wceq 1335   ∈ wcel 2128   ≠ wne 2327  ∀wral 2435   class class class wbr 3965  ‘cfv 5167  (class class class)co 5818  ℝcr 7714  0cc0 7715  1c1 7716   < clt 7895   ≤ cle 7896  ℕcn 8816  2c2 8867  ℤcz 9150  ℤ≥cuz 9422   ∥ cdvds 11665   gcd cgcd 11810  ℙcprime 11964 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545  ax-cnex 7806  ax-resscn 7807  ax-1cn 7808  ax-1re 7809  ax-icn 7810  ax-addcl 7811  ax-addrcl 7812  ax-mulcl 7813  ax-mulrcl 7814  ax-addcom 7815  ax-mulcom 7816  ax-addass 7817  ax-mulass 7818  ax-distr 7819  ax-i2m1 7820  ax-0lt1 7821  ax-1rid 7822  ax-0id 7823  ax-rnegex 7824  ax-precex 7825  ax-cnre 7826  ax-pre-ltirr 7827  ax-pre-ltwlin 7828  ax-pre-lttrn 7829  ax-pre-apti 7830  ax-pre-ltadd 7831  ax-pre-mulgt0 7832  ax-pre-mulext 7833  ax-arch 7834  ax-caucvg 7835 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4252  df-po 4255  df-iso 4256  df-iord 4325  df-on 4327  df-ilim 4328  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-f1 5172  df-fo 5173  df-f1o 5174  df-fv 5175  df-riota 5774  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1st 6082  df-2nd 6083  df-recs 6246  df-frec 6332  df-1o 6357  df-2o 6358  df-er 6473  df-en 6679  df-sup 6920  df-pnf 7897  df-mnf 7898  df-xr 7899  df-ltxr 7900  df-le 7901  df-sub 8031  df-neg 8032  df-reap 8433  df-ap 8440  df-div 8529  df-inn 8817  df-2 8875  df-3 8876  df-4 8877  df-n0 9074  df-z 9151  df-uz 9423  df-q 9511  df-rp 9543  df-fz 9895  df-fzo 10024  df-fl 10151  df-mod 10204  df-seqfrec 10327  df-exp 10401  df-cj 10724  df-re 10725  df-im 10726  df-rsqrt 10880  df-abs 10881  df-dvds 11666  df-gcd 11811  df-prm 11965 This theorem is referenced by:  prmrp  11999  euclemma  12000  cncongrprm  12011  isoddgcd1  12013  phiprmpw  12074  fermltl  12086  prmdiv  12087  prmdiveq  12088
 Copyright terms: Public domain W3C validator