Metamath Proof Explorer

Theorem dvdsexpb

Description: dvdssq generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 nn0abscl 
 |-  ( A e. ZZ -> ( abs ` A ) e. NN0 )
2 nn0abscl 
 |-  ( B e. ZZ -> ( abs ` B ) e. NN0 )
3 dvdsexpnn0 
 |-  ( ( ( abs ` A ) e. NN0 /\ ( abs ` B ) e. NN0 /\ N e. NN ) -> ( ( abs ` A ) || ( abs ` B ) <-> ( ( abs ` A ) ^ N ) || ( ( abs ` B ) ^ N ) ) )
4 1 2 3 syl3an12 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( abs ` A ) || ( abs ` B ) <-> ( ( abs ` A ) ^ N ) || ( ( abs ` B ) ^ N ) ) )
5 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> A e. ZZ )
6 5 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> A e. CC )
7 simp3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> N e. NN )
8 7 nnnn0d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> N e. NN0 )
9 6 8 absexpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )
10 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> B e. ZZ )
11 10 zcnd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> B e. CC )
12 11 8 absexpd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( abs ` ( B ^ N ) ) = ( ( abs ` B ) ^ N ) )
13 9 12 breq12d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( abs ` ( A ^ N ) ) || ( abs ` ( B ^ N ) ) <-> ( ( abs ` A ) ^ N ) || ( ( abs ` B ) ^ N ) ) )
14 4 13 bitr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( abs ` A ) || ( abs ` B ) <-> ( abs ` ( A ^ N ) ) || ( abs ` ( B ^ N ) ) ) )
15 absdvdsabsb 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> ( abs ` A ) || ( abs ` B ) ) )
16 15 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A || B <-> ( abs ` A ) || ( abs ` B ) ) )
17 5 8 zexpcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A ^ N ) e. ZZ )
18 10 8 zexpcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( B ^ N ) e. ZZ )
19 absdvdsabsb 
 |-  ( ( ( A ^ N ) e. ZZ /\ ( B ^ N ) e. ZZ ) -> ( ( A ^ N ) || ( B ^ N ) <-> ( abs ` ( A ^ N ) ) || ( abs ` ( B ^ N ) ) ) )
20 17 18 19 syl2anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( A ^ N ) || ( B ^ N ) <-> ( abs ` ( A ^ N ) ) || ( abs ` ( B ^ N ) ) ) )
21 14 16 20 3bitr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) )