Metamath Proof Explorer

Theorem dignn0flhalflem2

Description: Lemma 2 for dignn0flhalf . (Contributed by AV, 7-Jun-2012)

Ref Expression
Assertion dignn0flhalflem2 ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2 1 rehalfcld ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 / 2 ) ∈ ℝ )
3 2 flcld ⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℤ )
4 3 zred ⊢ ( 𝐴 ∈ ℤ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
5 4 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
6 2re ⊢ 2 ∈ ℝ
7 6 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ )
8 id ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
9 7 8 reexpcld ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℝ )
10 9 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
11 2cnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℂ )
12 2ne0 ⊢ 2 ≠ 0
13 12 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ≠ 0 )
14 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
15 14 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
16 11 13 15 expne0d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ≠ 0 )
17 5 10 16 redivcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
18 17 flcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ )
19 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℝ )
20 6 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℝ )
21 simp3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
22 1nn0 ⊢ 1 ∈ ℕ0
23 22 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℕ0 )
24 21 23 nn0addcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℕ0 )
25 20 24 reexpcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ∈ ℝ )
26 15 peano2zd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℤ )
27 11 13 26 expne0d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) ≠ 0 )
28 19 25 27 redivcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℝ )
29 28 flcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ∈ ℤ )
30 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
31 dignn0flhalflem1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑁 + 1 ) ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) < ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
32 30 31 syl3an3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) < ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
33 1zzd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℤ )
34 flsubz ⊢ ( ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) )
35 28 33 34 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) = ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) )
36 35 eqcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) = ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) − 1 ) ) )
37 nnz ⊢ ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ )
38 zob ⊢ ( 𝐴 ∈ ℤ → ( ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ↔ ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ ) )
39 37 38 imbitrrid ⊢ ( 𝐴 ∈ ℤ → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
40 39 imp ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ) → ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ )
41 zofldiv2 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) = ( ( 𝐴 − 1 ) / 2 ) )
42 40 41 syldan ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) = ( ( 𝐴 − 1 ) / 2 ) )
43 42 3adant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) = ( ( 𝐴 − 1 ) / 2 ) )
44 43 fvoveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
45 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
46 1cnd ⊢ ( 𝐴 ∈ ℤ → 1 ∈ ℂ )
47 45 46 subcld ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℂ )
48 2rp ⊢ 2 ∈ ℝ+
49 48 a1i ⊢ ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → 2 ∈ ℝ+ )
50 49 rpcnne0d ⊢ ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
51 48 a1i ⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℝ+ )
52 51 14 rpexpcld ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
53 52 rpcnne0d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) )
54 divdiv1 ⊢ ( ( ( 𝐴 − 1 ) ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) ) → ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
55 47 50 53 54 syl3an ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
56 10 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
57 11 56 mulcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
58 11 21 expp1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
59 57 58 eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
60 59 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 − 1 ) / ( 2 · ( 2 ↑ 𝑁 ) ) ) = ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
61 55 60 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
62 61 fveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ( 𝐴 − 1 ) / 2 ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
63 44 62 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
64 32 36 63 3brtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) < ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) )
65 19 rehalfcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / 2 ) ∈ ℝ )
66 65 10 16 redivcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
67 reflcl ⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
68 65 67 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) ∈ ℝ )
69 48 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → 2 ∈ ℝ+ )
70 69 15 rpexpcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
71 flle ⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 2 ) ) ≤ ( 𝐴 / 2 ) )
72 65 71 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / 2 ) ) ≤ ( 𝐴 / 2 ) )
73 68 65 70 72 lediv1dd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ≤ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) )
74 flwordi ⊢ ( ( ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ≤ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
75 17 66 73 74 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
76 divdiv1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) = ( 𝐴 / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
77 45 50 53 76 syl3an ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) = ( 𝐴 / ( 2 · ( 2 ↑ 𝑁 ) ) ) )
78 52 rpcnd ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℂ )
79 78 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
80 11 79 mulcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
81 11 13 15 expp1zd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
82 80 81 eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 · ( 2 ↑ 𝑁 ) ) = ( 2 ↑ ( 𝑁 + 1 ) ) )
83 82 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 2 · ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
84 77 83 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) = ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) )
85 84 eqcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) = ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) )
86 85 fveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) = ( ⌊ ‘ ( ( 𝐴 / 2 ) / ( 2 ↑ 𝑁 ) ) ) )
87 75 86 breqtrrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
88 zgtp1leeq ⊢ ( ( ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ∈ ℤ ) → ( ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) < ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∧ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) )
89 88 imp ⊢ ( ( ( ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ∧ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ∈ ℤ ) ∧ ( ( ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) − 1 ) < ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ∧ ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) ≤ ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) ) ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
90 18 29 64 87 89 syl22anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) )
91 90 eqcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( 𝐴 / ( 2 ↑ ( 𝑁 + 1 ) ) ) ) = ( ⌊ ‘ ( ( ⌊ ‘ ( 𝐴 / 2 ) ) / ( 2 ↑ 𝑁 ) ) ) )