Metamath Proof Explorer

Theorem dvdsexpnn0

Description: dvdsexpnn generalized to include zero bases. (Contributed by SN, 15-Sep-2024)

Ref Expression
Assertion dvdsexpnn0 
|- ( ( A e. NN0 /\ B e. NN0 /\ N e. NN ) -> ( A || B <-> ( A ^ N ) || ( 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 dvdsexpnn 
 |-  ( ( A e. NN /\ B e. NN /\ N e. NN ) -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) )
4 3 3expia 
 |-  ( ( A e. NN /\ B e. NN ) -> ( N e. NN -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
5 nncn 
 |-  ( B e. NN -> B e. CC )
6 expeq0 
 |-  ( ( B e. CC /\ N e. NN ) -> ( ( B ^ N ) = 0 <-> B = 0 ) )
7 5 6 sylan 
 |-  ( ( B e. NN /\ N e. NN ) -> ( ( B ^ N ) = 0 <-> B = 0 ) )
8 0exp 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )
9 8 adantl 
 |-  ( ( B e. NN /\ N e. NN ) -> ( 0 ^ N ) = 0 )
10 9 breq1d 
 |-  ( ( B e. NN /\ N e. NN ) -> ( ( 0 ^ N ) || ( B ^ N ) <-> 0 || ( B ^ N ) ) )
11 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
12 nnexpcl 
 |-  ( ( B e. NN /\ N e. NN0 ) -> ( B ^ N ) e. NN )
13 11 12 sylan2 
 |-  ( ( B e. NN /\ N e. NN ) -> ( B ^ N ) e. NN )
14 13 nnzd 
 |-  ( ( B e. NN /\ N e. NN ) -> ( B ^ N ) e. ZZ )
15 0dvds 
 |-  ( ( B ^ N ) e. ZZ -> ( 0 || ( B ^ N ) <-> ( B ^ N ) = 0 ) )
16 14 15 syl 
 |-  ( ( B e. NN /\ N e. NN ) -> ( 0 || ( B ^ N ) <-> ( B ^ N ) = 0 ) )
17 10 16 bitrd 
 |-  ( ( B e. NN /\ N e. NN ) -> ( ( 0 ^ N ) || ( B ^ N ) <-> ( B ^ N ) = 0 ) )
18 nnz 
 |-  ( B e. NN -> B e. ZZ )
19 0dvds 
 |-  ( B e. ZZ -> ( 0 || B <-> B = 0 ) )
20 18 19 syl 
 |-  ( B e. NN -> ( 0 || B <-> B = 0 ) )
21 20 adantr 
 |-  ( ( B e. NN /\ N e. NN ) -> ( 0 || B <-> B = 0 ) )
22 7 17 21 3bitr4rd 
 |-  ( ( B e. NN /\ N e. NN ) -> ( 0 || B <-> ( 0 ^ N ) || ( B ^ N ) ) )
23 breq1 
 |-  ( A = 0 -> ( A || B <-> 0 || B ) )
24 oveq1 
 |-  ( A = 0 -> ( A ^ N ) = ( 0 ^ N ) )
25 24 breq1d 
 |-  ( A = 0 -> ( ( A ^ N ) || ( B ^ N ) <-> ( 0 ^ N ) || ( B ^ N ) ) )
26 23 25 bibi12d 
 |-  ( A = 0 -> ( ( A || B <-> ( A ^ N ) || ( B ^ N ) ) <-> ( 0 || B <-> ( 0 ^ N ) || ( B ^ N ) ) ) )
27 22 26 syl5ibr 
 |-  ( A = 0 -> ( ( B e. NN /\ N e. NN ) -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
28 27 expdimp 
 |-  ( ( A = 0 /\ B e. NN ) -> ( N e. NN -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
29 nnz 
 |-  ( A e. NN -> A e. ZZ )
30 dvds0 
 |-  ( A e. ZZ -> A || 0 )
31 29 30 syl 
 |-  ( A e. NN -> A || 0 )
32 31 adantr 
 |-  ( ( A e. NN /\ N e. NN ) -> A || 0 )
33 nnexpcl 
 |-  ( ( A e. NN /\ N e. NN0 ) -> ( A ^ N ) e. NN )
34 11 33 sylan2 
 |-  ( ( A e. NN /\ N e. NN ) -> ( A ^ N ) e. NN )
35 34 nnzd 
 |-  ( ( A e. NN /\ N e. NN ) -> ( A ^ N ) e. ZZ )
36 dvds0 
 |-  ( ( A ^ N ) e. ZZ -> ( A ^ N ) || 0 )
37 35 36 syl 
 |-  ( ( A e. NN /\ N e. NN ) -> ( A ^ N ) || 0 )
38 8 adantl 
 |-  ( ( A e. NN /\ N e. NN ) -> ( 0 ^ N ) = 0 )
39 37 38 breqtrrd 
 |-  ( ( A e. NN /\ N e. NN ) -> ( A ^ N ) || ( 0 ^ N ) )
40 32 39 2thd 
 |-  ( ( A e. NN /\ N e. NN ) -> ( A || 0 <-> ( A ^ N ) || ( 0 ^ N ) ) )
41 breq2 
 |-  ( B = 0 -> ( A || B <-> A || 0 ) )
42 oveq1 
 |-  ( B = 0 -> ( B ^ N ) = ( 0 ^ N ) )
43 42 breq2d 
 |-  ( B = 0 -> ( ( A ^ N ) || ( B ^ N ) <-> ( A ^ N ) || ( 0 ^ N ) ) )
44 41 43 bibi12d 
 |-  ( B = 0 -> ( ( A || B <-> ( A ^ N ) || ( B ^ N ) ) <-> ( A || 0 <-> ( A ^ N ) || ( 0 ^ N ) ) ) )
45 40 44 syl5ibrcom 
 |-  ( ( A e. NN /\ N e. NN ) -> ( B = 0 -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
46 45 impancom 
 |-  ( ( A e. NN /\ B = 0 ) -> ( N e. NN -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
47 8 8 breq12d 
 |-  ( N e. NN -> ( ( 0 ^ N ) || ( 0 ^ N ) <-> 0 || 0 ) )
48 47 bicomd 
 |-  ( N e. NN -> ( 0 || 0 <-> ( 0 ^ N ) || ( 0 ^ N ) ) )
49 breq12 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A || B <-> 0 || 0 ) )
50 simpl 
 |-  ( ( A = 0 /\ B = 0 ) -> A = 0 )
51 50 oveq1d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( A ^ N ) = ( 0 ^ N ) )
52 simpr 
 |-  ( ( A = 0 /\ B = 0 ) -> B = 0 )
53 52 oveq1d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( B ^ N ) = ( 0 ^ N ) )
54 51 53 breq12d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( ( A ^ N ) || ( B ^ N ) <-> ( 0 ^ N ) || ( 0 ^ N ) ) )
55 49 54 bibi12d 
 |-  ( ( A = 0 /\ B = 0 ) -> ( ( A || B <-> ( A ^ N ) || ( B ^ N ) ) <-> ( 0 || 0 <-> ( 0 ^ N ) || ( 0 ^ N ) ) ) )
56 48 55 syl5ibr 
 |-  ( ( A = 0 /\ B = 0 ) -> ( N e. NN -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
57 4 28 46 56 ccase 
 |-  ( ( ( A e. NN \/ A = 0 ) /\ ( B e. NN \/ B = 0 ) ) -> ( N e. NN -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
58 1 2 57 syl2anb 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( N e. NN -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) ) )
59 58 3impia 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ N e. NN ) -> ( A || B <-> ( A ^ N ) || ( B ^ N ) ) )