0dig2nn0o

Description: The last bit of an odd integer is 1. (Contributed by AV, 3-Jun-2010)

		Ref	Expression
	Assertion	0dig2nn0o	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 0 digit (2) N = 1$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2	1	a1i	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 2 \in ℕ$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4	3	a1i	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 0 \in ℕ_{0}$
5		nn0rp0	$⊢ N \in ℕ_{0} \to N \in [0, +∞)$
6	5	adantr	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to N \in [0, +∞)$
7		nn0digval	$⊢ (2 \in ℕ \land 0 \in ℕ_{0} \land N \in [0, +∞)) \to 0 digit (2) N = ⌊\frac{N}{2^{0}}⌋ \mod 2$
8	2 4 6 7	syl3anc	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 0 digit (2) N = ⌊\frac{N}{2^{0}}⌋ \mod 2$
9		2cn	$⊢ 2 \in ℂ$
10		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
11	9 10	mp1i	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 2^{0} = 1$
12	11	oveq2d	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N}{2^{0}} = \frac{N}{1}$
13		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
14	13	div1d	$⊢ N \in ℕ_{0} \to \frac{N}{1} = N$
15	14	adantr	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N}{1} = N$
16	12 15	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N}{2^{0}} = N$
17	16	fveq2d	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\frac{N}{2^{0}}⌋ = ⌊N⌋$
18	17	oveq1d	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\frac{N}{2^{0}}⌋ \mod 2 = ⌊N⌋ \mod 2$
19		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
20		flid	$⊢ N \in ℤ \to ⌊N⌋ = N$
21	19 20	syl	$⊢ N \in ℕ_{0} \to ⌊N⌋ = N$
22	21	oveq1d	$⊢ N \in ℕ_{0} \to ⌊N⌋ \mod 2 = N \mod 2$
23	22	adantr	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊N⌋ \mod 2 = N \mod 2$
24		nn0z	$⊢ \frac{N + 1}{2} \in ℕ_{0} \to \frac{N + 1}{2} \in ℤ$
25	24	adantl	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N + 1}{2} \in ℤ$
26		2z	$⊢ 2 \in ℤ$
27	26	a1i	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 2 \in ℤ$
28		2ne0	$⊢ 2 \neq 0$
29	28	a1i	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 2 \neq 0$
30		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
31	30	nn0zd	$⊢ N \in ℕ_{0} \to N + 1 \in ℤ$
32	31	adantr	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to N + 1 \in ℤ$
33		dvdsval2	$⊢ (2 \in ℤ \land 2 \neq 0 \land N + 1 \in ℤ) \to (2 ∥ (N + 1) \leftrightarrow \frac{N + 1}{2} \in ℤ)$
34	27 29 32 33	syl3anc	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to (2 ∥ (N + 1) \leftrightarrow \frac{N + 1}{2} \in ℤ)$
35	25 34	mpbird	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 2 ∥ (N + 1)$
36		oddp1even	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow 2 ∥ (N + 1))$
37	19 36	syl	$⊢ N \in ℕ_{0} \to (\neg 2 ∥ N \leftrightarrow 2 ∥ (N + 1))$
38	37	adantr	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to (\neg 2 ∥ N \leftrightarrow 2 ∥ (N + 1))$
39	35 38	mpbird	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to \neg 2 ∥ N$
40	19	adantr	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to N \in ℤ$
41		mod2eq1n2dvds	$⊢ N \in ℤ \to (N \mod 2 = 1 \leftrightarrow \neg 2 ∥ N)$
42	40 41	syl	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to (N \mod 2 = 1 \leftrightarrow \neg 2 ∥ N)$
43	39 42	mpbird	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to N \mod 2 = 1$
44	23 43	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊N⌋ \mod 2 = 1$
45	18 44	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\frac{N}{2^{0}}⌋ \mod 2 = 1$
46	8 45	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to 0 digit (2) N = 1$

Metamath Proof Explorer

Theorem 0dig2nn0o

Proof