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 ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) = 2 5 6

Proof

Step Hyp Ref Expression
1 4nn ⊢ 4 ∈ ℕ
2 fmtnosqrt ⊢ ( 4 ∈ ℕ → ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) = ( 2 ↑ ( 2 ↑ ( 4 − 1 ) ) ) )
3 1 2 ax-mp ⊢ ( ⌊ ‘ ( √ ‘ ( 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 ⊢ ( ⌊ ‘ ( √ ‘ ( FermatNo ‘ 4 ) ) ) = 2 5 6