Theorem 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	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd 𝐵 ) = 1 ) )

Proof

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