dignn0flhalflem1

		Ref	Expression
	Assertion	dignn0flhalflem1	$⊢ (A \in ℤ \land \frac{A - 1}{2} \in ℕ \land N \in ℕ) \to ⌊(\frac{A}{2^{N}}) - 1⌋ < ⌊\frac{A - 1}{2^{N}}⌋$

Proof

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

Metamath Proof Explorer

Theorem dignn0flhalflem1

Proof