Metamath Proof Explorer

Theorem nnolog2flm1

Description: The floor of the binary logarithm of an odd integer greater than 1 is the floor of the binary logarithm of the integer decreased by 1. (Contributed by AV, 2-Jun-2020)

Ref Expression
Assertion nnolog2flm1 ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 eluz2nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
2 nnpw2blenfzo2 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∨ 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) )
3 1 2 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∨ 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) )
4 1 adantl ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ∈ ℕ )
5 nneo ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
6 5 bicomd ⊢ ( 𝑁 ∈ ℕ → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ↔ ( 𝑁 / 2 ) ∈ ℕ ) )
7 4 6 syl ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ↔ ( 𝑁 / 2 ) ∈ ℕ ) )
8 notnotb ⊢ ( ( 𝑁 / 2 ) ∈ ℕ ↔ ¬ ¬ ( 𝑁 / 2 ) ∈ ℕ )
9 7 8 bitrdi ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ↔ ¬ ¬ ( 𝑁 / 2 ) ∈ ℕ ) )
10 9 con4bid ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ↔ ¬ ( 𝑁 / 2 ) ∈ ℕ ) )
11 simpl ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) )
12 11 oveq1d ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 / 2 ) = ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) / 2 ) )
13 blennnelnn ⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ )
14 13 nnnn0d ⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ0 )
15 1 14 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) ∈ ℕ0 )
16 2m1e1 ⊢ ( 2 − 1 ) = 1
17 2cn ⊢ 2 ∈ ℂ
18 2ne0 ⊢ 2 ≠ 0
19 1ne2 ⊢ 1 ≠ 2
20 19 necomi ⊢ 2 ≠ 1
21 logbid1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 2 ) = 1 )
22 17 18 20 21 mp3an ⊢ ( 2 logb 2 ) = 1
23 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
24 2z ⊢ 2 ∈ ℤ
25 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
26 24 25 mp1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ( ℤ≥ ‘ 2 ) )
27 2rp ⊢ 2 ∈ ℝ+
28 27 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ+ )
29 1 nnrpd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ+ )
30 logbleb ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( 2 ≤ 𝑁 ↔ ( 2 logb 2 ) ≤ ( 2 logb 𝑁 ) ) )
31 26 28 29 30 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ≤ 𝑁 ↔ ( 2 logb 2 ) ≤ ( 2 logb 𝑁 ) ) )
32 23 31 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 logb 2 ) ≤ ( 2 logb 𝑁 ) )
33 22 32 eqbrtrrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ ( 2 logb 𝑁 ) )
34 20 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≠ 1 )
35 relogbcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb 𝑁 ) ∈ ℝ )
36 28 29 34 35 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 logb 𝑁 ) ∈ ℝ )
37 1zzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℤ )
38 flge ⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( 1 ≤ ( 2 logb 𝑁 ) ↔ 1 ≤ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) )
39 36 37 38 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 1 ≤ ( 2 logb 𝑁 ) ↔ 1 ≤ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) )
40 33 39 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ≤ ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
41 16 40 eqbrtrid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 − 1 ) ≤ ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
42 2re ⊢ 2 ∈ ℝ
43 42 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℝ )
44 1red ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 1 ∈ ℝ )
45 36 flcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ )
46 45 zred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℝ )
47 43 44 46 lesubaddd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 2 − 1 ) ≤ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ↔ 2 ≤ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) )
48 41 47 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
49 blennn ⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
50 1 49 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
51 48 50 breqtrrd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( #b ‘ 𝑁 ) )
52 nn0ge2m1nn ⊢ ( ( ( #b ‘ 𝑁 ) ∈ ℕ0 ∧ 2 ≤ ( #b ‘ 𝑁 ) ) → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ )
53 15 51 52 syl2anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ )
54 53 adantl ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ )
55 nnpw2even ⊢ ( ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ → ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) / 2 ) ∈ ℕ )
56 54 55 syl ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) / 2 ) ∈ ℕ )
57 12 56 eqeltrd ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 / 2 ) ∈ ℕ )
58 57 pm2.24d ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ¬ ( 𝑁 / 2 ) ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ) )
59 10 58 sylbid ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ) )
60 59 ex ⊢ ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ) ) )
61 1 13 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) ∈ ℕ )
62 nnm1nn0 ⊢ ( ( #b ‘ 𝑁 ) ∈ ℕ → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
63 61 62 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
64 63 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
65 1 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → 𝑁 ∈ ℕ )
66 nnpw2blenfzo ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
67 65 66 syl ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
68 61 nncnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) ∈ ℂ )
69 68 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( #b ‘ 𝑁 ) ∈ ℂ )
70 npcan1 ⊢ ( ( #b ‘ 𝑁 ) ∈ ℂ → ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) = ( #b ‘ 𝑁 ) )
71 69 70 syl ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) = ( #b ‘ 𝑁 ) )
72 71 oveq2d ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) = ( 2 ↑ ( #b ‘ 𝑁 ) ) )
73 72 oveq2d ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) = ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
74 67 73 eleqtrrd ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) )
75 fllog2 ⊢ ( ( ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )
76 64 74 75 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )
77 61 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( #b ‘ 𝑁 ) ∈ ℕ )
78 77 62 syl ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 )
79 elfzo2 ⊢ ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ) ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
80 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ) ↔ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) )
81 80 3anbi1i ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ) ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ↔ ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
82 79 81 bitri ⊢ ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ↔ ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
83 2nn ⊢ 2 ∈ ℕ
84 83 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ∈ ℕ )
85 84 63 jca ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ∈ ℕ ∧ ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 ) )
86 85 adantl ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ∈ ℕ ∧ ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 ) )
87 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℕ )
88 86 87 syl ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℕ )
89 88 nnzd ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℤ )
90 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
91 90 3ad2ant2 ⊢ ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℤ )
92 91 adantr ⊢ ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 − 1 ) ∈ ℤ )
93 92 adantr ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 − 1 ) ∈ ℤ )
94 84 63 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℕ )
95 94 nnred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℝ )
96 1 nnred ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℝ )
97 leaddsub ⊢ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ↔ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ ( 𝑁 − 1 ) ) )
98 95 44 96 97 syl3anc ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ↔ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ ( 𝑁 − 1 ) ) )
99 98 biimpcd ⊢ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ ( 𝑁 − 1 ) ) )
100 99 3ad2ant3 ⊢ ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ ( 𝑁 − 1 ) ) )
101 100 adantr ⊢ ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ ( 𝑁 − 1 ) ) )
102 101 imp ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ ( 𝑁 − 1 ) )
103 eluz2 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ↔ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℤ ∧ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ≤ ( 𝑁 − 1 ) ) )
104 89 93 102 103 syl3anbrc ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) )
105 70 eleq1d ⊢ ( ( #b ‘ 𝑁 ) ∈ ℂ → ( ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ∈ ℕ0 ↔ ( #b ‘ 𝑁 ) ∈ ℕ0 ) )
106 68 105 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ∈ ℕ0 ↔ ( #b ‘ 𝑁 ) ∈ ℕ0 ) )
107 15 106 mpbird ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ∈ ℕ0 )
108 84 107 jca ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ∈ ℕ ∧ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ∈ ℕ0 ) )
109 108 adantl ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ∈ ℕ ∧ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ∈ ℕ0 ) )
110 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℕ )
111 109 110 syl ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℕ )
112 111 nnzd ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℤ )
113 ltle ⊢ ( ( 𝑁 ∈ ℝ ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℝ ) → ( 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) → 𝑁 ≤ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
114 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
115 42 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ )
116 115 14 reexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℝ )
117 114 116 jca ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℝ ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℝ ) )
118 1 117 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑁 ∈ ℝ ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℝ ) )
119 113 118 syl11 ⊢ ( 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
120 119 adantl ⊢ ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ≤ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
121 120 imp ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ≤ ( 2 ↑ ( #b ‘ 𝑁 ) ) )
122 simpll2 ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑁 ∈ ℤ )
123 84 15 nnexpcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℕ )
124 123 nnzd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ )
125 124 adantl ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ )
126 zlem1lt ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ ) → ( 𝑁 ≤ ( 2 ↑ ( #b ‘ 𝑁 ) ) ↔ ( 𝑁 − 1 ) < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
127 122 125 126 syl2anc ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 ≤ ( 2 ↑ ( #b ‘ 𝑁 ) ) ↔ ( 𝑁 − 1 ) < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) )
128 121 127 mpbid ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 − 1 ) < ( 2 ↑ ( #b ‘ 𝑁 ) ) )
129 68 70 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) = ( #b ‘ 𝑁 ) )
130 129 oveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) = ( 2 ↑ ( #b ‘ 𝑁 ) ) )
131 130 adantl ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) = ( 2 ↑ ( #b ‘ 𝑁 ) ) )
132 128 131 breqtrrd ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 − 1 ) < ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) )
133 104 112 132 3jca ⊢ ( ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ∧ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℤ ∧ ( 𝑁 − 1 ) < ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) )
134 133 ex ⊢ ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ∧ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℤ ∧ ( 𝑁 − 1 ) < ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) ) )
135 134 3adant2 ⊢ ( ( ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ≤ 𝑁 ) ∧ ( 2 ↑ ( #b ‘ 𝑁 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ∧ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℤ ∧ ( 𝑁 − 1 ) < ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) ) )
136 82 135 sylbi ⊢ ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ∧ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℤ ∧ ( 𝑁 − 1 ) < ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) ) )
137 136 imp ⊢ ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ∧ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℤ ∧ ( 𝑁 − 1 ) < ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) )
138 elfzo2 ⊢ ( ( 𝑁 − 1 ) ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) ↔ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ) ∧ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ∈ ℤ ∧ ( 𝑁 − 1 ) < ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) )
139 137 138 sylibr ⊢ ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 − 1 ) ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) )
140 139 adantr ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( 𝑁 − 1 ) ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) )
141 fllog2 ⊢ ( ( ( ( #b ‘ 𝑁 ) − 1 ) ∈ ℕ0 ∧ ( 𝑁 − 1 ) ∈ ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ..^ ( 2 ↑ ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) ) ) ) → ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )
142 78 140 141 syl2anc ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )
143 76 142 eqtr4d ⊢ ( ( ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )
144 143 exp31 ⊢ ( 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ) ) )
145 60 144 jaoi ⊢ ( ( 𝑁 = ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) ∨ 𝑁 ∈ ( ( ( 2 ↑ ( ( #b ‘ 𝑁 ) − 1 ) ) + 1 ) ..^ ( 2 ↑ ( #b ‘ 𝑁 ) ) ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ) ) )
146 3 145 mpcom ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) ) )
147 146 imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = ( ⌊ ‘ ( 2 logb ( 𝑁 − 1 ) ) ) )