Proof of Theorem sqrtpwpw2p
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nncn 12274 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℂ) | 
| 2 | 1 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑁 ∈
ℂ) | 
| 3 |  | npcan1 11688 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁) | 
| 4 | 2, 3 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((𝑁 − 1) + 1)
= 𝑁) | 
| 5 | 4 | eqcomd 2743 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑁 = ((𝑁 − 1) +
1)) | 
| 6 | 5 | oveq2d 7447 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑𝑁) =
(2↑((𝑁 − 1) +
1))) | 
| 7 |  | 2cnd 12344 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 2 ∈ ℂ) | 
| 8 |  | nnm1nn0 12567 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑁 − 1) ∈
ℕ0) | 
| 10 | 7, 9 | expp1d 14187 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑((𝑁 −
1) + 1)) = ((2↑(𝑁
− 1)) · 2)) | 
| 11 | 6, 10 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑𝑁) =
((2↑(𝑁 − 1))
· 2)) | 
| 12 | 11 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(2↑𝑁))
= (2↑((2↑(𝑁
− 1)) · 2))) | 
| 13 |  | 2nn0 12543 | . . . . . . . . . 10
⊢ 2 ∈
ℕ0 | 
| 14 | 13 | a1i 11 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 2 ∈ ℕ0) | 
| 15 | 13 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 2 ∈
ℕ0) | 
| 16 | 15, 8 | nn0expcld 14285 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(2↑(𝑁 − 1))
∈ ℕ0) | 
| 17 | 16 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(𝑁 −
1)) ∈ ℕ0) | 
| 18 | 7, 14, 17 | expmuld 14189 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑((2↑(𝑁
− 1)) · 2)) = ((2↑(2↑(𝑁 − 1)))↑2)) | 
| 19 | 12, 18 | eqtrd 2777 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(2↑𝑁))
= ((2↑(2↑(𝑁
− 1)))↑2)) | 
| 20 |  | nn0ge0 12551 | . . . . . . . . 9
⊢ (𝑀 ∈ ℕ0
→ 0 ≤ 𝑀) | 
| 21 | 20 | adantl 481 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 0 ≤ 𝑀) | 
| 22 |  | nnnn0 12533 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 23 | 15, 22 | nn0expcld 14285 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(2↑𝑁) ∈
ℕ0) | 
| 24 | 15, 23 | nn0expcld 14285 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(2↑(2↑𝑁)) ∈
ℕ0) | 
| 25 | 24 | nn0red 12588 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(2↑(2↑𝑁)) ∈
ℝ) | 
| 26 |  | nn0re 12535 | . . . . . . . . . 10
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) | 
| 27 | 25, 26 | anim12i 613 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑(2↑𝑁))
∈ ℝ ∧ 𝑀
∈ ℝ)) | 
| 28 |  | addge01 11773 | . . . . . . . . 9
⊢
(((2↑(2↑𝑁)) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (0 ≤ 𝑀 ↔ (2↑(2↑𝑁)) ≤ ((2↑(2↑𝑁)) + 𝑀))) | 
| 29 | 27, 28 | syl 17 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (0 ≤ 𝑀 ↔
(2↑(2↑𝑁)) ≤
((2↑(2↑𝑁)) +
𝑀))) | 
| 30 | 21, 29 | mpbid 232 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(2↑𝑁))
≤ ((2↑(2↑𝑁)) +
𝑀)) | 
| 31 | 19, 30 | eqbrtrrd 5167 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑(2↑(𝑁
− 1)))↑2) ≤ ((2↑(2↑𝑁)) + 𝑀)) | 
| 32 | 24 | adantr 480 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(2↑𝑁))
∈ ℕ0) | 
| 33 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℕ0) | 
| 34 | 32, 33 | nn0addcld 12591 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑(2↑𝑁))
+ 𝑀) ∈
ℕ0) | 
| 35 |  | nn0re 12535 | . . . . . . . . 9
⊢
(((2↑(2↑𝑁)) + 𝑀) ∈ ℕ0 →
((2↑(2↑𝑁)) +
𝑀) ∈
ℝ) | 
| 36 |  | nn0ge0 12551 | . . . . . . . . 9
⊢
(((2↑(2↑𝑁)) + 𝑀) ∈ ℕ0 → 0 ≤
((2↑(2↑𝑁)) +
𝑀)) | 
| 37 | 35, 36 | jca 511 | . . . . . . . 8
⊢
(((2↑(2↑𝑁)) + 𝑀) ∈ ℕ0 →
(((2↑(2↑𝑁)) +
𝑀) ∈ ℝ ∧ 0
≤ ((2↑(2↑𝑁)) +
𝑀))) | 
| 38 | 34, 37 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((2↑(2↑𝑁)) + 𝑀) ∈ ℝ ∧ 0 ≤
((2↑(2↑𝑁)) +
𝑀))) | 
| 39 |  | resqrtth 15294 | . . . . . . 7
⊢
((((2↑(2↑𝑁)) + 𝑀) ∈ ℝ ∧ 0 ≤
((2↑(2↑𝑁)) +
𝑀)) →
((√‘((2↑(2↑𝑁)) + 𝑀))↑2) = ((2↑(2↑𝑁)) + 𝑀)) | 
| 40 | 38, 39 | syl 17 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((√‘((2↑(2↑𝑁)) + 𝑀))↑2) = ((2↑(2↑𝑁)) + 𝑀)) | 
| 41 | 31, 40 | breqtrrd 5171 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑(2↑(𝑁
− 1)))↑2) ≤ ((√‘((2↑(2↑𝑁)) + 𝑀))↑2)) | 
| 42 | 15, 16 | nn0expcld 14285 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑(2↑(𝑁 −
1))) ∈ ℕ0) | 
| 43 |  | nn0re 12535 | . . . . . . . . 9
⊢
((2↑(2↑(𝑁
− 1))) ∈ ℕ0 → (2↑(2↑(𝑁 − 1))) ∈
ℝ) | 
| 44 |  | nn0ge0 12551 | . . . . . . . . 9
⊢
((2↑(2↑(𝑁
− 1))) ∈ ℕ0 → 0 ≤ (2↑(2↑(𝑁 − 1)))) | 
| 45 | 43, 44 | jca 511 | . . . . . . . 8
⊢
((2↑(2↑(𝑁
− 1))) ∈ ℕ0 → ((2↑(2↑(𝑁 − 1))) ∈ ℝ
∧ 0 ≤ (2↑(2↑(𝑁 − 1))))) | 
| 46 | 42, 45 | syl 17 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
((2↑(2↑(𝑁 −
1))) ∈ ℝ ∧ 0 ≤ (2↑(2↑(𝑁 − 1))))) | 
| 47 | 46 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑(2↑(𝑁
− 1))) ∈ ℝ ∧ 0 ≤ (2↑(2↑(𝑁 − 1))))) | 
| 48 |  | resqrtcl 15292 | . . . . . . 7
⊢
((((2↑(2↑𝑁)) + 𝑀) ∈ ℝ ∧ 0 ≤
((2↑(2↑𝑁)) +
𝑀)) →
(√‘((2↑(2↑𝑁)) + 𝑀)) ∈ ℝ) | 
| 49 | 38, 48 | syl 17 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (√‘((2↑(2↑𝑁)) + 𝑀)) ∈ ℝ) | 
| 50 |  | sqrtge0 15296 | . . . . . . 7
⊢
((((2↑(2↑𝑁)) + 𝑀) ∈ ℝ ∧ 0 ≤
((2↑(2↑𝑁)) +
𝑀)) → 0 ≤
(√‘((2↑(2↑𝑁)) + 𝑀))) | 
| 51 | 38, 50 | syl 17 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 0 ≤ (√‘((2↑(2↑𝑁)) + 𝑀))) | 
| 52 |  | le2sq 14174 | . . . . . 6
⊢
((((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 837 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑(2↑(𝑁
− 1))) ≤ (√‘((2↑(2↑𝑁)) + 𝑀)) ↔ ((2↑(2↑(𝑁 − 1)))↑2) ≤
((√‘((2↑(2↑𝑁)) + 𝑀))↑2))) | 
| 54 | 41, 53 | mpbird 257 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(2↑(𝑁
− 1))) ≤ (√‘((2↑(2↑𝑁)) + 𝑀))) | 
| 55 | 54 | 3adant3 1133 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → (2↑(2↑(𝑁 − 1))) ≤
(√‘((2↑(2↑𝑁)) + 𝑀))) | 
| 56 | 26 | adantl 481 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 𝑀 ∈
ℝ) | 
| 57 |  | peano2nn0 12566 | . . . . . . . . . . . . 13
⊢
((2↑(𝑁 −
1)) ∈ ℕ0 → ((2↑(𝑁 − 1)) + 1) ∈
ℕ0) | 
| 58 | 16, 57 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
((2↑(𝑁 − 1)) +
1) ∈ ℕ0) | 
| 59 | 15, 58 | nn0expcld 14285 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(2↑((2↑(𝑁 −
1)) + 1)) ∈ ℕ0) | 
| 60 | 59 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑((2↑(𝑁
− 1)) + 1)) ∈ ℕ0) | 
| 61 |  | peano2nn0 12566 | . . . . . . . . . 10
⊢
((2↑((2↑(𝑁
− 1)) + 1)) ∈ ℕ0 → ((2↑((2↑(𝑁 − 1)) + 1)) + 1) ∈
ℕ0) | 
| 62 | 60, 61 | syl 17 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑((2↑(𝑁
− 1)) + 1)) + 1) ∈ ℕ0) | 
| 63 | 62 | nn0red 12588 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑((2↑(𝑁
− 1)) + 1)) + 1) ∈ ℝ) | 
| 64 | 32 | nn0red 12588 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(2↑𝑁))
∈ ℝ) | 
| 65 |  | axltadd 11334 | . . . . . . . 8
⊢ ((𝑀 ∈ ℝ ∧
((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 1373 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1) → ((2↑(2↑𝑁)) + 𝑀) < ((2↑(2↑𝑁)) + ((2↑((2↑(𝑁 − 1)) + 1)) + 1)))) | 
| 67 | 66 | 3impia 1118 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → ((2↑(2↑𝑁)) + 𝑀) < ((2↑(2↑𝑁)) + ((2↑((2↑(𝑁 − 1)) + 1)) + 1))) | 
| 68 | 24 | nn0cnd 12589 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑(2↑𝑁)) ∈
ℂ) | 
| 69 | 68 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → (2↑(2↑𝑁)) ∈ ℂ) | 
| 70 | 59 | nn0cnd 12589 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(2↑((2↑(𝑁 −
1)) + 1)) ∈ ℂ) | 
| 71 | 70 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → (2↑((2↑(𝑁 − 1)) + 1)) ∈
ℂ) | 
| 72 |  | 1cnd 11256 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → 1 ∈ ℂ) | 
| 73 | 69, 71, 72 | addassd 11283 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → (((2↑(2↑𝑁)) + (2↑((2↑(𝑁 − 1)) + 1))) + 1) =
((2↑(2↑𝑁)) +
((2↑((2↑(𝑁
− 1)) + 1)) + 1))) | 
| 74 | 67, 73 | breqtrrd 5171 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → ((2↑(2↑𝑁)) + 𝑀) < (((2↑(2↑𝑁)) + (2↑((2↑(𝑁 − 1)) + 1))) + 1)) | 
| 75 | 42 | nn0cnd 12589 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(2↑(2↑(𝑁 −
1))) ∈ ℂ) | 
| 76 |  | binom21 14258 | . . . . . . . . . 10
⊢
((2↑(2↑(𝑁
− 1))) ∈ ℂ → (((2↑(2↑(𝑁 − 1))) + 1)↑2) =
((((2↑(2↑(𝑁
− 1)))↑2) + (2 · (2↑(2↑(𝑁 − 1))))) + 1)) | 
| 77 | 75, 76 | syl 17 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(((2↑(2↑(𝑁
− 1))) + 1)↑2) = ((((2↑(2↑(𝑁 − 1)))↑2) + (2 ·
(2↑(2↑(𝑁 −
1))))) + 1)) | 
| 78 |  | 2cnd 12344 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ → 2 ∈
ℂ) | 
| 79 | 78, 15, 16 | expmuld 14189 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(2↑((2↑(𝑁 −
1)) · 2)) = ((2↑(2↑(𝑁 − 1)))↑2)) | 
| 80 | 78, 8 | expp1d 14187 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(2↑((𝑁 − 1) +
1)) = ((2↑(𝑁 −
1)) · 2)) | 
| 81 | 1, 3 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) + 1) = 𝑁) | 
| 82 | 81 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ →
(2↑((𝑁 − 1) +
1)) = (2↑𝑁)) | 
| 83 | 80, 82 | eqtr3d 2779 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ →
((2↑(𝑁 − 1))
· 2) = (2↑𝑁)) | 
| 84 | 83 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(2↑((2↑(𝑁 −
1)) · 2)) = (2↑(2↑𝑁))) | 
| 85 | 79, 84 | eqtr3d 2779 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
((2↑(2↑(𝑁 −
1)))↑2) = (2↑(2↑𝑁))) | 
| 86 | 78, 75 | mulcomd 11282 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ → (2
· (2↑(2↑(𝑁
− 1)))) = ((2↑(2↑(𝑁 − 1))) · 2)) | 
| 87 | 78, 16 | expp1d 14187 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ →
(2↑((2↑(𝑁 −
1)) + 1)) = ((2↑(2↑(𝑁 − 1))) · 2)) | 
| 88 | 86, 87 | eqtr4d 2780 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → (2
· (2↑(2↑(𝑁
− 1)))) = (2↑((2↑(𝑁 − 1)) + 1))) | 
| 89 | 85, 88 | oveq12d 7449 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(((2↑(2↑(𝑁
− 1)))↑2) + (2 · (2↑(2↑(𝑁 − 1))))) = ((2↑(2↑𝑁)) + (2↑((2↑(𝑁 − 1)) +
1)))) | 
| 90 | 89 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
((((2↑(2↑(𝑁
− 1)))↑2) + (2 · (2↑(2↑(𝑁 − 1))))) + 1) =
(((2↑(2↑𝑁)) +
(2↑((2↑(𝑁 −
1)) + 1))) + 1)) | 
| 91 | 77, 90 | eqtrd 2777 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
(((2↑(2↑(𝑁
− 1))) + 1)↑2) = (((2↑(2↑𝑁)) + (2↑((2↑(𝑁 − 1)) + 1))) + 1)) | 
| 92 | 91 | adantr 480 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((2↑(2↑(𝑁
− 1))) + 1)↑2) = (((2↑(2↑𝑁)) + (2↑((2↑(𝑁 − 1)) + 1))) + 1)) | 
| 93 | 40, 92 | breq12d 5156 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((√‘((2↑(2↑𝑁)) + 𝑀))↑2) < (((2↑(2↑(𝑁 − 1))) + 1)↑2)
↔ ((2↑(2↑𝑁))
+ 𝑀) <
(((2↑(2↑𝑁)) +
(2↑((2↑(𝑁 −
1)) + 1))) + 1))) | 
| 94 | 93 | 3adant3 1133 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ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 257 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → ((√‘((2↑(2↑𝑁)) + 𝑀))↑2) < (((2↑(2↑(𝑁 − 1))) +
1)↑2)) | 
| 96 | 34 | nn0red 12588 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((2↑(2↑𝑁))
+ 𝑀) ∈
ℝ) | 
| 97 |  | nn0ge0 12551 | . . . . . . . . . . 11
⊢
((2↑(2↑𝑁))
∈ ℕ0 → 0 ≤ (2↑(2↑𝑁))) | 
| 98 | 24, 97 | syl 17 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 0 ≤
(2↑(2↑𝑁))) | 
| 99 | 98, 20 | anim12i 613 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (0 ≤ (2↑(2↑𝑁)) ∧ 0 ≤ 𝑀)) | 
| 100 | 27, 99 | jca 511 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((2↑(2↑𝑁)) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ (0 ≤
(2↑(2↑𝑁)) ∧ 0
≤ 𝑀))) | 
| 101 |  | addge0 11752 | . . . . . . . 8
⊢
((((2↑(2↑𝑁)) ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧ (0 ≤
(2↑(2↑𝑁)) ∧ 0
≤ 𝑀)) → 0 ≤
((2↑(2↑𝑁)) +
𝑀)) | 
| 102 | 100, 101 | syl 17 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ 0 ≤ ((2↑(2↑𝑁)) + 𝑀)) | 
| 103 | 96, 102 | resqrtcld 15456 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (√‘((2↑(2↑𝑁)) + 𝑀)) ∈ ℝ) | 
| 104 |  | peano2nn0 12566 | . . . . . . . . 9
⊢
((2↑(2↑(𝑁
− 1))) ∈ ℕ0 → ((2↑(2↑(𝑁 − 1))) + 1) ∈
ℕ0) | 
| 105 | 42, 104 | syl 17 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ →
((2↑(2↑(𝑁 −
1))) + 1) ∈ ℕ0) | 
| 106 |  | nn0re 12535 | . . . . . . . . 9
⊢
(((2↑(2↑(𝑁
− 1))) + 1) ∈ ℕ0 → ((2↑(2↑(𝑁 − 1))) + 1) ∈
ℝ) | 
| 107 |  | nn0ge0 12551 | . . . . . . . . 9
⊢
(((2↑(2↑(𝑁
− 1))) + 1) ∈ ℕ0 → 0 ≤
((2↑(2↑(𝑁 −
1))) + 1)) | 
| 108 | 106, 107 | jca 511 | . . . . . . . 8
⊢
(((2↑(2↑(𝑁
− 1))) + 1) ∈ ℕ0 → (((2↑(2↑(𝑁 − 1))) + 1) ∈
ℝ ∧ 0 ≤ ((2↑(2↑(𝑁 − 1))) + 1))) | 
| 109 | 105, 108 | syl 17 | . . . . . . 7
⊢ (𝑁 ∈ ℕ →
(((2↑(2↑(𝑁
− 1))) + 1) ∈ ℝ ∧ 0 ≤ ((2↑(2↑(𝑁 − 1))) +
1))) | 
| 110 | 109 | adantr 480 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (((2↑(2↑(𝑁
− 1))) + 1) ∈ ℝ ∧ 0 ≤ ((2↑(2↑(𝑁 − 1))) +
1))) | 
| 111 |  | lt2sq 14173 | . . . . . 6
⊢
((((√‘((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 838 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((√‘((2↑(2↑𝑁)) + 𝑀)) < ((2↑(2↑(𝑁 − 1))) + 1) ↔
((√‘((2↑(2↑𝑁)) + 𝑀))↑2) < (((2↑(2↑(𝑁 − 1))) +
1)↑2))) | 
| 113 | 112 | 3adant3 1133 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → ((√‘((2↑(2↑𝑁)) + 𝑀)) < ((2↑(2↑(𝑁 − 1))) + 1) ↔
((√‘((2↑(2↑𝑁)) + 𝑀))↑2) < (((2↑(2↑(𝑁 − 1))) +
1)↑2))) | 
| 114 | 95, 113 | mpbird 257 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → (√‘((2↑(2↑𝑁)) + 𝑀)) < ((2↑(2↑(𝑁 − 1))) + 1)) | 
| 115 | 55, 114 | jca 511 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → ((2↑(2↑(𝑁 − 1))) ≤
(√‘((2↑(2↑𝑁)) + 𝑀)) ∧
(√‘((2↑(2↑𝑁)) + 𝑀)) < ((2↑(2↑(𝑁 − 1))) + 1))) | 
| 116 | 42 | nn0zd 12639 | . . . . . 6
⊢ (𝑁 ∈ ℕ →
(2↑(2↑(𝑁 −
1))) ∈ ℤ) | 
| 117 | 116 | adantr 480 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ (2↑(2↑(𝑁
− 1))) ∈ ℤ) | 
| 118 | 49, 117 | jca 511 | . . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0)
→ ((√‘((2↑(2↑𝑁)) + 𝑀)) ∈ ℝ ∧
(2↑(2↑(𝑁 −
1))) ∈ ℤ)) | 
| 119 | 118 | 3adant3 1133 | . . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) → ((√‘((2↑(2↑𝑁)) + 𝑀)) ∈ ℝ ∧
(2↑(2↑(𝑁 −
1))) ∈ ℤ)) | 
| 120 |  | flbi 13856 | . . 3
⊢
(((√‘((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 17 | . 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ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 257 | 1
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0
∧ 𝑀 <
((2↑((2↑(𝑁
− 1)) + 1)) + 1)) →
(⌊‘(√‘((2↑(2↑𝑁)) + 𝑀))) = (2↑(2↑(𝑁 − 1)))) |