NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  evenoddnnnul Unicode version

Theorem evenoddnnnul 4514
Description: Every nonempty finite cardinal is either even or odd. Theorem X.1.35 of [Rosser] p. 529. (Contributed by SF, 20-Jan-2015.)
Assertion
Ref Expression
evenoddnnnul Evenfin Oddfin Nn

Proof of Theorem evenoddnnnul
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 evennn 4506 . . . . . 6 Evenfin Nn
2 evennnul 4508 . . . . . 6 Evenfin
3 eldifsn 3839 . . . . . 6 Nn Nn
41, 2, 3sylanbrc 645 . . . . 5 Evenfin Nn
54ssriv 3277 . . . 4 Evenfin Nn
6 oddnn 4507 . . . . . 6 Oddfin Nn
7 oddnnul 4509 . . . . . 6 Oddfin
86, 7, 3sylanbrc 645 . . . . 5 Oddfin Nn
98ssriv 3277 . . . 4 Oddfin Nn
105, 9pm3.2i 441 . . 3 Evenfin Nn Oddfin Nn
11 unss 3437 . . 3 Evenfin Nn Oddfin Nn Evenfin Oddfin Nn
1210, 11mpbi 199 . 2 Evenfin Oddfin Nn
13 eldifsn 3839 . . . 4 Nn Nn
14 vex 2862 . . . . . . . . . . . 12
1514elsnc 3756 . . . . . . . . . . 11
16 df-ne 2518 . . . . . . . . . . . 12
1716con2bii 322 . . . . . . . . . . 11
1815, 17bitri 240 . . . . . . . . . 10
1918orbi1i 506 . . . . . . . . 9 Evenfin Oddfin Evenfin Oddfin
20 elun 3220 . . . . . . . . 9 Evenfin Oddfin Evenfin Oddfin
21 imor 401 . . . . . . . . 9 Evenfin Oddfin Evenfin Oddfin
2219, 20, 213bitr4i 268 . . . . . . . 8 Evenfin Oddfin Evenfin Oddfin
2322abbi2i 2464 . . . . . . 7 Evenfin Oddfin Evenfin Oddfin
24 snex 4111 . . . . . . . 8
25 evenfinex 4503 . . . . . . . . 9 Evenfin
26 oddfinex 4504 . . . . . . . . 9 Oddfin
2725, 26unex 4106 . . . . . . . 8 Evenfin Oddfin
2824, 27unex 4106 . . . . . . 7 Evenfin Oddfin
2923, 28eqeltrri 2424 . . . . . 6 Evenfin Oddfin
30 neeq1 2524 . . . . . . 7 0c 0c
31 eleq1 2413 . . . . . . 7 0c Evenfin Oddfin 0c Evenfin Oddfin
3230, 31imbi12d 311 . . . . . 6 0c Evenfin Oddfin 0c 0c Evenfin Oddfin
33 neeq1 2524 . . . . . . 7
34 eleq1 2413 . . . . . . 7 Evenfin Oddfin Evenfin Oddfin
3533, 34imbi12d 311 . . . . . 6 Evenfin Oddfin Evenfin Oddfin
36 neeq1 2524 . . . . . . 7 1c 1c
37 eleq1 2413 . . . . . . 7 1c Evenfin Oddfin 1c Evenfin Oddfin
3836, 37imbi12d 311 . . . . . 6 1c Evenfin Oddfin 1c 1c Evenfin Oddfin
39 neeq1 2524 . . . . . . 7
40 eleq1 2413 . . . . . . 7 Evenfin Oddfin Evenfin Oddfin
4139, 40imbi12d 311 . . . . . 6 Evenfin Oddfin Evenfin Oddfin
42 ssun1 3426 . . . . . . . 8 Evenfin Evenfin Oddfin
43 0ceven 4505 . . . . . . . 8 0c Evenfin
4442, 43sselii 3270 . . . . . . 7 0c Evenfin Oddfin
4544a1i 10 . . . . . 6 0c 0c Evenfin Oddfin
46 addcnnul 4453 . . . . . . . . . 10 1c 1c
4746simpld 445 . . . . . . . . 9 1c
48 sucevenodd 4510 . . . . . . . . . . . 12 Evenfin 1c 1c Oddfin
4948expcom 424 . . . . . . . . . . 11 1c Evenfin 1c Oddfin
50 sucoddeven 4511 . . . . . . . . . . . 12 Oddfin 1c 1c Evenfin
5150expcom 424 . . . . . . . . . . 11 1c Oddfin 1c Evenfin
5249, 51orim12d 811 . . . . . . . . . 10 1c Evenfin Oddfin 1c Oddfin 1c Evenfin
53 elun 3220 . . . . . . . . . 10 Evenfin Oddfin Evenfin Oddfin
54 elun 3220 . . . . . . . . . . 11 1c Evenfin Oddfin 1c Evenfin 1c Oddfin
55 orcom 376 . . . . . . . . . . 11 1c Evenfin 1c Oddfin 1c Oddfin 1c Evenfin
5654, 55bitri 240 . . . . . . . . . 10 1c Evenfin Oddfin 1c Oddfin 1c Evenfin
5752, 53, 563imtr4g 261 . . . . . . . . 9 1c Evenfin Oddfin 1c Evenfin Oddfin
5847, 57embantd 50 . . . . . . . 8 1c Evenfin Oddfin 1c Evenfin Oddfin
5958com12 27 . . . . . . 7 Evenfin Oddfin 1c 1c Evenfin Oddfin
6059a1i 10 . . . . . 6 Nn Evenfin Oddfin 1c 1c Evenfin Oddfin
6129, 32, 35, 38, 41, 45, 60finds 4411 . . . . 5 Nn Evenfin Oddfin
6261imp 418 . . . 4 Nn Evenfin Oddfin
6313, 62sylbi 187 . . 3 Nn Evenfin Oddfin
6463ssriv 3277 . 2 Nn Evenfin Oddfin
6512, 64eqssi 3288 1 Evenfin Oddfin Nn
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wo 357   wa 358   wceq 1642   wcel 1710  cab 2339   wne 2516  cvv 2859   cdif 3206   cun 3207   wss 3257  c0 3550  csn 3737  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   cplc 4375   Evenfin cevenfin 4436   Oddfin coddfin 4437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379  df-evenfin 4444  df-oddfin 4445
This theorem is referenced by:  vinf  4555
  Copyright terms: Public domain W3C validator