Metamath Proof Explorer

Theorem nn0rppwr

Description: If A and B are relatively prime, then so are A ^ N and B ^ N . rppwr extended to nonnegative integers. Less general than rpexp12i . (Contributed by Steven Nguyen, 4-Apr-2023)

Ref Expression
Assertion nn0rppwr ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
3 elnn0 ⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
4 rppwr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )
5 4 3expia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
6 simp1l ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 = 0 )
7 6 oveq1d ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
8 0exp ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
9 8 3ad2ant2 ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 0 ↑ 𝑁 ) = 0 )
10 7 9 eqtrd ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 ↑ 𝑁 ) = 0 )
11 6 oveq1d ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 𝐵 ) )
12 simp3 ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 gcd 𝐵 ) = 1 )
13 simp1r ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐵 ∈ ℕ )
14 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
15 gcd0id ⊢ ( 𝐵 ∈ ℤ → ( 0 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
16 14 15 syl ⊢ ( 𝐵 ∈ ℕ → ( 0 gcd 𝐵 ) = ( abs ‘ 𝐵 ) )
17 nnre ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
18 0red ⊢ ( 𝐵 ∈ ℕ → 0 ∈ ℝ )
19 nngt0 ⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
20 18 17 19 ltled ⊢ ( 𝐵 ∈ ℕ → 0 ≤ 𝐵 )
21 17 20 absidd ⊢ ( 𝐵 ∈ ℕ → ( abs ‘ 𝐵 ) = 𝐵 )
22 16 21 eqtrd ⊢ ( 𝐵 ∈ ℕ → ( 0 gcd 𝐵 ) = 𝐵 )
23 13 22 syl ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 0 gcd 𝐵 ) = 𝐵 )
24 11 12 23 3eqtr3rd ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐵 = 1 )
25 24 oveq1d ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐵 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
26 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
27 26 3ad2ant2 ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝑁 ∈ ℤ )
28 1exp ⊢ ( 𝑁 ∈ ℤ → ( 1 ↑ 𝑁 ) = 1 )
29 27 28 syl ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 1 ↑ 𝑁 ) = 1 )
30 25 29 eqtrd ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐵 ↑ 𝑁 ) = 1 )
31 10 30 oveq12d ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 0 gcd 1 ) )
32 1z ⊢ 1 ∈ ℤ
33 gcd0id ⊢ ( 1 ∈ ℤ → ( 0 gcd 1 ) = ( abs ‘ 1 ) )
34 32 33 ax-mp ⊢ ( 0 gcd 1 ) = ( abs ‘ 1 )
35 abs1 ⊢ ( abs ‘ 1 ) = 1
36 34 35 eqtri ⊢ ( 0 gcd 1 ) = 1
37 31 36 eqtrdi ⊢ ( ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 )
38 37 3exp ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
39 simp1r ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐵 = 0 )
40 39 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 gcd 𝐵 ) = ( 𝐴 gcd 0 ) )
41 simp3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 gcd 𝐵 ) = 1 )
42 simp1l ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∈ ℕ )
43 42 nnnn0d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∈ ℕ0 )
44 nn0gcdid0 ⊢ ( 𝐴 ∈ ℕ0 → ( 𝐴 gcd 0 ) = 𝐴 )
45 43 44 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 gcd 0 ) = 𝐴 )
46 40 41 45 3eqtr3rd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 = 1 )
47 46 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 ↑ 𝑁 ) = ( 1 ↑ 𝑁 ) )
48 26 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝑁 ∈ ℤ )
49 48 28 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 1 ↑ 𝑁 ) = 1 )
50 47 49 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 ↑ 𝑁 ) = 1 )
51 39 oveq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐵 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
52 8 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 0 ↑ 𝑁 ) = 0 )
53 51 52 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐵 ↑ 𝑁 ) = 0 )
54 50 53 oveq12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 1 gcd 0 ) )
55 1nn0 ⊢ 1 ∈ ℕ0
56 nn0gcdid0 ⊢ ( 1 ∈ ℕ0 → ( 1 gcd 0 ) = 1 )
57 55 56 mp1i ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 1 gcd 0 ) = 1 )
58 54 57 eqtrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 )
59 58 3exp ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
60 oveq12 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 gcd 𝐵 ) = ( 0 gcd 0 ) )
61 gcd0val ⊢ ( 0 gcd 0 ) = 0
62 0ne1 ⊢ 0 ≠ 1
63 61 62 eqnetri ⊢ ( 0 gcd 0 ) ≠ 1
64 63 a1i ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 0 gcd 0 ) ≠ 1 )
65 60 64 eqnetrd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 gcd 𝐵 ) ≠ 1 )
66 65 neneqd ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ¬ ( 𝐴 gcd 𝐵 ) = 1 )
67 66 pm2.21d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )
68 67 a1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
69 5 38 59 68 ccase ⊢ ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
70 2 3 69 syl2anb ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
71 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
72 71 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
73 nn0cn ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ )
74 73 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → 𝐴 ∈ ℂ )
75 74 exp0d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 0 ) = 1 )
76 72 75 eqtrd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = 1 )
77 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐵 ↑ 𝑁 ) = ( 𝐵 ↑ 0 ) )
78 77 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 𝑁 ) = ( 𝐵 ↑ 0 ) )
79 nn0cn ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℂ )
80 79 3ad2ant2 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → 𝐵 ∈ ℂ )
81 80 exp0d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 0 ) = 1 )
82 78 81 eqtrd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( 𝐵 ↑ 𝑁 ) = 1 )
83 76 82 oveq12d ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = ( 1 gcd 1 ) )
84 1gcd ⊢ ( 1 ∈ ℤ → ( 1 gcd 1 ) = 1 )
85 32 84 mp1i ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( 1 gcd 1 ) = 1 )
86 83 85 eqtrd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 )
87 86 3expia ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝑁 = 0 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )
88 87 a1dd ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝑁 = 0 → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
89 70 88 jaod ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) ) )
90 89 3impia ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )
91 1 90 syl3an3b ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ( ( 𝐴 ↑ 𝑁 ) gcd ( 𝐵 ↑ 𝑁 ) ) = 1 ) )