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