Theorem coprm 11668

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.

Step	Hyp	Ref	Expression
1		prmz 11638	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
2		gcddvds 11500	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) ∥ 𝑃 ∧ (𝑃 gcd 𝑁) ∥ 𝑁))
3	1, 2	sylan 279	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) ∥ 𝑃 ∧ (𝑃 gcd 𝑁) ∥ 𝑁))
4	3	simprd 113	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∥ 𝑁)
5		breq1 3898	. . . . 5 ⊢ ((𝑃 gcd 𝑁) = 𝑃 → ((𝑃 gcd 𝑁) ∥ 𝑁 ↔ 𝑃 ∥ 𝑁))
6	4, 5	syl5ibcom 154	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) = 𝑃 → 𝑃 ∥ 𝑁))
7	6	con3d 603	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃 ∥ 𝑁 → ¬ (𝑃 gcd 𝑁) = 𝑃))
8		0nnn 8657	. . . . . . . . 9 ⊢ ¬ 0 ∈ ℕ
9		prmnn 11637	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
10		eleq1 2177	. . . . . . . . . 10 ⊢ (𝑃 = 0 → (𝑃 ∈ ℕ ↔ 0 ∈ ℕ))
11	9, 10	syl5ibcom 154	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → (𝑃 = 0 → 0 ∈ ℕ))
12	8, 11	mtoi 636	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → ¬ 𝑃 = 0)
13	12	intnanrd 900	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → ¬ (𝑃 = 0 ∧ 𝑁 = 0))
14	13	adantr 272	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ¬ (𝑃 = 0 ∧ 𝑁 = 0))
15		gcdn0cl 11499	. . . . . . . 8 ⊢ (((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑃 = 0 ∧ 𝑁 = 0)) → (𝑃 gcd 𝑁) ∈ ℕ)
16	15	ex 114	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → (𝑃 gcd 𝑁) ∈ ℕ))
17	1, 16	sylan 279	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → (𝑃 gcd 𝑁) ∈ ℕ))
18	14, 17	mpd 13	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∈ ℕ)
19	3	simpld 111	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∥ 𝑃)
20		isprm2 11644	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
21	20	simprbi 271	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))
22		breq1 3898	. . . . . . . . 9 ⊢ (𝑧 = (𝑃 gcd 𝑁) → (𝑧 ∥ 𝑃 ↔ (𝑃 gcd 𝑁) ∥ 𝑃))
23		eqeq1 2121	. . . . . . . . . 10 ⊢ (𝑧 = (𝑃 gcd 𝑁) → (𝑧 = 1 ↔ (𝑃 gcd 𝑁) = 1))
24		eqeq1 2121	. . . . . . . . . 10 ⊢ (𝑧 = (𝑃 gcd 𝑁) → (𝑧 = 𝑃 ↔ (𝑃 gcd 𝑁) = 𝑃))
25	23, 24	orbi12d 765	. . . . . . . . 9 ⊢ (𝑧 = (𝑃 gcd 𝑁) → ((𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃)))
26	22, 25	imbi12d 233	. . . . . . . 8 ⊢ (𝑧 = (𝑃 gcd 𝑁) → ((𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
27	26	rspcv 2756	. . . . . . 7 ⊢ ((𝑃 gcd 𝑁) ∈ ℕ → (∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)) → ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
28	21, 27	syl5com 29	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ((𝑃 gcd 𝑁) ∈ ℕ → ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
29	28	adantr 272	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) ∈ ℕ → ((𝑃 gcd 𝑁) ∥ 𝑃 → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))))
30	18, 19, 29	mp2d 47	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))
31		biorf 716	. . . . 5 ⊢ (¬ (𝑃 gcd 𝑁) = 𝑃 → ((𝑃 gcd 𝑁) = 1 ↔ ((𝑃 gcd 𝑁) = 𝑃 ∨ (𝑃 gcd 𝑁) = 1)))
32		orcom 700	. . . . 5 ⊢ (((𝑃 gcd 𝑁) = 𝑃 ∨ (𝑃 gcd 𝑁) = 1) ↔ ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃))
33	31, 32	syl6bb 195	. . . 4 ⊢ (¬ (𝑃 gcd 𝑁) = 𝑃 → ((𝑃 gcd 𝑁) = 1 ↔ ((𝑃 gcd 𝑁) = 1 ∨ (𝑃 gcd 𝑁) = 𝑃)))
34	30, 33	syl5ibrcom 156	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 gcd 𝑁) = 𝑃 → (𝑃 gcd 𝑁) = 1))
35	7, 34	syld 45	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃 ∥ 𝑁 → (𝑃 gcd 𝑁) = 1))
36		iddvds 11354	. . . . . . 7 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 𝑃)
37	1, 36	syl 14	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ 𝑃)
38	37	adantr 272	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 𝑃 ∥ 𝑃)
39		dvdslegcd 11501	. . . . . . . . 9 ⊢ (((𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑃 = 0 ∧ 𝑁 = 0)) → ((𝑃 ∥ 𝑃 ∧ 𝑃 ∥ 𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁)))
40	39	ex 114	. . . . . . . 8 ⊢ ((𝑃 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → ((𝑃 ∥ 𝑃 ∧ 𝑃 ∥ 𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁))))
41	40	3anidm12 1256	. . . . . . 7 ⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → ((𝑃 ∥ 𝑃 ∧ 𝑃 ∥ 𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁))))
42	1, 41	sylan 279	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ (𝑃 = 0 ∧ 𝑁 = 0) → ((𝑃 ∥ 𝑃 ∧ 𝑃 ∥ 𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁))))
43	14, 42	mpd 13	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ 𝑃 ∧ 𝑃 ∥ 𝑁) → 𝑃 ≤ (𝑃 gcd 𝑁)))
44	38, 43	mpand 423	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 → 𝑃 ≤ (𝑃 gcd 𝑁)))
45		prmgt1 11658	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
46	45	adantr 272	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 1 < 𝑃)
47	1	zred 9077	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
48	47	adantr 272	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 𝑃 ∈ ℝ)
49	18	nnred 8643	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 gcd 𝑁) ∈ ℝ)
50		1re 7689	. . . . . . 7 ⊢ 1 ∈ ℝ
51		ltletr 7776	. . . . . . 7 ⊢ ((1 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ (𝑃 gcd 𝑁) ∈ ℝ) → ((1 < 𝑃 ∧ 𝑃 ≤ (𝑃 gcd 𝑁)) → 1 < (𝑃 gcd 𝑁)))
52	50, 51	mp3an1 1285	. . . . . 6 ⊢ ((𝑃 ∈ ℝ ∧ (𝑃 gcd 𝑁) ∈ ℝ) → ((1 < 𝑃 ∧ 𝑃 ≤ (𝑃 gcd 𝑁)) → 1 < (𝑃 gcd 𝑁)))
53	48, 49, 52	syl2anc 406	. . . . 5 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((1 < 𝑃 ∧ 𝑃 ≤ (𝑃 gcd 𝑁)) → 1 < (𝑃 gcd 𝑁)))
54	46, 53	mpand 423	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 ≤ (𝑃 gcd 𝑁) → 1 < (𝑃 gcd 𝑁)))
55		ltne 7772	. . . . . 6 ⊢ ((1 ∈ ℝ ∧ 1 < (𝑃 gcd 𝑁)) → (𝑃 gcd 𝑁) ≠ 1)
56	50, 55	mpan 418	. . . . 5 ⊢ (1 < (𝑃 gcd 𝑁) → (𝑃 gcd 𝑁) ≠ 1)
57	56	a1i 9	. . . 4 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (1 < (𝑃 gcd 𝑁) → (𝑃 gcd 𝑁) ≠ 1))
58	44, 54, 57	3syld 57	. . 3 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ 𝑁 → (𝑃 gcd 𝑁) ≠ 1))
59	58	necon2bd 2340	. 2 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → ((𝑃 gcd 𝑁) = 1 → ¬ 𝑃 ∥ 𝑁))
60	35, 59	impbid 128	1 ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃 ∥ 𝑁 ↔ (𝑃 gcd 𝑁) = 1))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 680   ∧ w3a 945   = wceq 1314   ∈ wcel 1463   ≠ wne 2282  ∀wral 2390   class class class wbr 3895  ‘cfv 5081  (class class class)co 5728  ℝcr 7546  0cc0 7547  1c1 7548   < clt 7724   ≤ cle 7725  ℕcn 8630  2c2 8681  ℤcz 8958  ℤ_≥cuz 9228   ∥ cdvds 11341   gcd cgcd 11483  ℙcprime 11634

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4003  ax-sep 4006  ax-nul 4014  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-setind 4412  ax-iinf 4462  ax-cnex 7636  ax-resscn 7637  ax-1cn 7638  ax-1re 7639  ax-icn 7640  ax-addcl 7641  ax-addrcl 7642  ax-mulcl 7643  ax-mulrcl 7644  ax-addcom 7645  ax-mulcom 7646  ax-addass 7647  ax-mulass 7648  ax-distr 7649  ax-i2m1 7650  ax-0lt1 7651  ax-1rid 7652  ax-0id 7653  ax-rnegex 7654  ax-precex 7655  ax-cnre 7656  ax-pre-ltirr 7657  ax-pre-ltwlin 7658  ax-pre-lttrn 7659  ax-pre-apti 7660  ax-pre-ltadd 7661  ax-pre-mulgt0 7662  ax-pre-mulext 7663  ax-arch 7664  ax-caucvg 7665

