Metamath Proof Explorer

Theorem 0dig2nn0o

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

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

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 1 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → 2 ∈ ℕ )
3 0nn0 ⊢ 0 ∈ ℕ0
4 3 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → 0 ∈ ℕ0 )
5 nn0rp0 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 [,) +∞ ) )
6 5 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → 𝑁 ∈ ( 0 [,) +∞ ) )
7 nn0digval ⊢ ( ( 2 ∈ ℕ ∧ 0 ∈ ℕ0 ∧ 𝑁 ∈ ( 0 [,) +∞ ) ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) )
8 2 4 6 7 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) )
9 2cn ⊢ 2 ∈ ℂ
10 exp0 ⊢ ( 2 ∈ ℂ → ( 2 ↑ 0 ) = 1 )
11 9 10 mp1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 2 ↑ 0 ) = 1 )
12 11 oveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 / ( 2 ↑ 0 ) ) = ( 𝑁 / 1 ) )
13 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
14 13 div1d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 / 1 ) = 𝑁 )
15 14 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 / 1 ) = 𝑁 )
16 12 15 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 / ( 2 ↑ 0 ) ) = 𝑁 )
17 16 fveq2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) = ( ⌊ ‘ 𝑁 ) )
18 17 oveq1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) = ( ( ⌊ ‘ 𝑁 ) mod 2 ) )
19 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
20 flid ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ 𝑁 ) = 𝑁 )
21 19 20 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ⌊ ‘ 𝑁 ) = 𝑁 )
22 21 oveq1d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ⌊ ‘ 𝑁 ) mod 2 ) = ( 𝑁 mod 2 ) )
23 22 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ 𝑁 ) mod 2 ) = ( 𝑁 mod 2 ) )
24 nn0z ⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
25 24 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ )
26 2z ⊢ 2 ∈ ℤ
27 26 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → 2 ∈ ℤ )
28 2ne0 ⊢ 2 ≠ 0
29 28 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → 2 ≠ 0 )
30 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
31 30 nn0zd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℤ )
32 31 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 + 1 ) ∈ ℤ )
33 dvdsval2 ⊢ ( ( 2 ∈ ℤ ∧ 2 ≠ 0 ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 2 ∥ ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
34 27 29 32 33 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 2 ∥ ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
35 25 34 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → 2 ∥ ( 𝑁 + 1 ) )
36 oddp1even ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) )
37 19 36 syl ⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) )
38 37 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) )
39 35 38 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ¬ 2 ∥ 𝑁 )
40 19 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → 𝑁 ∈ ℤ )
41 mod2eq1n2dvds ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 mod 2 ) = 1 ↔ ¬ 2 ∥ 𝑁 ) )
42 40 41 syl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( 𝑁 mod 2 ) = 1 ↔ ¬ 2 ∥ 𝑁 ) )
43 39 42 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑁 mod 2 ) = 1 )
44 23 43 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ 𝑁 ) mod 2 ) = 1 )
45 18 44 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 0 ) ) ) mod 2 ) = 1 )
46 8 45 eqtrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( 0 ( digit ‘ 2 ) 𝑁 ) = 1 )