Metamath Proof Explorer

Theorem nn0expgcd

Description: Exponentiation distributes over GCD. nn0gcdsq extended to nonnegative exponents. expgcd extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023)

Ref Expression
Assertion nn0expgcd 
|- ( ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
2 elnn0 
 |-  ( B e. NN0 <-> ( B e. NN \/ B = 0 ) )
3 expgcd 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
4 3 3expia 
 |-  ( ( A e. NN /\ B e. NN ) -> ( N e. NN0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
5 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
6 0exp 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )
7 6 3ad2ant3 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( 0 ^ N ) = 0 )
8 7 oveq1d 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( ( 0 ^ N ) gcd ( B ^ N ) ) = ( 0 gcd ( B ^ N ) ) )
9 simp2 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> B e. NN )
10 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
11 10 3ad2ant3 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> N e. NN0 )
12 9 11 nnexpcld 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( B ^ N ) e. NN )
13 12 nnzd 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( B ^ N ) e. ZZ )
14 gcd0id 
 |-  ( ( B ^ N ) e. ZZ -> ( 0 gcd ( B ^ N ) ) = ( abs ` ( B ^ N ) ) )
15 13 14 syl 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( 0 gcd ( B ^ N ) ) = ( abs ` ( B ^ N ) ) )
16 12 nnred 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( B ^ N ) e. RR )
17 0red 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> 0 e. RR )
18 12 nngt0d 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> 0 < ( B ^ N ) )
19 17 16 18 ltled 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> 0 <_ ( B ^ N ) )
20 16 19 absidd 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( abs ` ( B ^ N ) ) = ( B ^ N ) )
21 8 15 20 3eqtrrd 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( B ^ N ) = ( ( 0 ^ N ) gcd ( B ^ N ) ) )
22 oveq1 
 |-  ( A = 0 -> ( A gcd B ) = ( 0 gcd B ) )
23 22 3ad2ant1 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( A gcd B ) = ( 0 gcd B ) )
24 nnz 
 |-  ( B e. NN -> B e. ZZ )
25 24 3ad2ant2 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> B e. ZZ )
26 gcd0id 
 |-  ( B e. ZZ -> ( 0 gcd B ) = ( abs ` B ) )
27 25 26 syl 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( 0 gcd B ) = ( abs ` B ) )
28 nnre 
 |-  ( B e. NN -> B e. RR )
29 0red 
 |-  ( B e. NN -> 0 e. RR )
30 nngt0 
 |-  ( B e. NN -> 0 < B )
31 29 28 30 ltled 
 |-  ( B e. NN -> 0 <_ B )
32 28 31 absidd 
 |-  ( B e. NN -> ( abs ` B ) = B )
