Step |
Hyp |
Ref |
Expression |
1 |
|
nnon |
โข ( ๐ด โ ฯ โ ๐ด โ On ) |
2 |
|
onnbtwn |
โข ( ๐ด โ On โ ยฌ ( ๐ด โ ๐ต โง ๐ต โ suc ๐ด ) ) |
3 |
1 2
|
syl |
โข ( ๐ด โ ฯ โ ยฌ ( ๐ด โ ๐ต โง ๐ต โ suc ๐ด ) ) |
4 |
3
|
3ad2ant1 |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ = ( 2o ยทo ๐ด ) ) โ ยฌ ( ๐ด โ ๐ต โง ๐ต โ suc ๐ด ) ) |
5 |
|
suceq |
โข ( ๐ถ = ( 2o ยทo ๐ด ) โ suc ๐ถ = suc ( 2o ยทo ๐ด ) ) |
6 |
5
|
eqeq1d |
โข ( ๐ถ = ( 2o ยทo ๐ด ) โ ( suc ๐ถ = ( 2o ยทo ๐ต ) โ suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) ) |
7 |
6
|
3ad2ant3 |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ = ( 2o ยทo ๐ด ) ) โ ( suc ๐ถ = ( 2o ยทo ๐ต ) โ suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) ) |
8 |
|
ovex |
โข ( 2o ยทo ๐ด ) โ V |
9 |
8
|
sucid |
โข ( 2o ยทo ๐ด ) โ suc ( 2o ยทo ๐ด ) |
10 |
|
eleq2 |
โข ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ ( ( 2o ยทo ๐ด ) โ suc ( 2o ยทo ๐ด ) โ ( 2o ยทo ๐ด ) โ ( 2o ยทo ๐ต ) ) ) |
11 |
9 10
|
mpbii |
โข ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ ( 2o ยทo ๐ด ) โ ( 2o ยทo ๐ต ) ) |
12 |
|
2onn |
โข 2o โ ฯ |
13 |
|
nnmord |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง 2o โ ฯ ) โ ( ( ๐ด โ ๐ต โง โ
โ 2o ) โ ( 2o ยทo ๐ด ) โ ( 2o ยทo ๐ต ) ) ) |
14 |
12 13
|
mp3an3 |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โ ( ( ๐ด โ ๐ต โง โ
โ 2o ) โ ( 2o ยทo ๐ด ) โ ( 2o ยทo ๐ต ) ) ) |
15 |
|
simpl |
โข ( ( ๐ด โ ๐ต โง โ
โ 2o ) โ ๐ด โ ๐ต ) |
16 |
14 15
|
syl6bir |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โ ( ( 2o ยทo ๐ด ) โ ( 2o ยทo ๐ต ) โ ๐ด โ ๐ต ) ) |
17 |
11 16
|
syl5 |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ ๐ด โ ๐ต ) ) |
18 |
|
simpr |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) |
19 |
|
nnmcl |
โข ( ( 2o โ ฯ โง ๐ด โ ฯ ) โ ( 2o ยทo ๐ด ) โ ฯ ) |
20 |
12 19
|
mpan |
โข ( ๐ด โ ฯ โ ( 2o ยทo ๐ด ) โ ฯ ) |
21 |
|
nnon |
โข ( ( 2o ยทo ๐ด ) โ ฯ โ ( 2o ยทo ๐ด ) โ On ) |
22 |
|
oa1suc |
โข ( ( 2o ยทo ๐ด ) โ On โ ( ( 2o ยทo ๐ด ) +o 1o ) = suc ( 2o ยทo ๐ด ) ) |
23 |
20 21 22
|
3syl |
โข ( ๐ด โ ฯ โ ( ( 2o ยทo ๐ด ) +o 1o ) = suc ( 2o ยทo ๐ด ) ) |
24 |
|
1oex |
โข 1o โ V |
25 |
24
|
sucid |
โข 1o โ suc 1o |
26 |
|
df-2o |
โข 2o = suc 1o |
27 |
25 26
|
eleqtrri |
โข 1o โ 2o |
28 |
|
1onn |
โข 1o โ ฯ |
29 |
|
nnaord |
โข ( ( 1o โ ฯ โง 2o โ ฯ โง ( 2o ยทo ๐ด ) โ ฯ ) โ ( 1o โ 2o โ ( ( 2o ยทo ๐ด ) +o 1o ) โ ( ( 2o ยทo ๐ด ) +o 2o ) ) ) |
30 |
28 12 20 29
|
mp3an12i |
โข ( ๐ด โ ฯ โ ( 1o โ 2o โ ( ( 2o ยทo ๐ด ) +o 1o ) โ ( ( 2o ยทo ๐ด ) +o 2o ) ) ) |
31 |
27 30
|
mpbii |
โข ( ๐ด โ ฯ โ ( ( 2o ยทo ๐ด ) +o 1o ) โ ( ( 2o ยทo ๐ด ) +o 2o ) ) |
32 |
|
nnmsuc |
โข ( ( 2o โ ฯ โง ๐ด โ ฯ ) โ ( 2o ยทo suc ๐ด ) = ( ( 2o ยทo ๐ด ) +o 2o ) ) |
33 |
12 32
|
mpan |
โข ( ๐ด โ ฯ โ ( 2o ยทo suc ๐ด ) = ( ( 2o ยทo ๐ด ) +o 2o ) ) |
34 |
31 33
|
eleqtrrd |
โข ( ๐ด โ ฯ โ ( ( 2o ยทo ๐ด ) +o 1o ) โ ( 2o ยทo suc ๐ด ) ) |
35 |
23 34
|
eqeltrrd |
โข ( ๐ด โ ฯ โ suc ( 2o ยทo ๐ด ) โ ( 2o ยทo suc ๐ด ) ) |
36 |
35
|
ad2antrr |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ suc ( 2o ยทo ๐ด ) โ ( 2o ยทo suc ๐ด ) ) |
37 |
18 36
|
eqeltrrd |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ ( 2o ยทo ๐ต ) โ ( 2o ยทo suc ๐ด ) ) |
38 |
|
peano2 |
โข ( ๐ด โ ฯ โ suc ๐ด โ ฯ ) |
39 |
|
nnmord |
โข ( ( ๐ต โ ฯ โง suc ๐ด โ ฯ โง 2o โ ฯ ) โ ( ( ๐ต โ suc ๐ด โง โ
โ 2o ) โ ( 2o ยทo ๐ต ) โ ( 2o ยทo suc ๐ด ) ) ) |
40 |
12 39
|
mp3an3 |
โข ( ( ๐ต โ ฯ โง suc ๐ด โ ฯ ) โ ( ( ๐ต โ suc ๐ด โง โ
โ 2o ) โ ( 2o ยทo ๐ต ) โ ( 2o ยทo suc ๐ด ) ) ) |
41 |
38 40
|
sylan2 |
โข ( ( ๐ต โ ฯ โง ๐ด โ ฯ ) โ ( ( ๐ต โ suc ๐ด โง โ
โ 2o ) โ ( 2o ยทo ๐ต ) โ ( 2o ยทo suc ๐ด ) ) ) |
42 |
41
|
ancoms |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โ ( ( ๐ต โ suc ๐ด โง โ
โ 2o ) โ ( 2o ยทo ๐ต ) โ ( 2o ยทo suc ๐ด ) ) ) |
43 |
42
|
adantr |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ ( ( ๐ต โ suc ๐ด โง โ
โ 2o ) โ ( 2o ยทo ๐ต ) โ ( 2o ยทo suc ๐ด ) ) ) |
44 |
37 43
|
mpbird |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ ( ๐ต โ suc ๐ด โง โ
โ 2o ) ) |
45 |
44
|
simpld |
โข ( ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ ๐ต โ suc ๐ด ) |
46 |
45
|
ex |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ ๐ต โ suc ๐ด ) ) |
47 |
17 46
|
jcad |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ ) โ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ ( ๐ด โ ๐ต โง ๐ต โ suc ๐ด ) ) ) |
48 |
47
|
3adant3 |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ = ( 2o ยทo ๐ด ) ) โ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ ( ๐ด โ ๐ต โง ๐ต โ suc ๐ด ) ) ) |
49 |
7 48
|
sylbid |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ = ( 2o ยทo ๐ด ) ) โ ( suc ๐ถ = ( 2o ยทo ๐ต ) โ ( ๐ด โ ๐ต โง ๐ต โ suc ๐ด ) ) ) |
50 |
4 49
|
mtod |
โข ( ( ๐ด โ ฯ โง ๐ต โ ฯ โง ๐ถ = ( 2o ยทo ๐ด ) ) โ ยฌ suc ๐ถ = ( 2o ยทo ๐ต ) ) |