Step | Hyp | Ref
| Expression |
1 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = 𝐵 → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o 𝐵)) |
2 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝐵)) |
3 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
4 | 2, 3 | oveq12d 7231 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((𝐴 ·o 𝑥) +o 𝑥) = ((𝐴 ·o 𝐵) +o 𝐵)) |
5 | 1, 4 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝐵 → ((suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥) ↔ (suc 𝐴 ·o 𝐵) = ((𝐴 ·o 𝐵) +o 𝐵))) |
6 | 5 | imbi2d 344 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ω → (suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥)) ↔ (𝐴 ∈ ω → (suc 𝐴 ·o 𝐵) = ((𝐴 ·o 𝐵) +o 𝐵)))) |
7 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = ∅ → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o
∅)) |
8 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o
∅)) |
9 | | id 22 |
. . . . . 6
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
10 | 8, 9 | oveq12d 7231 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ·o 𝑥) +o 𝑥) = ((𝐴 ·o ∅) +o
∅)) |
11 | 7, 10 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = ∅ → ((suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥) ↔ (suc 𝐴 ·o ∅) = ((𝐴 ·o ∅)
+o ∅))) |
12 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = 𝑦 → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o 𝑦)) |
13 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦)) |
14 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
15 | 13, 14 | oveq12d 7231 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ·o 𝑥) +o 𝑥) = ((𝐴 ·o 𝑦) +o 𝑦)) |
16 | 12, 15 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑦 → ((suc 𝐴 ·o 𝑥) = ((𝐴 ·o 𝑥) +o 𝑥) ↔ (suc 𝐴 ·o 𝑦) = ((𝐴 ·o 𝑦) +o 𝑦))) |
17 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (suc 𝐴 ·o 𝑥) = (suc 𝐴 ·o suc 𝑦)) |
18 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦)) |
19 | | id 22 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦) |
20 | 18, 19 | oveq12d 7231 |
. . . . 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 7668 |
. . . . . . 7
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
23 | | nnm0 8333 |
. . . . . . 7
⊢ (suc
𝐴 ∈ ω →
(suc 𝐴 ·o
∅) = ∅) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω → (suc
𝐴 ·o
∅) = ∅) |
25 | | nnm0 8333 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) =
∅) |
26 | 24, 25 | eqtr4d 2780 |
. . . . 5
⊢ (𝐴 ∈ ω → (suc
𝐴 ·o
∅) = (𝐴
·o ∅)) |
27 | | peano1 7667 |
. . . . . . 7
⊢ ∅
∈ ω |
28 | | nnmcl 8340 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ ∅
∈ ω) → (𝐴
·o ∅) ∈ ω) |
29 | 27, 28 | mpan2 691 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅)
∈ ω) |
30 | | nna0 8332 |
. . . . . 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 7220 |
. . . . . 6
⊢ ((suc
𝐴 ·o
𝑦) = ((𝐴 ·o 𝑦) +o 𝑦) → ((suc 𝐴 ·o 𝑦) +o suc 𝐴) = (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴)) |
34 | | peano2b 7661 |
. . . . . . . 8
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈
ω) |
35 | | nnmsuc 8335 |
. . . . . . . 8
⊢ ((suc
𝐴 ∈ ω ∧
𝑦 ∈ ω) →
(suc 𝐴 ·o
suc 𝑦) = ((suc 𝐴 ·o 𝑦) +o suc 𝐴)) |
36 | 34, 35 | sylanb 584 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝐴 ·o suc
𝑦) = ((suc 𝐴 ·o 𝑦) +o suc 𝐴)) |
37 | | nnmcl 8340 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·o 𝑦) ∈
ω) |
38 | | peano2b 7661 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈
ω) |
39 | | nnaass 8350 |
. . . . . . . . . . . 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 1165 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) |
42 | 41 | 3expb 1122 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ (𝐴 ∈ ω ∧ 𝑦 ∈ ω)) →
(((𝐴 ·o
𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) |
43 | 42 | anidms 570 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦) = ((𝐴 ·o 𝑦) +o (𝐴 +o suc 𝑦))) |
44 | | nnmsuc 8335 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
45 | 44 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·o suc 𝑦) +o suc 𝑦) = (((𝐴 ·o 𝑦) +o 𝐴) +o suc 𝑦)) |
46 | | nnaass 8350 |
. . . . . . . . . . . . . 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 1165 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) |
49 | 48 | 3expb 1122 |
. . . . . . . . . . 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 570 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·o 𝑦) +o 𝑦) +o suc 𝐴) = ((𝐴 ·o 𝑦) +o (𝑦 +o suc 𝐴))) |
52 | | nnacom 8345 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o 𝑦) = (𝑦 +o 𝐴)) |
53 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ ((𝐴 +o 𝑦) = (𝑦 +o 𝐴) → suc (𝐴 +o 𝑦) = suc (𝑦 +o 𝐴)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝐴 +o 𝑦) = suc (𝑦 +o 𝐴)) |
55 | | nnasuc 8334 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o suc 𝑦) = suc (𝐴 +o 𝑦)) |
56 | | nnasuc 8334 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (𝑦 +o suc 𝐴) = suc (𝑦 +o 𝐴)) |
57 | 56 | ancoms 462 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 +o suc 𝐴) = suc (𝑦 +o 𝐴)) |
58 | 54, 55, 57 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +o suc 𝑦) = (𝑦 +o suc 𝐴)) |
59 | 58 | oveq2d 7229 |
. . . . . . . . 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 | syl5ibr 249 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((suc
𝐴 ·o
𝑦) = ((𝐴 ·o 𝑦) +o 𝑦) → (suc 𝐴 ·o suc 𝑦) = ((𝐴 ·o suc 𝑦) +o suc 𝑦))) |
64 | 63 | expcom 417 |
. . . 4
⊢ (𝑦 ∈ ω → (𝐴 ∈ ω → ((suc
𝐴 ·o
𝑦) = ((𝐴 ·o 𝑦) +o 𝑦) → (suc 𝐴 ·o suc 𝑦) = ((𝐴 ·o suc 𝑦) +o suc 𝑦)))) |
65 | 11, 16, 21, 32, 64 | finds2 7678 |
. . 3
⊢ (𝑥 ∈ ω → (𝐴 ∈ ω → (suc
𝐴 ·o
𝑥) = ((𝐴 ·o 𝑥) +o 𝑥))) |
66 | 6, 65 | vtoclga 3489 |
. 2
⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (suc
𝐴 ·o
𝐵) = ((𝐴 ·o 𝐵) +o 𝐵))) |
67 | 66 | impcom 411 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴 ·o
𝐵) = ((𝐴 ·o 𝐵) +o 𝐵)) |