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