Step | Hyp | Ref
| Expression |
1 | | oveq1 7177 |
. . . . 5
⊢ (𝑥 = 1 → (𝑥 + 𝐵) = (1 + 𝐵)) |
2 | | oveq2 7178 |
. . . . 5
⊢ (𝑥 = 1 → (𝐵 + 𝑥) = (𝐵 + 1)) |
3 | 1, 2 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 1 → ((𝑥 + 𝐵) = (𝐵 + 𝑥) ↔ (1 + 𝐵) = (𝐵 + 1))) |
4 | 3 | imbi2d 344 |
. . 3
⊢ (𝑥 = 1 → ((𝐵 ∈ ℕ → (𝑥 + 𝐵) = (𝐵 + 𝑥)) ↔ (𝐵 ∈ ℕ → (1 + 𝐵) = (𝐵 + 1)))) |
5 | | oveq1 7177 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 + 𝐵) = (𝑦 + 𝐵)) |
6 | | oveq2 7178 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 + 𝑥) = (𝐵 + 𝑦)) |
7 | 5, 6 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥 + 𝐵) = (𝐵 + 𝑥) ↔ (𝑦 + 𝐵) = (𝐵 + 𝑦))) |
8 | 7 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐵 ∈ ℕ → (𝑥 + 𝐵) = (𝐵 + 𝑥)) ↔ (𝐵 ∈ ℕ → (𝑦 + 𝐵) = (𝐵 + 𝑦)))) |
9 | | oveq1 7177 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝑥 + 𝐵) = ((𝑦 + 1) + 𝐵)) |
10 | | oveq2 7178 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (𝐵 + 𝑥) = (𝐵 + (𝑦 + 1))) |
11 | 9, 10 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 + 𝐵) = (𝐵 + 𝑥) ↔ ((𝑦 + 1) + 𝐵) = (𝐵 + (𝑦 + 1)))) |
12 | 11 | imbi2d 344 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝐵 ∈ ℕ → (𝑥 + 𝐵) = (𝐵 + 𝑥)) ↔ (𝐵 ∈ ℕ → ((𝑦 + 1) + 𝐵) = (𝐵 + (𝑦 + 1))))) |
13 | | oveq1 7177 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 + 𝐵) = (𝐴 + 𝐵)) |
14 | | oveq2 7178 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐵 + 𝑥) = (𝐵 + 𝐴)) |
15 | 13, 14 | eqeq12d 2754 |
. . . 4
⊢ (𝑥 = 𝐴 → ((𝑥 + 𝐵) = (𝐵 + 𝑥) ↔ (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
16 | 15 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝐵 ∈ ℕ → (𝑥 + 𝐵) = (𝐵 + 𝑥)) ↔ (𝐵 ∈ ℕ → (𝐴 + 𝐵) = (𝐵 + 𝐴)))) |
17 | | nnadd1com 39873 |
. . . 4
⊢ (𝐵 ∈ ℕ → (𝐵 + 1) = (1 + 𝐵)) |
18 | 17 | eqcomd 2744 |
. . 3
⊢ (𝐵 ∈ ℕ → (1 +
𝐵) = (𝐵 + 1)) |
19 | | oveq1 7177 |
. . . . . 6
⊢ ((𝑦 + 𝐵) = (𝐵 + 𝑦) → ((𝑦 + 𝐵) + 1) = ((𝐵 + 𝑦) + 1)) |
20 | 17 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℕ → (𝑦 + (𝐵 + 1)) = (𝑦 + (1 + 𝐵))) |
21 | 20 | adantl 485 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝑦 + (𝐵 + 1)) = (𝑦 + (1 + 𝐵))) |
22 | | nncn 11724 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℂ) |
23 | 22 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝑦 ∈
ℂ) |
24 | | nncn 11724 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℂ) |
25 | 24 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝐵 ∈
ℂ) |
26 | | 1cnd 10714 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 1 ∈
ℂ) |
27 | 23, 25, 26 | addassd 10741 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝑦 + 𝐵) + 1) = (𝑦 + (𝐵 + 1))) |
28 | 23, 26, 25 | addassd 10741 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝑦 + 1) + 𝐵) = (𝑦 + (1 + 𝐵))) |
29 | 21, 27, 28 | 3eqtr4d 2783 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝑦 + 𝐵) + 1) = ((𝑦 + 1) + 𝐵)) |
30 | 25, 23, 26 | addassd 10741 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐵 + 𝑦) + 1) = (𝐵 + (𝑦 + 1))) |
31 | 29, 30 | eqeq12d 2754 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝑦 + 𝐵) + 1) = ((𝐵 + 𝑦) + 1) ↔ ((𝑦 + 1) + 𝐵) = (𝐵 + (𝑦 + 1)))) |
32 | 19, 31 | syl5ib 247 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝑦 + 𝐵) = (𝐵 + 𝑦) → ((𝑦 + 1) + 𝐵) = (𝐵 + (𝑦 + 1)))) |
33 | 32 | ex 416 |
. . . 4
⊢ (𝑦 ∈ ℕ → (𝐵 ∈ ℕ → ((𝑦 + 𝐵) = (𝐵 + 𝑦) → ((𝑦 + 1) + 𝐵) = (𝐵 + (𝑦 + 1))))) |
34 | 33 | a2d 29 |
. . 3
⊢ (𝑦 ∈ ℕ → ((𝐵 ∈ ℕ → (𝑦 + 𝐵) = (𝐵 + 𝑦)) → (𝐵 ∈ ℕ → ((𝑦 + 1) + 𝐵) = (𝐵 + (𝑦 + 1))))) |
35 | 4, 8, 12, 16, 18, 34 | nnind 11734 |
. 2
⊢ (𝐴 ∈ ℕ → (𝐵 ∈ ℕ → (𝐴 + 𝐵) = (𝐵 + 𝐴))) |
36 | 35 | imp 410 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |