Step | Hyp | Ref
| Expression |
1 | | fmtnorn 41446 |
. 2
FermatNo FermatNo |
2 | | fmtnorn 41446 |
. 2
FermatNo FermatNo |
3 | | 2a1 28 |
. . . . . . . 8
FermatNo
|
4 | 3 | 2a1d 26 |
. . . . . . 7
FermatNo FermatNo
|
5 | | fmtnonn 41443 |
. . . . . . . . . . . 12
FermatNo |
6 | 5 | ad2antrl 764 |
. . . . . . . . . . 11
FermatNo |
7 | 6 | adantr 481 |
. . . . . . . . . 10
FermatNo
FermatNo FermatNo |
8 | | eleq1 2689 |
. . . . . . . . . . 11
FermatNo FermatNo
|
9 | 8 | ad2antll 765 |
. . . . . . . . . 10
FermatNo
FermatNo FermatNo
|
10 | 7, 9 | mpbid 222 |
. . . . . . . . 9
FermatNo
FermatNo |
11 | | fmtnonn 41443 |
. . . . . . . . . . . 12
FermatNo |
12 | 11 | ad2antll 765 |
. . . . . . . . . . 11
FermatNo |
13 | 12 | adantr 481 |
. . . . . . . . . 10
FermatNo
FermatNo FermatNo |
14 | | eleq1 2689 |
. . . . . . . . . . 11
FermatNo FermatNo
|
15 | 14 | ad2antrl 764 |
. . . . . . . . . 10
FermatNo
FermatNo FermatNo
|
16 | 13, 15 | mpbid 222 |
. . . . . . . . 9
FermatNo
FermatNo |
17 | | simpll 790 |
. . . . . . . . . . . . . . 15
FermatNo FermatNo |
18 | | simplr 792 |
. . . . . . . . . . . . . . 15
FermatNo FermatNo |
19 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
FermatNo FermatNo |
20 | 19 | con3i 150 |
. . . . . . . . . . . . . . . . 17
FermatNo FermatNo |
21 | 20 | adantl 482 |
. . . . . . . . . . . . . . . 16
FermatNo FermatNo
|
22 | 21 | neqned 2801 |
. . . . . . . . . . . . . . 15
FermatNo FermatNo |
23 | | goldbachth 41459 |
. . . . . . . . . . . . . . 15
FermatNo FermatNo |
24 | 17, 18, 22, 23 | syl3anc 1326 |
. . . . . . . . . . . . . 14
FermatNo FermatNo FermatNo FermatNo |
25 | 24 | ex 450 |
. . . . . . . . . . . . 13
FermatNo FermatNo
FermatNo FermatNo |
26 | | eqeq12 2635 |
. . . . . . . . . . . . . . . 16
FermatNo
FermatNo
FermatNo FermatNo
|
27 | 26 | notbid 308 |
. . . . . . . . . . . . . . 15
FermatNo
FermatNo
FermatNo FermatNo |
28 | | oveq12 6659 |
. . . . . . . . . . . . . . . 16
FermatNo
FermatNo
FermatNo FermatNo |
29 | 28 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
FermatNo
FermatNo
FermatNo FermatNo |
30 | 27, 29 | imbi12d 334 |
. . . . . . . . . . . . . 14
FermatNo
FermatNo
FermatNo FermatNo FermatNo
FermatNo
|
31 | 30 | ancoms 469 |
. . . . . . . . . . . . 13
FermatNo
FermatNo
FermatNo FermatNo FermatNo
FermatNo
|
32 | 25, 31 | syl5ibcom 235 |
. . . . . . . . . . . 12
FermatNo FermatNo
|
33 | 32 | com23 86 |
. . . . . . . . . . 11
FermatNo FermatNo |
34 | 33 | impcom 446 |
. . . . . . . . . 10
FermatNo
FermatNo
|
35 | 34 | imp 445 |
. . . . . . . . 9
FermatNo
FermatNo |
36 | | prmnn 15388 |
. . . . . . . . . . . 12
|
37 | | coprmdvds1 15365 |
. . . . . . . . . . . . 13
|
38 | 37 | imp 445 |
. . . . . . . . . . . 12
|
39 | 36, 38 | syl3anr1 1378 |
. . . . . . . . . . 11
|
40 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
41 | | 1nprm 15392 |
. . . . . . . . . . . . . . . . 17
|
42 | 41 | pm2.21i 116 |
. . . . . . . . . . . . . . . 16
|
43 | 40, 42 | syl6bi 243 |
. . . . . . . . . . . . . . 15
|
44 | 43 | com12 32 |
. . . . . . . . . . . . . 14
|
45 | 44 | a1d 25 |
. . . . . . . . . . . . 13
|
46 | 45 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
47 | 46 | impcom 446 |
. . . . . . . . . . 11
|
48 | 39, 47 | mpd 15 |
. . . . . . . . . 10
|
49 | 48 | ex 450 |
. . . . . . . . 9
|
50 | 10, 16, 35, 49 | syl3anc 1326 |
. . . . . . . 8
FermatNo
FermatNo
|
51 | 50 | exp43 640 |
. . . . . . 7
FermatNo FermatNo
|
52 | 4, 51 | pm2.61i 176 |
. . . . . 6
FermatNo
FermatNo
|
53 | 52 | rexlimdva 3031 |
. . . . 5
FermatNo FermatNo
|
54 | 53 | com23 86 |
. . . 4
FermatNo FermatNo
|
55 | 54 | rexlimiv 3027 |
. . 3
FermatNo FermatNo
|
56 | 55 | imp 445 |
. 2
FermatNo FermatNo
|
57 | 1, 2, 56 | syl2anb 496 |
1
FermatNo FermatNo
|