Proof of Theorem omopthlem1
Step | Hyp | Ref
| Expression |
1 | | omopthlem1.1 |
. . . . 5
⊢ 𝐴 ∈ ω |
2 | | peano2 7086 |
. . . . 5
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ suc 𝐴 ∈ ω |
4 | | omopthlem1.2 |
. . . 4
⊢ 𝐶 ∈ ω |
5 | | nnmwordi 7715 |
. . . 4
⊢ ((suc
𝐴 ∈ ω ∧
𝐶 ∈ ω ∧ suc
𝐴 ∈ ω) →
(suc 𝐴 ⊆ 𝐶 → (suc 𝐴 ·𝑜 suc 𝐴) ⊆ (suc 𝐴 ·𝑜 𝐶))) |
6 | 3, 4, 3, 5 | mp3an 1424 |
. . 3
⊢ (suc
𝐴 ⊆ 𝐶 → (suc 𝐴 ·𝑜 suc 𝐴) ⊆ (suc 𝐴 ·𝑜 𝐶)) |
7 | | nnmwordri 7716 |
. . . 4
⊢ ((suc
𝐴 ∈ ω ∧
𝐶 ∈ ω ∧
𝐶 ∈ ω) →
(suc 𝐴 ⊆ 𝐶 → (suc 𝐴 ·𝑜 𝐶) ⊆ (𝐶 ·𝑜 𝐶))) |
8 | 3, 4, 4, 7 | mp3an 1424 |
. . 3
⊢ (suc
𝐴 ⊆ 𝐶 → (suc 𝐴 ·𝑜 𝐶) ⊆ (𝐶 ·𝑜 𝐶)) |
9 | 6, 8 | sstrd 3613 |
. 2
⊢ (suc
𝐴 ⊆ 𝐶 → (suc 𝐴 ·𝑜 suc 𝐴) ⊆ (𝐶 ·𝑜 𝐶)) |
10 | 1 | nnoni 7072 |
. . 3
⊢ 𝐴 ∈ On |
11 | 4 | nnoni 7072 |
. . 3
⊢ 𝐶 ∈ On |
12 | 10, 11 | onsucssi 7041 |
. 2
⊢ (𝐴 ∈ 𝐶 ↔ suc 𝐴 ⊆ 𝐶) |
13 | 1, 1 | nnmcli 7695 |
. . . . . 6
⊢ (𝐴 ·𝑜
𝐴) ∈
ω |
14 | | 2onn 7720 |
. . . . . . 7
⊢
2𝑜 ∈ ω |
15 | 1, 14 | nnmcli 7695 |
. . . . . 6
⊢ (𝐴 ·𝑜
2𝑜) ∈ ω |
16 | 13, 15 | nnacli 7694 |
. . . . 5
⊢ ((𝐴 ·𝑜
𝐴) +𝑜
(𝐴
·𝑜 2𝑜)) ∈
ω |
17 | 16 | nnoni 7072 |
. . . 4
⊢ ((𝐴 ·𝑜
𝐴) +𝑜
(𝐴
·𝑜 2𝑜)) ∈ On |
18 | 4, 4 | nnmcli 7695 |
. . . . 5
⊢ (𝐶 ·𝑜
𝐶) ∈
ω |
19 | 18 | nnoni 7072 |
. . . 4
⊢ (𝐶 ·𝑜
𝐶) ∈
On |
20 | 17, 19 | onsucssi 7041 |
. . 3
⊢ (((𝐴 ·𝑜
𝐴) +𝑜
(𝐴
·𝑜 2𝑜)) ∈ (𝐶 ·𝑜 𝐶) ↔ suc ((𝐴 ·𝑜 𝐴) +𝑜 (𝐴 ·𝑜
2𝑜)) ⊆ (𝐶 ·𝑜 𝐶)) |
21 | 3, 1 | nnmcli 7695 |
. . . . . 6
⊢ (suc
𝐴
·𝑜 𝐴) ∈ ω |
22 | | nnasuc 7686 |
. . . . . 6
⊢ (((suc
𝐴
·𝑜 𝐴) ∈ ω ∧ 𝐴 ∈ ω) → ((suc 𝐴 ·𝑜
𝐴) +𝑜
suc 𝐴) = suc ((suc 𝐴 ·𝑜
𝐴) +𝑜
𝐴)) |
23 | 21, 1, 22 | mp2an 708 |
. . . . 5
⊢ ((suc
𝐴
·𝑜 𝐴) +𝑜 suc 𝐴) = suc ((suc 𝐴 ·𝑜 𝐴) +𝑜 𝐴) |
24 | | nnmsuc 7687 |
. . . . . 6
⊢ ((suc
𝐴 ∈ ω ∧
𝐴 ∈ ω) →
(suc 𝐴
·𝑜 suc 𝐴) = ((suc 𝐴 ·𝑜 𝐴) +𝑜 suc
𝐴)) |
25 | 3, 1, 24 | mp2an 708 |
. . . . 5
⊢ (suc
𝐴
·𝑜 suc 𝐴) = ((suc 𝐴 ·𝑜 𝐴) +𝑜 suc
𝐴) |
26 | | nnaass 7702 |
. . . . . . . 8
⊢ (((𝐴 ·𝑜
𝐴) ∈ ω ∧
𝐴 ∈ ω ∧
𝐴 ∈ ω) →
(((𝐴
·𝑜 𝐴) +𝑜 𝐴) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐴) +𝑜 (𝐴 +𝑜 𝐴))) |
27 | 13, 1, 1, 26 | mp3an 1424 |
. . . . . . 7
⊢ (((𝐴 ·𝑜
𝐴) +𝑜
𝐴) +𝑜
𝐴) = ((𝐴 ·𝑜 𝐴) +𝑜 (𝐴 +𝑜 𝐴)) |
28 | | nnmcom 7706 |
. . . . . . . . . 10
⊢ ((suc
𝐴 ∈ ω ∧
𝐴 ∈ ω) →
(suc 𝐴
·𝑜 𝐴) = (𝐴 ·𝑜 suc 𝐴)) |
29 | 3, 1, 28 | mp2an 708 |
. . . . . . . . 9
⊢ (suc
𝐴
·𝑜 𝐴) = (𝐴 ·𝑜 suc 𝐴) |
30 | | nnmsuc 7687 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝐴 ∈ ω) → (𝐴 ·𝑜
suc 𝐴) = ((𝐴 ·𝑜
𝐴) +𝑜
𝐴)) |
31 | 1, 1, 30 | mp2an 708 |
. . . . . . . . 9
⊢ (𝐴 ·𝑜
suc 𝐴) = ((𝐴 ·𝑜
𝐴) +𝑜
𝐴) |
32 | 29, 31 | eqtri 2644 |
. . . . . . . 8
⊢ (suc
𝐴
·𝑜 𝐴) = ((𝐴 ·𝑜 𝐴) +𝑜 𝐴) |
33 | 32 | oveq1i 6660 |
. . . . . . 7
⊢ ((suc
𝐴
·𝑜 𝐴) +𝑜 𝐴) = (((𝐴 ·𝑜 𝐴) +𝑜 𝐴) +𝑜 𝐴) |
34 | | nnm2 7729 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → (𝐴 ·𝑜
2𝑜) = (𝐴
+𝑜 𝐴)) |
35 | 1, 34 | ax-mp 5 |
. . . . . . . 8
⊢ (𝐴 ·𝑜
2𝑜) = (𝐴
+𝑜 𝐴) |
36 | 35 | oveq2i 6661 |
. . . . . . 7
⊢ ((𝐴 ·𝑜
𝐴) +𝑜
(𝐴
·𝑜 2𝑜)) = ((𝐴 ·𝑜 𝐴) +𝑜 (𝐴 +𝑜 𝐴)) |
37 | 27, 33, 36 | 3eqtr4ri 2655 |
. . . . . 6
⊢ ((𝐴 ·𝑜
𝐴) +𝑜
(𝐴
·𝑜 2𝑜)) = ((suc 𝐴 ·𝑜 𝐴) +𝑜 𝐴) |
38 | | suceq 5790 |
. . . . . 6
⊢ (((𝐴 ·𝑜
𝐴) +𝑜
(𝐴
·𝑜 2𝑜)) = ((suc 𝐴 ·𝑜 𝐴) +𝑜 𝐴) → suc ((𝐴 ·𝑜 𝐴) +𝑜 (𝐴 ·𝑜
2𝑜)) = suc ((suc 𝐴 ·𝑜 𝐴) +𝑜 𝐴)) |
39 | 37, 38 | ax-mp 5 |
. . . . 5
⊢ suc
((𝐴
·𝑜 𝐴) +𝑜 (𝐴 ·𝑜
2𝑜)) = suc ((suc 𝐴 ·𝑜 𝐴) +𝑜 𝐴) |
40 | 23, 25, 39 | 3eqtr4ri 2655 |
. . . 4
⊢ suc
((𝐴
·𝑜 𝐴) +𝑜 (𝐴 ·𝑜
2𝑜)) = (suc 𝐴 ·𝑜 suc 𝐴) |
41 | 40 | sseq1i 3629 |
. . 3
⊢ (suc
((𝐴
·𝑜 𝐴) +𝑜 (𝐴 ·𝑜
2𝑜)) ⊆ (𝐶 ·𝑜 𝐶) ↔ (suc 𝐴 ·𝑜 suc 𝐴) ⊆ (𝐶 ·𝑜 𝐶)) |
42 | 20, 41 | bitri 264 |
. 2
⊢ (((𝐴 ·𝑜
𝐴) +𝑜
(𝐴
·𝑜 2𝑜)) ∈ (𝐶 ·𝑜 𝐶) ↔ (suc 𝐴 ·𝑜 suc 𝐴) ⊆ (𝐶 ·𝑜 𝐶)) |
43 | 9, 12, 42 | 3imtr4i 281 |
1
⊢ (𝐴 ∈ 𝐶 → ((𝐴 ·𝑜 𝐴) +𝑜 (𝐴 ·𝑜
2𝑜)) ∈ (𝐶 ·𝑜 𝐶)) |