| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝐵 → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o 𝐵)) | 
| 2 |  | oveq2 7439 | . . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝐵)) | 
| 3 |  | id 22 | . . . . . 6
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) | 
| 4 | 2, 3 | oveq12d 7449 | . . . . 5
⊢ (𝑥 = 𝐵 → ((𝐴 ·o 𝑥) +o 𝑥) = ((𝐴 ·o 𝐵) +o 𝐵)) | 
| 5 | 1, 4 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 𝐵 → ((suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥) ↔ (suc 𝐴 ·o 𝐵) = ((𝐴 ·o 𝐵) +o 𝐵))) | 
| 6 | 5 | imbi2d 340 | . . 3
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ω → (suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥)) ↔ (𝐴 ∈ ω → (suc 𝐴 ·o 𝐵) = ((𝐴 ·o 𝐵) +o 𝐵)))) | 
| 7 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = ∅ → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o
∅)) | 
| 8 |  | oveq2 7439 | . . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o
∅)) | 
| 9 |  | id 22 | . . . . . 6
⊢ (𝑥 = ∅ → 𝑥 = ∅) | 
| 10 | 8, 9 | oveq12d 7449 | . . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ·o 𝑥) +o 𝑥) = ((𝐴 ·o ∅) +o
∅)) | 
| 11 | 7, 10 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = ∅ → ((suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥) ↔ (suc 𝐴 ·o ∅) = ((𝐴 ·o ∅)
+o ∅))) | 
| 12 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = 𝑦 → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o 𝑦)) | 
| 13 |  | oveq2 7439 | . . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦)) | 
| 14 |  | id 22 | . . . . . 6
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) | 
| 15 | 13, 14 | oveq12d 7449 | . . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ·o 𝑥) +o 𝑥) = ((𝐴 ·o 𝑦) +o 𝑦)) | 
| 16 | 12, 15 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = 𝑦 → ((suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥) ↔ (suc 𝐴 ·o 𝑦) = ((𝐴 ·o 𝑦) +o 𝑦))) | 
| 17 |  | oveq2 7439 | . . . . 5
⊢ (𝑥 = suc 𝑦 → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o suc 𝑦)) | 
| 18 |  | oveq2 7439 | . . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦)) | 
| 19 |  | id 22 | . . . . . 6
⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦) | 
| 20 | 18, 19 | oveq12d 7449 | . . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o 𝑥) +o 𝑥) = ((𝐴 ·o suc 𝑦) +o suc 𝑦)) | 
| 21 | 17, 20 | eqeq12d 2753 | . . . 4
⊢ (𝑥 = suc 𝑦 → ((suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥) ↔ (suc 𝐴 ·o suc 𝑦) = ((𝐴 ·o suc 𝑦) +o suc 𝑦))) | 
| 22 |  | peano2 7912 | . . . . . . 7
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) | 
| 23 |  | nnm0 8643 | . . . . . . 7
⊢ (suc
𝐴 ∈ ω →
(suc 𝐴 ·o
∅) = ∅) | 
| 24 | 22, 23 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ ω → (suc
𝐴 ·o
∅) = ∅) | 
| 25 |  | nnm0 8643 | . . . . . 6
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) =
∅) | 
| 26 | 24, 25 | eqtr4d 2780 | . . . . 5
⊢ (𝐴 ∈ ω → (suc
𝐴 ·o
∅) = (𝐴
·o ∅)) | 
| 27 |  | peano1 7910 | . . . . . . 7
⊢ ∅
∈ ω | 
| 28 |  | nnmcl 8650 | . . . . . . 7
⊢ ((𝐴 ∈ ω ∧ ∅
∈ ω) → (𝐴
·o ∅) ∈ ω) | 
| 29 | 27, 28 | mpan2 691 | . . . . . 6
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅)
∈ ω) | 
| 30 |  | nna0 8642 | . . . . . 6
⊢ ((𝐴 ·o ∅)
∈ ω → ((𝐴
·o ∅) +o ∅) = (𝐴 ·o
∅)) | 
| 31 | 29, 30 | syl 17 | . . . . 5
⊢ (𝐴 ∈ ω → ((𝐴 ·o ∅)
+o ∅) = (𝐴
·o ∅)) | 
| 32 | 26, 31 | eqtr4d 2780 | . . . 4
⊢ (𝐴 ∈ ω → (suc
𝐴 ·o
∅) = ((𝐴
·o ∅) +o ∅)) | 
| 33 |  | oveq1 7438 | . . . . . 6
⊢ ((suc
𝐴 ·o
𝑦) = ((𝐴 ·o 𝑦) +o 𝑦) → ((suc 𝐴 ·o 𝑦) +o suc 𝐴) = (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴)) | 
| 34 |  | peano2b 7904 | . . . . . . . 8
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈
ω) | 
| 35 |  | nnmsuc 8645 | . . . . . . . 8
⊢ ((suc
𝐴 ∈ ω ∧
𝑦 ∈ ω) →
(suc 𝐴 ·o
suc 𝑦) = ((suc 𝐴 ·o 𝑦) +o suc 𝐴)) | 
| 36 | 34, 35 | sylanb 581 | . . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝐴 ·o suc
𝑦) = ((suc 𝐴 ·o 𝑦) +o suc 𝐴)) | 
| 37 |  | nnmcl 8650 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·o 𝑦) ∈
ω) | 
| 38 |  | peano2b 7904 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈
ω) | 
| 39 |  | nnaass 8660 | . . . . . . . . . . . 12
⊢ (((𝐴 ·o 𝑦) ∈ ω ∧ 𝐴 ∈ ω ∧ suc 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) | 
| 40 | 38, 39 | syl3an3b 1407 | . . . . . . . . . . 11
⊢ (((𝐴 ·o 𝑦) ∈ ω ∧ 𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) | 
| 41 | 37, 40 | syl3an1 1164 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) | 
| 42 | 41 | 3expb 1121 | . . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ (𝐴 ∈ ω ∧ 𝑦 ∈ ω)) →
(((𝐴 ·o
𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) | 
| 43 | 42 | anidms 566 | . . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) | 
| 44 |  | nnmsuc 8645 | . . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) | 
| 45 | 44 | oveq1d 7446 | . . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·o suc 𝑦) +o suc 𝑦) = (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦)) | 
| 46 |  | nnaass 8660 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ·o 𝑦) ∈ ω ∧ 𝑦 ∈ ω ∧ suc 𝐴 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) | 
| 47 | 34, 46 | syl3an3b 1407 | . . . . . . . . . . . . 13
⊢ (((𝐴 ·o 𝑦) ∈ ω ∧ 𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) | 
| 48 | 37, 47 | syl3an1 1164 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) | 
| 49 | 48 | 3expb 1121 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ω)) →
(((𝐴 ·o
𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) | 
| 50 | 49 | an42s 661 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ (𝐴 ∈ ω ∧ 𝑦 ∈ ω)) →
(((𝐴 ·o
𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) | 
| 51 | 50 | anidms 566 | . . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) | 
| 52 |  | nnacom 8655 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o 𝑦) = (𝑦 +o 𝐴)) | 
| 53 |  | suceq 6450 | . . . . . . . . . . . 12
⊢ ((𝐴 +o 𝑦) = (𝑦 +o 𝐴) → suc (𝐴 +o 𝑦) = suc (𝑦 +o 𝐴)) | 
| 54 | 52, 53 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝐴 +o 𝑦) = suc (𝑦 +o 𝐴)) | 
| 55 |  | nnasuc 8644 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o suc 𝑦) = suc (𝐴 +o 𝑦)) | 
| 56 |  | nnasuc 8644 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (𝑦 +o suc 𝐴) = suc (𝑦 +o 𝐴)) | 
| 57 | 56 | ancoms 458 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 +o suc 𝐴) = suc (𝑦 +o 𝐴)) | 
| 58 | 54, 55, 57 | 3eqtr4d 2787 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o suc 𝑦) = (𝑦 +o suc 𝐴)) | 
| 59 | 58 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦)) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) | 
| 60 | 51, 59 | eqtr4d 2780 | . . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) | 
| 61 | 43, 45, 60 | 3eqtr4d 2787 | . . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·o suc 𝑦) +o suc 𝑦) = (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴)) | 
| 62 | 36, 61 | eqeq12d 2753 | . . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((suc
𝐴 ·o suc
𝑦) = ((𝐴 ·o suc 𝑦) +o suc 𝑦) ↔ ((suc 𝐴 ·o 𝑦) +o suc 𝐴) = (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴))) | 
| 63 | 33, 62 | imbitrrid 246 | . . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((suc
𝐴 ·o
𝑦) = ((𝐴 ·o 𝑦) +o 𝑦) → (suc 𝐴 ·o suc 𝑦) = ((𝐴 ·o suc 𝑦) +o suc 𝑦))) | 
| 64 | 63 | expcom 413 | . . . 4
⊢ (𝑦 ∈ ω → (𝐴 ∈ ω → ((suc
𝐴 ·o
𝑦) = ((𝐴 ·o 𝑦) +o 𝑦) → (suc 𝐴 ·o suc 𝑦) = ((𝐴 ·o suc 𝑦) +o suc 𝑦)))) | 
| 65 | 11, 16, 21, 32, 64 | finds2 7920 | . . 3
⊢ (𝑥 ∈ ω → (𝐴 ∈ ω → (suc
𝐴 ·o
𝑥) = ((𝐴 ·o 𝑥) +o 𝑥))) | 
| 66 | 6, 65 | vtoclga 3577 | . 2
⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (suc
𝐴 ·o
𝐵) = ((𝐴 ·o 𝐵) +o 𝐵))) | 
| 67 | 66 | impcom 407 | 1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ·o
𝐵) = ((𝐴 ·o 𝐵) +o 𝐵)) |