Theorem dignn0ehalf

Description: The digits of the half of an even nonnegative integer are the digits of the integer shifted by 1. (Contributed by AV, 3-Jun-2010)

	Ref	Expression
Assertion	dignn0ehalf	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \left(I+1\right)\mathrm{digit}\left(2\right)A=I\mathrm{digit}\left(2\right)\left(\frac{A}{2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0cn	$$⊢A\in {\mathbb{N}}_0\to A\in ℂ$$
2	1	3ad2ant2	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to A\in ℂ$$
3		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
4	3	a1i	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \left(2\in ℂ\wedge 2\ne 0\right)$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6	5	a1i	$$⊢I\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
7		id	$$⊢I\in {\mathbb{N}}_0\to I\in {\mathbb{N}}_0$$
8	6 7	nn0expcld	$$⊢I\in {\mathbb{N}}_0\to 2^I\in {\mathbb{N}}_0$$
9	8	nn0cnd	$$⊢I\in {\mathbb{N}}_0\to 2^I\in ℂ$$
10		2cnd	$$⊢I\in {\mathbb{N}}_0\to 2\in ℂ$$
11		2ne0	$$⊢2\ne 0$$
12	11	a1i	$$⊢I\in {\mathbb{N}}_0\to 2\ne 0$$
13		nn0z	$$⊢I\in {\mathbb{N}}_0\to I\in \mathbb{Z}$$
14	10 12 13	expne0d	$$⊢I\in {\mathbb{N}}_0\to 2^I\ne 0$$
15	9 14	jca	$$⊢I\in {\mathbb{N}}_0\to \left(2^I\in ℂ\wedge 2^I\ne 0\right)$$
16	15	3ad2ant3	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \left(2^I\in ℂ\wedge 2^I\ne 0\right)$$
17		divdiv1	$$⊢\left(A\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2^I\in ℂ\wedge 2^I\ne 0\right)\right)\to \frac{\frac{A}{2}}{2^I}=\frac{A}{22^I}$$
18	2 4 16 17	syl3anc	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \frac{\frac{A}{2}}{2^I}=\frac{A}{22^I}$$
19	10 9	mulcomd	$$⊢I\in {\mathbb{N}}_0\to 22^I=2^I\cdot 2$$
20	19	3ad2ant3	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to 22^I=2^I\cdot 2$$
21		2cnd	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to 2\in ℂ$$
22		simp3	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to I\in {\mathbb{N}}_0$$
23	21 22	expp1d	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to 2^{I+1}=2^I\cdot 2$$
24	20 23	eqtr4d	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to 22^I=2^{I+1}$$
25	24	oveq2d	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \frac{A}{22^I}=\frac{A}{2^{I+1}}$$
26	18 25	eqtr2d	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \frac{A}{2^{I+1}}=\frac{\frac{A}{2}}{2^I}$$
27	26	fveq2d	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to ⌊\frac{A}{2^{I+1}}⌋=⌊\frac{\frac{A}{2}}{2^I}⌋$$
28	27	oveq1d	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to ⌊\frac{A}{2^{I+1}}⌋\mathrm{mod}2=⌊\frac{\frac{A}{2}}{2^I}⌋\mathrm{mod}2$$
29		2nn	$$⊢2\in \mathbb{N}$$
30	29	a1i	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to 2\in \mathbb{N}$$
31		peano2nn0	$$⊢I\in {\mathbb{N}}_0\to I+1\in {\mathbb{N}}_0$$
32	31	3ad2ant3	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to I+1\in {\mathbb{N}}_0$$
33		nn0rp0	$$⊢A\in {\mathbb{N}}_0\to A\in \left[0,\mathrm{+\infty }\right)$$
34	33	3ad2ant2	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to A\in \left[0,\mathrm{+\infty }\right)$$
35		nn0digval	$$⊢\left(2\in \mathbb{N}\wedge I+1\in {\mathbb{N}}_0\wedge A\in \left[0,\mathrm{+\infty }\right)\right)\to \left(I+1\right)\mathrm{digit}\left(2\right)A=⌊\frac{A}{2^{I+1}}⌋\mathrm{mod}2$$
36	30 32 34 35	syl3anc	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \left(I+1\right)\mathrm{digit}\left(2\right)A=⌊\frac{A}{2^{I+1}}⌋\mathrm{mod}2$$
37		nn0rp0	$$⊢\frac{A}{2}\in {\mathbb{N}}_0\to \frac{A}{2}\in \left[0,\mathrm{+\infty }\right)$$
38	37	3ad2ant1	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \frac{A}{2}\in \left[0,\mathrm{+\infty }\right)$$
39		nn0digval	$$⊢\left(2\in \mathbb{N}\wedge I\in {\mathbb{N}}_0\wedge \frac{A}{2}\in \left[0,\mathrm{+\infty }\right)\right)\to I\mathrm{digit}\left(2\right)\left(\frac{A}{2}\right)=⌊\frac{\frac{A}{2}}{2^I}⌋\mathrm{mod}2$$
40	30 22 38 39	syl3anc	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to I\mathrm{digit}\left(2\right)\left(\frac{A}{2}\right)=⌊\frac{\frac{A}{2}}{2^I}⌋\mathrm{mod}2$$
41	28 36 40	3eqtr4d	$$⊢\left(\frac{A}{2}\in {\mathbb{N}}_0\wedge A\in {\mathbb{N}}_0\wedge I\in {\mathbb{N}}_0\right)\to \left(I+1\right)\mathrm{digit}\left(2\right)A=I\mathrm{digit}\left(2\right)\left(\frac{A}{2}\right)$$