This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )