Metamath Proof Explorer

Theorem fmtno4sqrt

Description: The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021)

Ref Expression
Assertion fmtno4sqrt 
|- ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) = ; ; 2 5 6

Proof

Step Hyp Ref Expression
1 4nn 
 |-  4 e. NN
2 fmtnosqrt 
 |-  ( 4 e. NN -> ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) = ( 2 ^ ( 2 ^ ( 4 - 1 ) ) ) )
3 1 2 ax-mp 
 |-  ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) = ( 2 ^ ( 2 ^ ( 4 - 1 ) ) )
4 4m1e3 
 |-  ( 4 - 1 ) = 3
5 4 oveq2i 
 |-  ( 2 ^ ( 4 - 1 ) ) = ( 2 ^ 3 )
6 cu2 
 |-  ( 2 ^ 3 ) = 8
7 5 6 eqtri 
 |-  ( 2 ^ ( 4 - 1 ) ) = 8
8 7 oveq2i 
 |-  ( 2 ^ ( 2 ^ ( 4 - 1 ) ) ) = ( 2 ^ 8 )
9 2exp8 
 |-  ( 2 ^ 8 ) = ; ; 2 5 6
10 8 9 eqtri 
 |-  ( 2 ^ ( 2 ^ ( 4 - 1 ) ) ) = ; ; 2 5 6
11 3 10 eqtri 
 |-  ( |_ ` ( sqrt ` ( FermatNo ` 4 ) ) ) = ; ; 2 5 6