Step |
Hyp |
Ref |
Expression |
1 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
2 |
|
fmtno |
⊢ ( 2 ∈ ℕ0 → ( FermatNo ‘ 2 ) = ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 ) ) |
3 |
1 2
|
ax-mp |
⊢ ( FermatNo ‘ 2 ) = ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 ) |
4 |
|
sq2 |
⊢ ( 2 ↑ 2 ) = 4 |
5 |
4
|
oveq2i |
⊢ ( 2 ↑ ( 2 ↑ 2 ) ) = ( 2 ↑ 4 ) |
6 |
5
|
oveq1i |
⊢ ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 ) = ( ( 2 ↑ 4 ) + 1 ) |
7 |
|
2exp4 |
⊢ ( 2 ↑ 4 ) = ; 1 6 |
8 |
7
|
oveq1i |
⊢ ( ( 2 ↑ 4 ) + 1 ) = ( ; 1 6 + 1 ) |
9 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
10 |
|
6nn0 |
⊢ 6 ∈ ℕ0 |
11 |
|
6p1e7 |
⊢ ( 6 + 1 ) = 7 |
12 |
|
eqid |
⊢ ; 1 6 = ; 1 6 |
13 |
9 10 11 12
|
decsuc |
⊢ ( ; 1 6 + 1 ) = ; 1 7 |
14 |
6 8 13
|
3eqtri |
⊢ ( ( 2 ↑ ( 2 ↑ 2 ) ) + 1 ) = ; 1 7 |
15 |
3 14
|
eqtri |
⊢ ( FermatNo ‘ 2 ) = ; 1 7 |