rplpwr

Description: If A and B are relatively prime, then so are A ^ N and B . (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ k = 1 \to A^{k} = A^{1}$
2	1	oveq1d	$⊢ k = 1 \to A^{k} \gcd B = A^{1} \gcd B$
3	2	eqeq1d	$⊢ k = 1 \to (A^{k} \gcd B = 1 \leftrightarrow A^{1} \gcd B = 1)$
4	3	imbi2d	$⊢ k = 1 \to ((((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{k} \gcd B = 1) \leftrightarrow (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{1} \gcd B = 1))$
5		oveq2	$⊢ k = n \to A^{k} = A^{n}$
6	5	oveq1d	$⊢ k = n \to A^{k} \gcd B = A^{n} \gcd B$
7	6	eqeq1d	$⊢ k = n \to (A^{k} \gcd B = 1 \leftrightarrow A^{n} \gcd B = 1)$
8	7	imbi2d	$⊢ k = n \to ((((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{k} \gcd B = 1) \leftrightarrow (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{n} \gcd B = 1))$
9		oveq2	$⊢ k = n + 1 \to A^{k} = A^{n + 1}$
10	9	oveq1d	$⊢ k = n + 1 \to A^{k} \gcd B = A^{n + 1} \gcd B$
11	10	eqeq1d	$⊢ k = n + 1 \to (A^{k} \gcd B = 1 \leftrightarrow A^{n + 1} \gcd B = 1)$
12	11	imbi2d	$⊢ k = n + 1 \to ((((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{k} \gcd B = 1) \leftrightarrow (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{n + 1} \gcd B = 1))$
13		oveq2	$⊢ k = N \to A^{k} = A^{N}$
14	13	oveq1d	$⊢ k = N \to A^{k} \gcd B = A^{N} \gcd B$
15	14	eqeq1d	$⊢ k = N \to (A^{k} \gcd B = 1 \leftrightarrow A^{N} \gcd B = 1)$
16	15	imbi2d	$⊢ k = N \to ((((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{k} \gcd B = 1) \leftrightarrow (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{N} \gcd B = 1))$
17		nncn	$⊢ A \in ℕ \to A \in ℂ$
18	17	exp1d	$⊢ A \in ℕ \to A^{1} = A$
19	18	oveq1d	$⊢ A \in ℕ \to A^{1} \gcd B = A \gcd B$
20	19	adantr	$⊢ (A \in ℕ \land B \in ℕ) \to A^{1} \gcd B = A \gcd B$
21	20	eqeq1d	$⊢ (A \in ℕ \land B \in ℕ) \to (A^{1} \gcd B = 1 \leftrightarrow A \gcd B = 1)$
22	21	biimpar	$⊢ ((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{1} \gcd B = 1$
23		df-3an	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \leftrightarrow ((A \in ℕ \land B \in ℕ) \land n \in ℕ)$
24		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A \in ℕ$
25	24	nncnd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A \in ℂ$
26		simpl3	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to n \in ℕ$
27	26	nnnn0d	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to n \in ℕ_{0}$
28	25 27	expp1d	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n + 1} = A^{n} A$
29		simp1	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to A \in ℕ$
30		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
31	30	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to n \in ℕ_{0}$
32	29 31	nnexpcld	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to A^{n} \in ℕ$
33	32	nnzd	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to A^{n} \in ℤ$
34	33	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n} \in ℤ$
35	34	zcnd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n} \in ℂ$
36	35 25	mulcomd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n} A = A A^{n}$
37	28 36	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n + 1} = A A^{n}$
38	37	oveq2d	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to B \gcd A^{n + 1} = B \gcd A A^{n}$
39		simpl2	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to B \in ℕ$
40	32	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n} \in ℕ$
41		nnz	$⊢ A \in ℕ \to A \in ℤ$
42	41	3ad2ant1	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to A \in ℤ$
43		nnz	$⊢ B \in ℕ \to B \in ℤ$
44	43	3ad2ant2	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to B \in ℤ$
45	42 44	gcdcomd	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to A \gcd B = B \gcd A$
46	45	eqeq1d	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to (A \gcd B = 1 \leftrightarrow B \gcd A = 1)$
47	46	biimpa	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to B \gcd A = 1$
48		rpmulgcd	$⊢ ((B \in ℕ \land A \in ℕ \land A^{n} \in ℕ) \land B \gcd A = 1) \to B \gcd A A^{n} = B \gcd A^{n}$
49	39 24 40 47 48	syl31anc	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to B \gcd A A^{n} = B \gcd A^{n}$
50	38 49	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to B \gcd A^{n + 1} = B \gcd A^{n}$
51		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
52	51	3ad2ant3	$⊢ (A \in ℕ \land B \in ℕ \land n \in ℕ) \to n + 1 \in ℕ$
53	52	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to n + 1 \in ℕ$
54	53	nnnn0d	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to n + 1 \in ℕ_{0}$
55	24 54	nnexpcld	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n + 1} \in ℕ$
56	55	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n + 1} \in ℤ$
57	44	adantr	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to B \in ℤ$
58	56 57	gcdcomd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n + 1} \gcd B = B \gcd A^{n + 1}$
59	34 57	gcdcomd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n} \gcd B = B \gcd A^{n}$
60	50 58 59	3eqtr4d	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to A^{n + 1} \gcd B = A^{n} \gcd B$
61	60	eqeq1d	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to (A^{n + 1} \gcd B = 1 \leftrightarrow A^{n} \gcd B = 1)$
62	61	biimprd	$⊢ ((A \in ℕ \land B \in ℕ \land n \in ℕ) \land A \gcd B = 1) \to (A^{n} \gcd B = 1 \to A^{n + 1} \gcd B = 1)$
63	23 62	sylanbr	$⊢ (((A \in ℕ \land B \in ℕ) \land n \in ℕ) \land A \gcd B = 1) \to (A^{n} \gcd B = 1 \to A^{n + 1} \gcd B = 1)$
64	63	an32s	$⊢ (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \land n \in ℕ) \to (A^{n} \gcd B = 1 \to A^{n + 1} \gcd B = 1)$
65	64	expcom	$⊢ n \in ℕ \to (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to (A^{n} \gcd B = 1 \to A^{n + 1} \gcd B = 1))$
66	65	a2d	$⊢ n \in ℕ \to ((((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{n} \gcd B = 1) \to (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{n + 1} \gcd B = 1))$
67	4 8 12 16 22 66	nnind	$⊢ N \in ℕ \to (((A \in ℕ \land B \in ℕ) \land A \gcd B = 1) \to A^{N} \gcd B = 1)$
68	67	expd	$⊢ N \in ℕ \to ((A \in ℕ \land B \in ℕ) \to (A \gcd B = 1 \to A^{N} \gcd B = 1))$
69	68	com12	$⊢ (A \in ℕ \land B \in ℕ) \to (N \in ℕ \to (A \gcd B = 1 \to A^{N} \gcd B = 1))$
70	69	3impia	$⊢ (A \in ℕ \land B \in ℕ \land N \in ℕ) \to (A \gcd B = 1 \to A^{N} \gcd B = 1)$

Metamath Proof Explorer

Theorem rplpwr

Proof