fmtnosqrt

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

		Ref	Expression
	Assertion	fmtnosqrt	$⊢ N \in ℕ \to ⌊\sqrt{FermatNo (N)}⌋ = 2^{2^{N - 1}}$

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
2		fmtno	$⊢ N \in ℕ_{0} \to FermatNo (N) = 2^{2^{N}} + 1$
3	1 2	syl	$⊢ N \in ℕ \to FermatNo (N) = 2^{2^{N}} + 1$
4	3	fveq2d	$⊢ N \in ℕ \to \sqrt{FermatNo (N)} = \sqrt{2^{2^{N}} + 1}$
5	4	fveq2d	$⊢ N \in ℕ \to ⌊\sqrt{FermatNo (N)}⌋ = ⌊\sqrt{2^{2^{N}} + 1}⌋$
6		id	$⊢ N \in ℕ \to N \in ℕ$
7		1nn0	$⊢ 1 \in ℕ_{0}$
8	7	a1i	$⊢ N \in ℕ \to 1 \in ℕ_{0}$
9		2nn	$⊢ 2 \in ℕ$
10	9	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
11		2nn0	$⊢ 2 \in ℕ_{0}$
12	11	a1i	$⊢ N \in ℕ \to 2 \in ℕ_{0}$
13		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
14	12 13	nn0expcld	$⊢ N \in ℕ \to 2^{N - 1} \in ℕ_{0}$
15		peano2nn0	$⊢ 2^{N - 1} \in ℕ_{0} \to 2^{N - 1} + 1 \in ℕ_{0}$
16	14 15	syl	$⊢ N \in ℕ \to 2^{N - 1} + 1 \in ℕ_{0}$
17	10 16	nnexpcld	$⊢ N \in ℕ \to 2^{2^{N - 1} + 1} \in ℕ$
18		nngt0	$⊢ 2^{2^{N - 1} + 1} \in ℕ \to 0 < 2^{2^{N - 1} + 1}$
19	17 18	syl	$⊢ N \in ℕ \to 0 < 2^{2^{N - 1} + 1}$
20	12 16	nn0expcld	$⊢ N \in ℕ \to 2^{2^{N - 1} + 1} \in ℕ_{0}$
21	20	nn0red	$⊢ N \in ℕ \to 2^{2^{N - 1} + 1} \in ℝ$
22		1re	$⊢ 1 \in ℝ$
23	22	a1i	$⊢ N \in ℕ \to 1 \in ℝ$
24	21 23	jca	$⊢ N \in ℕ \to (2^{2^{N - 1} + 1} \in ℝ \land 1 \in ℝ)$
25		ltaddpos2	$⊢ (2^{2^{N - 1} + 1} \in ℝ \land 1 \in ℝ) \to (0 < 2^{2^{N - 1} + 1} \leftrightarrow 1 < 2^{2^{N - 1} + 1} + 1)$
26	24 25	syl	$⊢ N \in ℕ \to (0 < 2^{2^{N - 1} + 1} \leftrightarrow 1 < 2^{2^{N - 1} + 1} + 1)$
27	19 26	mpbid	$⊢ N \in ℕ \to 1 < 2^{2^{N - 1} + 1} + 1$
28	6 8 27	3jca	$⊢ N \in ℕ \to (N \in ℕ \land 1 \in ℕ_{0} \land 1 < 2^{2^{N - 1} + 1} + 1)$
29		sqrtpwpw2p	$⊢ (N \in ℕ \land 1 \in ℕ_{0} \land 1 < 2^{2^{N - 1} + 1} + 1) \to ⌊\sqrt{2^{2^{N}} + 1}⌋ = 2^{2^{N - 1}}$
30	28 29	syl	$⊢ N \in ℕ \to ⌊\sqrt{2^{2^{N}} + 1}⌋ = 2^{2^{N - 1}}$
31	5 30	eqtrd	$⊢ N \in ℕ \to ⌊\sqrt{FermatNo (N)}⌋ = 2^{2^{N - 1}}$

Metamath Proof Explorer

Theorem fmtnosqrt

Proof