Step | Hyp | Ref
| Expression |
1 | | evennn 4506 |
. . . . . 6
![(](lp.gif) Evenfin Nn ![)](rp.gif) |
2 | | evennnul 4508 |
. . . . . 6
![(](lp.gif) Evenfin ![(/)](varnothing.gif) ![)](rp.gif) |
3 | | eldifsn 3839 |
. . . . . 6
![(](lp.gif) Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif)
Nn ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
4 | 1, 2, 3 | sylanbrc 645 |
. . . . 5
![(](lp.gif) Evenfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
5 | 4 | ssriv 3277 |
. . . 4
Evenfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
6 | | oddnn 4507 |
. . . . . 6
![(](lp.gif) Oddfin Nn ![)](rp.gif) |
7 | | oddnnul 4509 |
. . . . . 6
![(](lp.gif) Oddfin ![(/)](varnothing.gif) ![)](rp.gif) |
8 | 6, 7, 3 | sylanbrc 645 |
. . . . 5
![(](lp.gif) Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | ssriv 3277 |
. . . 4
Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
10 | 5, 9 | pm3.2i 441 |
. . 3
Evenfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
11 | | unss 3437 |
. . 3
![(](lp.gif) Evenfin
Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) Evenfin Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 10, 11 | mpbi 199 |
. 2
Evenfin Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |
13 | | eldifsn 3839 |
. . . 4
![(](lp.gif) Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![(](lp.gif)
Nn ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | vex 2862 |
. . . . . . . . . . . 12
![_V](rmcv.gif) |
15 | 14 | elsnc 3756 |
. . . . . . . . . . 11
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
16 | | df-ne 2518 |
. . . . . . . . . . . 12
![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
17 | 16 | con2bii 322 |
. . . . . . . . . . 11
![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) |
18 | 15, 17 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
19 | 18 | orbi1i 506 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif)
Evenfin Oddfin ![)](rp.gif) ![(](lp.gif) Evenfin
Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | | elun 3220 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) Evenfin Oddfin ![)](rp.gif)
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif)
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | | imor 401 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 19, 20, 21 | 3bitr4i 268 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) Evenfin Oddfin ![)](rp.gif)
![(](lp.gif) Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | abbi2i 2464 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) Evenfin Oddfin ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
24 | | snex 4111 |
. . . . . . . 8
![{](lbrace.gif) ![(/)](varnothing.gif) ![_V](rmcv.gif) |
25 | | evenfinex 4503 |
. . . . . . . . 9
Evenfin ![_V](rmcv.gif) |
26 | | oddfinex 4504 |
. . . . . . . . 9
Oddfin ![_V](rmcv.gif) |
27 | 25, 26 | unex 4106 |
. . . . . . . 8
Evenfin Oddfin ![_V](rmcv.gif) |
28 | 24, 27 | unex 4106 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) ![(/)](varnothing.gif) Evenfin Oddfin ![)](rp.gif) ![_V](rmcv.gif) |
29 | 23, 28 | eqeltrri 2424 |
. . . . . 6
![{](lbrace.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif)
![_V](rmcv.gif) |
30 | | neeq1 2524 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif)
0c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | eleq1 2413 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) Evenfin
Oddfin 0c Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 30, 31 | imbi12d 311 |
. . . . . 6
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) Evenfin
Oddfin ![)](rp.gif)
0c
0c
Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | neeq1 2524 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | eleq1 2413 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
Evenfin Oddfin Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 33, 34 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | | neeq1 2524 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | eleq1 2413 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) Evenfin
Oddfin ![(](lp.gif)
1c
Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 36, 37 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) Evenfin
Oddfin ![)](rp.gif)
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | neeq1 2524 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
40 | | eleq1 2413 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
Evenfin Oddfin Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 39, 40 | imbi12d 311 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | | ssun1 3426 |
. . . . . . . 8
Evenfin Evenfin Oddfin ![)](rp.gif) |
43 | | 0ceven 4505 |
. . . . . . . 8
0c
Evenfin |
44 | 42, 43 | sselii 3270 |
. . . . . . 7
0c
Evenfin Oddfin ![)](rp.gif) |
45 | 44 | a1i 10 |
. . . . . 6
0c 0c
Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) |
46 | | addcnnul 4453 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif)
1c ![(/)](varnothing.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | simpld 445 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
![(/)](varnothing.gif) ![)](rp.gif) |
48 | | sucevenodd 4510 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Evenfin ![(](lp.gif)
1c
![(/)](varnothing.gif) ![(](lp.gif)
1c
Oddfin ![)](rp.gif) |
49 | 48 | expcom 424 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif)
Evenfin ![(](lp.gif)
1c
Oddfin ![)](rp.gif) ![)](rp.gif) |
50 | | sucoddeven 4511 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Oddfin ![(](lp.gif)
1c
![(/)](varnothing.gif) ![(](lp.gif)
1c
Evenfin ![)](rp.gif) |
51 | 50 | expcom 424 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif)
Oddfin ![(](lp.gif)
1c
Evenfin ![)](rp.gif) ![)](rp.gif) |
52 | 49, 51 | orim12d 811 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
Evenfin
Oddfin ![(](lp.gif) ![(](lp.gif) 1c
Oddfin ![(](lp.gif)
1c
Evenfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | | elun 3220 |
. . . . . . . . . 10
![(](lp.gif) Evenfin Oddfin ![(](lp.gif) Evenfin
Oddfin ![)](rp.gif) ![)](rp.gif) |
54 | | elun 3220 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif)
1c
Evenfin Oddfin ![(](lp.gif) ![(](lp.gif)
1c
Evenfin ![(](lp.gif)
1c
Oddfin ![)](rp.gif) ![)](rp.gif) |
55 | | orcom 376 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
Evenfin ![(](lp.gif)
1c
Oddfin ![(](lp.gif) ![(](lp.gif) 1c Oddfin ![(](lp.gif) 1c Evenfin ![)](rp.gif) ![)](rp.gif) |
56 | 54, 55 | bitri 240 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif)
1c
Evenfin Oddfin ![(](lp.gif) ![(](lp.gif)
1c
Oddfin ![(](lp.gif)
1c
Evenfin ![)](rp.gif) ![)](rp.gif) |
57 | 52, 53, 56 | 3imtr4g 261 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif)
Evenfin Oddfin ![(](lp.gif)
1c
Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 47, 57 | embantd 50 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![(](lp.gif)
1c
Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 58 | com12 27 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c
Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
60 | 59 | a1i 10 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Evenfin
Oddfin ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
61 | 29, 32, 35, 38, 41, 45, 60 | finds 4411 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif)
Evenfin Oddfin
![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
62 | 61 | imp 418 |
. . . 4
![(](lp.gif) ![(](lp.gif) Nn ![(/)](varnothing.gif) Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) |
63 | 13, 62 | sylbi 187 |
. . 3
![(](lp.gif) Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Evenfin Oddfin ![)](rp.gif) ![)](rp.gif) |
64 | 63 | ssriv 3277 |
. 2
Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) Evenfin Oddfin ![)](rp.gif) |
65 | 12, 64 | eqssi 3288 |
1
Evenfin Oddfin Nn ![{](lbrace.gif) ![(/)](varnothing.gif) ![}](rbrace.gif) ![)](rp.gif) |