Step | Hyp | Ref
| Expression |
1 | | nnc0suc 4412 |
. . . . . . . 8
Nn
0c Nn
1c |
2 | | addceq2 4384 |
. . . . . . . . . 10
0c
0c |
3 | | addcid1 4405 |
. . . . . . . . . 10
0c
|
4 | 2, 3 | syl6req 2402 |
. . . . . . . . 9
0c |
5 | | addceq2 4384 |
. . . . . . . . . . 11
1c
1c |
6 | | addcass 4415 |
. . . . . . . . . . 11
1c
1c |
7 | 5, 6 | syl6eqr 2403 |
. . . . . . . . . 10
1c
1c |
8 | 7 | reximi 2721 |
. . . . . . . . 9
Nn 1c Nn 1c |
9 | 4, 8 | orim12i 502 |
. . . . . . . 8
0c Nn
1c
Nn
1c |
10 | 1, 9 | sylbi 187 |
. . . . . . 7
Nn Nn 1c |
11 | 10 | orcomd 377 |
. . . . . 6
Nn Nn 1c
|
12 | | eqeq1 2359 |
. . . . . . . 8
1c
1c |
13 | 12 | rexbidv 2635 |
. . . . . . 7
Nn 1c Nn
1c |
14 | | eqeq2 2362 |
. . . . . . 7
|
15 | 13, 14 | orbi12d 690 |
. . . . . 6
Nn 1c Nn 1c
|
16 | 11, 15 | syl5ibrcom 213 |
. . . . 5
Nn Nn 1c |
17 | 16 | rexlimiv 2732 |
. . . 4
Nn
Nn 1c |
18 | 6 | eqeq2i 2363 |
. . . . . . 7
1c
1c |
19 | | peano2 4403 |
. . . . . . . 8
Nn
1c
Nn |
20 | 5 | eqeq2d 2364 |
. . . . . . . . 9
1c
1c |
21 | 20 | rspcev 2955 |
. . . . . . . 8
1c
Nn 1c
Nn |
22 | 19, 21 | sylan 457 |
. . . . . . 7
Nn 1c
Nn |
23 | 18, 22 | sylan2b 461 |
. . . . . 6
Nn 1c
Nn |
24 | 23 | rexlimiva 2733 |
. . . . 5
Nn 1c Nn
|
25 | | peano1 4402 |
. . . . . . 7
0c
Nn |
26 | 3 | eqcomi 2357 |
. . . . . . 7
0c |
27 | 2 | eqeq2d 2364 |
. . . . . . . 8
0c 0c |
28 | 27 | rspcev 2955 |
. . . . . . 7
0c Nn
0c
Nn |
29 | 25, 26, 28 | mp2an 653 |
. . . . . 6
Nn |
30 | | eqeq1 2359 |
. . . . . . 7
|
31 | 30 | rexbidv 2635 |
. . . . . 6
Nn Nn |
32 | 29, 31 | mpbii 202 |
. . . . 5
Nn |
33 | 24, 32 | jaoi 368 |
. . . 4
Nn 1c Nn
|
34 | 17, 33 | impbii 180 |
. . 3
Nn
Nn 1c |
35 | 34 | a1i 10 |
. 2
Nn
Nn 1c |
36 | | opklefing 4448 |
. . 3
fin Nn |
37 | 36 | 3adant3 975 |
. 2
fin
Nn |
38 | | opkltfing 4449 |
. . . . . 6
fin
Nn 1c |
39 | 38 | adantr 451 |
. . . . 5
fin
Nn 1c |
40 | | ibar 490 |
. . . . . 6
Nn 1c
Nn 1c |
41 | 40 | adantl 452 |
. . . . 5
Nn 1c Nn 1c |
42 | 39, 41 | bitr4d 247 |
. . . 4
fin Nn 1c |
43 | 42 | orbi1d 683 |
. . 3
fin
Nn 1c |
44 | 43 | 3impa 1146 |
. 2
fin Nn 1c |
45 | 35, 37, 44 | 3bitr4d 276 |
1
fin fin |