Proof of Theorem goldbachthlem2
Step | Hyp | Ref
| Expression |
1 | | fmtnonn 41443 |
. . . . . 6
FermatNo |
2 | 1 | nnzd 11481 |
. . . . 5
FermatNo |
3 | | fmtnonn 41443 |
. . . . . 6
FermatNo |
4 | 3 | nnzd 11481 |
. . . . 5
FermatNo |
5 | 2, 4 | anim12ci 591 |
. . . 4
FermatNo FermatNo |
6 | 5 | 3adant3 1081 |
. . 3
FermatNo FermatNo |
7 | | gcddvds 15225 |
. . 3
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo
FermatNo |
8 | 6, 7 | syl 17 |
. 2
FermatNo FermatNo
FermatNo
FermatNo FermatNo FermatNo |
9 | | goldbachthlem1 41457 |
. . . 4
FermatNo FermatNo |
10 | | gcdcl 15228 |
. . . . . . 7
FermatNo FermatNo FermatNo
FermatNo |
11 | 6, 10 | syl 17 |
. . . . . 6
FermatNo FermatNo |
12 | 11 | nn0zd 11480 |
. . . . 5
FermatNo FermatNo |
13 | 4 | 3ad2ant2 1083 |
. . . . 5
FermatNo |
14 | | 2z 11409 |
. . . . . . . 8
|
15 | 14 | a1i 11 |
. . . . . . 7
|
16 | 2, 15 | zsubcld 11487 |
. . . . . 6
FermatNo |
17 | 16 | 3ad2ant1 1082 |
. . . . 5
FermatNo |
18 | | dvdstr 15018 |
. . . . 5
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo
FermatNo
FermatNo
FermatNo FermatNo FermatNo
FermatNo |
19 | 12, 13, 17, 18 | syl3anc 1326 |
. . . 4
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo
FermatNo |
20 | 9, 19 | mpan2d 710 |
. . 3
FermatNo FermatNo
FermatNo
FermatNo FermatNo FermatNo |
21 | 2 | 3ad2ant1 1082 |
. . . . . 6
FermatNo |
22 | | dvds2sub 15016 |
. . . . . 6
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo
FermatNo
FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo |
23 | 12, 21, 17, 22 | syl3anc 1326 |
. . . . 5
FermatNo
FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo
FermatNo FermatNo |
24 | 23 | ancomsd 470 |
. . . 4
FermatNo
FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo
FermatNo FermatNo |
25 | 1 | nncnd 11036 |
. . . . . . . 8
FermatNo |
26 | 25 | 3ad2ant1 1082 |
. . . . . . 7
FermatNo |
27 | | 2cnd 11093 |
. . . . . . 7
|
28 | 26, 27 | nncand 10397 |
. . . . . 6
FermatNo FermatNo |
29 | 28 | breq2d 4665 |
. . . . 5
FermatNo FermatNo
FermatNo FermatNo
FermatNo FermatNo |
30 | | 2prm 15405 |
. . . . . . 7
|
31 | 1, 3 | anim12ci 591 |
. . . . . . . . 9
FermatNo FermatNo |
32 | 31 | 3adant3 1081 |
. . . . . . . 8
FermatNo FermatNo |
33 | | gcdnncl 15229 |
. . . . . . . 8
FermatNo FermatNo FermatNo
FermatNo |
34 | 32, 33 | syl 17 |
. . . . . . 7
FermatNo FermatNo |
35 | | dvdsprime 15400 |
. . . . . . 7
FermatNo FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo
FermatNo |
36 | 30, 34, 35 | sylancr 695 |
. . . . . 6
FermatNo FermatNo
FermatNo FermatNo FermatNo
FermatNo |
37 | 5, 7 | syl 17 |
. . . . . . . . 9
FermatNo
FermatNo FermatNo FermatNo FermatNo
FermatNo |
38 | | breq1 4656 |
. . . . . . . . . . . . . 14
FermatNo FermatNo FermatNo
FermatNo FermatNo
FermatNo |
39 | 38 | adantl 482 |
. . . . . . . . . . . . 13
FermatNo
FermatNo
FermatNo FermatNo
FermatNo FermatNo |
40 | | fmtnoodd 41445 |
. . . . . . . . . . . . . . 15
FermatNo |
41 | 40 | pm2.21d 118 |
. . . . . . . . . . . . . 14
FermatNo FermatNo
FermatNo |
42 | 41 | ad2antrr 762 |
. . . . . . . . . . . . 13
FermatNo
FermatNo
FermatNo FermatNo
FermatNo |
43 | 39, 42 | sylbid 230 |
. . . . . . . . . . . 12
FermatNo
FermatNo
FermatNo FermatNo
FermatNo
FermatNo FermatNo |
44 | 43 | ex 450 |
. . . . . . . . . . 11
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
45 | 44 | com23 86 |
. . . . . . . . . 10
FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo FermatNo |
46 | 45 | adantld 483 |
. . . . . . . . 9
FermatNo FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo FermatNo FermatNo |
47 | 37, 46 | mpd 15 |
. . . . . . . 8
FermatNo
FermatNo FermatNo
FermatNo |
48 | 47 | 3adant3 1081 |
. . . . . . 7
FermatNo FermatNo FermatNo FermatNo |
49 | | gcdcom 15235 |
. . . . . . . . . 10
FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo |
50 | 6, 49 | syl 17 |
. . . . . . . . 9
FermatNo FermatNo FermatNo FermatNo |
51 | 50 | eqeq1d 2624 |
. . . . . . . 8
FermatNo FermatNo FermatNo FermatNo |
52 | 51 | biimpd 219 |
. . . . . . 7
FermatNo FermatNo FermatNo FermatNo |
53 | 48, 52 | jaod 395 |
. . . . . 6
FermatNo
FermatNo FermatNo
FermatNo
FermatNo FermatNo |
54 | 36, 53 | sylbid 230 |
. . . . 5
FermatNo FermatNo
FermatNo FermatNo |
55 | 29, 54 | sylbid 230 |
. . . 4
FermatNo FermatNo
FermatNo FermatNo FermatNo FermatNo |
56 | 24, 55 | syld 47 |
. . 3
FermatNo
FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo |
57 | 20, 56 | syland 498 |
. 2
FermatNo
FermatNo FermatNo FermatNo FermatNo
FermatNo FermatNo FermatNo |
58 | 8, 57 | mpd 15 |
1
FermatNo FermatNo |