Step | Hyp | Ref
| Expression |
1 | | eqeq1 2359 |
. . . . . . . 8
1c
1c |
2 | 1 | rexbidv 2635 |
. . . . . . 7
Nn 1c Nn 1c |
3 | | neeq1 2524 |
. . . . . . 7
|
4 | 2, 3 | anbi12d 691 |
. . . . . 6
Nn 1c Nn 1c |
5 | | df-oddfin 4445 |
. . . . . 6
Oddfin
Nn 1c |
6 | 4, 5 | elab2g 2987 |
. . . . 5
Oddfin
Oddfin Nn 1c |
7 | 6 | ibi 232 |
. . . 4
Oddfin Nn 1c |
8 | | peano2 4403 |
. . . . . . . 8
Nn
1c
Nn |
9 | | addc32 4416 |
. . . . . . . . . . 11
1c
1c |
10 | 9 | addceq1i 4386 |
. . . . . . . . . 10
1c
1c
1c
1c |
11 | | addcass 4415 |
. . . . . . . . . 10
1c
1c
1c
1c |
12 | 10, 11 | eqtri 2373 |
. . . . . . . . 9
1c
1c
1c
1c |
13 | | addceq12 4385 |
. . . . . . . . . . . 12
1c
1c 1c
1c |
14 | 13 | anidms 626 |
. . . . . . . . . . 11
1c
1c 1c |
15 | 14 | eqeq2d 2364 |
. . . . . . . . . 10
1c 1c 1c 1c
1c
1c
1c |
16 | 15 | rspcev 2955 |
. . . . . . . . 9
1c
Nn 1c 1c
1c
1c
Nn
1c
1c
|
17 | 12, 16 | mpan2 652 |
. . . . . . . 8
1c
Nn Nn 1c
1c
|
18 | 8, 17 | syl 15 |
. . . . . . 7
Nn Nn
1c
1c
|
19 | | addceq1 4383 |
. . . . . . . . . . 11
1c
1c 1c
1c |
20 | 19 | eqeq1d 2361 |
. . . . . . . . . 10
1c
1c
1c
1c
|
21 | 20 | rexbidv 2635 |
. . . . . . . . 9
1c
Nn
1c
Nn
1c
1c
|
22 | 21 | biimprd 214 |
. . . . . . . 8
1c
Nn
1c
1c
Nn
1c
|
23 | 22 | com12 27 |
. . . . . . 7
Nn
1c
1c
1c Nn
1c
|
24 | 18, 23 | syl 15 |
. . . . . 6
Nn 1c Nn
1c
|
25 | 24 | rexlimiv 2732 |
. . . . 5
Nn 1c Nn 1c
|
26 | 25 | adantr 451 |
. . . 4
Nn 1c Nn
1c
|
27 | 7, 26 | syl 15 |
. . 3
Oddfin Nn
1c
|
28 | 27 | anim1i 551 |
. 2
Oddfin
1c
Nn 1c
1c |
29 | | 1cex 4142 |
. . . . 5
1c
|
30 | | addcexg 4393 |
. . . . 5
Oddfin 1c
1c |
31 | 29, 30 | mpan2 652 |
. . . 4
Oddfin
1c
|
32 | | eqeq1 2359 |
. . . . . . 7
1c
1c
|
33 | 32 | rexbidv 2635 |
. . . . . 6
1c Nn Nn
1c
|
34 | | neeq1 2524 |
. . . . . 6
1c 1c |
35 | 33, 34 | anbi12d 691 |
. . . . 5
1c Nn Nn
1c
1c
|
36 | | df-evenfin 4444 |
. . . . 5
Evenfin
Nn |
37 | 35, 36 | elab2g 2987 |
. . . 4
1c
1c Evenfin
Nn
1c
1c
|
38 | 31, 37 | syl 15 |
. . 3
Oddfin
1c
Evenfin
Nn
1c
1c
|
39 | 38 | adantr 451 |
. 2
Oddfin
1c
1c Evenfin
Nn
1c
1c
|
40 | 28, 39 | mpbird 223 |
1
Oddfin
1c
1c
Evenfin |