Step |
Hyp |
Ref |
Expression |
1 |
|
3nn0 |
⊢ 3 ∈ ℕ0 |
2 |
|
fmtno |
⊢ ( 3 ∈ ℕ0 → ( 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 ∈ ℕ0 |
10 |
|
5nn0 |
⊢ 5 ∈ ℕ0 |
11 |
9 10
|
deccl |
⊢ ; 2 5 ∈ ℕ0 |
12 |
|
6nn0 |
⊢ 6 ∈ ℕ0 |
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 |