Description: The 3 rd Fermat number, see remark in ApostolNT p. 7. (Contributed by AV, 13-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | fmtno3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3nn0 | |
|
2 | fmtno | |
|
3 | 1 2 | ax-mp | |
4 | cu2 | |
|
5 | 4 | oveq2i | |
6 | 5 | oveq1i | |
7 | 2exp8 | |
|
8 | 7 | oveq1i | |
9 | 2nn0 | |
|
10 | 5nn0 | |
|
11 | 9 10 | deccl | |
12 | 6nn0 | |
|
13 | 6p1e7 | |
|
14 | eqid | |
|
15 | 11 12 13 14 | decsuc | |
16 | 6 8 15 | 3eqtri | |
17 | 3 16 | eqtri | |