Theorem prmrp 16752

Description: Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.)

Assertion

Ref	Expression
prmrp	⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))

Proof of Theorem prmrp

Step	Hyp	Ref	Expression
1		prmz 16715	. . 3 ⊢ (𝑄 ∈ ℙ → 𝑄 ∈ ℤ)
2		coprm 16751	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℤ) → (¬ 𝑃 ∥ 𝑄 ↔ (𝑃 gcd 𝑄) = 1))
3	1, 2	sylan2 593	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → (¬ 𝑃 ∥ 𝑄 ↔ (𝑃 gcd 𝑄) = 1))
4		prmuz2 16736	. . . 4 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
5		dvdsprm 16743	. . . 4 ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑄 ∈ ℙ) → (𝑃 ∥ 𝑄 ↔ 𝑃 = 𝑄))
6	4, 5	sylan 580	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → (𝑃 ∥ 𝑄 ↔ 𝑃 = 𝑄))
7	6	necon3bbid 2977	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → (¬ 𝑃 ∥ 𝑄 ↔ 𝑃 ≠ 𝑄))
8	3, 7	bitr3d 281	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1538   ∈ wcel 2107   ≠ wne 2939   class class class wbr 5149  ‘cfv 6566  (class class class)co 7435  1c1 11160  2c2 12325  ℤcz 12617  ℤ_≥cuz 12882   ∥ cdvds 16293   gcd cgcd 16534  ℙcprime 16711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5303  ax-nul 5313  ax-pow 5372  ax-pr 5439  ax-un 7758  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236  ax-pre-sup 11237

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3435  df-v 3481  df-sbc 3793  df-csb 3910  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-pss 3984  df-nul 4341  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4914  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5642  df-we 5644  df-xp 5696  df-rel 5697  df-cnv 5698  df-co 5699  df-dm 5700  df-rn 5701  df-res 5702  df-ima 5703  df-pred 6326  df-ord 6392  df-on 6393  df-lim 6394  df-suc 6395  df-iota 6519  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7392  df-ov 7438  df-oprab 7439  df-mpo 7440  df-om 7892  df-2nd 8020  df-frecs 8311  df-wrecs 8342  df-recs 8416  df-rdg 8455  df-1o 8511  df-2o 8512  df-er 8750  df-en 8991  df-dom 8992  df-sdom 8993  df-fin 8994  df-sup 9486  df-inf 9487  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11498  df-neg 11499  df-div 11925  df-nn 12271  df-2 12333  df-3 12334  df-n0 12531  df-z 12618  df-uz 12883  df-rp 13039  df-seq 14046  df-exp 14106  df-cj 15141  df-re 15142  df-im 15143  df-sqrt 15277  df-abs 15278  df-dvds 16294  df-gcd 16535  df-prm 16712

This theorem is referenced by:  3lcm2e6  16772  fvprmselgcd1  17085  ablfac1b  20111  2logb9irr  26861  logbprmirr  26862  lgseisenlem1  27442  lgseisenlem2  27443  lgsquadlem2  27448  lgsquadlem3  27449  lgsquad2lem2  27452  lgsquad2  27453  2lgsoddprm  27483  ostth3  27705  12gcd5e1  41997  60gcd7e1  41999  nzprmdif  44329  odz2prm2pw  47499  fmtnoprmfac1  47501  fmtnoprmfac2  47503