0dig2nn0e

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

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

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2	1	a1i	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to 2 \in ℕ$
3		0nn0	$⊢ 0 \in ℕ_{0}$
4	3	a1i	$⊢ (N \in ℕ_{0} \land \frac{N}{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}{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}{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}{2} \in ℕ_{0}) \to 2^{0} = 1$
12	11	oveq2d	$⊢ (N \in ℕ_{0} \land \frac{N}{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}{2} \in ℕ_{0}) \to \frac{N}{1} = N$
16	12 15	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to \frac{N}{2^{0}} = N$
17	16	fveq2d	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to ⌊\frac{N}{2^{0}}⌋ = ⌊N⌋$
18	17	oveq1d	$⊢ (N \in ℕ_{0} \land \frac{N}{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	adantr	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to ⌊N⌋ = N$
23	22	oveq1d	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to ⌊N⌋ \mod 2 = N \mod 2$
24		nn0z	$⊢ \frac{N}{2} \in ℕ_{0} \to \frac{N}{2} \in ℤ$
25	24	adantl	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to \frac{N}{2} \in ℤ$
26		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
27	26	adantr	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to N \in ℝ$
28		2rp	$⊢ 2 \in ℝ^{+}$
29		mod0	$⊢ (N \in ℝ \land 2 \in ℝ^{+}) \to (N \mod 2 = 0 \leftrightarrow \frac{N}{2} \in ℤ)$
30	27 28 29	sylancl	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to (N \mod 2 = 0 \leftrightarrow \frac{N}{2} \in ℤ)$
31	25 30	mpbird	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to N \mod 2 = 0$
32	23 31	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to ⌊N⌋ \mod 2 = 0$
33	18 32	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to ⌊\frac{N}{2^{0}}⌋ \mod 2 = 0$
34	8 33	eqtrd	$⊢ (N \in ℕ_{0} \land \frac{N}{2} \in ℕ_{0}) \to 0 digit (2) N = 0$

Metamath Proof Explorer

Theorem 0dig2nn0e

Proof