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 syl5ib ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝐴 + 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 zexpcl ⊢ ( ( 2 ∈ ℤ ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
51 48 49 50 syl2anc ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
52 51 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
53 52 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℤ )
54 simpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ )
55 53 54 zmulcld ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ )
56 55 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ) )
57 5 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
58 57 zcnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
59 39 negcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → - 1 ∈ ℂ )
60 58 39 negsubd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 + - 1 ) = ( 𝑁 − 1 ) )
61 60 eqcomd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 1 ) = ( 𝑁 + - 1 ) )
62 58 59 61 mvrladdd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) − 𝑁 ) = - 1 )
63 62 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( ( 𝑁 − 1 ) − 𝑁 ) ) = ( 2 ↑ - 1 ) )
64 2cnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ∈ ℂ )
65 2ne0 ⊢ 2 ≠ 0
66 65 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ≠ 0 )
67 1zzd ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
68 5 67 zsubcld ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℤ )
69 68 5 jca ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
70 69 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
71 expsub ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 2 ↑ ( ( 𝑁 − 1 ) − 𝑁 ) ) = ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) )
72 64 66 70 71 syl21anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( ( 𝑁 − 1 ) − 𝑁 ) ) = ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) )
73 expn1 ⊢ ( 2 ∈ ℂ → ( 2 ↑ - 1 ) = ( 1 / 2 ) )
74 64 73 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ - 1 ) = ( 1 / 2 ) )
75 63 72 74 3eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) = ( 1 / 2 ) )
76 75 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 · ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 · ( 1 / 2 ) ) )
77 2cnd ⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
78 77 49 expcld ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
79 78 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
80 3 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 2 ∈ ℝ+ )
81 80 57 rpexpcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
82 81 rpcnne0d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) )
83 div12 ⊢ ( ( ( 2 ↑ ( 𝑁 − 1 ) ) ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 · ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) ) )
84 79 38 82 83 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 · ( ( 2 ↑ ( 𝑁 − 1 ) ) / ( 2 ↑ 𝑁 ) ) ) )
85 38 64 66 divrecd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 2 ) = ( 𝐴 · ( 1 / 2 ) ) )
86 76 84 85 3eqtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 / 2 ) )
87 86 eleq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 2 ↑ ( 𝑁 − 1 ) ) · ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) ∈ ℤ ↔ ( 𝐴 / 2 ) ∈ ℤ ) )
88 56 87 sylibd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) ∈ ℤ → ( 𝐴 / 2 ) ∈ ℤ ) )
89 47 88 sylbid ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 → ( 𝐴 / 2 ) ∈ ℤ ) )
90 zeo2 ⊢ ( 𝐴 ∈ ℤ → ( ( 𝐴 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
91 90 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
92 89 91 sylibd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 → ¬ ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ ) )
93 92 necon2ad ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 + 1 ) / 2 ) ∈ ℤ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) )
94 30 45 93 3syld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) )
95 94 ex ⊢ ( 𝐴 ∈ ℤ → ( 𝑁 ∈ ℕ → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) ) )
96 95 com23 ⊢ ( 𝐴 ∈ ℤ → ( ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ → ( 𝑁 ∈ ℕ → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 ) ) )
97 96 3imp ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ≠ 0 )
98 97 neneqd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ¬ ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 )
99 98 iffalsed ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → if ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) = 0 , ( ( 2 ↑ 𝑁 ) − 1 ) , - 1 ) = - 1 )
100 28 99 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) = - 1 )
101 neg1lt0 ⊢ - 1 < 0
102 2re ⊢ 2 ∈ ℝ
103 1lt2 ⊢ 1 < 2
104 expgt1 ⊢ ( ( 2 ∈ ℝ ∧ 𝑁 ∈ ℕ ∧ 1 < 2 ) → 1 < ( 2 ↑ 𝑁 ) )
105 102 103 104 mp3an13 ⊢ ( 𝑁 ∈ ℕ → 1 < ( 2 ↑ 𝑁 ) )
106 1red ⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℝ )
107 106 7 posdifd ⊢ ( 𝑁 ∈ ℕ → ( 1 < ( 2 ↑ 𝑁 ) ↔ 0 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
108 105 107 mpbid ⊢ ( 𝑁 ∈ ℕ → 0 < ( ( 2 ↑ 𝑁 ) − 1 ) )
109 106 renegcld ⊢ ( 𝑁 ∈ ℕ → - 1 ∈ ℝ )
110 0red ⊢ ( 𝑁 ∈ ℕ → 0 ∈ ℝ )
111 7 106 resubcld ⊢ ( 𝑁 ∈ ℕ → ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℝ )
112 lttr ⊢ ( ( - 1 ∈ ℝ ∧ 0 ∈ ℝ ∧ ( ( 2 ↑ 𝑁 ) − 1 ) ∈ ℝ ) → ( ( - 1 < 0 ∧ 0 < ( ( 2 ↑ 𝑁 ) − 1 ) ) → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
113 109 110 111 112 syl3anc ⊢ ( 𝑁 ∈ ℕ → ( ( - 1 < 0 ∧ 0 < ( ( 2 ↑ 𝑁 ) − 1 ) ) → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
114 108 113 mpan2d ⊢ ( 𝑁 ∈ ℕ → ( - 1 < 0 → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) ) )
115 101 114 mpi ⊢ ( 𝑁 ∈ ℕ → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) )
116 115 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → - 1 < ( ( 2 ↑ 𝑁 ) − 1 ) )
117 100 116 eqbrtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) − 1 ) )
118 2 10 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℝ )
119 ltsubadd2b ⊢ ( ( ( 1 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ ) ∧ ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ∈ ℝ ) ) → ( ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) − 1 ) ↔ ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) )
120 18 8 118 16 119 syl22anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) − ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) − 1 ) ↔ ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) ) )
121 117 120 mpbid ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
122 modid0 ⊢ ( ( 2 ↑ 𝑁 ) ∈ ℝ+ → ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) = 0 )
123 10 122 syl ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) = 0 )
124 123 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) = ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − 0 ) )
125 118 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
126 125 subid1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − 0 ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
127 124 126 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
128 127 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) )
129 modsubmodmod ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) )
130 2 8 10 129 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) − ( ( 2 ↑ 𝑁 ) mod ( 2 ↑ 𝑁 ) ) ) mod ( 2 ↑ 𝑁 ) ) = ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) )
131 modabs2 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
132 2 10 131 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
133 128 130 132 3eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) = ( 𝐴 mod ( 2 ↑ 𝑁 ) ) )
134 133 oveq2d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) = ( ( 2 ↑ 𝑁 ) + ( 𝐴 mod ( 2 ↑ 𝑁 ) ) ) )
135 121 134 breqtrrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) )
136 19 20 2 135 ltsub2dd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 − ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) ) < ( 𝐴 − ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) ) )
137 31 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℂ )
138 8 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
139 11 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
140 137 138 139 subsub4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 − ( ( 2 ↑ 𝑁 ) + ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) ) )
141 1cnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ )
142 16 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ∈ ℂ )
143 137 141 142 subsub4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) = ( 𝐴 − ( 1 + ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) ) )
144 136 140 143 3brtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) < ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) )
145 12 17 10 144 ltdiv1dd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) < ( ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
146 7 recnd ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ∈ ℂ )
147 146 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
148 65 a1i ⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
149 77 148 5 expne0d ⊢ ( 𝑁 ∈ ℕ → ( 2 ↑ 𝑁 ) ≠ 0 )
150 149 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 ↑ 𝑁 ) ≠ 0 )
151 divsub1dir ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) → ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) = ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) )
152 151 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ∈ ℂ ∧ ( 2 ↑ 𝑁 ) ≠ 0 ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) = ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) )
153 137 147 150 152 syl3anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) = ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) )
154 fldivmod ⊢ ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
155 9 10 154 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
156 153 155 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) = ( ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) − ( ( 𝐴 − ( 2 ↑ 𝑁 ) ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
157 fldivmod ⊢ ( ( ( 𝐴 − 1 ) ∈ ℝ ∧ ( 2 ↑ 𝑁 ) ∈ ℝ+ ) → ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
158 15 10 157 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ 𝑁 ) ) ) = ( ( ( 𝐴 − 1 ) − ( ( 𝐴 − 1 ) mod ( 2 ↑ 𝑁 ) ) ) / ( 2 ↑ 𝑁 ) ) )
159 145 156 158 3brtr4d ⊢ ( ( 𝐴 ∈ ℤ ∧ ( ( 𝐴 − 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( ( 𝐴 / ( 2 ↑ 𝑁 ) ) − 1 ) ) < ( ⌊ ‘ ( ( 𝐴 − 1 ) / ( 2 ↑ 𝑁 ) ) ) )