Theorem sqrtpwpw2p

Description: The floor of the square root of 2 to the power of 2 to the power of a positive integer plus a bounded nonnegative integer. (Contributed by AV, 28-Jul-2021)

	Ref	Expression
Assertion	sqrtpwpw2p	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to ⌊\sqrt{2^{2^N}+M}⌋=2^{2^{N-1}}$$

Proof

Step	Hyp	Ref	Expression
1		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
2	1	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to N\in ℂ$$
3		npcan1	$$⊢N\in ℂ\to N-1+1=N$$
4	2 3	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to N-1+1=N$$
5	4	eqcomd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to N=N-1+1$$
6	5	oveq2d	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^N=2^{N-1+1}$$
7		2cnd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2\in ℂ$$
8		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
9	8	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to N-1\in {\mathbb{N}}_0$$
10	7 9	expp1d	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{N-1+1}=2^{N-1}\cdot 2$$
11	6 10	eqtrd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^N=2^{N-1}\cdot 2$$
12	11	oveq2d	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^N}=2^{2^{N-1}\cdot 2}$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14	13	a1i	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2\in {\mathbb{N}}_0$$
15	13	a1i	$$⊢N\in \mathbb{N}\to 2\in {\mathbb{N}}_0$$
16	15 8	nn0expcld	$$⊢N\in \mathbb{N}\to 2^{N-1}\in {\mathbb{N}}_0$$
17	16	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{N-1}\in {\mathbb{N}}_0$$
18	7 14 17	expmuld	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^{N-1}\cdot 2}={\left(2^{2^{N-1}}\right)}^2$$
19	12 18	eqtrd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^N}={\left(2^{2^{N-1}}\right)}^2$$
20		nn0ge0	$$⊢M\in {\mathbb{N}}_0\to 0\le M$$
21	20	adantl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 0\le M$$
22		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
23	15 22	nn0expcld	$$⊢N\in \mathbb{N}\to 2^N\in {\mathbb{N}}_0$$
24	15 23	nn0expcld	$$⊢N\in \mathbb{N}\to 2^{2^N}\in {\mathbb{N}}_0$$
25	24	nn0red	$$⊢N\in \mathbb{N}\to 2^{2^N}\in ℝ$$
26		nn0re	$$⊢M\in {\mathbb{N}}_0\to M\in ℝ$$
27	25 26	anim12i	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(2^{2^N}\in ℝ\wedge M\in ℝ\right)$$
28		addge01	$$⊢\left(2^{2^N}\in ℝ\wedge M\in ℝ\right)\to \left(0\le M\leftrightarrow 2^{2^N}\le 2^{2^N}+M\right)$$
29	27 28	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(0\le M\leftrightarrow 2^{2^N}\le 2^{2^N}+M\right)$$
30	21 29	mpbid	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^N}\le 2^{2^N}+M$$
31	19 30	eqbrtrrd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to {\left(2^{2^{N-1}}\right)}^2\le 2^{2^N}+M$$
32	24	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^N}\in {\mathbb{N}}_0$$
33		simpr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to M\in {\mathbb{N}}_0$$
34	32 33	nn0addcld	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^N}+M\in {\mathbb{N}}_0$$
35		nn0re	$$⊢2^{2^N}+M\in {\mathbb{N}}_0\to 2^{2^N}+M\in ℝ$$
36		nn0ge0	$$⊢2^{2^N}+M\in {\mathbb{N}}_0\to 0\le 2^{2^N}+M$$
37	35 36	jca	$$⊢2^{2^N}+M\in {\mathbb{N}}_0\to \left(2^{2^N}+M\in ℝ\wedge 0\le 2^{2^N}+M\right)$$
38	34 37	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(2^{2^N}+M\in ℝ\wedge 0\le 2^{2^N}+M\right)$$
39		resqrtth	$$⊢\left(2^{2^N}+M\in ℝ\wedge 0\le 2^{2^N}+M\right)\to {\sqrt{2^{2^N}+M}}^2=2^{2^N}+M$$
40	38 39	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to {\sqrt{2^{2^N}+M}}^2=2^{2^N}+M$$
41	31 40	breqtrrd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to {\left(2^{2^{N-1}}\right)}^2\le {\sqrt{2^{2^N}+M}}^2$$
42	15 16	nn0expcld	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}}\in {\mathbb{N}}_0$$
43		nn0re	$$⊢2^{2^{N-1}}\in {\mathbb{N}}_0\to 2^{2^{N-1}}\in ℝ$$
44		nn0ge0	$$⊢2^{2^{N-1}}\in {\mathbb{N}}_0\to 0\le 2^{2^{N-1}}$$
45	43 44	jca	$$⊢2^{2^{N-1}}\in {\mathbb{N}}_0\to \left(2^{2^{N-1}}\in ℝ\wedge 0\le 2^{2^{N-1}}\right)$$
46	42 45	syl	$$⊢N\in \mathbb{N}\to \left(2^{2^{N-1}}\in ℝ\wedge 0\le 2^{2^{N-1}}\right)$$
47	46	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(2^{2^{N-1}}\in ℝ\wedge 0\le 2^{2^{N-1}}\right)$$
48		resqrtcl	$$⊢\left(2^{2^N}+M\in ℝ\wedge 0\le 2^{2^N}+M\right)\to \sqrt{2^{2^N}+M}\in ℝ$$
49	38 48	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \sqrt{2^{2^N}+M}\in ℝ$$
50		sqrtge0	$$⊢\left(2^{2^N}+M\in ℝ\wedge 0\le 2^{2^N}+M\right)\to 0\le \sqrt{2^{2^N}+M}$$
51	38 50	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 0\le \sqrt{2^{2^N}+M}$$
52		le2sq	$$⊢\left(\left(2^{2^{N-1}}\in ℝ\wedge 0\le 2^{2^{N-1}}\right)\wedge \left(\sqrt{2^{2^N}+M}\in ℝ\wedge 0\le \sqrt{2^{2^N}+M}\right)\right)\to \left(2^{2^{N-1}}\le \sqrt{2^{2^N}+M}\leftrightarrow {\left(2^{2^{N-1}}\right)}^2\le {\sqrt{2^{2^N}+M}}^2\right)$$
53	47 49 51 52	syl12anc	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(2^{2^{N-1}}\le \sqrt{2^{2^N}+M}\leftrightarrow {\left(2^{2^{N-1}}\right)}^2\le {\sqrt{2^{2^N}+M}}^2\right)$$
54	41 53	mpbird	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^{N-1}}\le \sqrt{2^{2^N}+M}$$
55	54	3adant3	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to 2^{2^{N-1}}\le \sqrt{2^{2^N}+M}$$
56	26	adantl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to M\in ℝ$$
57		peano2nn0	$$⊢2^{N-1}\in {\mathbb{N}}_0\to 2^{N-1}+1\in {\mathbb{N}}_0$$
58	16 57	syl	$$⊢N\in \mathbb{N}\to 2^{N-1}+1\in {\mathbb{N}}_0$$
59	15 58	nn0expcld	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}+1}\in {\mathbb{N}}_0$$
60	59	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^{N-1}+1}\in {\mathbb{N}}_0$$
61		peano2nn0	$$⊢2^{2^{N-1}+1}\in {\mathbb{N}}_0\to 2^{2^{N-1}+1}+1\in {\mathbb{N}}_0$$
62	60 61	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^{N-1}+1}+1\in {\mathbb{N}}_0$$
63	62	nn0red	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^{N-1}+1}+1\in ℝ$$
64	32	nn0red	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^N}\in ℝ$$
65		axltadd	$$⊢\left(M\in ℝ\wedge 2^{2^{N-1}+1}+1\in ℝ\wedge 2^{2^N}\in ℝ\right)\to \left(M<2^{2^{N-1}+1}+1\to 2^{2^N}+M<2^{2^N}+2^{2^{N-1}+1}+1\right)$$
66	56 63 64 65	syl3anc	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(M<2^{2^{N-1}+1}+1\to 2^{2^N}+M<2^{2^N}+2^{2^{N-1}+1}+1\right)$$
67	66	3impia	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to 2^{2^N}+M<2^{2^N}+2^{2^{N-1}+1}+1$$
68	24	nn0cnd	$$⊢N\in \mathbb{N}\to 2^{2^N}\in ℂ$$
69	68	3ad2ant1	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to 2^{2^N}\in ℂ$$
70	59	nn0cnd	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}+1}\in ℂ$$
71	70	3ad2ant1	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to 2^{2^{N-1}+1}\in ℂ$$
72		1cnd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to 1\in ℂ$$
73	69 71 72	addassd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to 2^{2^N}+2^{2^{N-1}+1}+1=2^{2^N}+2^{2^{N-1}+1}+1$$
74	67 73	breqtrrd	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to 2^{2^N}+M<2^{2^N}+2^{2^{N-1}+1}+1$$
75	42	nn0cnd	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}}\in ℂ$$
76		binom21	$$⊢2^{2^{N-1}}\in ℂ\to {\left(2^{2^{N-1}}+1\right)}^2={\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}+1$$
77	75 76	syl	$$⊢N\in \mathbb{N}\to {\left(2^{2^{N-1}}+1\right)}^2={\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}+1$$
78		2cnd	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
79	78 15 16	expmuld	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}\cdot 2}={\left(2^{2^{N-1}}\right)}^2$$
80	78 8	expp1d	$$⊢N\in \mathbb{N}\to 2^{N-1+1}=2^{N-1}\cdot 2$$
81	1 3	syl	$$⊢N\in \mathbb{N}\to N-1+1=N$$
82	81	oveq2d	$$⊢N\in \mathbb{N}\to 2^{N-1+1}=2^N$$
83	80 82	eqtr3d	$$⊢N\in \mathbb{N}\to 2^{N-1}\cdot 2=2^N$$
84	83	oveq2d	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}\cdot 2}=2^{2^N}$$
85	79 84	eqtr3d	$$⊢N\in \mathbb{N}\to {\left(2^{2^{N-1}}\right)}^2=2^{2^N}$$
86	78 75	mulcomd	$$⊢N\in \mathbb{N}\to 22^{2^{N-1}}=2^{2^{N-1}}\cdot 2$$
87	78 16	expp1d	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}+1}=2^{2^{N-1}}\cdot 2$$
88	86 87	eqtr4d	$$⊢N\in \mathbb{N}\to 22^{2^{N-1}}=2^{2^{N-1}+1}$$
89	85 88	oveq12d	$$⊢N\in \mathbb{N}\to {\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}=2^{2^N}+2^{2^{N-1}+1}$$
90	89	oveq1d	$$⊢N\in \mathbb{N}\to {\left(2^{2^{N-1}}\right)}^2+22^{2^{N-1}}+1=2^{2^N}+2^{2^{N-1}+1}+1$$
91	77 90	eqtrd	$$⊢N\in \mathbb{N}\to {\left(2^{2^{N-1}}+1\right)}^2=2^{2^N}+2^{2^{N-1}+1}+1$$
92	91	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to {\left(2^{2^{N-1}}+1\right)}^2=2^{2^N}+2^{2^{N-1}+1}+1$$
93	40 92	breq12d	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left({\sqrt{2^{2^N}+M}}^2<{\left(2^{2^{N-1}}+1\right)}^2\leftrightarrow 2^{2^N}+M<2^{2^N}+2^{2^{N-1}+1}+1\right)$$
94	93	3adant3	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to \left({\sqrt{2^{2^N}+M}}^2<{\left(2^{2^{N-1}}+1\right)}^2\leftrightarrow 2^{2^N}+M<2^{2^N}+2^{2^{N-1}+1}+1\right)$$
95	74 94	mpbird	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to {\sqrt{2^{2^N}+M}}^2<{\left(2^{2^{N-1}}+1\right)}^2$$
96	34	nn0red	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^N}+M\in ℝ$$
97		nn0ge0	$$⊢2^{2^N}\in {\mathbb{N}}_0\to 0\le 2^{2^N}$$
98	24 97	syl	$$⊢N\in \mathbb{N}\to 0\le 2^{2^N}$$
99	98 20	anim12i	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(0\le 2^{2^N}\wedge 0\le M\right)$$
100	27 99	jca	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(\left(2^{2^N}\in ℝ\wedge M\in ℝ\right)\wedge \left(0\le 2^{2^N}\wedge 0\le M\right)\right)$$
101		addge0	$$⊢\left(\left(2^{2^N}\in ℝ\wedge M\in ℝ\right)\wedge \left(0\le 2^{2^N}\wedge 0\le M\right)\right)\to 0\le 2^{2^N}+M$$
102	100 101	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 0\le 2^{2^N}+M$$
103	96 102	resqrtcld	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \sqrt{2^{2^N}+M}\in ℝ$$
104		peano2nn0	$$⊢2^{2^{N-1}}\in {\mathbb{N}}_0\to 2^{2^{N-1}}+1\in {\mathbb{N}}_0$$
105	42 104	syl	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}}+1\in {\mathbb{N}}_0$$
106		nn0re	$$⊢2^{2^{N-1}}+1\in {\mathbb{N}}_0\to 2^{2^{N-1}}+1\in ℝ$$
107		nn0ge0	$$⊢2^{2^{N-1}}+1\in {\mathbb{N}}_0\to 0\le 2^{2^{N-1}}+1$$
108	106 107	jca	$$⊢2^{2^{N-1}}+1\in {\mathbb{N}}_0\to \left(2^{2^{N-1}}+1\in ℝ\wedge 0\le 2^{2^{N-1}}+1\right)$$
109	105 108	syl	$$⊢N\in \mathbb{N}\to \left(2^{2^{N-1}}+1\in ℝ\wedge 0\le 2^{2^{N-1}}+1\right)$$
110	109	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(2^{2^{N-1}}+1\in ℝ\wedge 0\le 2^{2^{N-1}}+1\right)$$
111		lt2sq	$$⊢\left(\left(\sqrt{2^{2^N}+M}\in ℝ\wedge 0\le \sqrt{2^{2^N}+M}\right)\wedge \left(2^{2^{N-1}}+1\in ℝ\wedge 0\le 2^{2^{N-1}}+1\right)\right)\to \left(\sqrt{2^{2^N}+M}<2^{2^{N-1}}+1\leftrightarrow {\sqrt{2^{2^N}+M}}^2<{\left(2^{2^{N-1}}+1\right)}^2\right)$$
112	103 51 110 111	syl21anc	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(\sqrt{2^{2^N}+M}<2^{2^{N-1}}+1\leftrightarrow {\sqrt{2^{2^N}+M}}^2<{\left(2^{2^{N-1}}+1\right)}^2\right)$$
113	112	3adant3	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to \left(\sqrt{2^{2^N}+M}<2^{2^{N-1}}+1\leftrightarrow {\sqrt{2^{2^N}+M}}^2<{\left(2^{2^{N-1}}+1\right)}^2\right)$$
114	95 113	mpbird	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to \sqrt{2^{2^N}+M}<2^{2^{N-1}}+1$$
115	55 114	jca	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to \left(2^{2^{N-1}}\le \sqrt{2^{2^N}+M}\wedge \sqrt{2^{2^N}+M}<2^{2^{N-1}}+1\right)$$
116	42	nn0zd	$$⊢N\in \mathbb{N}\to 2^{2^{N-1}}\in \mathbb{Z}$$
117	116	adantr	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to 2^{2^{N-1}}\in \mathbb{Z}$$
118	49 117	jca	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\right)\to \left(\sqrt{2^{2^N}+M}\in ℝ\wedge 2^{2^{N-1}}\in \mathbb{Z}\right)$$
119	118	3adant3	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to \left(\sqrt{2^{2^N}+M}\in ℝ\wedge 2^{2^{N-1}}\in \mathbb{Z}\right)$$
120		flbi	$$⊢\left(\sqrt{2^{2^N}+M}\in ℝ\wedge 2^{2^{N-1}}\in \mathbb{Z}\right)\to \left(⌊\sqrt{2^{2^N}+M}⌋=2^{2^{N-1}}\leftrightarrow \left(2^{2^{N-1}}\le \sqrt{2^{2^N}+M}\wedge \sqrt{2^{2^N}+M}<2^{2^{N-1}}+1\right)\right)$$
121	119 120	syl	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to \left(⌊\sqrt{2^{2^N}+M}⌋=2^{2^{N-1}}\leftrightarrow \left(2^{2^{N-1}}\le \sqrt{2^{2^N}+M}\wedge \sqrt{2^{2^N}+M}<2^{2^{N-1}}+1\right)\right)$$
122	115 121	mpbird	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{N}}_0\wedge M<2^{2^{N-1}+1}+1\right)\to ⌊\sqrt{2^{2^N}+M}⌋=2^{2^{N-1}}$$