This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-nel 2378  df-ral 2395  df-rex 2396  df-reu 2397  df-rmo 2398  df-rab 2399  df-v 2659  df-sbc 2879  df-csb 2972  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-if 3441  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-int 3738  df-iun 3781  df-br 3896  df-opab 3950  df-mpt 3951  df-tr 3987  df-id 4175  df-po 4178  df-iso 4179  df-iord 4248  df-on 4250  df-ilim 4251  df-suc 4253  df-iom 4465  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-rn 4510  df-res 4511  df-ima 4512  df-iota 5046  df-fun 5083  df-fn 5084  df-f 5085  df-f1 5086  df-fo 5087  df-f1o 5088  df-fv 5089  df-riota 5684  df-ov 5731  df-oprab 5732  df-mpo 5733  df-1st 5992  df-2nd 5993  df-recs 6156  df-frec 6242  df-1o 6267  df-2o 6268  df-er 6383  df-en 6589  df-sup 6823  df-pnf 7726  df-mnf 7727  df-xr 7728  df-ltxr 7729  df-le 7730  df-sub 7858  df-neg 7859  df-reap 8255  df-ap 8262  df-div 8346  df-inn 8631  df-2 8689  df-3 8690  df-4 8691  df-n0 8882  df-z 8959  df-uz 9229  df-q 9314  df-rp 9344  df-fz 9684  df-fzo 9813  df-fl 9936  df-mod 9989  df-seqfrec 10112  df-exp 10186  df-cj 10507  df-re 10508  df-im 10509  df-rsqrt 10662  df-abs 10663  df-dvds 11342  df-gcd 11484  df-prm 11635

This theorem is referenced by:  prmrp  11669  euclemma  11670  cncongrprm  11681  isoddgcd1  11683  phiprmpw  11743