Metamath Proof Explorer


Theorem fmtno3

Description: The 3 rd Fermat number, see remark in ApostolNT p. 7. (Contributed by AV, 13-Jun-2021)

Ref Expression
Assertion fmtno3 FermatNo3=257

Proof

Step Hyp Ref Expression
1 3nn0 30
2 fmtno 30FermatNo3=223+1
3 1 2 ax-mp FermatNo3=223+1
4 cu2 23=8
5 4 oveq2i 223=28
6 5 oveq1i 223+1=28+1
7 2exp8 28=256
8 7 oveq1i 28+1=256+1
9 2nn0 20
10 5nn0 50
11 9 10 deccl 250
12 6nn0 60
13 6p1e7 6+1=7
14 eqid 256=256
15 11 12 13 14 decsuc 256+1=257
16 6 8 15 3eqtri 223+1=257
17 3 16 eqtri FermatNo3=257