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