Proof of Theorem omopthlem2
Step | Hyp | Ref
| Expression |
1 | | omopthlem2.3 |
. . . . . . 7
⊢ 𝐶 ∈ ω |
2 | 1, 1 | nnmcli 7582 |
. . . . . 6
⊢ (𝐶 ·𝑜
𝐶) ∈
ω |
3 | | omopthlem2.4 |
. . . . . 6
⊢ 𝐷 ∈ ω |
4 | 2, 3 | nnacli 7581 |
. . . . 5
⊢ ((𝐶 ·𝑜
𝐶) +𝑜
𝐷) ∈
ω |
5 | 4 | nnoni 6964 |
. . . 4
⊢ ((𝐶 ·𝑜
𝐶) +𝑜
𝐷) ∈
On |
6 | 5 | onirri 5751 |
. . 3
⊢ ¬
((𝐶
·𝑜 𝐶) +𝑜 𝐷) ∈ ((𝐶 ·𝑜 𝐶) +𝑜 𝐷) |
7 | | eleq1 2676 |
. . 3
⊢ (((𝐶 ·𝑜
𝐶) +𝑜
𝐷) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) → (((𝐶 ·𝑜 𝐶) +𝑜 𝐷) ∈ ((𝐶 ·𝑜 𝐶) +𝑜 𝐷) ↔ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ∈ ((𝐶 ·𝑜 𝐶) +𝑜 𝐷))) |
8 | 6, 7 | mtbii 315 |
. 2
⊢ (((𝐶 ·𝑜
𝐶) +𝑜
𝐷) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) → ¬ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) ∈ ((𝐶 ·𝑜
𝐶) +𝑜
𝐷)) |
9 | | nnaword1 7596 |
. . . 4
⊢ (((𝐶 ·𝑜
𝐶) ∈ ω ∧
𝐷 ∈ ω) →
(𝐶
·𝑜 𝐶) ⊆ ((𝐶 ·𝑜 𝐶) +𝑜 𝐷)) |
10 | 2, 3, 9 | mp2an 704 |
. . 3
⊢ (𝐶 ·𝑜
𝐶) ⊆ ((𝐶 ·𝑜
𝐶) +𝑜
𝐷) |
11 | | omopthlem2.2 |
. . . . . . . . 9
⊢ 𝐵 ∈ ω |
12 | | omopthlem2.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ ω |
13 | 12, 11 | nnacli 7581 |
. . . . . . . . . 10
⊢ (𝐴 +𝑜 𝐵) ∈
ω |
14 | 13, 12 | nnacli 7581 |
. . . . . . . . 9
⊢ ((𝐴 +𝑜 𝐵) +𝑜 𝐴) ∈
ω |
15 | | nnaword1 7596 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ ((𝐴 +𝑜 𝐵) +𝑜 𝐴) ∈ ω) → 𝐵 ⊆ (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) +𝑜 𝐴))) |
16 | 11, 14, 15 | mp2an 704 |
. . . . . . . 8
⊢ 𝐵 ⊆ (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) +𝑜 𝐴)) |
17 | | nnacom 7584 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ ((𝐴 +𝑜 𝐵) +𝑜 𝐴) ∈ ω) → (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) +𝑜 𝐴)) = (((𝐴 +𝑜 𝐵) +𝑜 𝐴) +𝑜 𝐵)) |
18 | 11, 14, 17 | mp2an 704 |
. . . . . . . 8
⊢ (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) +𝑜 𝐴)) = (((𝐴 +𝑜 𝐵) +𝑜 𝐴) +𝑜 𝐵) |
19 | 16, 18 | sseqtri 3600 |
. . . . . . 7
⊢ 𝐵 ⊆ (((𝐴 +𝑜 𝐵) +𝑜 𝐴) +𝑜 𝐵) |
20 | | nnaass 7589 |
. . . . . . . . 9
⊢ (((𝐴 +𝑜 𝐵) ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (((𝐴 +𝑜 𝐵) +𝑜 𝐴) +𝑜 𝐵) = ((𝐴 +𝑜 𝐵) +𝑜 (𝐴 +𝑜 𝐵))) |
21 | 13, 12, 11, 20 | mp3an 1416 |
. . . . . . . 8
⊢ (((𝐴 +𝑜 𝐵) +𝑜 𝐴) +𝑜 𝐵) = ((𝐴 +𝑜 𝐵) +𝑜 (𝐴 +𝑜 𝐵)) |
22 | | nnm2 7616 |
. . . . . . . . 9
⊢ ((𝐴 +𝑜 𝐵) ∈ ω → ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) = ((𝐴 +𝑜 𝐵) +𝑜 (𝐴 +𝑜 𝐵))) |
23 | 13, 22 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) = ((𝐴 +𝑜 𝐵) +𝑜 (𝐴 +𝑜 𝐵)) |
24 | 21, 23 | eqtr4i 2635 |
. . . . . . 7
⊢ (((𝐴 +𝑜 𝐵) +𝑜 𝐴) +𝑜 𝐵) = ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) |
25 | 19, 24 | sseqtri 3600 |
. . . . . 6
⊢ 𝐵 ⊆ ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) |
26 | | 2onn 7607 |
. . . . . . . 8
⊢
2𝑜 ∈ ω |
27 | 13, 26 | nnmcli 7582 |
. . . . . . 7
⊢ ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) ∈ ω |
28 | 13, 13 | nnmcli 7582 |
. . . . . . 7
⊢ ((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) ∈
ω |
29 | | nnawordi 7588 |
. . . . . . 7
⊢ ((𝐵 ∈ ω ∧ ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) ∈ ω ∧ ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) ∈ ω) → (𝐵 ⊆ ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) → (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵))) ⊆ (((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵))))) |
30 | 11, 27, 28, 29 | mp3an 1416 |
. . . . . 6
⊢ (𝐵 ⊆ ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) → (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵))) ⊆ (((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)))) |
31 | 25, 30 | ax-mp 5 |
. . . . 5
⊢ (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵))) ⊆ (((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵))) |
32 | | nnacom 7584 |
. . . . . 6
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) ∈ ω ∧
𝐵 ∈ ω) →
(((𝐴 +𝑜
𝐵)
·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)))) |
33 | 28, 11, 32 | mp2an 704 |
. . . . 5
⊢ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (𝐵 +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵))) |
34 | | nnacom 7584 |
. . . . . 6
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) ∈ ω ∧
((𝐴 +𝑜
𝐵)
·𝑜 2𝑜) ∈ ω) →
(((𝐴 +𝑜
𝐵)
·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜)) = (((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)))) |
35 | 28, 27, 34 | mp2an 704 |
. . . . 5
⊢ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
((𝐴 +𝑜
𝐵)
·𝑜 2𝑜)) = (((𝐴 +𝑜 𝐵) ·𝑜
2𝑜) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵))) |
36 | 31, 33, 35 | 3sstr4i 3607 |
. . . 4
⊢ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) ⊆ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
((𝐴 +𝑜
𝐵)
·𝑜 2𝑜)) |
37 | 13, 1 | omopthlem1 7622 |
. . . 4
⊢ ((𝐴 +𝑜 𝐵) ∈ 𝐶 → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜)) ∈ (𝐶 ·𝑜 𝐶)) |
38 | 28, 11 | nnacli 7581 |
. . . . . 6
⊢ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) ∈
ω |
39 | 38 | nnoni 6964 |
. . . . 5
⊢ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) ∈
On |
40 | 2 | nnoni 6964 |
. . . . 5
⊢ (𝐶 ·𝑜
𝐶) ∈
On |
41 | | ontr2 5689 |
. . . . 5
⊢
(((((𝐴
+𝑜 𝐵)
·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ∈ On ∧ (𝐶 ·𝑜 𝐶) ∈ On) → (((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) ⊆ (((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
((𝐴 +𝑜
𝐵)
·𝑜 2𝑜)) ∧ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜)) ∈ (𝐶 ·𝑜 𝐶)) → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐶))) |
42 | 39, 40, 41 | mp2an 704 |
. . . 4
⊢
(((((𝐴
+𝑜 𝐵)
·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ⊆ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜)) ∧ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 ((𝐴 +𝑜 𝐵) ·𝑜
2𝑜)) ∈ (𝐶 ·𝑜 𝐶)) → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐶)) |
43 | 36, 37, 42 | sylancr 694 |
. . 3
⊢ ((𝐴 +𝑜 𝐵) ∈ 𝐶 → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐶)) |
44 | 10, 43 | sseldi 3566 |
. 2
⊢ ((𝐴 +𝑜 𝐵) ∈ 𝐶 → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ∈ ((𝐶 ·𝑜 𝐶) +𝑜 𝐷)) |
45 | 8, 44 | nsyl3 132 |
1
⊢ ((𝐴 +𝑜 𝐵) ∈ 𝐶 → ¬ ((𝐶 ·𝑜 𝐶) +𝑜 𝐷) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵)) |