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 ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < ( ( 2 ↑ ( ( 2 ↑ ( 𝑁 − 1 ) ) + 1 ) ) + 1 ) ) → ( ⌊ ‘ ( √ ‘ ( ( 2 ↑ ( 2 ↑ 𝑁 ) ) + 𝑀 ) ) ) = ( 2 ↑ ( 2 ↑ ( 𝑁 − 1 ) ) ) )

Proof

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