Metamath Proof Explorer

Theorem dvdsexpnn0

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

Ref Expression
Assertion dvdsexpnn0 ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ A ∈ ℕ 0 ↔ A ∈ ℕ ∨ A = 0
2 elnn0 ⊢ B ∈ ℕ 0 ↔ B ∈ ℕ ∨ B = 0
3 dvdsexpnn ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N
4 3 3expia ⊢ A ∈ ℕ ∧ B ∈ ℕ → N ∈ ℕ → A ∥ B ↔ A N ∥ B N
5 nncn ⊢ B ∈ ℕ → B ∈ ℂ
6 expeq0 ⊢ B ∈ ℂ ∧ N ∈ ℕ → B N = 0 ↔ B = 0
7 5 6 sylan ⊢ B ∈ ℕ ∧ N ∈ ℕ → B N = 0 ↔ B = 0
8 0exp ⊢ N ∈ ℕ → 0 N = 0
9 8 adantl ⊢ B ∈ ℕ ∧ N ∈ ℕ → 0 N = 0
10 9 breq1d ⊢ B ∈ ℕ ∧ N ∈ ℕ → 0 N ∥ B N ↔ 0 ∥ B N
11 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
12 nnexpcl ⊢ B ∈ ℕ ∧ N ∈ ℕ 0 → B N ∈ ℕ
13 11 12 sylan2 ⊢ B ∈ ℕ ∧ N ∈ ℕ → B N ∈ ℕ
14 13 nnzd ⊢ B ∈ ℕ ∧ N ∈ ℕ → B N ∈ ℤ
15 0dvds ⊢ B N ∈ ℤ → 0 ∥ B N ↔ B N = 0
16 14 15 syl ⊢ B ∈ ℕ ∧ N ∈ ℕ → 0 ∥ B N ↔ B N = 0
17 10 16 bitrd ⊢ B ∈ ℕ ∧ N ∈ ℕ → 0 N ∥ B N ↔ B N = 0
18 nnz ⊢ B ∈ ℕ → B ∈ ℤ
19 0dvds ⊢ B ∈ ℤ → 0 ∥ B ↔ B = 0
20 18 19 syl ⊢ B ∈ ℕ → 0 ∥ B ↔ B = 0
21 20 adantr ⊢ B ∈ ℕ ∧ N ∈ ℕ → 0 ∥ B ↔ B = 0
22 7 17 21 3bitr4rd ⊢ B ∈ ℕ ∧ N ∈ ℕ → 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 ∈ ℕ ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N
28 27 expdimp ⊢ A = 0 ∧ B ∈ ℕ → N ∈ ℕ → A ∥ B ↔ A N ∥ B N
29 nnz ⊢ A ∈ ℕ → A ∈ ℤ
30 dvds0 ⊢ A ∈ ℤ → A ∥ 0
31 29 30 syl ⊢ A ∈ ℕ → A ∥ 0
32 31 adantr ⊢ A ∈ ℕ ∧ N ∈ ℕ → A ∥ 0
33 nnexpcl ⊢ A ∈ ℕ ∧ N ∈ ℕ 0 → A N ∈ ℕ
34 11 33 sylan2 ⊢ A ∈ ℕ ∧ N ∈ ℕ → A N ∈ ℕ
35 34 nnzd ⊢ A ∈ ℕ ∧ N ∈ ℕ → A N ∈ ℤ
36 dvds0 ⊢ A N ∈ ℤ → A N ∥ 0
37 35 36 syl ⊢ A ∈ ℕ ∧ N ∈ ℕ → A N ∥ 0
38 8 adantl ⊢ A ∈ ℕ ∧ N ∈ ℕ → 0 N = 0
39 37 38 breqtrrd ⊢ A ∈ ℕ ∧ N ∈ ℕ → A N ∥ 0 N
40 32 39 2thd ⊢ A ∈ ℕ ∧ N ∈ ℕ → 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 ∈ ℕ ∧ N ∈ ℕ → B = 0 → A ∥ B ↔ A N ∥ B N
46 45 impancom ⊢ A ∈ ℕ ∧ B = 0 → N ∈ ℕ → A ∥ B ↔ A N ∥ B N
47 8 8 breq12d ⊢ N ∈ ℕ → 0 N ∥ 0 N ↔ 0 ∥ 0
48 47 bicomd ⊢ N ∈ ℕ → 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 ∈ ℕ → A ∥ B ↔ A N ∥ B N
57 4 28 46 56 ccase ⊢ A ∈ ℕ ∨ A = 0 ∧ B ∈ ℕ ∨ B = 0 → N ∈ ℕ → A ∥ B ↔ A N ∥ B N
58 1 2 57 syl2anb ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 → N ∈ ℕ → A ∥ B ↔ A N ∥ B N
59 58 3impia ⊢ A ∈ ℕ 0 ∧ B ∈ ℕ 0 ∧ N ∈ ℕ → A ∥ B ↔ A N ∥ B N