Step | Hyp | Ref
| Expression |
1 | | isgbe 41639 |
. 2
GoldbachEven Even Odd
Odd |
2 | | oddprmuzge3 41625 |
. . . . . . . . . . . . 13
Odd
|
3 | 2 | ancoms 469 |
. . . . . . . . . . . 12
Odd |
4 | | oddprmuzge3 41625 |
. . . . . . . . . . . . 13
Odd
|
5 | 4 | ancoms 469 |
. . . . . . . . . . . 12
Odd |
6 | | eluz2 11693 |
. . . . . . . . . . . . . 14
|
7 | | eluz2 11693 |
. . . . . . . . . . . . . . 15
|
8 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
9 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
10 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
11 | 10, 10 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
12 | | pm3.22 465 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
13 | | le2add 10510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
14 | 11, 12, 13 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
15 | 14 | ancomsd 470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
16 | | 3p3e6 11161 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
17 | 16 | breq1i 4660 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
18 | | 5lt6 11204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
19 | | 5re 11099 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
21 | | 6re 11101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
23 | | readdcl 10019 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
24 | 23 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
25 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
26 | 20, 22, 24, 25 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
27 | 18, 26 | mpani 712 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
28 | 17, 27 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
29 | 15, 28 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
30 | 8, 9, 29 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
31 | 30 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
|
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | 32 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 33 | exp4b 632 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 34 | 3imp 1256 |
. . . . . . . . . . . . . . . . . 18
|
36 | 35 | com13 88 |
. . . . . . . . . . . . . . . . 17
|
37 | 36 | imp 445 |
. . . . . . . . . . . . . . . 16
|
38 | 37 | 3adant1 1079 |
. . . . . . . . . . . . . . 15
|
39 | 7, 38 | syl5bi 232 |
. . . . . . . . . . . . . 14
|
40 | 6, 39 | sylbi 207 |
. . . . . . . . . . . . 13
|
41 | 40 | imp 445 |
. . . . . . . . . . . 12
|
42 | 3, 5, 41 | syl2an 494 |
. . . . . . . . . . 11
Odd
Odd
|
43 | 42 | an4s 869 |
. . . . . . . . . 10
Odd
Odd
|
44 | 43 | ex 450 |
. . . . . . . . 9
Odd Odd
|
45 | 44 | 3adant3 1081 |
. . . . . . . 8
Odd Odd
|
46 | 45 | impcom 446 |
. . . . . . 7
Odd
Odd
|
47 | | breq2 4657 |
. . . . . . . . 9
|
48 | 47 | 3ad2ant3 1084 |
. . . . . . . 8
Odd Odd
|
49 | 48 | adantl 482 |
. . . . . . 7
Odd
Odd |
50 | 46, 49 | mpbird 247 |
. . . . . 6
Odd
Odd
|
51 | 50 | ex 450 |
. . . . 5
Odd
Odd |
52 | 51 | a1i 11 |
. . . 4
Even
Odd
Odd |
53 | 52 | rexlimdvv 3037 |
. . 3
Even Odd Odd
|
54 | 53 | imp 445 |
. 2
Even
Odd
Odd |
55 | 1, 54 | sylbi 207 |
1
GoldbachEven |