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{\mathrm{FermatNo}\left(4\right)}⌋=256$$

Proof

Step	Hyp	Ref	Expression
1		4nn	$$⊢4\in \mathbb{N}$$
2		fmtnosqrt	$$⊢4\in \mathbb{N}\to ⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋=2^{2^{4-1}}$$
3	1 2	ax-mp	$$⊢⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋=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=256$$
10	8 9	eqtri	$$⊢2^{2^{4-1}}=256$$
11	3 10	eqtri	$$⊢⌊\sqrt{\mathrm{FermatNo}\left(4\right)}⌋=256$$