Proof of Theorem omopthi
Step | Hyp | Ref
| Expression |
1 | | omopth.1 |
. . . . . . . . . . . . 13
⊢ 𝐴 ∈ ω |
2 | | omopth.2 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈ ω |
3 | 1, 2 | nnacli 7694 |
. . . . . . . . . . . 12
⊢ (𝐴 +𝑜 𝐵) ∈
ω |
4 | 3 | nnoni 7072 |
. . . . . . . . . . 11
⊢ (𝐴 +𝑜 𝐵) ∈ On |
5 | 4 | onordi 5832 |
. . . . . . . . . 10
⊢ Ord
(𝐴 +𝑜
𝐵) |
6 | | omopth.3 |
. . . . . . . . . . . . 13
⊢ 𝐶 ∈ ω |
7 | | omopth.4 |
. . . . . . . . . . . . 13
⊢ 𝐷 ∈ ω |
8 | 6, 7 | nnacli 7694 |
. . . . . . . . . . . 12
⊢ (𝐶 +𝑜 𝐷) ∈
ω |
9 | 8 | nnoni 7072 |
. . . . . . . . . . 11
⊢ (𝐶 +𝑜 𝐷) ∈ On |
10 | 9 | onordi 5832 |
. . . . . . . . . 10
⊢ Ord
(𝐶 +𝑜
𝐷) |
11 | | ordtri3 5759 |
. . . . . . . . . 10
⊢ ((Ord
(𝐴 +𝑜
𝐵) ∧ Ord (𝐶 +𝑜 𝐷)) → ((𝐴 +𝑜 𝐵) = (𝐶 +𝑜 𝐷) ↔ ¬ ((𝐴 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐷) ∨ (𝐶 +𝑜 𝐷) ∈ (𝐴 +𝑜 𝐵)))) |
12 | 5, 10, 11 | mp2an 708 |
. . . . . . . . 9
⊢ ((𝐴 +𝑜 𝐵) = (𝐶 +𝑜 𝐷) ↔ ¬ ((𝐴 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐷) ∨ (𝐶 +𝑜 𝐷) ∈ (𝐴 +𝑜 𝐵))) |
13 | 12 | con2bii 347 |
. . . . . . . 8
⊢ (((𝐴 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐷) ∨ (𝐶 +𝑜 𝐷) ∈ (𝐴 +𝑜 𝐵)) ↔ ¬ (𝐴 +𝑜 𝐵) = (𝐶 +𝑜 𝐷)) |
14 | 1, 2, 8, 7 | omopthlem2 7736 |
. . . . . . . . . 10
⊢ ((𝐴 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐷) → ¬ (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵)) |
15 | | eqcom 2629 |
. . . . . . . . . 10
⊢ ((((𝐶 +𝑜 𝐷) ·𝑜
(𝐶 +𝑜
𝐷)) +𝑜
𝐷) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) ↔ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
16 | 14, 15 | sylnib 318 |
. . . . . . . . 9
⊢ ((𝐴 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐷) → ¬ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
17 | 6, 7, 3, 2 | omopthlem2 7736 |
. . . . . . . . 9
⊢ ((𝐶 +𝑜 𝐷) ∈ (𝐴 +𝑜 𝐵) → ¬ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
18 | 16, 17 | jaoi 394 |
. . . . . . . 8
⊢ (((𝐴 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐷) ∨ (𝐶 +𝑜 𝐷) ∈ (𝐴 +𝑜 𝐵)) → ¬ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
19 | 13, 18 | sylbir 225 |
. . . . . . 7
⊢ (¬
(𝐴 +𝑜
𝐵) = (𝐶 +𝑜 𝐷) → ¬ (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
20 | 19 | con4i 113 |
. . . . . 6
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (𝐴 +𝑜 𝐵) = (𝐶 +𝑜 𝐷)) |
21 | | id 22 |
. . . . . . . . 9
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
22 | 20, 20 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) = ((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷))) |
23 | 22 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐷) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
24 | 21, 23 | eqtr4d 2659 |
. . . . . . . 8
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐷)) |
25 | 3, 3 | nnmcli 7695 |
. . . . . . . . 9
⊢ ((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) ∈
ω |
26 | | nnacan 7708 |
. . . . . . . . 9
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) ∈ ω ∧
𝐵 ∈ ω ∧
𝐷 ∈ ω) →
((((𝐴 +𝑜
𝐵)
·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐷) ↔ 𝐵 = 𝐷)) |
27 | 25, 2, 7, 26 | mp3an 1424 |
. . . . . . . 8
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐷) ↔ 𝐵 = 𝐷) |
28 | 24, 27 | sylib 208 |
. . . . . . 7
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → 𝐵 = 𝐷) |
29 | 28 | oveq2d 6666 |
. . . . . 6
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (𝐶 +𝑜 𝐵) = (𝐶 +𝑜 𝐷)) |
30 | 20, 29 | eqtr4d 2659 |
. . . . 5
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (𝐴 +𝑜 𝐵) = (𝐶 +𝑜 𝐵)) |
31 | | nnacom 7697 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (𝐵 +𝑜 𝐴) = (𝐴 +𝑜 𝐵)) |
32 | 2, 1, 31 | mp2an 708 |
. . . . 5
⊢ (𝐵 +𝑜 𝐴) = (𝐴 +𝑜 𝐵) |
33 | | nnacom 7697 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐵 +𝑜 𝐶) = (𝐶 +𝑜 𝐵)) |
34 | 2, 6, 33 | mp2an 708 |
. . . . 5
⊢ (𝐵 +𝑜 𝐶) = (𝐶 +𝑜 𝐵) |
35 | 30, 32, 34 | 3eqtr4g 2681 |
. . . 4
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (𝐵 +𝑜 𝐴) = (𝐵 +𝑜 𝐶)) |
36 | | nnacan 7708 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐵 +𝑜 𝐴) = (𝐵 +𝑜 𝐶) ↔ 𝐴 = 𝐶)) |
37 | 2, 1, 6, 36 | mp3an 1424 |
. . . 4
⊢ ((𝐵 +𝑜 𝐴) = (𝐵 +𝑜 𝐶) ↔ 𝐴 = 𝐶) |
38 | 35, 37 | sylib 208 |
. . 3
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → 𝐴 = 𝐶) |
39 | 38, 28 | jca 554 |
. 2
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |
40 | | oveq12 6659 |
. . . 4
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 +𝑜 𝐵) = (𝐶 +𝑜 𝐷)) |
41 | 40, 40 | oveq12d 6668 |
. . 3
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) = ((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷))) |
42 | | simpr 477 |
. . 3
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → 𝐵 = 𝐷) |
43 | 41, 42 | oveq12d 6668 |
. 2
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (((𝐴 +𝑜 𝐵) ·𝑜 (𝐴 +𝑜 𝐵)) +𝑜 𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷)) |
44 | 39, 43 | impbii 199 |
1
⊢ ((((𝐴 +𝑜 𝐵) ·𝑜
(𝐴 +𝑜
𝐵)) +𝑜
𝐵) = (((𝐶 +𝑜 𝐷) ·𝑜 (𝐶 +𝑜 𝐷)) +𝑜 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |