dignn0flhalflem2

		Ref	Expression
	Assertion	dignn0flhalflem2	$⊢ (A \in ℤ \land \frac{A - 1}{2} \in ℕ \land N \in ℕ_{0}) \to ⌊\frac{A}{2^{N + 1}}⌋ = ⌊\frac{⌊\frac{A}{2}⌋}{2^{N}}⌋$

Proof

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

Metamath Proof Explorer

Theorem dignn0flhalflem2

Proof