Metamath Proof Explorer

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 
|- ( ( N e. NN /\ M e. NN0 /\ M < ( ( 2 ^ ( ( 2 ^ ( N - 1 ) ) + 1 ) ) + 1 ) ) -> ( |_ ` ( sqrt ` ( ( 2 ^ ( 2 ^ N ) ) + M ) ) ) = ( 2 ^ ( 2 ^ ( N - 1 ) ) ) )

Proof

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