Proof of Theorem nnneo
Step | Hyp | Ref
| Expression |
1 | | nnon 6963 |
. . . 4
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
2 | | onnbtwn 5735 |
. . . 4
⊢ (𝐴 ∈ On → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝐴 ∈ ω → ¬
(𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) |
4 | 3 | 3ad2ant1 1075 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) |
5 | | suceq 5707 |
. . . . 5
⊢ (𝐶 = (2𝑜
·𝑜 𝐴) → suc 𝐶 = suc (2𝑜
·𝑜 𝐴)) |
6 | 5 | eqeq1d 2612 |
. . . 4
⊢ (𝐶 = (2𝑜
·𝑜 𝐴) → (suc 𝐶 = (2𝑜
·𝑜 𝐵) ↔ suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵))) |
7 | 6 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → (suc 𝐶 = (2𝑜
·𝑜 𝐵) ↔ suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵))) |
8 | | ovex 6577 |
. . . . . . . 8
⊢
(2𝑜 ·𝑜 𝐴) ∈ V |
9 | 8 | sucid 5721 |
. . . . . . 7
⊢
(2𝑜 ·𝑜 𝐴) ∈ suc (2𝑜
·𝑜 𝐴) |
10 | | eleq2 2677 |
. . . . . . 7
⊢ (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → ((2𝑜
·𝑜 𝐴) ∈ suc (2𝑜
·𝑜 𝐴) ↔ (2𝑜
·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵))) |
11 | 9, 10 | mpbii 222 |
. . . . . 6
⊢ (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → (2𝑜
·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵)) |
12 | | 2onn 7607 |
. . . . . . . 8
⊢
2𝑜 ∈ ω |
13 | | nnmord 7599 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧
2𝑜 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵))) |
14 | 12, 13 | mp3an3 1405 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵))) |
15 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 2𝑜)
→ 𝐴 ∈ 𝐵) |
16 | 14, 15 | syl6bir 243 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
((2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 𝐵) → 𝐴 ∈ 𝐵)) |
17 | 11, 16 | syl5 33 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → 𝐴 ∈ 𝐵)) |
18 | | simpr 476 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) |
19 | | nnmcl 7579 |
. . . . . . . . . . . . 13
⊢
((2𝑜 ∈ ω ∧ 𝐴 ∈ ω) →
(2𝑜 ·𝑜 𝐴) ∈ ω) |
20 | 12, 19 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω →
(2𝑜 ·𝑜 𝐴) ∈ ω) |
21 | | nnon 6963 |
. . . . . . . . . . . 12
⊢
((2𝑜 ·𝑜 𝐴) ∈ ω →
(2𝑜 ·𝑜 𝐴) ∈ On) |
22 | | oa1suc 7498 |
. . . . . . . . . . . 12
⊢
((2𝑜 ·𝑜 𝐴) ∈ On → ((2𝑜
·𝑜 𝐴) +𝑜
1𝑜) = suc (2𝑜
·𝑜 𝐴)) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω →
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) = suc (2𝑜
·𝑜 𝐴)) |
24 | | 1onn 7606 |
. . . . . . . . . . . . . . . 16
⊢
1𝑜 ∈ ω |
25 | 24 | elexi 3186 |
. . . . . . . . . . . . . . 15
⊢
1𝑜 ∈ V |
26 | 25 | sucid 5721 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ suc 1𝑜 |
27 | | df-2o 7448 |
. . . . . . . . . . . . . 14
⊢
2𝑜 = suc 1𝑜 |
28 | 26, 27 | eleqtrri 2687 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ 2𝑜 |
29 | | nnaord 7586 |
. . . . . . . . . . . . . . 15
⊢
((1𝑜 ∈ ω ∧ 2𝑜
∈ ω ∧ (2𝑜 ·𝑜 𝐴) ∈ ω) →
(1𝑜 ∈ 2𝑜 ↔
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜))) |
30 | 24, 12, 29 | mp3an12 1406 |
. . . . . . . . . . . . . 14
⊢
((2𝑜 ·𝑜 𝐴) ∈ ω →
(1𝑜 ∈ 2𝑜 ↔
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜))) |
31 | 20, 30 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω →
(1𝑜 ∈ 2𝑜 ↔
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜))) |
32 | 28, 31 | mpbii 222 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω →
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜)) |
33 | | nnmsuc 7574 |
. . . . . . . . . . . . 13
⊢
((2𝑜 ∈ ω ∧ 𝐴 ∈ ω) →
(2𝑜 ·𝑜 suc 𝐴) = ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜)) |
34 | 12, 33 | mpan 702 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω →
(2𝑜 ·𝑜 suc 𝐴) = ((2𝑜
·𝑜 𝐴) +𝑜
2𝑜)) |
35 | 32, 34 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω →
((2𝑜 ·𝑜 𝐴) +𝑜
1𝑜) ∈ (2𝑜
·𝑜 suc 𝐴)) |
36 | 23, 35 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → suc
(2𝑜 ·𝑜 𝐴) ∈ (2𝑜
·𝑜 suc 𝐴)) |
37 | 36 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → suc (2𝑜
·𝑜 𝐴) ∈ (2𝑜
·𝑜 suc 𝐴)) |
38 | 18, 37 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → (2𝑜
·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴)) |
39 | | peano2 6978 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
40 | | nnmord 7599 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ω ∧ suc 𝐴 ∈ ω ∧
2𝑜 ∈ ω) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
41 | 12, 40 | mp3an3 1405 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ω ∧ suc 𝐴 ∈ ω) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
42 | 39, 41 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
43 | 42 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
44 | 43 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → ((𝐵 ∈ suc 𝐴 ∧ ∅ ∈ 2𝑜)
↔ (2𝑜 ·𝑜 𝐵) ∈ (2𝑜
·𝑜 suc 𝐴))) |
45 | 38, 44 | mpbird 246 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → (𝐵 ∈ suc 𝐴 ∧ ∅ ∈
2𝑜)) |
46 | 45 | simpld 474 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵)) → 𝐵 ∈ suc 𝐴) |
47 | 46 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → 𝐵 ∈ suc 𝐴)) |
48 | 17, 47 | jcad 554 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc
(2𝑜 ·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))) |
49 | 48 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → (suc (2𝑜
·𝑜 𝐴) = (2𝑜
·𝑜 𝐵) → (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))) |
50 | 7, 49 | sylbid 229 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → (suc 𝐶 = (2𝑜
·𝑜 𝐵) → (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴))) |
51 | 4, 50 | mtod 188 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = (2𝑜
·𝑜 𝐴)) → ¬ suc 𝐶 = (2𝑜
·𝑜 𝐵)) |