Step | Hyp | Ref
| Expression |
1 | | oveq2 5861 |
. . . . 5
⊢ (𝑥 = 1 → (𝐴 · 𝑥) = (𝐴 · 1)) |
2 | 1 | eleq1d 2239 |
. . . 4
⊢ (𝑥 = 1 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 1) ∈
ℕ)) |
3 | 2 | imbi2d 229 |
. . 3
⊢ (𝑥 = 1 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 1) ∈
ℕ))) |
4 | | oveq2 5861 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 · 𝑥) = (𝐴 · 𝑦)) |
5 | 4 | eleq1d 2239 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 𝑦) ∈ ℕ)) |
6 | 5 | imbi2d 229 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 𝑦) ∈ ℕ))) |
7 | | oveq2 5861 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝐴 · 𝑥) = (𝐴 · (𝑦 + 1))) |
8 | 7 | eleq1d 2239 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · (𝑦 + 1)) ∈ ℕ)) |
9 | 8 | imbi2d 229 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ))) |
10 | | oveq2 5861 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐴 · 𝑥) = (𝐴 · 𝐵)) |
11 | 10 | eleq1d 2239 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐴 · 𝑥) ∈ ℕ ↔ (𝐴 · 𝐵) ∈ ℕ)) |
12 | 11 | imbi2d 229 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ℕ → (𝐴 · 𝑥) ∈ ℕ) ↔ (𝐴 ∈ ℕ → (𝐴 · 𝐵) ∈ ℕ))) |
13 | | nncn 8886 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
14 | | mulid1 7917 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 · 1) = 𝐴) |
15 | 14 | eleq1d 2239 |
. . . . 5
⊢ (𝐴 ∈ ℂ → ((𝐴 · 1) ∈ ℕ
↔ 𝐴 ∈
ℕ)) |
16 | 15 | biimprd 157 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℕ → (𝐴 · 1) ∈
ℕ)) |
17 | 13, 16 | mpcom 36 |
. . 3
⊢ (𝐴 ∈ ℕ → (𝐴 · 1) ∈
ℕ) |
18 | | nnaddcl 8898 |
. . . . . . . 8
⊢ (((𝐴 · 𝑦) ∈ ℕ ∧ 𝐴 ∈ ℕ) → ((𝐴 · 𝑦) + 𝐴) ∈ ℕ) |
19 | 18 | ancoms 266 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ (𝐴 · 𝑦) ∈ ℕ) → ((𝐴 · 𝑦) + 𝐴) ∈ ℕ) |
20 | | nncn 8886 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
21 | | ax-1cn 7867 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
22 | | adddi 7906 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 ·
(𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1))) |
23 | 21, 22 | mp3an3 1321 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + (𝐴 · 1))) |
24 | 14 | oveq2d 5869 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℂ → ((𝐴 · 𝑦) + (𝐴 · 1)) = ((𝐴 · 𝑦) + 𝐴)) |
25 | 24 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝐴 · 𝑦) + (𝐴 · 1)) = ((𝐴 · 𝑦) + 𝐴)) |
26 | 23, 25 | eqtrd 2203 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + 𝐴)) |
27 | 13, 20, 26 | syl2an 287 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝐴 · (𝑦 + 1)) = ((𝐴 · 𝑦) + 𝐴)) |
28 | 27 | eleq1d 2239 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 · (𝑦 + 1)) ∈ ℕ ↔ ((𝐴 · 𝑦) + 𝐴) ∈ ℕ)) |
29 | 19, 28 | syl5ibr 155 |
. . . . . 6
⊢ ((𝐴 ∈ ℕ ∧ 𝑦 ∈ ℕ) → ((𝐴 ∈ ℕ ∧ (𝐴 · 𝑦) ∈ ℕ) → (𝐴 · (𝑦 + 1)) ∈ ℕ)) |
30 | 29 | exp4b 365 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (𝑦 ∈ ℕ → (𝐴 ∈ ℕ → ((𝐴 · 𝑦) ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ)))) |
31 | 30 | pm2.43b 52 |
. . . 4
⊢ (𝑦 ∈ ℕ → (𝐴 ∈ ℕ → ((𝐴 · 𝑦) ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ))) |
32 | 31 | a2d 26 |
. . 3
⊢ (𝑦 ∈ ℕ → ((𝐴 ∈ ℕ → (𝐴 · 𝑦) ∈ ℕ) → (𝐴 ∈ ℕ → (𝐴 · (𝑦 + 1)) ∈ ℕ))) |
33 | 3, 6, 9, 12, 17, 32 | nnind 8894 |
. 2
⊢ (𝐵 ∈ ℕ → (𝐴 ∈ ℕ → (𝐴 · 𝐵) ∈ ℕ)) |
34 | 33 | impcom 124 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) |