dignn0flhalf

Description: The digits of the rounded half of a nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 7-Jun-2010)

		Ref	Expression
	Assertion	dignn0flhalf	$⊢ (A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋$

Proof

Step	Hyp	Ref	Expression
1		eluzge2nn0	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ_{0}$
2		nn0eo	$⊢ A \in ℕ_{0} \to (\frac{A}{2} \in ℕ_{0} \lor \frac{A + 1}{2} \in ℕ_{0})$
3	1 2	syl	$⊢ A \in ℤ_{\geq 2} \to (\frac{A}{2} \in ℕ_{0} \lor \frac{A + 1}{2} \in ℕ_{0})$
4		dignn0ehalf	$⊢ (\frac{A}{2} \in ℕ_{0} \land A \in ℕ_{0} \land I \in ℕ_{0}) \to (I + 1) digit (2) A = I digit (2) (\frac{A}{2})$
5	1 4	syl3an2	$⊢ (\frac{A}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to (I + 1) digit (2) A = I digit (2) (\frac{A}{2})$
6		eluzelz	$⊢ A \in ℤ_{\geq 2} \to A \in ℤ$
7		nn0z	$⊢ \frac{A}{2} \in ℕ_{0} \to \frac{A}{2} \in ℤ$
8		zefldiv2	$⊢ (A \in ℤ \land \frac{A}{2} \in ℤ) \to ⌊\frac{A}{2}⌋ = \frac{A}{2}$
9	6 7 8	syl2anr	$⊢ (\frac{A}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to ⌊\frac{A}{2}⌋ = \frac{A}{2}$
10	9	eqcomd	$⊢ (\frac{A}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2}) \to \frac{A}{2} = ⌊\frac{A}{2}⌋$
11	10	3adant3	$⊢ (\frac{A}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to \frac{A}{2} = ⌊\frac{A}{2}⌋$
12	11	oveq2d	$⊢ (\frac{A}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to I digit (2) (\frac{A}{2}) = I digit (2) ⌊\frac{A}{2}⌋$
13	5 12	eqtrd	$⊢ (\frac{A}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋$
14	13	3exp	$⊢ \frac{A}{2} \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to (I \in ℕ_{0} \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋))$
15	6	3ad2ant2	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to A \in ℤ$
16		simp2	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to A \in ℤ_{\geq 2}$
17		simp1	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to \frac{A + 1}{2} \in ℕ_{0}$
18		nno	$⊢ (A \in ℤ_{\geq 2} \land \frac{A + 1}{2} \in ℕ_{0}) \to \frac{A - 1}{2} \in ℕ$
19	16 17 18	syl2anc	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to \frac{A - 1}{2} \in ℕ$
20		simp3	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to I \in ℕ_{0}$
21		dignn0flhalflem2	$⊢ (A \in ℤ \land \frac{A - 1}{2} \in ℕ \land I \in ℕ_{0}) \to ⌊\frac{A}{2^{I + 1}}⌋ = ⌊\frac{⌊\frac{A}{2}⌋}{2^{I}}⌋$
22	15 19 20 21	syl3anc	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to ⌊\frac{A}{2^{I + 1}}⌋ = ⌊\frac{⌊\frac{A}{2}⌋}{2^{I}}⌋$
23	22	oveq1d	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to ⌊\frac{A}{2^{I + 1}}⌋ \mod 2 = ⌊\frac{⌊\frac{A}{2}⌋}{2^{I}}⌋ \mod 2$
24		2nn	$⊢ 2 \in ℕ$
25	24	a1i	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to 2 \in ℕ$
26		peano2nn0	$⊢ I \in ℕ_{0} \to I + 1 \in ℕ_{0}$
27	26	3ad2ant3	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to I + 1 \in ℕ_{0}$
28		nn0rp0	$⊢ A \in ℕ_{0} \to A \in [0, +∞)$
29	1 28	syl	$⊢ A \in ℤ_{\geq 2} \to A \in [0, +∞)$
30	29	3ad2ant2	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to A \in [0, +∞)$
31		nn0digval	$⊢ (2 \in ℕ \land I + 1 \in ℕ_{0} \land A \in [0, +∞)) \to (I + 1) digit (2) A = ⌊\frac{A}{2^{I + 1}}⌋ \mod 2$
32	25 27 30 31	syl3anc	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to (I + 1) digit (2) A = ⌊\frac{A}{2^{I + 1}}⌋ \mod 2$
33		eluzelre	$⊢ A \in ℤ_{\geq 2} \to A \in ℝ$
34	33	rehalfcld	$⊢ A \in ℤ_{\geq 2} \to \frac{A}{2} \in ℝ$
35	1	nn0ge0d	$⊢ A \in ℤ_{\geq 2} \to 0 \leq A$
36		2re	$⊢ 2 \in ℝ$
37		2pos	$⊢ 0 < 2$
38	36 37	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
39	38	a1i	$⊢ A \in ℤ_{\geq 2} \to (2 \in ℝ \land 0 < 2)$
40		divge0	$⊢ ((A \in ℝ \land 0 \leq A) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{A}{2}$
41	33 35 39 40	syl21anc	$⊢ A \in ℤ_{\geq 2} \to 0 \leq \frac{A}{2}$
42		flge0nn0	$⊢ (\frac{A}{2} \in ℝ \land 0 \leq \frac{A}{2}) \to ⌊\frac{A}{2}⌋ \in ℕ_{0}$
43	34 41 42	syl2anc	$⊢ A \in ℤ_{\geq 2} \to ⌊\frac{A}{2}⌋ \in ℕ_{0}$
44	43	3ad2ant2	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to ⌊\frac{A}{2}⌋ \in ℕ_{0}$
45		nn0rp0	$⊢ ⌊\frac{A}{2}⌋ \in ℕ_{0} \to ⌊\frac{A}{2}⌋ \in [0, +∞)$
46	44 45	syl	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to ⌊\frac{A}{2}⌋ \in [0, +∞)$
47		nn0digval	$⊢ (2 \in ℕ \land I \in ℕ_{0} \land ⌊\frac{A}{2}⌋ \in [0, +∞)) \to I digit (2) ⌊\frac{A}{2}⌋ = ⌊\frac{⌊\frac{A}{2}⌋}{2^{I}}⌋ \mod 2$
48	25 20 46 47	syl3anc	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to I digit (2) ⌊\frac{A}{2}⌋ = ⌊\frac{⌊\frac{A}{2}⌋}{2^{I}}⌋ \mod 2$
49	23 32 48	3eqtr4d	$⊢ (\frac{A + 1}{2} \in ℕ_{0} \land A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋$
50	49	3exp	$⊢ \frac{A + 1}{2} \in ℕ_{0} \to (A \in ℤ_{\geq 2} \to (I \in ℕ_{0} \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋))$
51	14 50	jaoi	$⊢ (\frac{A}{2} \in ℕ_{0} \lor \frac{A + 1}{2} \in ℕ_{0}) \to (A \in ℤ_{\geq 2} \to (I \in ℕ_{0} \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋))$
52	3 51	mpcom	$⊢ A \in ℤ_{\geq 2} \to (I \in ℕ_{0} \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋)$
53	52	imp	$⊢ (A \in ℤ_{\geq 2} \land I \in ℕ_{0}) \to (I + 1) digit (2) A = I digit (2) ⌊\frac{A}{2}⌋$

Metamath Proof Explorer

Theorem dignn0flhalf

Proof