rpexp

Description: If two numbers A and B are relatively prime, then they are still relatively prime if raised to a power. (Contributed by Mario Carneiro, 24-Feb-2014)

		Ref	Expression
	Assertion	rpexp	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ) \to (A^{N} \gcd B = 1 \leftrightarrow A \gcd B = 1)$

Proof

Step	Hyp	Ref	Expression
1		0exp	$⊢ N \in ℕ \to 0^{N} = 0$
2	1	oveq1d	$⊢ N \in ℕ \to 0^{N} \gcd 0 = 0 \gcd 0$
3	2	eqeq1d	$⊢ N \in ℕ \to (0^{N} \gcd 0 = 1 \leftrightarrow 0 \gcd 0 = 1)$
4		oveq1	$⊢ A = 0 \to A^{N} = 0^{N}$
5		oveq12	$⊢ (A^{N} = 0^{N} \land B = 0) \to A^{N} \gcd B = 0^{N} \gcd 0$
6	4 5	sylan	$⊢ (A = 0 \land B = 0) \to A^{N} \gcd B = 0^{N} \gcd 0$
7	6	eqeq1d	$⊢ (A = 0 \land B = 0) \to (A^{N} \gcd B = 1 \leftrightarrow 0^{N} \gcd 0 = 1)$
8		oveq12	$⊢ (A = 0 \land B = 0) \to A \gcd B = 0 \gcd 0$
9	8	eqeq1d	$⊢ (A = 0 \land B = 0) \to (A \gcd B = 1 \leftrightarrow 0 \gcd 0 = 1)$
10	7 9	bibi12d	$⊢ (A = 0 \land B = 0) \to ((A^{N} \gcd B = 1 \leftrightarrow A \gcd B = 1) \leftrightarrow (0^{N} \gcd 0 = 1 \leftrightarrow 0 \gcd 0 = 1))$
11	3 10	syl5ibrcom	$⊢ N \in ℕ \to ((A = 0 \land B = 0) \to (A^{N} \gcd B = 1 \leftrightarrow A \gcd B = 1))$
12	11	3ad2ant3	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ) \to ((A = 0 \land B = 0) \to (A^{N} \gcd B = 1 \leftrightarrow A \gcd B = 1))$
13		exprmfct	$⊢ A^{N} \gcd B \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (A^{N} \gcd B)$
14		simpl1	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to A \in ℤ$
15		simpl3	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to N \in ℕ$
16	15	nnnn0d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to N \in ℕ_{0}$
17		zexpcl	$⊢ (A \in ℤ \land N \in ℕ_{0}) \to A^{N} \in ℤ$
18	14 16 17	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to A^{N} \in ℤ$
19	18	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to A^{N} \in ℤ$
20		simpl2	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to B \in ℤ$
21	20	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to B \in ℤ$
22		gcddvds	$⊢ (A^{N} \in ℤ \land B \in ℤ) \to ((A^{N} \gcd B) ∥ A^{N} \land (A^{N} \gcd B) ∥ B)$
23	19 21 22	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((A^{N} \gcd B) ∥ A^{N} \land (A^{N} \gcd B) ∥ B)$
24	23	simpld	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (A^{N} \gcd B) ∥ A^{N}$
25		prmz	$⊢ p \in ℙ \to p \in ℤ$
26	25	adantl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to p \in ℤ$
27		simpr	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to \neg (A = 0 \land B = 0)$
28	14	zcnd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to A \in ℂ$
29		expeq0	$⊢ (A \in ℂ \land N \in ℕ) \to (A^{N} = 0 \leftrightarrow A = 0)$
30	28 15 29	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A^{N} = 0 \leftrightarrow A = 0)$
31	30	anbi1d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to ((A^{N} = 0 \land B = 0) \leftrightarrow (A = 0 \land B = 0))$
32	27 31	mtbird	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to \neg (A^{N} = 0 \land B = 0)$
33		gcdn0cl	$⊢ ((A^{N} \in ℤ \land B \in ℤ) \land \neg (A^{N} = 0 \land B = 0)) \to A^{N} \gcd B \in ℕ$
34	18 20 32 33	syl21anc	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to A^{N} \gcd B \in ℕ$
35	34	nnzd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to A^{N} \gcd B \in ℤ$
36	35	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to A^{N} \gcd B \in ℤ$
37		dvdstr	$⊢ (p \in ℤ \land A^{N} \gcd B \in ℤ \land A^{N} \in ℤ) \to ((p ∥ (A^{N} \gcd B) \land (A^{N} \gcd B) ∥ A^{N}) \to p ∥ A^{N})$
38	26 36 19 37	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((p ∥ (A^{N} \gcd B) \land (A^{N} \gcd B) ∥ A^{N}) \to p ∥ A^{N})$
39	24 38	mpan2d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A^{N} \gcd B) \to p ∥ A^{N})$
40		simpr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to p \in ℙ$
41		simpll1	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to A \in ℤ$
42	15	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to N \in ℕ$
43		prmdvdsexp	$⊢ (p \in ℙ \land A \in ℤ \land N \in ℕ) \to (p ∥ A^{N} \leftrightarrow p ∥ A)$
44	40 41 42 43	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ A^{N} \leftrightarrow p ∥ A)$
45	39 44	sylibd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A^{N} \gcd B) \to p ∥ A)$
46	23	simprd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (A^{N} \gcd B) ∥ B$
47		dvdstr	$⊢ (p \in ℤ \land A^{N} \gcd B \in ℤ \land B \in ℤ) \to ((p ∥ (A^{N} \gcd B) \land (A^{N} \gcd B) ∥ B) \to p ∥ B)$
48	26 36 21 47	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((p ∥ (A^{N} \gcd B) \land (A^{N} \gcd B) ∥ B) \to p ∥ B)$
49	46 48	mpan2d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A^{N} \gcd B) \to p ∥ B)$
50	45 49	jcad	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A^{N} \gcd B) \to (p ∥ A \land p ∥ B))$
51		dvdsgcd	$⊢ (p \in ℤ \land A \in ℤ \land B \in ℤ) \to ((p ∥ A \land p ∥ B) \to p ∥ (A \gcd B))$
52	26 41 21 51	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((p ∥ A \land p ∥ B) \to p ∥ (A \gcd B))$
53		nprmdvds1	$⊢ p \in ℙ \to \neg p ∥ 1$
54		breq2	$⊢ A \gcd B = 1 \to (p ∥ (A \gcd B) \leftrightarrow p ∥ 1)$
55	54	notbid	$⊢ A \gcd B = 1 \to (\neg p ∥ (A \gcd B) \leftrightarrow \neg p ∥ 1)$
56	53 55	syl5ibrcom	$⊢ p \in ℙ \to (A \gcd B = 1 \to \neg p ∥ (A \gcd B))$
57	56	necon2ad	$⊢ p \in ℙ \to (p ∥ (A \gcd B) \to A \gcd B \neq 1)$
58	57	adantl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A \gcd B) \to A \gcd B \neq 1)$
59	50 52 58	3syld	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A^{N} \gcd B) \to A \gcd B \neq 1)$
60	59	rexlimdva	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (\exists p \in ℙ p ∥ (A^{N} \gcd B) \to A \gcd B \neq 1)$
61		gcdn0cl	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℕ$
62	61	3adantl3	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℕ$
63		eluz2b3	$⊢ A \gcd B \in ℤ_{\geq 2} \leftrightarrow (A \gcd B \in ℕ \land A \gcd B \neq 1)$
64	63	baib	$⊢ A \gcd B \in ℕ \to (A \gcd B \in ℤ_{\geq 2} \leftrightarrow A \gcd B \neq 1)$
65	62 64	syl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A \gcd B \in ℤ_{\geq 2} \leftrightarrow A \gcd B \neq 1)$
66	60 65	sylibrd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (\exists p \in ℙ p ∥ (A^{N} \gcd B) \to A \gcd B \in ℤ_{\geq 2})$
67	13 66	syl5	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A^{N} \gcd B \in ℤ_{\geq 2} \to A \gcd B \in ℤ_{\geq 2})$
68		exprmfct	$⊢ A \gcd B \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (A \gcd B)$
69	62	nnzd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℤ$
70	69	adantr	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to A \gcd B \in ℤ$
71		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
72	41 21 71	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
73	72	simpld	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (A \gcd B) ∥ A$
74		iddvdsexp	$⊢ (A \in ℤ \land N \in ℕ) \to A ∥ A^{N}$
75	41 42 74	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to A ∥ A^{N}$
76	70 41 19 73 75	dvdstrd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (A \gcd B) ∥ A^{N}$
77		dvdstr	$⊢ (p \in ℤ \land A \gcd B \in ℤ \land A^{N} \in ℤ) \to ((p ∥ (A \gcd B) \land (A \gcd B) ∥ A^{N}) \to p ∥ A^{N})$
78	26 70 19 77	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((p ∥ (A \gcd B) \land (A \gcd B) ∥ A^{N}) \to p ∥ A^{N})$
79	76 78	mpan2d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A \gcd B) \to p ∥ A^{N})$
80	72	simprd	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (A \gcd B) ∥ B$
81		dvdstr	$⊢ (p \in ℤ \land A \gcd B \in ℤ \land B \in ℤ) \to ((p ∥ (A \gcd B) \land (A \gcd B) ∥ B) \to p ∥ B)$
82	26 70 21 81	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((p ∥ (A \gcd B) \land (A \gcd B) ∥ B) \to p ∥ B)$
83	80 82	mpan2d	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A \gcd B) \to p ∥ B)$
84	79 83	jcad	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A \gcd B) \to (p ∥ A^{N} \land p ∥ B))$
85		dvdsgcd	$⊢ (p \in ℤ \land A^{N} \in ℤ \land B \in ℤ) \to ((p ∥ A^{N} \land p ∥ B) \to p ∥ (A^{N} \gcd B))$
86	26 19 21 85	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to ((p ∥ A^{N} \land p ∥ B) \to p ∥ (A^{N} \gcd B))$
87		breq2	$⊢ A^{N} \gcd B = 1 \to (p ∥ (A^{N} \gcd B) \leftrightarrow p ∥ 1)$
88	87	notbid	$⊢ A^{N} \gcd B = 1 \to (\neg p ∥ (A^{N} \gcd B) \leftrightarrow \neg p ∥ 1)$
89	53 88	syl5ibrcom	$⊢ p \in ℙ \to (A^{N} \gcd B = 1 \to \neg p ∥ (A^{N} \gcd B))$
90	89	necon2ad	$⊢ p \in ℙ \to (p ∥ (A^{N} \gcd B) \to A^{N} \gcd B \neq 1)$
91	90	adantl	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A^{N} \gcd B) \to A^{N} \gcd B \neq 1)$
92	84 86 91	3syld	$⊢ (((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \land p \in ℙ) \to (p ∥ (A \gcd B) \to A^{N} \gcd B \neq 1)$
93	92	rexlimdva	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (\exists p \in ℙ p ∥ (A \gcd B) \to A^{N} \gcd B \neq 1)$
94		eluz2b3	$⊢ A^{N} \gcd B \in ℤ_{\geq 2} \leftrightarrow (A^{N} \gcd B \in ℕ \land A^{N} \gcd B \neq 1)$
95	94	baib	$⊢ A^{N} \gcd B \in ℕ \to (A^{N} \gcd B \in ℤ_{\geq 2} \leftrightarrow A^{N} \gcd B \neq 1)$
96	34 95	syl	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A^{N} \gcd B \in ℤ_{\geq 2} \leftrightarrow A^{N} \gcd B \neq 1)$
97	93 96	sylibrd	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (\exists p \in ℙ p ∥ (A \gcd B) \to A^{N} \gcd B \in ℤ_{\geq 2})$
98	68 97	syl5	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A \gcd B \in ℤ_{\geq 2} \to A^{N} \gcd B \in ℤ_{\geq 2})$
99	67 98	impbid	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A^{N} \gcd B \in ℤ_{\geq 2} \leftrightarrow A \gcd B \in ℤ_{\geq 2})$
100	99 96 65	3bitr3d	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A^{N} \gcd B \neq 1 \leftrightarrow A \gcd B \neq 1)$
101	100	necon4bid	$⊢ ((A \in ℤ \land B \in ℤ \land N \in ℕ) \land \neg (A = 0 \land B = 0)) \to (A^{N} \gcd B = 1 \leftrightarrow A \gcd B = 1)$
102	101	ex	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ) \to (\neg (A = 0 \land B = 0) \to (A^{N} \gcd B = 1 \leftrightarrow A \gcd B = 1))$
103	12 102	pm2.61d	$⊢ (A \in ℤ \land B \in ℤ \land N \in ℕ) \to (A^{N} \gcd B = 1 \leftrightarrow A \gcd B = 1)$

Metamath Proof Explorer

Theorem rpexp

Proof