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 \in ℕ \land K \in ℤ_{\geq #_{b(N)\toK digit (2) N = 0}})$

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
3	1 2	mp1i	$⊢ (N \in ℕ \land K \in ℤ_{\geq #_{b(N)\to2 \in ℤ_{\geq 2}}})$
4		simpl	$⊢ (N \in ℕ \land K \in ℤ_{\geq #_{b(N)\toN \in ℕ}})$
5		blennn	$⊢ N \in ℕ \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
6	5	fveq2d	$⊢ N \in ℕ \to ℤ_{\geq #_{b(N)=ℤ_{\geq (⌊\log_{2} N⌋ + 1)}}}$
7	6	eleq2d	$⊢ N \in ℕ \to (K \in ℤ_{\geq #_{b(N)\leftrightarrowK \in ℤ_{\geq (⌊\log_{2} N⌋ + 1)}}})$
8	7	biimpa	$⊢ (N \in ℕ \land K \in ℤ_{\geq #_{b(N)\toK \in ℤ_{\geq (⌊\log_{2} N⌋ + 1)}}})$
9		dignnld	$⊢ (2 \in ℤ_{\geq 2} \land N \in ℕ \land K \in ℤ_{\geq (⌊\log_{2} N⌋ + 1)}) \to K digit (2) N = 0$
10	3 4 8 9	syl3anc	$⊢ (N \in ℕ \land K \in ℤ_{\geq #_{b(N)\toK digit (2) N = 0}})$

Metamath Proof Explorer