Metamath Proof Explorer

Theorem dignn0flhalflem1

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

Ref Expression
Assertion dignn0flhalflem1 ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) < ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℝ )
3 2rp ⊢ 2 ∈ ℝ+
4 3 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
5 nnz ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
6 4 5 rpexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
7 6 rpred ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℝ )
8 7 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
9 2 8 resubcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − ( 2 ↑ 𝑁 ) ) ∈ ℝ )
10 6 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
11 9 10 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ∈ ℝ )
12 9 11 resubcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) ∈ ℝ )
13 peano2zm ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℤ )
14 13 zred ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 − 1 ) ∈ ℝ )
15 14 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − 1 ) ∈ ℝ )
16 15 10 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ∈ ℝ )
17 15 16 resubcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) ∈ ℝ )
18 1red ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℝ )
19 18 16 readdcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) ∈ ℝ )
20 8 11 readdcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) ∈ ℝ )
21 2nn ⊢ 2 ∈ ℕ
22 21 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℕ )
23 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
24 22 23 nnexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℕ )
25 24 anim2i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ∈ ℕ ) )
26 25 3adant2 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ∈ ℕ ) )
27 m1modmmod ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 2 ↑ 𝑁 ) ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = if ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 , ( ( 2 ↑ 𝑁 ) − 1 ) , - 1 ) )
28 26 27 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = if ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 , ( ( 2 ↑ 𝑁 ) − 1 ) , - 1 ) )
29 nnz ⊢ ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ )
30 29 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ ) )
31 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
32 xp1d2m1eqxm1d2 ⊢ ( 𝐴 ∈ ℂ → ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) = ( ( 𝐴 − 1 ) / 2 ) )
33 32 eqcomd ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 − 1 ) / 2 ) = ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) )
34 31 33 syl ⊢ ( 𝐴 ∈ ℤ → ( ( 𝐴 − 1 ) / 2 ) = ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) )
35 34 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) / 2 ) = ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) )
36 35 eleq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ ↔ ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) ∈ ℤ ) )
37 peano2z ⊢ ( ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) ∈ ℤ → ( ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) + 1 ) ∈ ℤ )
38 31 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
39 1cnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ )
40 38 39 addcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 + 1 ) ∈ ℂ )
41 40 halfcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 + 1 ) / 2 ) ∈ ℂ )
42 41 39 npcand ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) + 1 ) = ( ( 𝐴 + 1 ) / 2 ) )
43 42 eleq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) + 1 ) ∈ ℤ ↔ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
44 37 43 imbitrid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝐴 + 1 ) / 2 ) − 1 ) ∈ ℤ → ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
45 36 44 sylbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℤ → ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
46 mod0 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 ↔ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
47 1 6 46 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 ↔ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) )
48 22 nnzd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℤ )
49 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
50 48 49 zexpcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
51 50 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
52 51 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
53 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
54 52 53 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ )
55 54 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ) )
56 5 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
57 56 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
58 39 negcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → - 1 ∈ ℂ )
59 57 39 negsubd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 + - 1 ) = ( 𝑁 − 1 ) )
60 57 58 59 mvlladdcd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) − 𝑁 ) = - 1 )
61 60 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( ( 𝑁 − 1 ) − 𝑁 ) ) = ( 2 ↑ - 1 ) )
62 2cnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ∈ ℂ )
63 2ne0 ⊢ 2 ≠ 0
64 63 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ≠ 0 )
65 1zzd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
66 5 65 zsubcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℤ )
67 66 5 jca ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
68 67 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
69 expsub ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 2 ↑ ( ( 𝑁 − 1 ) − 𝑁 ) ) = ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) )
70 62 64 68 69 syl21anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( ( 𝑁 − 1 ) − 𝑁 ) ) = ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) )
71 expn1 ⊢ ( 2 ∈ ℂ → ( 2 ↑ - 1 ) = ( 1 / 2 ) )
72 62 71 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ - 1 ) = ( 1 / 2 ) )
73 61 70 72 3eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) = ( 1 / 2 ) )
74 73 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 · ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 · ( 1 / 2 ) ) )
75 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
76 75 49 expcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
77 76 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
78 3 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ∈ ℝ+ )
79 78 56 rpexpcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
80 79 rpcnne0d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) )
81 div12 ⊢ ( ( ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 · ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) ) )
82 77 38 80 81 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 · ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) ) )
83 38 62 64 divrecd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 2 ) = ( 𝐴 · ( 1 / 2 ) ) )
84 74 82 83 3eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 / 2 ) )
85 84 eleq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ↔ ( 𝐴 / 2 ) ∈ ℤ ) )
86 55 85 sylibd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ → ( 𝐴 / 2 ) ∈ ℤ ) )
87 47 86 sylbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 → ( 𝐴 / 2 ) ∈ ℤ ) )
88 zeo2 ⊢ ( 𝐴 ∈ ℤ → ( ( 𝐴 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
89 88 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
90 87 89 sylibd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 → ¬ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
91 90 necon2ad ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) )
92 30 45 91 3syld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) )
93 92 ex ⊢ ( 𝐴 ∈ ℤ → ( 𝑁 ∈ ℕ → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) ) )
94 93 com23 ⊢ ( 𝐴 ∈ ℤ → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 𝑁 ∈ ℕ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) ) )
95 94 3imp ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 )
96 95 neneqd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ¬ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 )
97 96 iffalsed ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → if ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 , ( ( 2 ↑ 𝑁 ) − 1 ) , - 1 ) = - 1 )
98 28 97 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = - 1 )
99 neg1lt0 ⊢ - 1 < 0
100 2re ⊢ 2 ∈ ℝ
101 1lt2 ⊢ 1 < 2
102 expgt1 ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 2 ) → 1 < ( 2 ↑ 𝑁 ) )
103 100 101 102 mp3an13 ⊢ ( 𝑁 ∈ ℕ → 1 < ( 2 ↑ 𝑁 ) )
104 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
105 104 7 posdifd ⊢ ( 𝑁 ∈ ℕ → ( 1 < ( 2 ↑ 𝑁 ) ↔ 0 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
106 103 105 mpbid ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 2 ↑ 𝑁 ) − 1 ) )
107 104 renegcld ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℝ )
108 0red ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
109 7 104 resubcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℝ )
110 lttr ⊢ ( ( - 1 ∈ ℝ ∧ 0 ∈ ℝ ∧ ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℝ ) → ( ( - 1 < 0 ∧ 0 < ( ( 2 ↑ 𝑁 ) − 1 ) ) → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
111 107 108 109 110 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 < 0 ∧ 0 < ( ( 2 ↑ 𝑁 ) − 1 ) ) → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
112 106 111 mpan2d ⊢ ( 𝑁 ∈ ℕ → ( - 1 < 0 → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
113 99 112 mpi ⊢ ( 𝑁 ∈ ℕ → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) )
114 113 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) )
115 98 114 eqbrtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) − 1 ) )
116 2 10 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℝ )
117 ltsubadd2b ⊢ ( ( ( 1 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ ) ∧ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ∈ ℝ ) ) → ( ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) − 1 ) ↔ ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) )
118 18 8 116 16 117 syl22anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) − 1 ) ↔ ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) )
119 115 118 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
120 modid0 ⊢ ( ( 2 ↑ 𝑁 ) ∈ ℝ+ → ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) = 0 )
121 10 120 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) = 0 )
122 121 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) = ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − 0 ) )
123 116 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
124 123 subid1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − 0 ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
125 122 124 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
126 125 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) )
127 modsubmodmod ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) )
128 2 8 10 127 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) )
129 modabs2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
130 2 10 129 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
131 126 128 130 3eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
132 131 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) = ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
133 119 132 breqtrrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) )
134 19 20 2 133 ltsub2dd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) ) < ( 𝐴 − ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) ) )
135 31 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
136 8 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
137 11 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
138 135 136 137 subsub4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 − ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) ) )
139 1cnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ )
140 16 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
141 135 139 140 subsub4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 − ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) ) )
142 134 138 141 3brtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) )
143 12 17 10 142 ltdiv1dd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) < ( ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
144 7 recnd ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℂ )
145 144 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
146 63 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
147 75 146 5 expne0d ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ≠ 0 )
148 147 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ≠ 0 )
149 divsub1dir ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) → ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) = ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) )
150 149 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) = ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) )
151 135 145 148 150 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) = ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) )
152 fldivmod ⊢ ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
153 9 10 152 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
154 151 153 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) = ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
155 fldivmod ⊢ ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
156 15 10 155 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
157 143 154 156 3brtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) < ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ 𝑁 ) ) ) )