Metamath Proof Explorer

Theorem dig2nn0ld

Description: The leading digits of a positive integer in a binary system are 0. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion dig2nn0ld ⊢ N ∈ ℕ ∧ K ∈ ℤ ≥ # b ⁡ N → K digit ⁡ 2 N = 0

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 uzid ⊢ 2 ∈ ℤ → 2 ∈ ℤ ≥ 2
3 1 2 mp1i ⊢ N ∈ ℕ ∧ K ∈ ℤ ≥ # b ⁡ N → 2 ∈ ℤ ≥ 2
4 simpl ⊢ N ∈ ℕ ∧ K ∈ ℤ ≥ # b ⁡ N → N ∈ ℕ
5 blennn ⊢ N ∈ ℕ → # b ⁡ N = log 2 N + 1
6 5 fveq2d ⊢ N ∈ ℕ → ℤ ≥ # b ⁡ N = ℤ ≥ log 2 N + 1
7 6 eleq2d ⊢ N ∈ ℕ → K ∈ ℤ ≥ # b ⁡ N ↔ K ∈ ℤ ≥ log 2 N + 1
8 7 biimpa ⊢ N ∈ ℕ ∧ K ∈ ℤ ≥ # b ⁡ N → K ∈ ℤ ≥ log 2 N + 1
9 dignnld ⊢ 2 ∈ ℤ ≥ 2 ∧ N ∈ ℕ ∧ K ∈ ℤ ≥ log 2 N + 1 → K digit ⁡ 2 N = 0
10 3 4 8 9 syl3anc ⊢ N ∈ ℕ ∧ K ∈ ℤ ≥ # b ⁡ N → K digit ⁡ 2 N = 0