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	$⊢ (N \in ℕ \land M \in ℕ_{0} \land M < 2^{2^{N - 1} + 1} + 1) \to ⌊\sqrt{2^{2^{N}} + M}⌋ = 2^{2^{N - 1}}$

Proof

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

Metamath Proof Explorer

Theorem sqrtpwpw2p

Proof