Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝐵 → (suc 𝐴 ·𝑜 𝑥) = (suc 𝐴 ·𝑜 𝐵)) |
2 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 𝐵)) |
3 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
4 | 2, 3 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((𝐴 ·𝑜 𝑥) +𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐵)) |
5 | 1, 4 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝐵 → ((suc 𝐴 ·𝑜 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝑥) ↔ (suc 𝐴 ·𝑜 𝐵) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐵))) |
6 | 5 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐴 ∈ ω → (suc 𝐴 ·𝑜
𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝑥)) ↔ (𝐴 ∈ ω → (suc 𝐴 ·𝑜
𝐵) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐵)))) |
7 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = ∅ → (suc 𝐴 ·𝑜
𝑥) = (suc 𝐴 ·𝑜
∅)) |
8 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·𝑜
𝑥) = (𝐴 ·𝑜
∅)) |
9 | | id 22 |
. . . . . 6
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
10 | 8, 9 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ·𝑜
𝑥) +𝑜
𝑥) = ((𝐴 ·𝑜 ∅)
+𝑜 ∅)) |
11 | 7, 10 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = ∅ → ((suc 𝐴 ·𝑜
𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝑥) ↔ (suc 𝐴 ·𝑜 ∅) =
((𝐴
·𝑜 ∅) +𝑜
∅))) |
12 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝑦 → (suc 𝐴 ·𝑜 𝑥) = (suc 𝐴 ·𝑜 𝑦)) |
13 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 𝑦)) |
14 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝑦 → 𝑥 = 𝑦) |
15 | 13, 14 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ·𝑜 𝑥) +𝑜 𝑥) = ((𝐴 ·𝑜 𝑦) +𝑜 𝑦)) |
16 | 12, 15 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝑦 → ((suc 𝐴 ·𝑜 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝑥) ↔ (suc 𝐴 ·𝑜 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 𝑦))) |
17 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (suc 𝐴 ·𝑜 𝑥) = (suc 𝐴 ·𝑜 suc 𝑦)) |
18 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 suc 𝑦)) |
19 | | id 22 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → 𝑥 = suc 𝑦) |
20 | 18, 19 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 𝑥) +𝑜 𝑥) = ((𝐴 ·𝑜 suc 𝑦) +𝑜 suc
𝑦)) |
21 | 17, 20 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((suc 𝐴 ·𝑜 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝑥) ↔ (suc 𝐴 ·𝑜 suc 𝑦) = ((𝐴 ·𝑜 suc 𝑦) +𝑜 suc
𝑦))) |
22 | | peano2 7086 |
. . . . . . 7
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
23 | | nnm0 7685 |
. . . . . . 7
⊢ (suc
𝐴 ∈ ω →
(suc 𝐴
·𝑜 ∅) = ∅) |
24 | 22, 23 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω → (suc
𝐴
·𝑜 ∅) = ∅) |
25 | | nnm0 7685 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝐴 ·𝑜
∅) = ∅) |
26 | 24, 25 | eqtr4d 2659 |
. . . . 5
⊢ (𝐴 ∈ ω → (suc
𝐴
·𝑜 ∅) = (𝐴 ·𝑜
∅)) |
27 | | peano1 7085 |
. . . . . . 7
⊢ ∅
∈ ω |
28 | | nnmcl 7692 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ ∅
∈ ω) → (𝐴
·𝑜 ∅) ∈ ω) |
29 | 27, 28 | mpan2 707 |
. . . . . 6
⊢ (𝐴 ∈ ω → (𝐴 ·𝑜
∅) ∈ ω) |
30 | | nna0 7684 |
. . . . . 6
⊢ ((𝐴 ·𝑜
∅) ∈ ω → ((𝐴 ·𝑜 ∅)
+𝑜 ∅) = (𝐴 ·𝑜
∅)) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ω → ((𝐴 ·𝑜
∅) +𝑜 ∅) = (𝐴 ·𝑜
∅)) |
32 | 26, 31 | eqtr4d 2659 |
. . . 4
⊢ (𝐴 ∈ ω → (suc
𝐴
·𝑜 ∅) = ((𝐴 ·𝑜 ∅)
+𝑜 ∅)) |
33 | | oveq1 6657 |
. . . . . 6
⊢ ((suc
𝐴
·𝑜 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 𝑦) → ((suc 𝐴 ·𝑜 𝑦) +𝑜 suc
𝐴) = (((𝐴 ·𝑜 𝑦) +𝑜 𝑦) +𝑜 suc
𝐴)) |
34 | | peano2b 7081 |
. . . . . . . 8
⊢ (𝐴 ∈ ω ↔ suc 𝐴 ∈
ω) |
35 | | nnmsuc 7687 |
. . . . . . . 8
⊢ ((suc
𝐴 ∈ ω ∧
𝑦 ∈ ω) →
(suc 𝐴
·𝑜 suc 𝑦) = ((suc 𝐴 ·𝑜 𝑦) +𝑜 suc
𝐴)) |
36 | 34, 35 | sylanb 489 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (suc
𝐴
·𝑜 suc 𝑦) = ((suc 𝐴 ·𝑜 𝑦) +𝑜 suc
𝐴)) |
37 | | nnmcl 7692 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜
𝑦) ∈
ω) |
38 | | peano2b 7081 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈
ω) |
39 | | nnaass 7702 |
. . . . . . . . . . . 12
⊢ (((𝐴 ·𝑜
𝑦) ∈ ω ∧
𝐴 ∈ ω ∧ suc
𝑦 ∈ ω) →
(((𝐴
·𝑜 𝑦) +𝑜 𝐴) +𝑜 suc 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 (𝐴 +𝑜 suc 𝑦))) |
40 | 38, 39 | syl3an3b 1364 |
. . . . . . . . . . 11
⊢ (((𝐴 ·𝑜
𝑦) ∈ ω ∧
𝐴 ∈ ω ∧
𝑦 ∈ ω) →
(((𝐴
·𝑜 𝑦) +𝑜 𝐴) +𝑜 suc 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 (𝐴 +𝑜 suc 𝑦))) |
41 | 37, 40 | syl3an1 1359 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜
𝑦) +𝑜
𝐴) +𝑜
suc 𝑦) = ((𝐴 ·𝑜
𝑦) +𝑜
(𝐴 +𝑜
suc 𝑦))) |
42 | 41 | 3expb 1266 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ (𝐴 ∈ ω ∧ 𝑦 ∈ ω)) →
(((𝐴
·𝑜 𝑦) +𝑜 𝐴) +𝑜 suc 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 (𝐴 +𝑜 suc 𝑦))) |
43 | 42 | anidms 677 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜
𝑦) +𝑜
𝐴) +𝑜
suc 𝑦) = ((𝐴 ·𝑜
𝑦) +𝑜
(𝐴 +𝑜
suc 𝑦))) |
44 | | nnmsuc 7687 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜
suc 𝑦) = ((𝐴 ·𝑜
𝑦) +𝑜
𝐴)) |
45 | 44 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·𝑜
suc 𝑦)
+𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝑦) +𝑜 𝐴) +𝑜 suc
𝑦)) |
46 | | nnaass 7702 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ·𝑜
𝑦) ∈ ω ∧
𝑦 ∈ ω ∧ suc
𝐴 ∈ ω) →
(((𝐴
·𝑜 𝑦) +𝑜 𝑦) +𝑜 suc 𝐴) = ((𝐴 ·𝑜 𝑦) +𝑜 (𝑦 +𝑜 suc 𝐴))) |
47 | 34, 46 | syl3an3b 1364 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ·𝑜
𝑦) ∈ ω ∧
𝑦 ∈ ω ∧
𝐴 ∈ ω) →
(((𝐴
·𝑜 𝑦) +𝑜 𝑦) +𝑜 suc 𝐴) = ((𝐴 ·𝑜 𝑦) +𝑜 (𝑦 +𝑜 suc 𝐴))) |
48 | 37, 47 | syl3an1 1359 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (((𝐴 ·𝑜
𝑦) +𝑜
𝑦) +𝑜
suc 𝐴) = ((𝐴 ·𝑜
𝑦) +𝑜
(𝑦 +𝑜
suc 𝐴))) |
49 | 48 | 3expb 1266 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ (𝑦 ∈ ω ∧ 𝐴 ∈ ω)) →
(((𝐴
·𝑜 𝑦) +𝑜 𝑦) +𝑜 suc 𝐴) = ((𝐴 ·𝑜 𝑦) +𝑜 (𝑦 +𝑜 suc 𝐴))) |
50 | 49 | an42s 870 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝑦 ∈ ω) ∧ (𝐴 ∈ ω ∧ 𝑦 ∈ ω)) →
(((𝐴
·𝑜 𝑦) +𝑜 𝑦) +𝑜 suc 𝐴) = ((𝐴 ·𝑜 𝑦) +𝑜 (𝑦 +𝑜 suc 𝐴))) |
51 | 50 | anidms 677 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜
𝑦) +𝑜
𝑦) +𝑜
suc 𝐴) = ((𝐴 ·𝑜
𝑦) +𝑜
(𝑦 +𝑜
suc 𝐴))) |
52 | | nnacom 7697 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 𝑦) = (𝑦 +𝑜 𝐴)) |
53 | | suceq 5790 |
. . . . . . . . . . . 12
⊢ ((𝐴 +𝑜 𝑦) = (𝑦 +𝑜 𝐴) → suc (𝐴 +𝑜 𝑦) = suc (𝑦 +𝑜 𝐴)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → suc
(𝐴 +𝑜
𝑦) = suc (𝑦 +𝑜 𝐴)) |
55 | | nnasuc 7686 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 suc 𝑦) = suc (𝐴 +𝑜 𝑦)) |
56 | | nnasuc 7686 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ 𝐴 ∈ ω) → (𝑦 +𝑜 suc 𝐴) = suc (𝑦 +𝑜 𝐴)) |
57 | 56 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 +𝑜 suc 𝐴) = suc (𝑦 +𝑜 𝐴)) |
58 | 54, 55, 57 | 3eqtr4d 2666 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 +𝑜 suc 𝑦) = (𝑦 +𝑜 suc 𝐴)) |
59 | 58 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·𝑜
𝑦) +𝑜
(𝐴 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
𝑦) +𝑜
(𝑦 +𝑜
suc 𝐴))) |
60 | 51, 59 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜
𝑦) +𝑜
𝑦) +𝑜
suc 𝐴) = ((𝐴 ·𝑜
𝑦) +𝑜
(𝐴 +𝑜
suc 𝑦))) |
61 | 43, 45, 60 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·𝑜
suc 𝑦)
+𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝑦) +𝑜 𝑦) +𝑜 suc
𝐴)) |
62 | 36, 61 | eqeq12d 2637 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((suc
𝐴
·𝑜 suc 𝑦) = ((𝐴 ·𝑜 suc 𝑦) +𝑜 suc
𝑦) ↔ ((suc 𝐴 ·𝑜
𝑦) +𝑜
suc 𝐴) = (((𝐴 ·𝑜
𝑦) +𝑜
𝑦) +𝑜
suc 𝐴))) |
63 | 33, 62 | syl5ibr 236 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → ((suc
𝐴
·𝑜 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 𝑦) → (suc 𝐴 ·𝑜 suc 𝑦) = ((𝐴 ·𝑜 suc 𝑦) +𝑜 suc
𝑦))) |
64 | 63 | expcom 451 |
. . . 4
⊢ (𝑦 ∈ ω → (𝐴 ∈ ω → ((suc
𝐴
·𝑜 𝑦) = ((𝐴 ·𝑜 𝑦) +𝑜 𝑦) → (suc 𝐴 ·𝑜 suc 𝑦) = ((𝐴 ·𝑜 suc 𝑦) +𝑜 suc
𝑦)))) |
65 | 11, 16, 21, 32, 64 | finds2 7094 |
. . 3
⊢ (𝑥 ∈ ω → (𝐴 ∈ ω → (suc
𝐴
·𝑜 𝑥) = ((𝐴 ·𝑜 𝑥) +𝑜 𝑥))) |
66 | 6, 65 | vtoclga 3272 |
. 2
⊢ (𝐵 ∈ ω → (𝐴 ∈ ω → (suc
𝐴
·𝑜 𝐵) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐵))) |
67 | 66 | impcom 446 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
𝐴
·𝑜 𝐵) = ((𝐴 ·𝑜 𝐵) +𝑜 𝐵)) |