Proof of Theorem fmtnoprmfac1
Step | Hyp | Ref
| Expression |
1 | | breq1 4656 |
. . . . . . 7
FermatNo FermatNo |
2 | 1 | adantr 481 |
. . . . . 6
FermatNo
FermatNo |
3 | | nnnn0 11299 |
. . . . . . . . 9
|
4 | | fmtnoodd 41445 |
. . . . . . . . 9
FermatNo |
5 | 3, 4 | syl 17 |
. . . . . . . 8
FermatNo |
6 | 5 | adantl 482 |
. . . . . . 7
FermatNo |
7 | 6 | pm2.21d 118 |
. . . . . 6
FermatNo
|
8 | 2, 7 | sylbid 230 |
. . . . 5
FermatNo
|
9 | 8 | a1d 25 |
. . . 4
FermatNo
|
10 | 9 | ex 450 |
. . 3
FermatNo
|
11 | 10 | 3impd 1281 |
. 2
FermatNo
|
12 | | simpr1 1067 |
. . . . 5
FermatNo |
13 | | neqne 2802 |
. . . . . . . . . 10
|
14 | 13 | anim2i 593 |
. . . . . . . . 9
|
15 | | eldifsn 4317 |
. . . . . . . . 9
|
16 | 14, 15 | sylibr 224 |
. . . . . . . 8
|
17 | 16 | ex 450 |
. . . . . . 7
|
18 | 17 | 3ad2ant2 1083 |
. . . . . 6
FermatNo
|
19 | 18 | impcom 446 |
. . . . 5
FermatNo
|
20 | | simpr3 1069 |
. . . . 5
FermatNo FermatNo |
21 | | fmtnoprmfac1lem 41476 |
. . . . 5
FermatNo |
22 | 12, 19, 20, 21 | syl3anc 1326 |
. . . 4
FermatNo
|
23 | | prmnn 15388 |
. . . . . . . 8
|
24 | 23 | ad2antll 765 |
. . . . . . 7
|
25 | | 2z 11409 |
. . . . . . . 8
|
26 | 25 | a1i 11 |
. . . . . . 7
|
27 | 13 | necomd 2849 |
. . . . . . . . 9
|
28 | 27 | adantr 481 |
. . . . . . . 8
|
29 | | 2prm 15405 |
. . . . . . . . . . . 12
|
30 | 29 | a1i 11 |
. . . . . . . . . . 11
|
31 | 30 | anim1i 592 |
. . . . . . . . . 10
|
32 | 31 | adantl 482 |
. . . . . . . . 9
|
33 | | prmrp 15424 |
. . . . . . . . 9
|
34 | 32, 33 | syl 17 |
. . . . . . . 8
|
35 | 28, 34 | mpbird 247 |
. . . . . . 7
|
36 | | odzphi 15501 |
. . . . . . 7
|
37 | 24, 26, 35, 36 | syl3anc 1326 |
. . . . . 6
|
38 | | phiprm 15482 |
. . . . . . . . 9
|
39 | 38 | ad2antll 765 |
. . . . . . . 8
|
40 | 39 | breq2d 4665 |
. . . . . . 7
|
41 | | breq1 4656 |
. . . . . . . . . . 11
|
42 | 41 | adantl 482 |
. . . . . . . . . 10
|
43 | | 2nn 11185 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
45 | | peano2nn 11032 |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
|
47 | 44, 46 | nnexpcld 13030 |
. . . . . . . . . . . . . . 15
|
48 | 23 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
|
49 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . 17
|
50 | | eluzle 11700 |
. . . . . . . . . . . . . . . . 17
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . 16
|
52 | | nn0ge2m1nn 11360 |
. . . . . . . . . . . . . . . 16
|
53 | 48, 51, 52 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
54 | 47, 53 | anim12i 590 |
. . . . . . . . . . . . . 14
|
55 | 54 | adantl 482 |
. . . . . . . . . . . . 13
|
56 | | nndivides 14990 |
. . . . . . . . . . . . 13
|
57 | 55, 56 | syl 17 |
. . . . . . . . . . . 12
|
58 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . 15
|
60 | 23 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
|
61 | 60 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
63 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . 17
|
64 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . 19
|
65 | 64 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
66 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | 3, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | 44, 67 | nnexpcld 13030 |
. . . . . . . . . . . . . . . . . . . . 21
|
69 | 68 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
|
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
72 | 65, 71 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
|
73 | 62, 63, 72 | subadd2d 10411 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | adantll 750 |
. . . . . . . . . . . . . . 15
|
75 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . 15
|
77 | 59, 74, 76 | 3bitrd 294 |
. . . . . . . . . . . . . 14
|
78 | 77 | rexbidva 3049 |
. . . . . . . . . . . . 13
|
79 | 78 | biimpd 219 |
. . . . . . . . . . . 12
|
80 | 57, 79 | sylbid 230 |
. . . . . . . . . . 11
|
81 | 80 | adantr 481 |
. . . . . . . . . 10
|
82 | 42, 81 | sylbid 230 |
. . . . . . . . 9
|
83 | 82 | ex 450 |
. . . . . . . 8
|
84 | 83 | com23 86 |
. . . . . . 7
|
85 | 40, 84 | sylbid 230 |
. . . . . 6
|
86 | 37, 85 | mpd 15 |
. . . . 5
|
87 | 86 | 3adantr3 1222 |
. . . 4
FermatNo |
88 | 22, 87 | mpd 15 |
. . 3
FermatNo
|
89 | 88 | ex 450 |
. 2
FermatNo
|
90 | 11, 89 | pm2.61i 176 |
1
FermatNo
|