Metamath Proof Explorer

Theorem dvdsexpnn0

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

Ref Expression
Assertion dvdsexpnn0 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
2 elnn0 ⊢ ( 𝐵 ∈ ℕ0 ↔ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) )
3 dvdsexpnn ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
4 3 3expia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∈ ℕ → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
5 nncn ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
6 expeq0 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐵 ↑ 𝑁 ) = 0 ↔ 𝐵 = 0 ) )
7 5 6 sylan ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐵 ↑ 𝑁 ) = 0 ↔ 𝐵 = 0 ) )
8 0exp ⊢ ( 𝑁 ∈ ℕ → ( 0 ↑ 𝑁 ) = 0 )
9 8 adantl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 ↑ 𝑁 ) = 0 )
10 9 breq1d ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 0 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ↔ 0 ∥ ( 𝐵 ↑ 𝑁 ) ) )
11 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
12 nnexpcl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ 𝑁 ) ∈ ℕ )
13 11 12 sylan2 ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℕ )
14 13 nnzd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑ 𝑁 ) ∈ ℤ )
15 0dvds ⊢ ( ( 𝐵 ↑ 𝑁 ) ∈ ℤ → ( 0 ∥ ( 𝐵 ↑ 𝑁 ) ↔ ( 𝐵 ↑ 𝑁 ) = 0 ) )
16 14 15 syl ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 ∥ ( 𝐵 ↑ 𝑁 ) ↔ ( 𝐵 ↑ 𝑁 ) = 0 ) )
17 10 16 bitrd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 0 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ↔ ( 𝐵 ↑ 𝑁 ) = 0 ) )
18 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
19 0dvds ⊢ ( 𝐵 ∈ ℤ → ( 0 ∥ 𝐵 ↔ 𝐵 = 0 ) )
20 18 19 syl ⊢ ( 𝐵 ∈ ℕ → ( 0 ∥ 𝐵 ↔ 𝐵 = 0 ) )
21 20 adantr ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 ∥ 𝐵 ↔ 𝐵 = 0 ) )
22 7 17 21 3bitr4rd ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 ∥ 𝐵 ↔ ( 0 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
23 breq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ∥ 𝐵 ↔ 0 ∥ 𝐵 ) )
24 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
25 24 breq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ↔ ( 0 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )
26 23 25 bibi12d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ↔ ( 0 ∥ 𝐵 ↔ ( 0 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
27 22 26 imbitrrid ⊢ ( 𝐴 = 0 → ( ( 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
28 27 expdimp ⊢ ( ( 𝐴 = 0 ∧ 𝐵 ∈ ℕ ) → ( 𝑁 ∈ ℕ → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
29 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
30 dvds0 ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∥ 0 )
31 29 30 syl ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∥ 0 )
32 31 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∥ 0 )
33 nnexpcl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
34 11 33 sylan2 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℕ )
35 34 nnzd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℤ )
36 dvds0 ⊢ ( ( 𝐴 ↑ 𝑁 ) ∈ ℤ → ( 𝐴 ↑ 𝑁 ) ∥ 0 )
37 35 36 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) ∥ 0 )
38 8 adantl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 0 ↑ 𝑁 ) = 0 )
39 37 38 breqtrrd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) )
40 32 39 2thd ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 0 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) ) )
41 breq2 ⊢ ( 𝐵 = 0 → ( 𝐴 ∥ 𝐵 ↔ 𝐴 ∥ 0 ) )
42 oveq1 ⊢ ( 𝐵 = 0 → ( 𝐵 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
43 42 breq2d ⊢ ( 𝐵 = 0 → ( ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) ) )
44 41 43 bibi12d ⊢ ( 𝐵 = 0 → ( ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ↔ ( 𝐴 ∥ 0 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) ) ) )
45 40 44 syl5ibrcom ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐵 = 0 → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
46 45 impancom ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
47 8 8 breq12d ⊢ ( 𝑁 ∈ ℕ → ( ( 0 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) ↔ 0 ∥ 0 ) )
48 47 bicomd ⊢ ( 𝑁 ∈ ℕ → ( 0 ∥ 0 ↔ ( 0 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) ) )
49 breq12 ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 ∥ 𝐵 ↔ 0 ∥ 0 ) )
50 simpl ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → 𝐴 = 0 )
51 50 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐴 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
52 simpr ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → 𝐵 = 0 )
53 52 oveq1d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝐵 ↑ 𝑁 ) = ( 0 ↑ 𝑁 ) )
54 51 53 breq12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ↔ ( 0 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) ) )
55 49 54 bibi12d ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ↔ ( 0 ∥ 0 ↔ ( 0 ↑ 𝑁 ) ∥ ( 0 ↑ 𝑁 ) ) ) )
56 48 55 imbitrrid ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → ( 𝑁 ∈ ℕ → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
57 4 28 46 56 ccase ⊢ ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ ( 𝐵 ∈ ℕ ∨ 𝐵 = 0 ) ) → ( 𝑁 ∈ ℕ → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
58 1 2 57 syl2anb ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) ) )
59 58 3impia ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∥ 𝐵 ↔ ( 𝐴 ↑ 𝑁 ) ∥ ( 𝐵 ↑ 𝑁 ) ) )