Proof of Theorem dvdsexpnn0
Step | Hyp | Ref
| Expression |
1 | | elnn0 12218 |
. . 3
⊢ (𝐴 ∈ ℕ0
↔ (𝐴 ∈ ℕ
∨ 𝐴 =
0)) |
2 | | elnn0 12218 |
. . 3
⊢ (𝐵 ∈ ℕ0
↔ (𝐵 ∈ ℕ
∨ 𝐵 =
0)) |
3 | | dvdsexpnn 40320 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) |
4 | 3 | 3expia 1119 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝑁 ∈ ℕ → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
5 | | nncn 11964 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
6 | | expeq0 13794 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ) → ((𝐵↑𝑁) = 0 ↔ 𝐵 = 0)) |
7 | 5, 6 | sylan 579 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐵↑𝑁) = 0 ↔ 𝐵 = 0)) |
8 | | 0exp 13799 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(0↑𝑁) =
0) |
9 | 8 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(0↑𝑁) =
0) |
10 | 9 | breq1d 5088 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((0↑𝑁) ∥ (𝐵↑𝑁) ↔ 0 ∥ (𝐵↑𝑁))) |
11 | | nnnn0 12223 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
12 | | nnexpcl 13776 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐵↑𝑁) ∈
ℕ) |
13 | 11, 12 | sylan2 592 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐵↑𝑁) ∈ ℕ) |
14 | 13 | nnzd 12407 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐵↑𝑁) ∈ ℤ) |
15 | | 0dvds 15967 |
. . . . . . . . 9
⊢ ((𝐵↑𝑁) ∈ ℤ → (0 ∥ (𝐵↑𝑁) ↔ (𝐵↑𝑁) = 0)) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (0
∥ (𝐵↑𝑁) ↔ (𝐵↑𝑁) = 0)) |
17 | 10, 16 | bitrd 278 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
((0↑𝑁) ∥ (𝐵↑𝑁) ↔ (𝐵↑𝑁) = 0)) |
18 | | nnz 12325 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
19 | | 0dvds 15967 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℤ → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝐵 ∈ ℕ → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
21 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (0
∥ 𝐵 ↔ 𝐵 = 0)) |
22 | 7, 17, 21 | 3bitr4rd 311 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (0
∥ 𝐵 ↔
(0↑𝑁) ∥ (𝐵↑𝑁))) |
23 | | breq1 5081 |
. . . . . . 7
⊢ (𝐴 = 0 → (𝐴 ∥ 𝐵 ↔ 0 ∥ 𝐵)) |
24 | | oveq1 7275 |
. . . . . . . 8
⊢ (𝐴 = 0 → (𝐴↑𝑁) = (0↑𝑁)) |
25 | 24 | breq1d 5088 |
. . . . . . 7
⊢ (𝐴 = 0 → ((𝐴↑𝑁) ∥ (𝐵↑𝑁) ↔ (0↑𝑁) ∥ (𝐵↑𝑁))) |
26 | 23, 25 | bibi12d 345 |
. . . . . 6
⊢ (𝐴 = 0 → ((𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)) ↔ (0 ∥ 𝐵 ↔ (0↑𝑁) ∥ (𝐵↑𝑁)))) |
27 | 22, 26 | syl5ibr 245 |
. . . . 5
⊢ (𝐴 = 0 → ((𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
28 | 27 | expdimp 452 |
. . . 4
⊢ ((𝐴 = 0 ∧ 𝐵 ∈ ℕ) → (𝑁 ∈ ℕ → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
29 | | nnz 12325 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
30 | | dvds0 15962 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℤ → 𝐴 ∥ 0) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → 𝐴 ∥ 0) |
32 | 31 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝐴 ∥ 0) |
33 | | nnexpcl 13776 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0)
→ (𝐴↑𝑁) ∈
ℕ) |
34 | 11, 33 | sylan2 592 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) ∈ ℕ) |
35 | 34 | nnzd 12407 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) ∈ ℤ) |
36 | | dvds0 15962 |
. . . . . . . . 9
⊢ ((𝐴↑𝑁) ∈ ℤ → (𝐴↑𝑁) ∥ 0) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) ∥ 0) |
38 | 8 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) →
(0↑𝑁) =
0) |
39 | 37, 38 | breqtrrd 5106 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) ∥ (0↑𝑁)) |
40 | 32, 39 | 2thd 264 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 0 ↔ (𝐴↑𝑁) ∥ (0↑𝑁))) |
41 | | breq2 5082 |
. . . . . . 7
⊢ (𝐵 = 0 → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ 0)) |
42 | | oveq1 7275 |
. . . . . . . 8
⊢ (𝐵 = 0 → (𝐵↑𝑁) = (0↑𝑁)) |
43 | 42 | breq2d 5090 |
. . . . . . 7
⊢ (𝐵 = 0 → ((𝐴↑𝑁) ∥ (𝐵↑𝑁) ↔ (𝐴↑𝑁) ∥ (0↑𝑁))) |
44 | 41, 43 | bibi12d 345 |
. . . . . 6
⊢ (𝐵 = 0 → ((𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)) ↔ (𝐴 ∥ 0 ↔ (𝐴↑𝑁) ∥ (0↑𝑁)))) |
45 | 40, 44 | syl5ibrcom 246 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐵 = 0 → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
46 | 45 | impancom 451 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 = 0) → (𝑁 ∈ ℕ → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
47 | 8, 8 | breq12d 5091 |
. . . . . 6
⊢ (𝑁 ∈ ℕ →
((0↑𝑁) ∥
(0↑𝑁) ↔ 0 ∥
0)) |
48 | 47 | bicomd 222 |
. . . . 5
⊢ (𝑁 ∈ ℕ → (0
∥ 0 ↔ (0↑𝑁)
∥ (0↑𝑁))) |
49 | | breq12 5083 |
. . . . . 6
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴 ∥ 𝐵 ↔ 0 ∥ 0)) |
50 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐴 = 0) |
51 | 50 | oveq1d 7283 |
. . . . . . 7
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐴↑𝑁) = (0↑𝑁)) |
52 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → 𝐵 = 0) |
53 | 52 | oveq1d 7283 |
. . . . . . 7
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝐵↑𝑁) = (0↑𝑁)) |
54 | 51, 53 | breq12d 5091 |
. . . . . 6
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴↑𝑁) ∥ (𝐵↑𝑁) ↔ (0↑𝑁) ∥ (0↑𝑁))) |
55 | 49, 54 | bibi12d 345 |
. . . . 5
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → ((𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)) ↔ (0 ∥ 0 ↔ (0↑𝑁) ∥ (0↑𝑁)))) |
56 | 48, 55 | syl5ibr 245 |
. . . 4
⊢ ((𝐴 = 0 ∧ 𝐵 = 0) → (𝑁 ∈ ℕ → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
57 | 4, 28, 46, 56 | ccase 1034 |
. . 3
⊢ (((𝐴 ∈ ℕ ∨ 𝐴 = 0) ∧ (𝐵 ∈ ℕ ∨ 𝐵 = 0)) → (𝑁 ∈ ℕ → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
58 | 1, 2, 57 | syl2anb 597 |
. 2
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0) → (𝑁 ∈ ℕ → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁)))) |
59 | 58 | 3impia 1115 |
1
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0 ∧ 𝑁
∈ ℕ) → (𝐴
∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) |