Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . . 5
|
2 | | 4z 11411 |
. . . . 5
|
3 | | 2re 11090 |
. . . . . 6
|
4 | | 4re 11097 |
. . . . . 6
|
5 | | 2lt4 11198 |
. . . . . 6
|
6 | 3, 4, 5 | ltleii 10160 |
. . . . 5
|
7 | | eluz2 11693 |
. . . . 5
|
8 | 1, 2, 6, 7 | mpbir3an 1244 |
. . . 4
|
9 | | fmtnoprmfac2 41479 |
. . . 4
FermatNo
|
10 | 8, 9 | mp3an1 1411 |
. . 3
FermatNo
|
11 | | elnnuz 11724 |
. . . . . . 7
|
12 | | 4nn 11187 |
. . . . . . . . . 10
|
13 | | nnuz 11723 |
. . . . . . . . . 10
|
14 | 12, 13 | eleqtri 2699 |
. . . . . . . . 9
|
15 | | fzouzsplit 12503 |
. . . . . . . . 9
..^ |
16 | 14, 15 | ax-mp 5 |
. . . . . . . 8
..^ |
17 | 16 | eleq2i 2693 |
. . . . . . 7
..^ |
18 | | elun 3753 |
. . . . . . . 8
..^ ..^ |
19 | | fzo1to4tp 12556 |
. . . . . . . . . . 11
..^ |
20 | 19 | eleq2i 2693 |
. . . . . . . . . 10
..^ |
21 | | vex 3203 |
. . . . . . . . . . 11
|
22 | 21 | eltp 4230 |
. . . . . . . . . 10
|
23 | 20, 22 | bitri 264 |
. . . . . . . . 9
..^ |
24 | 23 | orbi1i 542 |
. . . . . . . 8
..^ |
25 | 18, 24 | bitri 264 |
. . . . . . 7
..^ |
26 | 11, 17, 25 | 3bitri 286 |
. . . . . 6
|
27 | | 4p2e6 11162 |
. . . . . . . . . . . . 13
|
28 | 27 | oveq2i 6661 |
. . . . . . . . . . . 12
|
29 | | 2exp6 15795 |
. . . . . . . . . . . 12
; |
30 | 28, 29 | eqtri 2644 |
. . . . . . . . . . 11
; |
31 | 30 | oveq2i 6661 |
. . . . . . . . . 10
; |
32 | 31 | oveq1i 6660 |
. . . . . . . . 9
; |
33 | 32 | eqeq2i 2634 |
. . . . . . . 8
; |
34 | | simpl 473 |
. . . . . . . . . . . . . . 15
;
; |
35 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
; ; |
36 | | 6nn0 11313 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | | 4nn0 11311 |
. . . . . . . . . . . . . . . . . . . . . 22
|
38 | 36, 37 | deccl 11512 |
. . . . . . . . . . . . . . . . . . . . 21
; |
39 | 38 | nn0cni 11304 |
. . . . . . . . . . . . . . . . . . . 20
; |
40 | 39 | mulid2i 10043 |
. . . . . . . . . . . . . . . . . . 19
; ; |
41 | 35, 40 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
; ; |
42 | 41 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
; ; |
43 | | 4p1e5 11154 |
. . . . . . . . . . . . . . . . . 18
|
44 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
; ; |
45 | 36, 37, 43, 44 | decsuc 11535 |
. . . . . . . . . . . . . . . . 17
; ; |
46 | 42, 45 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
; ; |
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . 15
; ; ; |
48 | 34, 47 | eqtrd 2656 |
. . . . . . . . . . . . . 14
;
; |
49 | 48 | ex 450 |
. . . . . . . . . . . . 13
;
; |
50 | | simpl 473 |
. . . . . . . . . . . . . . 15
;
; |
51 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
; ; |
52 | | 2nn0 11309 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | | 6cn 11102 |
. . . . . . . . . . . . . . . . . . . . . 22
|
54 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . . . . . 22
|
55 | | 6t2e12 11641 |
. . . . . . . . . . . . . . . . . . . . . 22
; |
56 | 53, 54, 55 | mulcomli 10047 |
. . . . . . . . . . . . . . . . . . . . 21
; |
57 | 56 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . 20
; |
58 | | 4cn 11098 |
. . . . . . . . . . . . . . . . . . . . . 22
|
59 | | 4t2e8 11181 |
. . . . . . . . . . . . . . . . . . . . . 22
|
60 | 58, 54, 59 | mulcomli 10047 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | 60 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 36, 37, 52, 57, 61 | decmul10add 11593 |
. . . . . . . . . . . . . . . . . . 19
; ;; |
63 | 51, 62 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
; ;; |
64 | 63 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
; ;; |
65 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . . . 19
|
66 | 65, 52 | deccl 11512 |
. . . . . . . . . . . . . . . . . 18
; |
67 | | 8nn0 11315 |
. . . . . . . . . . . . . . . . . 18
|
68 | | 8p1e9 11158 |
. . . . . . . . . . . . . . . . . 18
|
69 | | 0nn0 11307 |
. . . . . . . . . . . . . . . . . . 19
|
70 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
;; ;; |
71 | | 8cn 11106 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | addid2i 10224 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 66, 69, 67, 70, 72 | decaddi 11579 |
. . . . . . . . . . . . . . . . . 18
;; ;; |
74 | 66, 67, 68, 73 | decsuc 11535 |
. . . . . . . . . . . . . . . . 17
;; ;; |
75 | 64, 74 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
; ;; |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . 15
; ; ;; |
77 | 50, 76 | eqtrd 2656 |
. . . . . . . . . . . . . 14
;
;; |
78 | 77 | ex 450 |
. . . . . . . . . . . . 13
;
;; |
79 | | simpl 473 |
. . . . . . . . . . . . . . 15
;
; |
80 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
; ; |
81 | | 3nn0 11310 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | | 6t3e18 11642 |
. . . . . . . . . . . . . . . . . . . . 21
; |
83 | | 3cn 11095 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 53, 83 | mulcomi 10046 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | 82, 84 | eqtr3i 2646 |
. . . . . . . . . . . . . . . . . . . 20
; |
86 | | 4t3e12 11632 |
. . . . . . . . . . . . . . . . . . . . 21
; |
87 | 58, 83 | mulcomi 10046 |
. . . . . . . . . . . . . . . . . . . . 21
|
88 | 86, 87 | eqtr3i 2646 |
. . . . . . . . . . . . . . . . . . . 20
; |
89 | 36, 37, 81, 85, 88 | decmul10add 11593 |
. . . . . . . . . . . . . . . . . . 19
; ;; ; |
90 | 80, 89 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
; ;; ; |
91 | 90 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
; ;; ; |
92 | | 9nn0 11316 |
. . . . . . . . . . . . . . . . . . 19
|
93 | 65, 92 | deccl 11512 |
. . . . . . . . . . . . . . . . . 18
; |
94 | | 2p1e3 11151 |
. . . . . . . . . . . . . . . . . 18
|
95 | 65, 67 | deccl 11512 |
. . . . . . . . . . . . . . . . . . 19
; |
96 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
;; ;; |
97 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
; ; |
98 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
; ; |
99 | 65, 67, 68, 98 | decsuc 11535 |
. . . . . . . . . . . . . . . . . . 19
; ; |
100 | 54 | addid2i 10224 |
. . . . . . . . . . . . . . . . . . 19
|
101 | 95, 69, 65, 52, 96, 97, 99, 100 | decadd 11570 |
. . . . . . . . . . . . . . . . . 18
;; ; ;; |
102 | 93, 52, 94, 101 | decsuc 11535 |
. . . . . . . . . . . . . . . . 17
;; ; ;; |
103 | 91, 102 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
; ;; |
104 | 103 | adantl 482 |
. . . . . . . . . . . . . . 15
; ; ;; |
105 | 79, 104 | eqtrd 2656 |
. . . . . . . . . . . . . 14
;
;; |
106 | 105 | ex 450 |
. . . . . . . . . . . . 13
;
;; |
107 | 49, 78, 106 | 3orim123d 1407 |
. . . . . . . . . . . 12
;
; ;; ;; |
108 | 107 | a1i 11 |
. . . . . . . . . . 11
FermatNo ;
; ;; ;; |
109 | 108 | com13 88 |
. . . . . . . . . 10
;
FermatNo ; ;; ;; |
110 | | fmtno4sqrt 41483 |
. . . . . . . . . . . . 13
FermatNo ;; |
111 | 110 | breq2i 4661 |
. . . . . . . . . . . 12
FermatNo
;; |
112 | | breq1 4656 |
. . . . . . . . . . . . . 14
; ;; ; ;; |
113 | 112 | adantl 482 |
. . . . . . . . . . . . 13
; ;;
; ;; |
114 | | eluz2 11693 |
. . . . . . . . . . . . . . . . 17
|
115 | | 6t4e24 11643 |
. . . . . . . . . . . . . . . . . . . . . . 23
; |
116 | 53, 58, 115 | mulcomli 10047 |
. . . . . . . . . . . . . . . . . . . . . 22
; |
117 | 52, 37, 43, 116 | decsuc 11535 |
. . . . . . . . . . . . . . . . . . . . 21
; |
118 | | 4t4e16 11633 |
. . . . . . . . . . . . . . . . . . . . 21
; |
119 | 37, 36, 37, 44, 36, 65, 117, 118 | decmul2c 11589 |
. . . . . . . . . . . . . . . . . . . 20
; ;; |
120 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . 22
|
121 | 38 | nn0rei 11303 |
. . . . . . . . . . . . . . . . . . . . . . . 24
; |
122 | 36, 12 | decnncl 11518 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
; |
123 | 122 | nngt0i 11054 |
. . . . . . . . . . . . . . . . . . . . . . . 24
; |
124 | 121, 123 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . 23
; ; |
125 | 124 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
; ; |
126 | | lemul1 10875 |
. . . . . . . . . . . . . . . . . . . . . 22
; ; ; ; |
127 | 4, 120, 125, 126 | mp3an2i 1429 |
. . . . . . . . . . . . . . . . . . . . 21
; ; |
128 | 127 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
; ; |
129 | 119, 128 | syl5eqbrr 4689 |
. . . . . . . . . . . . . . . . . . 19
;; ; |
130 | | 5nn0 11312 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
131 | 52, 130 | deccl 11512 |
. . . . . . . . . . . . . . . . . . . . . 22
; |
132 | 131, 36 | deccl 11512 |
. . . . . . . . . . . . . . . . . . . . 21
;; |
133 | 132 | nn0zi 11402 |
. . . . . . . . . . . . . . . . . . . 20
;; |
134 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
|
135 | 38 | nn0zi 11402 |
. . . . . . . . . . . . . . . . . . . . . . 23
; |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
; |
137 | 134, 136 | zmulcld 11488 |
. . . . . . . . . . . . . . . . . . . . 21
; |
138 | 137 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
; |
139 | | zleltp1 11428 |
. . . . . . . . . . . . . . . . . . . 20
;; ; ;; ;
;; ; |
140 | 133, 138,
139 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
;;
;
;; ; |
141 | 129, 140 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
;; ; |
142 | 141 | 3adant1 1079 |
. . . . . . . . . . . . . . . . 17
;; ; |
143 | 114, 142 | sylbi 207 |
. . . . . . . . . . . . . . . 16
;; ; |
144 | 132 | nn0rei 11303 |
. . . . . . . . . . . . . . . . . 18
;; |
145 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . 17
;; |
146 | | eluzelre 11698 |
. . . . . . . . . . . . . . . . . . 19
|
147 | 121 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
; |
148 | 146, 147 | remulcld 10070 |
. . . . . . . . . . . . . . . . . 18
; |
149 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . 18
;
; |
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . 17
; |
151 | 145, 150 | ltnled 10184 |
. . . . . . . . . . . . . . . 16
;; ;
; ;; |
152 | 143, 151 | mpbid 222 |
. . . . . . . . . . . . . . 15
; ;; |
153 | 152 | pm2.21d 118 |
. . . . . . . . . . . . . 14
; ;;
; ;; ;; |
154 | 153 | adantr 481 |
. . . . . . . . . . . . 13
; ; ;;
; ;; ;; |
155 | 113, 154 | sylbid 230 |
. . . . . . . . . . . 12
; ;;
; ;; ;; |
156 | 111, 155 | syl5bi 232 |
. . . . . . . . . . 11
; FermatNo ; ;; ;; |
157 | 156 | ex 450 |
. . . . . . . . . 10
; FermatNo ; ;; ;; |
158 | 109, 157 | jaoi 394 |
. . . . . . . . 9
; FermatNo ; ;; ;; |
159 | 158 | adantr 481 |
. . . . . . . 8
FermatNo ;
FermatNo ; ;; ;; |
160 | 33, 159 | syl5bi 232 |
. . . . . . 7
FermatNo
FermatNo ; ;; ;; |
161 | 160 | ex 450 |
. . . . . 6
FermatNo
FermatNo ; ;; ;; |
162 | 26, 161 | sylbi 207 |
. . . . 5
FermatNo
FermatNo ; ;; ;; |
163 | 162 | com12 32 |
. . . 4
FermatNo
FermatNo ; ;; ;; |
164 | 163 | rexlimdv 3030 |
. . 3
FermatNo
FermatNo ; ;; ;; |
165 | 10, 164 | mpd 15 |
. 2
FermatNo
FermatNo ; ;; ;; |
166 | 165 | 3impia 1261 |
1
FermatNo
FermatNo
; ;; ;; |