Step | Hyp | Ref
| Expression |
1 | | noel 3555 |
. 2
Ncfin Spfin ![(/)](varnothing.gif) |
2 | | spfinex 4538 |
. . . . . . . 8
Spfin ![_V](rmcv.gif) |
3 | | ncfinprop 4475 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Spfin ![_V](rmcv.gif)
Ncfin Spfin Nn Spfin Ncfin Spfin ![)](rp.gif) ![)](rp.gif) |
4 | 2, 3 | mpan2 652 |
. . . . . . 7
![(](lp.gif) Fin Ncfin Spfin Nn Spfin Ncfin Spfin ![)](rp.gif) ![)](rp.gif) |
5 | | ne0i 3557 |
. . . . . . . 8
Spfin Ncfin Spfin Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) |
6 | 5 | anim2i 552 |
. . . . . . 7
![(](lp.gif) Ncfin
Spfin Nn Spfin Ncfin Spfin Ncfin Spfin Nn Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 4, 6 | syl 15 |
. . . . . 6
![(](lp.gif) Fin Ncfin Spfin Nn Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | eldifsn 3840 |
. . . . . 6
Ncfin Spfin
Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Ncfin Spfin Nn Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 7, 8 | sylibr 203 |
. . . . 5
![(](lp.gif) Fin Ncfin Spfin
Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | evenoddnnnul 4515 |
. . . . 5
Evenfin Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
11 | 9, 10 | syl6eleqr 2444 |
. . . 4
![(](lp.gif) Fin Ncfin Spfin
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) |
12 | | vfinncsp 4555 |
. . . . . . . . . 10
![(](lp.gif) Fin Ncfin Spfin
Tfin Ncfin Spfin 1c![)](rp.gif) ![)](rp.gif) |
13 | 12 | adantr 451 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Evenfin Ncfin Spfin
Tfin Ncfin Spfin 1c![)](rp.gif) ![)](rp.gif) |
14 | | eventfin 4518 |
. . . . . . . . . . 11
Ncfin Spfin Evenfin Tfin Ncfin Spfin Evenfin ![)](rp.gif) |
15 | 14 | adantl 452 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Evenfin Tfin
Ncfin Spfin Evenfin ![)](rp.gif) |
16 | | evennnul 4509 |
. . . . . . . . . . . 12
Ncfin Spfin Evenfin Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) |
17 | 16 | adantl 452 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Evenfin Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) |
18 | 13, 17 | eqnetrrd 2537 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Evenfin Tfin Ncfin Spfin 1c ![(/)](varnothing.gif) ![)](rp.gif) |
19 | | sucevenodd 4511 |
. . . . . . . . . 10
![(](lp.gif) Tfin
Ncfin Spfin Evenfin Tfin Ncfin Spfin 1c ![(/)](varnothing.gif) Tfin Ncfin Spfin 1c
Oddfin ![)](rp.gif) |
20 | 15, 18, 19 | syl2anc 642 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Evenfin Tfin Ncfin Spfin 1c
Oddfin ![)](rp.gif) |
21 | 13, 20 | eqeltrd 2427 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Evenfin Ncfin Spfin Oddfin ![)](rp.gif) |
22 | 21 | ex 423 |
. . . . . . 7
![(](lp.gif) Fin Ncfin Spfin Evenfin Ncfin Spfin Oddfin ![)](rp.gif) ![)](rp.gif) |
23 | 22 | ancld 536 |
. . . . . 6
![(](lp.gif) Fin Ncfin Spfin Evenfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 12 | adantr 451 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Oddfin Ncfin Spfin
Tfin Ncfin Spfin 1c![)](rp.gif) ![)](rp.gif) |
25 | | oddtfin 4519 |
. . . . . . . . . . 11
Ncfin Spfin Oddfin Tfin Ncfin Spfin Oddfin ![)](rp.gif) |
26 | 25 | adantl 452 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Oddfin Tfin
Ncfin Spfin Oddfin ![)](rp.gif) |
27 | | oddnnul 4510 |
. . . . . . . . . . . 12
Ncfin Spfin Oddfin Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) |
28 | 27 | adantl 452 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Oddfin Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) |
29 | 24, 28 | eqnetrrd 2537 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Oddfin Tfin Ncfin Spfin 1c ![(/)](varnothing.gif) ![)](rp.gif) |
30 | | sucoddeven 4512 |
. . . . . . . . . 10
![(](lp.gif) Tfin
Ncfin Spfin Oddfin Tfin Ncfin Spfin 1c ![(/)](varnothing.gif) Tfin Ncfin Spfin 1c
Evenfin ![)](rp.gif) |
31 | 26, 29, 30 | syl2anc 642 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Oddfin Tfin Ncfin Spfin 1c
Evenfin ![)](rp.gif) |
32 | 24, 31 | eqeltrd 2427 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Fin Ncfin Spfin Oddfin Ncfin Spfin Evenfin ![)](rp.gif) |
33 | 32 | ex 423 |
. . . . . . 7
![(](lp.gif) Fin Ncfin Spfin Oddfin Ncfin Spfin Evenfin ![)](rp.gif) ![)](rp.gif) |
34 | 33 | ancrd 537 |
. . . . . 6
![(](lp.gif) Fin Ncfin Spfin Oddfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 23, 34 | jaod 369 |
. . . . 5
![(](lp.gif) Fin ![(](lp.gif)
Ncfin Spfin Evenfin Ncfin Spfin Oddfin Ncfin Spfin Evenfin Ncfin Spfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | elun 3221 |
. . . . 5
Ncfin Spfin
Evenfin Oddfin
Ncfin Spfin Evenfin Ncfin Spfin Oddfin ![)](rp.gif) ![)](rp.gif) |
37 | | elin 3220 |
. . . . 5
Ncfin Spfin
Evenfin Oddfin
Ncfin Spfin Evenfin Ncfin Spfin Oddfin ![)](rp.gif) ![)](rp.gif) |
38 | 35, 36, 37 | 3imtr4g 261 |
. . . 4
![(](lp.gif) Fin Ncfin Spfin
Evenfin Oddfin
Ncfin Spfin
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 11, 38 | mpd 14 |
. . 3
![(](lp.gif) Fin Ncfin Spfin
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) |
40 | | evenodddisj 4517 |
. . 3
Evenfin Oddfin ![(/)](varnothing.gif) |
41 | 39, 40 | syl6eleq 2443 |
. 2
![(](lp.gif) Fin Ncfin Spfin ![(/)](varnothing.gif) ![)](rp.gif) |
42 | 1, 41 | mto 167 |
1
Fin |