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 
|- ( ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 elnn0 
 |-  ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
3 elnn0 
 |-  ( B e. NN0 <-> ( B e. NN \/ B = 0 ) )
4 rppwr 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )
5 4 3expia 
 |-  ( ( A e. NN /\ B e. NN ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
6 simp1l 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> A = 0 )
7 6 oveq1d 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A ^ N ) = ( 0 ^ N ) )
8 0exp 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )
9 8 3ad2ant2 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( 0 ^ N ) = 0 )
10 7 9 eqtrd 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A ^ N ) = 0 )
11 6 oveq1d 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A gcd B ) = ( 0 gcd B ) )
12 simp3 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A gcd B ) = 1 )
13 simp1r 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> B e. NN )
14 nnz 
 |-  ( B e. NN -> B e. ZZ )
15 gcd0id 
 |-  ( B e. ZZ -> ( 0 gcd B ) = ( abs ` B ) )
16 14 15 syl 
 |-  ( B e. NN -> ( 0 gcd B ) = ( abs ` B ) )
17 nnre 
 |-  ( B e. NN -> B e. RR )
18 0red 
 |-  ( B e. NN -> 0 e. RR )
19 nngt0 
 |-  ( B e. NN -> 0 < B )
20 18 17 19 ltled 
 |-  ( B e. NN -> 0 <_ B )
21 17 20 absidd 
 |-  ( B e. NN -> ( abs ` B ) = B )
22 16 21 eqtrd 
 |-  ( B e. NN -> ( 0 gcd B ) = B )
23 13 22 syl 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( 0 gcd B ) = B )
24 11 12 23 3eqtr3rd 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> B = 1 )
25 24 oveq1d 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( B ^ N ) = ( 1 ^ N ) )
26 nnz 
 |-  ( N e. NN -> N e. ZZ )
27 26 3ad2ant2 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> N e. ZZ )
28 1exp 
 |-  ( N e. ZZ -> ( 1 ^ N ) = 1 )
29 27 28 syl 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( 1 ^ N ) = 1 )
30 25 29 eqtrd 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( B ^ N ) = 1 )
31 10 30 oveq12d 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( 0 gcd 1 ) )
32 1z 
 |-  1 e. ZZ
33 gcd0id 
 |-  ( 1 e. ZZ -> ( 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 
 |-  ( ( ( A = 0 /\ B e. NN ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 )
38 37 3exp 
 |-  ( ( A = 0 /\ B e. NN ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
39 simp1r 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> B = 0 )
40 39 oveq2d 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A gcd B ) = ( A gcd 0 ) )
41 simp3 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A gcd B ) = 1 )
42 simp1l 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> A e. NN )
43 42 nnnn0d 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> A e. NN0 )
44 nn0gcdid0 
 |-  ( A e. NN0 -> ( A gcd 0 ) = A )
45 43 44 syl 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A gcd 0 ) = A )
46 40 41 45 3eqtr3rd 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> A = 1 )
47 46 oveq1d 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A ^ N ) = ( 1 ^ N ) )
48 26 3ad2ant2 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> N e. ZZ )
49 48 28 syl 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( 1 ^ N ) = 1 )
50 47 49 eqtrd 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( A ^ N ) = 1 )
51 39 oveq1d 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( B ^ N ) = ( 0 ^ N ) )
52 8 3ad2ant2 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( 0 ^ N ) = 0 )
53 51 52 eqtrd 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( B ^ N ) = 0 )
54 50 53 oveq12d 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( 1 gcd 0 ) )
55 1nn0 
 |-  1 e. NN0
56 nn0gcdid0 
 |-  ( 1 e. NN0 -> ( 1 gcd 0 ) = 1 )
57 55 56 mp1i 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( 1 gcd 0 ) = 1 )
58 54 57 eqtrd 
 |-  ( ( ( A e. NN /\ B = 0 ) /\ N e. NN /\ ( A gcd B ) = 1 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 )
59 58 3exp 
 |-  ( ( A e. NN /\ B = 0 ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
60 oveq12 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A gcd B ) = ( 0 gcd 0 ) )
61 gcd0val 
 |-  ( 0 gcd 0 ) = 0
62 0ne1 
 |-  0 =/= 1
63 61 62 eqnetri 
 |-  ( 0 gcd 0 ) =/= 1
64 63 a1i 
 |-  ( ( A = 0 /\ B = 0 ) -> ( 0 gcd 0 ) =/= 1 )
65 60 64 eqnetrd 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A gcd B ) =/= 1 )
66 65 neneqd 
 |-  ( ( A = 0 /\ B = 0 ) -> -. ( A gcd B ) = 1 )
67 66 pm2.21d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )
68 67 a1d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
69 5 38 59 68 ccase 
 |-  ( ( ( A e. NN \/ A = 0 ) /\ ( B e. NN \/ B = 0 ) ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
70 2 3 69 syl2anb 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( N e. NN -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
71 oveq2 
 |-  ( N = 0 -> ( A ^ N ) = ( A ^ 0 ) )
72 71 3ad2ant3 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( A ^ N ) = ( A ^ 0 ) )
73 nn0cn 
 |-  ( A e. NN0 -> A e. CC )
74 73 3ad2ant1 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> A e. CC )
75 74 exp0d 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( A ^ 0 ) = 1 )
76 72 75 eqtrd 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( A ^ N ) = 1 )
77 oveq2 
 |-  ( N = 0 -> ( B ^ N ) = ( B ^ 0 ) )
78 77 3ad2ant3 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( B ^ N ) = ( B ^ 0 ) )
79 nn0cn 
 |-  ( B e. NN0 -> B e. CC )
80 79 3ad2ant2 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> B e. CC )
81 80 exp0d 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( B ^ 0 ) = 1 )
82 78 81 eqtrd 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( B ^ N ) = 1 )
83 76 82 oveq12d 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( 1 gcd 1 ) )
84 1gcd 
 |-  ( 1 e. ZZ -> ( 1 gcd 1 ) = 1 )
85 32 84 mp1i 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( 1 gcd 1 ) = 1 )
86 83 85 eqtrd 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N = 0 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 )
87 86 3expia 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( N = 0 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )
88 87 a1dd 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( N = 0 -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
89 70 88 jaod 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( N e. NN \/ N = 0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) ) )
90 89 3impia 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ ( N e. NN \/ N = 0 ) ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )
91 1 90 syl3an3b 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) -> ( ( A gcd B ) = 1 -> ( ( A ^ N ) gcd ( B ^ N ) ) = 1 ) )