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	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg P ∥ N \leftrightarrow P \gcd N = 1)$

Proof

Step	Hyp	Ref	Expression
1		prmz	$⊢ P \in ℙ \to P \in ℤ$
2		gcddvds	$⊢ (P \in ℤ \land N \in ℤ) \to ((P \gcd N) ∥ P \land (P \gcd N) ∥ N)$
3	1 2	sylan	$⊢ (P \in ℙ \land N \in ℤ) \to ((P \gcd N) ∥ P \land (P \gcd N) ∥ N)$
4	3	simprd	$⊢ (P \in ℙ \land N \in ℤ) \to (P \gcd N) ∥ N$
5		breq1	$⊢ P \gcd N = P \to ((P \gcd N) ∥ N \leftrightarrow P ∥ N)$
6	4 5	syl5ibcom	$⊢ (P \in ℙ \land N \in ℤ) \to (P \gcd N = P \to P ∥ N)$
7	6	con3d	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg P ∥ N \to \neg P \gcd N = P)$
8		0nnn	$⊢ \neg 0 \in ℕ$
9		prmnn	$⊢ P \in ℙ \to P \in ℕ$
10		eleq1	$⊢ P = 0 \to (P \in ℕ \leftrightarrow 0 \in ℕ)$
11	9 10	syl5ibcom	$⊢ P \in ℙ \to (P = 0 \to 0 \in ℕ)$
12	8 11	mtoi	$⊢ P \in ℙ \to \neg P = 0$
13	12	intnanrd	$⊢ P \in ℙ \to \neg (P = 0 \land N = 0)$
14	13	adantr	$⊢ (P \in ℙ \land N \in ℤ) \to \neg (P = 0 \land N = 0)$
15		gcdn0cl	$⊢ ((P \in ℤ \land N \in ℤ) \land \neg (P = 0 \land N = 0)) \to P \gcd N \in ℕ$
16	15	ex	$⊢ (P \in ℤ \land N \in ℤ) \to (\neg (P = 0 \land N = 0) \to P \gcd N \in ℕ)$
17	1 16	sylan	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg (P = 0 \land N = 0) \to P \gcd N \in ℕ)$
18	14 17	mpd	$⊢ (P \in ℙ \land N \in ℤ) \to P \gcd N \in ℕ$
19	3	simpld	$⊢ (P \in ℙ \land N \in ℤ) \to (P \gcd N) ∥ P$
20		isprm2	$⊢ P \in ℙ \leftrightarrow (P \in ℤ_{\geq 2} \land \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)))$
21	20	simprbi	$⊢ P \in ℙ \to \forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P))$
22		breq1	$⊢ z = P \gcd N \to (z ∥ P \leftrightarrow (P \gcd N) ∥ P)$
23		eqeq1	$⊢ z = P \gcd N \to (z = 1 \leftrightarrow P \gcd N = 1)$
24		eqeq1	$⊢ z = P \gcd N \to (z = P \leftrightarrow P \gcd N = P)$
25	23 24	orbi12d	$⊢ z = P \gcd N \to ((z = 1 \lor z = P) \leftrightarrow (P \gcd N = 1 \lor P \gcd N = P))$
26	22 25	imbi12d	$⊢ z = P \gcd N \to ((z ∥ P \to (z = 1 \lor z = P)) \leftrightarrow ((P \gcd N) ∥ P \to (P \gcd N = 1 \lor P \gcd N = P)))$
27	26	rspcv	$⊢ P \gcd N \in ℕ \to (\forall z \in ℕ (z ∥ P \to (z = 1 \lor z = P)) \to ((P \gcd N) ∥ P \to (P \gcd N = 1 \lor P \gcd N = P)))$
28	21 27	syl5com	$⊢ P \in ℙ \to (P \gcd N \in ℕ \to ((P \gcd N) ∥ P \to (P \gcd N = 1 \lor P \gcd N = P)))$
29	28	adantr	$⊢ (P \in ℙ \land N \in ℤ) \to (P \gcd N \in ℕ \to ((P \gcd N) ∥ P \to (P \gcd N = 1 \lor P \gcd N = P)))$
30	18 19 29	mp2d	$⊢ (P \in ℙ \land N \in ℤ) \to (P \gcd N = 1 \lor P \gcd N = P)$
31		biorf	$⊢ \neg P \gcd N = P \to (P \gcd N = 1 \leftrightarrow (P \gcd N = P \lor P \gcd N = 1))$
32		orcom	$⊢ (P \gcd N = P \lor P \gcd N = 1) \leftrightarrow (P \gcd N = 1 \lor P \gcd N = P)$
33	31 32	bitrdi	$⊢ \neg P \gcd N = P \to (P \gcd N = 1 \leftrightarrow (P \gcd N = 1 \lor P \gcd N = P))$
34	30 33	syl5ibrcom	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg P \gcd N = P \to P \gcd N = 1)$
35	7 34	syld	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg P ∥ N \to P \gcd N = 1)$
36		iddvds	$⊢ P \in ℤ \to P ∥ P$
37	1 36	syl	$⊢ P \in ℙ \to P ∥ P$
38	37	adantr	$⊢ (P \in ℙ \land N \in ℤ) \to P ∥ P$
39		dvdslegcd	$⊢ ((P \in ℤ \land P \in ℤ \land N \in ℤ) \land \neg (P = 0 \land N = 0)) \to ((P ∥ P \land P ∥ N) \to P \leq P \gcd N)$
40	39	ex	$⊢ (P \in ℤ \land P \in ℤ \land N \in ℤ) \to (\neg (P = 0 \land N = 0) \to ((P ∥ P \land P ∥ N) \to P \leq P \gcd N))$
41	40	3anidm12	$⊢ (P \in ℤ \land N \in ℤ) \to (\neg (P = 0 \land N = 0) \to ((P ∥ P \land P ∥ N) \to P \leq P \gcd N))$
42	1 41	sylan	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg (P = 0 \land N = 0) \to ((P ∥ P \land P ∥ N) \to P \leq P \gcd N))$
43	14 42	mpd	$⊢ (P \in ℙ \land N \in ℤ) \to ((P ∥ P \land P ∥ N) \to P \leq P \gcd N)$
44	38 43	mpand	$⊢ (P \in ℙ \land N \in ℤ) \to (P ∥ N \to P \leq P \gcd N)$
45		prmgt1	$⊢ P \in ℙ \to 1 < P$
46	45	adantr	$⊢ (P \in ℙ \land N \in ℤ) \to 1 < P$
47		1re	$⊢ 1 \in ℝ$
48	1	zred	$⊢ P \in ℙ \to P \in ℝ$
49	18	nnred	$⊢ (P \in ℙ \land N \in ℤ) \to P \gcd N \in ℝ$
50		ltletr	$⊢ (1 \in ℝ \land P \in ℝ \land P \gcd N \in ℝ) \to ((1 < P \land P \leq P \gcd N) \to 1 < P \gcd N)$
51	47 48 49 50	mp3an2ani	$⊢ (P \in ℙ \land N \in ℤ) \to ((1 < P \land P \leq P \gcd N) \to 1 < P \gcd N)$
52	46 51	mpand	$⊢ (P \in ℙ \land N \in ℤ) \to (P \leq P \gcd N \to 1 < P \gcd N)$
53		ltne	$⊢ (1 \in ℝ \land 1 < P \gcd N) \to P \gcd N \neq 1$
54	47 53	mpan	$⊢ 1 < P \gcd N \to P \gcd N \neq 1$
55	54	a1i	$⊢ (P \in ℙ \land N \in ℤ) \to (1 < P \gcd N \to P \gcd N \neq 1)$
56	44 52 55	3syld	$⊢ (P \in ℙ \land N \in ℤ) \to (P ∥ N \to P \gcd N \neq 1)$
57	56	necon2bd	$⊢ (P \in ℙ \land N \in ℤ) \to (P \gcd N = 1 \to \neg P ∥ N)$
58	35 57	impbid	$⊢ (P \in ℙ \land N \in ℤ) \to (\neg P ∥ N \leftrightarrow P \gcd N = 1)$

Metamath Proof Explorer

Theorem coprm

Proof