Metamath Proof Explorer

Theorem dvdsexpnn

Description: dvdssqlem generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024)

Ref Expression
Assertion dvdsexpnn 
|- ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( A e. NN -> A e. ZZ )
2 nnz 
 |-  ( B e. NN -> B e. ZZ )
3 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
4 dvdsexpim 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN0 ) -> ( A || B -> ( A ^ N ) || ( B ^ N ) ) )
5 1 2 3 4 syl3an 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A || B -> ( A ^ N ) || ( B ^ N ) ) )
6 gcdnncl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. NN )
7 6 nnrpd 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) e. RR+ )
8 7 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A gcd B ) e. RR+ )
9 8 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> ( A gcd B ) e. RR+ )
10 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> A e. NN )
11 10 nnrpd 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> A e. RR+ )
12 simpl3 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> N e. NN )
13 expgcd 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN0 ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
14 3 13 syl3an3 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
15 14 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> ( ( A gcd B ) ^ N ) = ( ( A ^ N ) gcd ( B ^ N ) ) )
16 simp1 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> A e. NN )
17 3 3ad2ant3 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> N e. NN0 )
18 16 17 nnexpcld 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A ^ N ) e. NN )
19 simp2 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> B e. NN )
20 19 17 nnexpcld 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( B ^ N ) e. NN )
21 gcdeq 
 |-  ( ( ( A ^ N ) e. NN /\ ( B ^ N ) e. NN ) -> ( ( ( A ^ N ) gcd ( B ^ N ) ) = ( A ^ N ) <-> ( A ^ N ) || ( B ^ N ) ) )
22 18 20 21 syl2anc 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( ( A ^ N ) gcd ( B ^ N ) ) = ( A ^ N ) <-> ( A ^ N ) || ( B ^ N ) ) )
23 22 biimpar 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> ( ( A ^ N ) gcd ( B ^ N ) ) = ( A ^ N ) )
24 15 23 eqtrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> ( ( A gcd B ) ^ N ) = ( A ^ N ) )
25 9 11 12 24 exp11nnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> ( A gcd B ) = A )
26 gcddvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) || A /\ ( A gcd B ) || B ) )
27 26 simprd 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A gcd B ) || B )
28 1 2 27 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A gcd B ) || B )
29 28 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A gcd B ) || B )
30 29 adantr 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> ( A gcd B ) || B )
31 25 30 eqbrtrrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ N e. NN ) /\ ( A ^ N ) || ( B ^ N ) ) -> A || B )
32 31 ex 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( ( A ^ N ) || ( B ^ N ) -> A || B ) )
33 5 32 impbid 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) )