Step |
Hyp |
Ref |
Expression |
1 |
|
3nn0 |
|- 3 e. NN0 |
2 |
|
fmtno |
|- ( 3 e. NN0 -> ( FermatNo ` 3 ) = ( ( 2 ^ ( 2 ^ 3 ) ) + 1 ) ) |
3 |
1 2
|
ax-mp |
|- ( FermatNo ` 3 ) = ( ( 2 ^ ( 2 ^ 3 ) ) + 1 ) |
4 |
|
cu2 |
|- ( 2 ^ 3 ) = 8 |
5 |
4
|
oveq2i |
|- ( 2 ^ ( 2 ^ 3 ) ) = ( 2 ^ 8 ) |
6 |
5
|
oveq1i |
|- ( ( 2 ^ ( 2 ^ 3 ) ) + 1 ) = ( ( 2 ^ 8 ) + 1 ) |
7 |
|
2exp8 |
|- ( 2 ^ 8 ) = ; ; 2 5 6 |
8 |
7
|
oveq1i |
|- ( ( 2 ^ 8 ) + 1 ) = ( ; ; 2 5 6 + 1 ) |
9 |
|
2nn0 |
|- 2 e. NN0 |
10 |
|
5nn0 |
|- 5 e. NN0 |
11 |
9 10
|
deccl |
|- ; 2 5 e. NN0 |
12 |
|
6nn0 |
|- 6 e. NN0 |
13 |
|
6p1e7 |
|- ( 6 + 1 ) = 7 |
14 |
|
eqid |
|- ; ; 2 5 6 = ; ; 2 5 6 |
15 |
11 12 13 14
|
decsuc |
|- ( ; ; 2 5 6 + 1 ) = ; ; 2 5 7 |
16 |
6 8 15
|
3eqtri |
|- ( ( 2 ^ ( 2 ^ 3 ) ) + 1 ) = ; ; 2 5 7 |
17 |
3 16
|
eqtri |
|- ( FermatNo ` 3 ) = ; ; 2 5 7 |