Step | Hyp | Ref
| Expression |
1 | | oveq2 5520 |
. . . . . 6
⊢ (𝑥 = 𝐶 → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
𝐶)) |
2 | | oveq2 5520 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝐶)) |
3 | 2 | oveq2d 5528 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))) |
4 | 1, 3 | eqeq12d 2054 |
. . . . 5
⊢ (𝑥 = 𝐶 → (((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶)))) |
5 | 4 | imbi2d 219 |
. . . 4
⊢ (𝑥 = 𝐶 → (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))))) |
6 | | oveq2 5520 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
∅)) |
7 | | oveq2 5520 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐵 ·𝑜
𝑥) = (𝐵 ·𝑜
∅)) |
8 | 7 | oveq2d 5528 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·𝑜
(𝐵
·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
∅))) |
9 | 6, 8 | eqeq12d 2054 |
. . . . 5
⊢ (𝑥 = ∅ → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜
∅)))) |
10 | | oveq2 5520 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦)) |
11 | | oveq2 5520 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝑦)) |
12 | 11 | oveq2d 5528 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
13 | 10, 12 | eqeq12d 2054 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
14 | | oveq2 5520 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
suc 𝑦)) |
15 | | oveq2 5520 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 suc 𝑦)) |
16 | 15 | oveq2d 5528 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦))) |
17 | 14, 16 | eqeq12d 2054 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))) |
18 | | nnmcl 6060 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
𝐵) ∈
ω) |
19 | | nnm0 6054 |
. . . . . . 7
⊢ ((𝐴 ·𝑜
𝐵) ∈ ω →
((𝐴
·𝑜 𝐵) ·𝑜 ∅) =
∅) |
20 | 18, 19 | syl 14 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 ∅) = ∅) |
21 | | nnm0 6054 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → (𝐵 ·𝑜
∅) = ∅) |
22 | 21 | oveq2d 5528 |
. . . . . . 7
⊢ (𝐵 ∈ ω → (𝐴 ·𝑜
(𝐵
·𝑜 ∅)) = (𝐴 ·𝑜
∅)) |
23 | | nnm0 6054 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝐴 ·𝑜
∅) = ∅) |
24 | 22, 23 | sylan9eqr 2094 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
(𝐵
·𝑜 ∅)) = ∅) |
25 | 20, 24 | eqtr4d 2075 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜
∅))) |
26 | | oveq1 5519 |
. . . . . . . . 9
⊢ (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
27 | | nnmsuc 6056 |
. . . . . . . . . . . 12
⊢ (((𝐴 ·𝑜
𝐵) ∈ ω ∧
𝑦 ∈ ω) →
((𝐴
·𝑜 𝐵) ·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) +𝑜
(𝐴
·𝑜 𝐵))) |
28 | 18, 27 | sylan 267 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝑦 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) +𝑜
(𝐴
·𝑜 𝐵))) |
29 | 28 | 3impa 1099 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) +𝑜
(𝐴
·𝑜 𝐵))) |
30 | | nnmsuc 6056 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ·𝑜
suc 𝑦) = ((𝐵 ·𝑜
𝑦) +𝑜
𝐵)) |
31 | 30 | 3adant1 922 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ·𝑜
suc 𝑦) = ((𝐵 ·𝑜
𝑦) +𝑜
𝐵)) |
32 | 31 | oveq2d 5528 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜
(𝐵
·𝑜 suc 𝑦)) = (𝐴 ·𝑜 ((𝐵 ·𝑜
𝑦) +𝑜
𝐵))) |
33 | | nnmcl 6060 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ·𝑜
𝑦) ∈
ω) |
34 | | nndi 6065 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ ω ∧ (𝐵 ·𝑜
𝑦) ∈ ω ∧
𝐵 ∈ ω) →
(𝐴
·𝑜 ((𝐵 ·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
35 | 33, 34 | syl3an2 1169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ω ∧ (𝐵 ∈ ω ∧ 𝑦 ∈ ω) ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
36 | 35 | 3exp 1103 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ω → ((𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐵 ∈ ω → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))))) |
37 | 36 | expd 245 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (𝐵 ∈ ω → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵)))))) |
38 | 37 | com34 77 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵)))))) |
39 | 38 | pm2.43d 44 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))))) |
40 | 39 | 3imp 1098 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
41 | 32, 40 | eqtrd 2072 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ·𝑜
(𝐵
·𝑜 suc 𝑦)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
42 | 29, 41 | eqeq12d 2054 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)) ↔ (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵)))) |
43 | 26, 42 | syl5ibr 145 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝑦 ∈ ω) → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))) |
44 | 43 | 3exp 1103 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝑦 ∈ ω → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))))) |
45 | 44 | com3r 73 |
. . . . . 6
⊢ (𝑦 ∈ ω → (𝐴 ∈ ω → (𝐵 ∈ ω → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))))) |
46 | 45 | impd 242 |
. . . . 5
⊢ (𝑦 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦))))) |
47 | 9, 13, 17, 25, 46 | finds2 4324 |
. . . 4
⊢ (𝑥 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))) |
48 | 5, 47 | vtoclga 2619 |
. . 3
⊢ (𝐶 ∈ ω → ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶)))) |
49 | 48 | expdcom 1331 |
. 2
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐶 ∈ ω → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))))) |
50 | 49 | 3imp 1098 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))) |