Metamath Proof Explorer

Theorem fllog2

Description: The floor of the binary logarithm of 2 to the power of an element of a half-open integer interval bounded by powers of 2 is equal to the integer. (Contributed by AV, 31-May-2020)

Ref Expression
Assertion fllog2 ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = 𝐼 )

Proof

Step Hyp Ref Expression
1 nn0z ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℤ )
2 1 adantr ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝐼 ∈ ℤ )
3 2rp ⊢ 2 ∈ ℝ+
4 elfzoelz ⊢ ( 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) → 𝑁 ∈ ℤ )
5 4 zred ⊢ ( 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) → 𝑁 ∈ ℝ )
6 5 adantl ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝑁 ∈ ℝ )
7 elfzo2 ⊢ ( 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ↔ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( 𝐼 + 1 ) ) ) )
8 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ↔ ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 2 ↑ 𝐼 ) ≤ 𝑁 ) )
9 2re ⊢ 2 ∈ ℝ
10 2pos ⊢ 0 < 2
11 10 a1i ⊢ ( 𝐼 ∈ ℕ0 → 0 < 2 )
12 expgt0 ⊢ ( ( 2 ∈ ℝ ∧ 𝐼 ∈ ℤ ∧ 0 < 2 ) → 0 < ( 2 ↑ 𝐼 ) )
13 9 1 11 12 mp3an2i ⊢ ( 𝐼 ∈ ℕ0 → 0 < ( 2 ↑ 𝐼 ) )
14 13 adantl ⊢ ( ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 0 < ( 2 ↑ 𝐼 ) )
15 0red ⊢ ( ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 0 ∈ ℝ )
16 zre ⊢ ( ( 2 ↑ 𝐼 ) ∈ ℤ → ( 2 ↑ 𝐼 ) ∈ ℝ )
17 16 adantr ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ↑ 𝐼 ) ∈ ℝ )
18 17 adantr ⊢ ( ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 2 ↑ 𝐼 ) ∈ ℝ )
19 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
20 19 ad2antlr ⊢ ( ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
21 ltletr ⊢ ( ( 0 ∈ ℝ ∧ ( 2 ↑ 𝐼 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 < ( 2 ↑ 𝐼 ) ∧ ( 2 ↑ 𝐼 ) ≤ 𝑁 ) → 0 < 𝑁 ) )
22 15 18 20 21 syl3anc ⊢ ( ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 0 < ( 2 ↑ 𝐼 ) ∧ ( 2 ↑ 𝐼 ) ≤ 𝑁 ) → 0 < 𝑁 ) )
23 14 22 mpand ⊢ ( ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 → 0 < 𝑁 ) )
24 23 ex ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐼 ∈ ℕ0 → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 → 0 < 𝑁 ) ) )
25 24 com23 ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) ) )
26 25 3impia ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 2 ↑ 𝐼 ) ≤ 𝑁 ) → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) )
27 8 26 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) )
28 27 3ad2ant1 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( 𝐼 + 1 ) ) ) → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) )
29 7 28 sylbi ⊢ ( 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) )
30 29 impcom ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 0 < 𝑁 )
31 6 30 elrpd ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝑁 ∈ ℝ+ )
32 1ne2 ⊢ 1 ≠ 2
33 32 necomi ⊢ 2 ≠ 1
34 33 a1i ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 2 ≠ 1 )
35 relogbcl ⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb 𝑁 ) ∈ ℝ )
36 3 31 34 35 mp3an2i ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( 2 logb 𝑁 ) ∈ ℝ )
37 36 flcld ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ )
38 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) → 𝑁 ∈ ℤ )
39 zltlem1 ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) → ( 𝑁 < ( 2 ↑ ( 𝐼 + 1 ) ) ↔ 𝑁 ≤ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) )
40 38 39 sylan ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) → ( 𝑁 < ( 2 ↑ ( 𝐼 + 1 ) ) ↔ 𝑁 ≤ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) )
41 2z ⊢ 2 ∈ ℤ
42 uzid ⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
43 41 42 ax-mp ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
44 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) → 𝑁 ∈ ℝ )
45 44 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
46 9 a1i ⊢ ( 𝐼 ∈ ℕ0 → 2 ∈ ℝ )
47 46 1 11 3jca ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ∈ ℝ ∧ 𝐼 ∈ ℤ ∧ 0 < 2 ) )
48 47 3ad2ant3 ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℕ0 ) → ( 2 ∈ ℝ ∧ 𝐼 ∈ ℤ ∧ 0 < 2 ) )
49 48 12 syl ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℕ0 ) → 0 < ( 2 ↑ 𝐼 ) )
50 0red ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℕ0 ) → 0 ∈ ℝ )
51 16 3ad2ant1 ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℕ0 ) → ( 2 ↑ 𝐼 ) ∈ ℝ )
52 19 3ad2ant2 ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
53 50 51 52 21 syl3anc ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℕ0 ) → ( ( 0 < ( 2 ↑ 𝐼 ) ∧ ( 2 ↑ 𝐼 ) ≤ 𝑁 ) → 0 < 𝑁 ) )
54 49 53 mpand ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ ℕ0 ) → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 → 0 < 𝑁 ) )
55 54 3exp ⊢ ( ( 2 ↑ 𝐼 ) ∈ ℤ → ( 𝑁 ∈ ℤ → ( 𝐼 ∈ ℕ0 → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 → 0 < 𝑁 ) ) ) )
56 55 com34 ⊢ ( ( 2 ↑ 𝐼 ) ∈ ℤ → ( 𝑁 ∈ ℤ → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) ) ) )
57 56 3imp ⊢ ( ( ( 2 ↑ 𝐼 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 2 ↑ 𝐼 ) ≤ 𝑁 ) → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) )
58 8 57 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) → ( 𝐼 ∈ ℕ0 → 0 < 𝑁 ) )
59 58 imp ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ 𝐼 ∈ ℕ0 ) → 0 < 𝑁 )
60 45 59 elrpd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ+ )
61 60 adantlr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ+ )
62 9 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 2 ∈ ℝ )
63 peano2nn0 ⊢ ( 𝐼 ∈ ℕ0 → ( 𝐼 + 1 ) ∈ ℕ0 )
64 63 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝐼 + 1 ) ∈ ℕ0 )
65 62 64 reexpcld ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℝ )
66 peano2rem ⊢ ( ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℝ → ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ )
67 65 66 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ )
68 nn0p1nn ⊢ ( 𝐼 ∈ ℕ0 → ( 𝐼 + 1 ) ∈ ℕ )
69 1lt2 ⊢ 1 < 2
70 69 a1i ⊢ ( 𝐼 ∈ ℕ0 → 1 < 2 )
71 46 68 70 3jca ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ∈ ℝ ∧ ( 𝐼 + 1 ) ∈ ℕ ∧ 1 < 2 ) )
72 71 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 2 ∈ ℝ ∧ ( 𝐼 + 1 ) ∈ ℕ ∧ 1 < 2 ) )
73 expgt1 ⊢ ( ( 2 ∈ ℝ ∧ ( 𝐼 + 1 ) ∈ ℕ ∧ 1 < 2 ) → 1 < ( 2 ↑ ( 𝐼 + 1 ) ) )
74 72 73 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 1 < ( 2 ↑ ( 𝐼 + 1 ) ) )
75 1red ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 1 ∈ ℝ )
76 zre ⊢ ( ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ → ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℝ )
77 76 ad2antlr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℝ )
78 75 77 posdifd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 1 < ( 2 ↑ ( 𝐼 + 1 ) ) ↔ 0 < ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) )
79 74 78 mpbid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 0 < ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) )
80 67 79 elrpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ+ )
81 logbleb ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ∧ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ+ ) → ( 𝑁 ≤ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ↔ ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) )
82 43 61 80 81 mp3an2i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑁 ≤ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ↔ ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) )
83 44 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) → 𝑁 ∈ ℝ )
84 83 adantr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
85 59 adantlr ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 0 < 𝑁 )
86 84 85 elrpd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 𝑁 ∈ ℝ+ )
87 33 a1i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → 2 ≠ 1 )
88 3 86 87 35 mp3an2i ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 2 logb 𝑁 ) ∈ ℝ )
89 88 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) ∧ ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) → ( 2 logb 𝑁 ) ∈ ℝ )
90 43 a1i ⊢ ( 𝐼 ∈ ℕ0 → 2 ∈ ( ℤ≥ ‘ 2 ) )
91 46 63 reexpcld ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℝ )
92 91 66 syl ⊢ ( 𝐼 ∈ ℕ0 → ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ )
93 9 68 70 73 mp3an2i ⊢ ( 𝐼 ∈ ℕ0 → 1 < ( 2 ↑ ( 𝐼 + 1 ) ) )
94 1red ⊢ ( 𝐼 ∈ ℕ0 → 1 ∈ ℝ )
95 94 91 posdifd ⊢ ( 𝐼 ∈ ℕ0 → ( 1 < ( 2 ↑ ( 𝐼 + 1 ) ) ↔ 0 < ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) )
96 93 95 mpbid ⊢ ( 𝐼 ∈ ℕ0 → 0 < ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) )
97 92 96 elrpd ⊢ ( 𝐼 ∈ ℕ0 → ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ+ )
98 90 97 jca ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ+ ) )
99 98 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ+ ) )
100 relogbzcl ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ∈ ℝ+ ) → ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ∈ ℝ )
101 99 100 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ∈ ℝ )
102 101 adantr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) ∧ ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) → ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ∈ ℝ )
103 simpr ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) ∧ ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) → ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) )
104 flwordi ⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ∈ ℝ ∧ ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ ( ⌊ ‘ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) )
105 89 102 103 104 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) ∧ ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ ( ⌊ ‘ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) )
106 105 ex ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ ( ⌊ ‘ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) ) )
107 68 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝐼 + 1 ) ∈ ℕ )
108 logbpw2m1 ⊢ ( ( 𝐼 + 1 ) ∈ ℕ → ( ⌊ ‘ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) = ( ( 𝐼 + 1 ) − 1 ) )
109 107 108 syl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ⌊ ‘ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) = ( ( 𝐼 + 1 ) − 1 ) )
110 nn0cn ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℂ )
111 pncan1 ⊢ ( 𝐼 ∈ ℂ → ( ( 𝐼 + 1 ) − 1 ) = 𝐼 )
112 110 111 syl ⊢ ( 𝐼 ∈ ℕ0 → ( ( 𝐼 + 1 ) − 1 ) = 𝐼 )
113 112 adantl ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 𝐼 + 1 ) − 1 ) = 𝐼 )
114 109 113 eqtrd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ⌊ ‘ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) = 𝐼 )
115 114 breq2d ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ ( ⌊ ‘ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) ) ↔ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) )
116 106 115 sylibd ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( ( 2 logb 𝑁 ) ≤ ( 2 logb ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) )
117 82 116 sylbid ⊢ ( ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) ∧ 𝐼 ∈ ℕ0 ) → ( 𝑁 ≤ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) )
118 117 ex ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) → ( 𝐼 ∈ ℕ0 → ( 𝑁 ≤ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) ) )
119 118 com23 ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) → ( 𝑁 ≤ ( ( 2 ↑ ( 𝐼 + 1 ) ) − 1 ) → ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) ) )
120 40 119 sylbid ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ) → ( 𝑁 < ( 2 ↑ ( 𝐼 + 1 ) ) → ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) ) )
121 120 3impia ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ ( 2 ↑ 𝐼 ) ) ∧ ( 2 ↑ ( 𝐼 + 1 ) ) ∈ ℤ ∧ 𝑁 < ( 2 ↑ ( 𝐼 + 1 ) ) ) → ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) )
122 7 121 sylbi ⊢ ( 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) → ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ) )
123 122 impcom ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 )
124 nn0re ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ∈ ℝ )
125 nn0ge0 ⊢ ( 𝐼 ∈ ℕ0 → 0 ≤ 𝐼 )
126 flge0nn0 ⊢ ( ( 𝐼 ∈ ℝ ∧ 0 ≤ 𝐼 ) → ( ⌊ ‘ 𝐼 ) ∈ ℕ0 )
127 124 125 126 syl2anc ⊢ ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ 𝐼 ) ∈ ℕ0 )
128 127 nn0red ⊢ ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ 𝐼 ) ∈ ℝ )
129 128 adantr ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ⌊ ‘ 𝐼 ) ∈ ℝ )
130 124 adantr ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝐼 ∈ ℝ )
131 flle ⊢ ( 𝐼 ∈ ℝ → ( ⌊ ‘ 𝐼 ) ≤ 𝐼 )
132 124 131 syl ⊢ ( 𝐼 ∈ ℕ0 → ( ⌊ ‘ 𝐼 ) ≤ 𝐼 )
133 132 adantr ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ⌊ ‘ 𝐼 ) ≤ 𝐼 )
134 3 a1i ⊢ ( 𝐼 ∈ ℕ0 → 2 ∈ ℝ+ )
135 134 1 rpexpcld ⊢ ( 𝐼 ∈ ℕ0 → ( 2 ↑ 𝐼 ) ∈ ℝ+ )
136 33 a1i ⊢ ( 𝐼 ∈ ℕ0 → 2 ≠ 1 )
137 relogbcl ⊢ ( ( 2 ∈ ℝ+ ∧ ( 2 ↑ 𝐼 ) ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb ( 2 ↑ 𝐼 ) ) ∈ ℝ )
138 3 135 136 137 mp3an2i ⊢ ( 𝐼 ∈ ℕ0 → ( 2 logb ( 2 ↑ 𝐼 ) ) ∈ ℝ )
139 138 adantr ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( 2 logb ( 2 ↑ 𝐼 ) ) ∈ ℝ )
140 nnlogbexp ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐼 ∈ ℤ ) → ( 2 logb ( 2 ↑ 𝐼 ) ) = 𝐼 )
141 90 1 140 syl2anc ⊢ ( 𝐼 ∈ ℕ0 → ( 2 logb ( 2 ↑ 𝐼 ) ) = 𝐼 )
142 141 eqcomd ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 = ( 2 logb ( 2 ↑ 𝐼 ) ) )
143 124 142 eqled ⊢ ( 𝐼 ∈ ℕ0 → 𝐼 ≤ ( 2 logb ( 2 ↑ 𝐼 ) ) )
144 143 adantr ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝐼 ≤ ( 2 logb ( 2 ↑ 𝐼 ) ) )
145 elfzole1 ⊢ ( 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) → ( 2 ↑ 𝐼 ) ≤ 𝑁 )
146 145 adantl ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( 2 ↑ 𝐼 ) ≤ 𝑁 )
147 135 adantr ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( 2 ↑ 𝐼 ) ∈ ℝ+ )
148 logbleb ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 2 ↑ 𝐼 ) ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ) → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 ↔ ( 2 logb ( 2 ↑ 𝐼 ) ) ≤ ( 2 logb 𝑁 ) ) )
149 43 147 31 148 mp3an2i ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ( 2 ↑ 𝐼 ) ≤ 𝑁 ↔ ( 2 logb ( 2 ↑ 𝐼 ) ) ≤ ( 2 logb 𝑁 ) ) )
150 146 149 mpbid ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( 2 logb ( 2 ↑ 𝐼 ) ) ≤ ( 2 logb 𝑁 ) )
151 130 139 36 144 150 letrd ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝐼 ≤ ( 2 logb 𝑁 ) )
152 129 130 36 133 151 letrd ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ⌊ ‘ 𝐼 ) ≤ ( 2 logb 𝑁 ) )
153 flflp1 ⊢ ( ( 𝐼 ∈ ℝ ∧ ( 2 logb 𝑁 ) ∈ ℝ ) → ( ( ⌊ ‘ 𝐼 ) ≤ ( 2 logb 𝑁 ) ↔ 𝐼 < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) )
154 130 36 153 syl2anc ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ( ⌊ ‘ 𝐼 ) ≤ ( 2 logb 𝑁 ) ↔ 𝐼 < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) )
155 152 154 mpbid ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝐼 < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
156 zgeltp1eq ⊢ ( ( 𝐼 ∈ ℤ ∧ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ ) → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ∧ 𝐼 < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) → 𝐼 = ( ⌊ ‘ ( 2 logb 𝑁 ) ) ) )
157 156 imp ⊢ ( ( ( 𝐼 ∈ ℤ ∧ ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ ) ∧ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ≤ 𝐼 ∧ 𝐼 < ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ) ) → 𝐼 = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
158 2 37 123 155 157 syl22anc ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → 𝐼 = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
159 158 eqcomd ⊢ ( ( 𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ( ( 2 ↑ 𝐼 ) ..^ ( 2 ↑ ( 𝐼 + 1 ) ) ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) = 𝐼 )