Metamath Proof Explorer

Theorem 0dig2nn0e

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

Ref Expression
Assertion 0dig2nn0e ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = 0 )

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 1 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 2 ∈ ℕ )
3 0nn0 ⊢ 0 ∈ ℕ0
4 3 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 0 ∈ ℕ0 )
5 nn0rp0 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 [,) +∞ ) )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 𝑁 ∈ ( 0 [,) +∞ ) )
7 nn0digval ⊢ ( ( 2 ∈ ℕ ∧ 0 ∈ ℕ0 ∧ 𝑁 ∈ ( 0 [,) +∞ ) ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) )
8 2 4 6 7 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) )
9 2cn ⊢ 2 ∈ ℂ
10 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
11 9 10 mp1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 2 ↑ 0 ) = 1 )
12 11 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 / ( 2 ↑ 0 ) ) = ( 𝑁 / 1 ) )
13 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
14 13 div1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 / 1 ) = 𝑁 )
15 14 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 / 1 ) = 𝑁 )
16 12 15 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 / ( 2 ↑ 0 ) ) = 𝑁 )
17 16 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) = ( ⌊ ‘ 𝑁 ) )
18 17 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) = ( ( ⌊ ‘ 𝑁 ) mod 2 ) )
19 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
20 flid ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
21 19 20 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ⌊ ‘ 𝑁 ) = 𝑁 )
22 21 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ 𝑁 ) = 𝑁 )
23 22 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ 𝑁 ) mod 2 ) = ( 𝑁 mod 2 ) )
24 nn0z ⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 → ( 𝑁 / 2 ) ∈ ℤ )
25 24 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 / 2 ) ∈ ℤ )
26 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 𝑁 ∈ ℝ )
28 2rp ⊢ 2 ∈ ℝ+
29 mod0 ⊢ ( ( 𝑁 ∈ ℝ ∧ 2 ∈ ℝ+ ) → ( ( 𝑁 mod 2 ) = 0 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
30 27 28 29 sylancl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( 𝑁 mod 2 ) = 0 ↔ ( 𝑁 / 2 ) ∈ ℤ ) )
31 25 30 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 mod 2 ) = 0 )
32 23 31 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ 𝑁 ) mod 2 ) = 0 )
33 18 32 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) = 0 )
34 8 33 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = 0 )