33 32 3ad2ant2 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( abs ` B ) = B )
34 23 27 33 3eqtrd 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( A gcd B ) = B )
35 34 oveq1d 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) ^ N ) = ( B ^ N ) )
36 oveq1 
 |-  ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
37 36 3ad2ant1 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( A ^ N ) = ( 0 ^ N ) )
38 37 oveq1d 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( ( 0 ^ N ) gcd ( B ^ N ) ) )
39 21 35 38 3eqtr4d 
 |-  ( ( A = 0 /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
40 39 3expia 
 |-  ( ( A = 0 /\ B e. NN ) -> ( N e. NN -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
41 1z 
 |-  1 e. ZZ
42 gcd1 
 |-  ( 1 e. ZZ -> ( 1 gcd 1 ) = 1 )
43 41 42 ax-mp 
 |-  ( 1 gcd 1 ) = 1
44 43 eqcomi 
 |-  1 = ( 1 gcd 1 )
45 simp1 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> A = 0 )
46 45 oveq1d 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( A gcd B ) = ( 0 gcd B ) )
47 simp2 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> B e. NN )
48 47 nnzd 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> B e. ZZ )
49 48 26 syl 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( 0 gcd B ) = ( abs ` B ) )
50 32 3ad2ant2 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( abs ` B ) = B )
51 46 49 50 3eqtrd 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( A gcd B ) = B )
52 simp3 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> N = 0 )
53 51 52 oveq12d 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( B ^ 0 ) )
54 47 nncnd 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> B e. CC )
55 54 exp0d 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( B ^ 0 ) = 1 )
56 53 55 eqtrd 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( ( A gcd B ) ^ N ) = 1 )
57 45 52 oveq12d 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( A ^ N ) = ( 0 ^ 0 ) )
58 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
59 58 a1i 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( 0 ^ 0 ) = 1 )
60 57 59 eqtrd 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( A ^ N ) = 1 )
61 52 oveq2d 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( B ^ N ) = ( B ^ 0 ) )
62 61 55 eqtrd 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( B ^ N ) = 1 )
63 60 62 oveq12d 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( 1 gcd 1 ) )
64 44 56 63 3eqtr4a 
 |-  ( ( A = 0 /\ B e. NN /\ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
65 64 3expia 
 |-  ( ( A = 0 /\ B e. NN ) -> ( N = 0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
66 40 65 jaod 
 |-  ( ( A = 0 /\ B e. NN ) -> ( ( N e. NN \/ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
67 5 66 biimtrid 
 |-  ( ( A = 0 /\ B e. NN ) -> ( N e. NN0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
68 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
69 68 3ad2ant1 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> A e. NN0 )
70 10 3ad2ant3 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> N e. NN0 )
71 69 70 nn0expcld 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( A ^ N ) e. NN0 )
72 nn0gcdid0 
 |-  ( ( A ^ N ) e. NN0 -> ( ( A ^ N ) gcd 0 ) = ( A ^ N ) )
73 71 72 syl 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( ( A ^ N ) gcd 0 ) = ( A ^ N ) )
74 simp2 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> B = 0 )
75 74 oveq1d 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( B ^ N ) = ( 0 ^ N ) )
76 6 3ad2ant3 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( 0 ^ N ) = 0 )
77 75 76 eqtrd 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( B ^ N ) = 0 )
78 77 oveq2d 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( ( A ^ N ) gcd 0 ) )
79 74 oveq2d 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( A gcd B ) = ( A gcd 0 ) )
80 nn0gcdid0 
 |-  ( A e. NN0 -> ( A gcd 0 ) = A )
81 68 80 syl 
 |-  ( A e. NN -> ( A gcd 0 ) = A )
82 81 3ad2ant1 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( A gcd 0 ) = A )
83 79 82 eqtrd 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( A gcd B ) = A )
84 83 oveq1d 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( ( A gcd B ) ^ N ) = ( A ^ N ) )
85 73 78 84 3eqtr4rd 
 |-  ( ( A e. NN /\ B = 0 /\ N e. NN ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
86 85 3expia 
 |-  ( ( A e. NN /\ B = 0 ) -> ( N e. NN -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
87 nncn 
 |-  ( A e. NN -> A e. CC )
88 87 exp0d 
 |-  ( A e. NN -> ( A ^ 0 ) = 1 )
89 88 43 eqtr4di 
 |-  ( A e. NN -> ( A ^ 0 ) = ( 1 gcd 1 ) )
90 81 oveq1d 
 |-  ( A e. NN -> ( ( A gcd 0 ) ^ 0 ) = ( A ^ 0 ) )
91 58 a1i 
 |-  ( A e. NN -> ( 0 ^ 0 ) = 1 )
92 88 91 oveq12d 
 |-  ( A e. NN -> ( ( A ^ 0 ) gcd ( 0 ^ 0 ) ) = ( 1 gcd 1 ) )
93 89 90 92 3eqtr4d 
 |-  ( A e. NN -> ( ( A gcd 0 ) ^ 0 ) = ( ( A ^ 0 ) gcd ( 0 ^ 0 ) ) )
94 93 3ad2ant1 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> ( ( A gcd 0 ) ^ 0 ) = ( ( A ^ 0 ) gcd ( 0 ^ 0 ) ) )
95 simp2 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> B = 0 )
96 95 oveq2d 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> ( A gcd B ) = ( A gcd 0 ) )
97 simp3 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> N = 0 )
98 96 97 oveq12d 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( A gcd 0 ) ^ 0 ) )
99 97 oveq2d 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> ( A ^ N ) = ( A ^ 0 ) )
100 95 97 oveq12d 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> ( B ^ N ) = ( 0 ^ 0 ) )
101 99 100 oveq12d 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( ( A ^ 0 ) gcd ( 0 ^ 0 ) ) )
102 94 98 101 3eqtr4d 
 |-  ( ( A e. NN /\ B = 0 /\ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
103 102 3expia 
 |-  ( ( A e. NN /\ B = 0 ) -> ( N = 0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
104 86 103 jaod 
 |-  ( ( A e. NN /\ B = 0 ) -> ( ( N e. NN \/ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
105 5 104 biimtrid 
 |-  ( ( A e. NN /\ B = 0 ) -> ( N e. NN0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
106 gcd0val 
 |-  ( 0 gcd 0 ) = 0
107 6 106 eqtr4di 
 |-  ( N e. NN -> ( 0 ^ N ) = ( 0 gcd 0 ) )
108 106 a1i 
 |-  ( N e. NN -> ( 0 gcd 0 ) = 0 )
109 108 oveq1d 
 |-  ( N e. NN -> ( ( 0 gcd 0 ) ^ N ) = ( 0 ^ N ) )
110 6 6 oveq12d 
 |-  ( N e. NN -> ( ( 0 ^ N ) gcd ( 0 ^ N ) ) = ( 0 gcd 0 ) )
111 107 109 110 3eqtr4d 
 |-  ( N e. NN -> ( ( 0 gcd 0 ) ^ N ) = ( ( 0 ^ N ) gcd ( 0 ^ N ) ) )
112 111 3ad2ant3 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> ( ( 0 gcd 0 ) ^ N ) = ( ( 0 ^ N ) gcd ( 0 ^ N ) ) )
113 simp1 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> A = 0 )
114 simp2 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> B = 0 )
115 113 114 oveq12d 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> ( A gcd B ) = ( 0 gcd 0 ) )
116 115 oveq1d 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> ( ( A gcd B ) ^ N ) = ( ( 0 gcd 0 ) ^ N ) )
117 113 oveq1d 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> ( A ^ N ) = ( 0 ^ N ) )
118 114 oveq1d 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> ( B ^ N ) = ( 0 ^ N ) )
119 117 118 oveq12d 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( ( 0 ^ N ) gcd ( 0 ^ N ) ) )
120 112 116 119 3eqtr4d 
 |-  ( ( A = 0 /\ B = 0 /\ N e. NN ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
121 120 3expia 
 |-  ( ( A = 0 /\ B = 0 ) -> ( N e. NN -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
122 58 43 eqtr4i 
 |-  ( 0 ^ 0 ) = ( 1 gcd 1 )
123 106 oveq1i 
 |-  ( ( 0 gcd 0 ) ^ 0 ) = ( 0 ^ 0 )
124 58 58 oveq12i 
 |-  ( ( 0 ^ 0 ) gcd ( 0 ^ 0 ) ) = ( 1 gcd 1 )
125 122 123 124 3eqtr4i 
 |-  ( ( 0 gcd 0 ) ^ 0 ) = ( ( 0 ^ 0 ) gcd ( 0 ^ 0 ) )
126 simp1 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> A = 0 )
127 simp2 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> B = 0 )
128 126 127 oveq12d 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> ( A gcd B ) = ( 0 gcd 0 ) )
129 simp3 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> N = 0 )
130 128 129 oveq12d 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( 0 gcd 0 ) ^ 0 ) )
131 126 129 oveq12d 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> ( A ^ N ) = ( 0 ^ 0 ) )
132 127 129 oveq12d 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> ( B ^ N ) = ( 0 ^ 0 ) )
133 131 132 oveq12d 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( ( 0 ^ 0 ) gcd ( 0 ^ 0 ) ) )
134 125 130 133 3eqtr4a 
 |-  ( ( A = 0 /\ B = 0 /\ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
135 134 3expia 
 |-  ( ( A = 0 /\ B = 0 ) -> ( N = 0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
136 121 135 jaod 
 |-  ( ( A = 0 /\ B = 0 ) -> ( ( N e. NN \/ N = 0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
137 5 136 biimtrid 
 |-  ( ( A = 0 /\ B = 0 ) -> ( N e. NN0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
138 4 67 105 137 ccase 
 |-  ( ( ( A e. NN \/ A = 0 ) /\ ( B e. NN \/ B = 0 ) ) -> ( N e. NN0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
139 1 2 138 syl2anb 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( N e. NN0 -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) ) )
140 139 3impia 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )