P. 423 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42201-42300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	expnegico01 42201	An integer greater than 1 to the power of a negative integer is in the closed-below, open-above interval between 0 and 1. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝑁 < 0) → (𝐵↑𝑁) ∈ (0[,)1))
Theorem	elfzolborelfzop1 42202	An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a lower bound increased by 1. (Contributed by AV, 2-Jun-2020.)
⊢ (𝐾 ∈ (𝑀..^𝑁) → (𝐾 = 𝑀 ∨ 𝐾 ∈ ((𝑀 + 1)..^𝑁)))
Theorem	pw2m1lepw2m1 42203	2 to the power of a positive integer decreased by 1 is less than or equal to 2 to the power of the integer minus 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐼 ∈ ℕ → (2↑(𝐼 − 1)) ≤ ((2↑𝐼) − 1))
Theorem	zgtp1leeq 42204	If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ) → (((𝐴 − 1) < 𝐼 ∧ 𝐼 ≤ 𝐴) → 𝐼 = 𝐴))
Theorem	flsubz 42205	An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 − 𝑁)) = ((⌊‘𝐴) − 𝑁))
20.34.15.2  The modulo (remainder) operation (extension)
Theorem	fldivmod 42206	Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵))
Theorem	mod0mul 42207*	If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) = 0 → ∃𝑥 ∈ ℤ 𝐴 = (𝑥 · 𝑁)))
Theorem	modn0mul 42208*	If an integer is not 0 modulo a positive integer, this integer must be the sum of the product of another integer and the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) ≠ 0 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (1..^𝑁)𝐴 = ((𝑥 · 𝑁) + 𝑦)))
Theorem	m1modmmod 42209	An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = if((𝐴 mod 𝑁) = 0, (𝑁 − 1), -1))
Theorem	difmodm1lt 42210	The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd 𝐴 and 𝑁 = 2, since ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) would be (1 − 0) = 1 which is not less than (𝑁 − 1) = 1. (Contributed by AV, 6-Jun-2012.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1))
20.34.15.3  Even and odd integers
Theorem	nn0onn0ex 42211*	For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ∃𝑚 ∈ ℕ0 𝑁 = ((2 · 𝑚) + 1))
Theorem	nn0enn0ex 42212*	For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ (𝑁 / 2) ∈ ℕ0) → ∃𝑚 ∈ ℕ0 𝑁 = (2 · 𝑚))
Theorem	nneop 42213	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ))
Theorem	nneom 42214	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	nn0eo 42215	A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.)
⊢ (𝑁 ∈ ℕ0 → ((𝑁 / 2) ∈ ℕ0 ∨ ((𝑁 + 1) / 2) ∈ ℕ0))
Theorem	nnpw2even 42216	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ((2↑𝑁) / 2) ∈ ℕ)
Theorem	zefldiv2 42217	The floor of an even integer divided by 2 is equal to the integer divided by 2. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = (𝑁 / 2))
Theorem	zofldiv2 42218	The floor of an odd integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝑁 ∈ ℤ ∧ ((𝑁 + 1) / 2) ∈ ℤ) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2))
Theorem	nn0ofldiv2 42219	The floor of an odd nonnegative integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.) (Proof shortened by AV, 7-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2))
Theorem	flnn0div2ge 42220	The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.)
⊢ (𝑁 ∈ ℕ0 → ((𝑁 − 1) / 2) ≤ (⌊‘(𝑁 / 2)))
Theorem	flnn0ohalf 42221	The floor of the half of an odd positive integer is equal to the floor of the half of the integer decreased by 1. (Contributed by AV, 5-Jun-2012.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (⌊‘(𝑁 / 2)) = (⌊‘((𝑁 − 1) / 2)))
20.34.15.4  The natural logarithm on complex numbers (extension)
Theorem	logge0b 42222	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → (0 ≤ (log‘𝐴) ↔ 1 ≤ 𝐴))
Theorem	loggt0b 42223	The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → (0 < (log‘𝐴) ↔ 1 < 𝐴))
Theorem	logle1b 42224	The logarithm of a number is less than or equal to 1 iff the number is less than or equal to Euler's constant. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) ≤ 1 ↔ 𝐴 ≤ e))
Theorem	loglt1b 42225	The logarithm of a number is less than 1 iff the number is less than Euler's constant. (Contributed by AV, 30-May-2020.)
⊢ (𝐴 ∈ ℝ+ → ((log‘𝐴) < 1 ↔ 𝐴 < e))
Theorem	logcxp0 42226	Logarithm of a complex power. Generalisation of logcxp 24096. (Contributed by AV, 22-May-2020.)
⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℂ ∧ (𝐵 · (log‘𝐴)) ∈ ran log) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	regt1loggt0 42227	The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.)
⊢ (𝐵 ∈ (1(,)+∞) → 0 < (log‘𝐵))
20.34.15.5  Division of functions
Syntax	cfdiv 42228	Extend class notation with the division operator of two functions.
class /f
Definition	df-fdiv 42229*	Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
⊢ /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘𝑓 / 𝑔) ↾ (𝑔 supp 0)))
Theorem	fdivval 42230	The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 /f 𝐺) = ((𝐹 ∘𝑓 / 𝐺) ↾ (𝐺 supp 0)))
Theorem	fdivmpt 42231*	The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) = (𝑥 ∈ (𝐺 supp 0) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥))))
Theorem	fdivmptf 42232	The quotient of two functions into the complex numbers is a function into the complex numbers. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℂ)
Theorem	refdivmptf 42233	The quotient of two functions into the real numbers is a function into the real numbers. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺):(𝐺 supp 0)⟶ℝ)
Theorem	fdivpm 42234	The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℂ ↑pm 𝐴))
Theorem	refdivpm 42235	The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℝ ↑pm 𝐴))
Theorem	fdivmptfv 42236	The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.)
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋)))
Theorem	refdivmptfv 42237	The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.)
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋)))
20.34.15.6  Upper bounds
Syntax	cbigo 42238	Extend class notation with the class of the "big-O" function.
class Ο
Definition	df-bigo 42239*	Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of [AhoHopUll] p. 2. This is a generalisation of "big-O of one", see df-o1 13938 and df-lo1 13939. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 42248. (Contributed by AV, 15-May-2020.)
⊢ Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))})
Theorem	bigoval 42240*	Set of functions of order G(x). (Contributed by AV, 15-May-2020.)
⊢ (𝐺 ∈ (ℝ ↑pm ℝ) → (Ο‘𝐺) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))})
Theorem	elbigofrcl 42241	Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐺 ∈ (ℝ ↑pm ℝ))
Theorem	elbigo 42242*	Properties of a function of order G(x). (Contributed by AV, 16-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
Theorem	elbigo2 42243*	Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.)
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
Theorem	elbigo2r 42244*	Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.)
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ (𝑀 · (𝐺‘𝑥))))) → 𝐹 ∈ (Ο‘𝐺))
Theorem	elbigof 42245	A function of order G(x) is a function. (Contributed by AV, 18-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐹:dom 𝐹⟶ℝ)
Theorem	elbigodm 42246	The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → dom 𝐹 ⊆ ℝ)
Theorem	elbigoimp 42247*	The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.)
⊢ ((𝐹 ∈ (Ο‘𝐺) ∧ 𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ dom 𝐺) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
Theorem	elbigolo1 42248	A function (into the positive reals) is of order G(x) iff the quotient of the function and G(x) (also a function into the positive reals) is an eventually upper bounded function. (Contributed by AV, 20-May-2020.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 /f 𝐺) ∈ ≤𝑂(1)))
20.34.15.7  Logarithm to an arbitrary base (extension)
Theorem	rege1logbrege0 42249	The general logarithm, with a real base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (1(,)+∞) ∧ 𝑋 ∈ (1[,)+∞)) → 0 ≤ (𝐵 logb 𝑋))
Theorem	rege1logbzge0 42250	The general logarithm, with an integer base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ (1[,)+∞)) → 0 ≤ (𝐵 logb 𝑋))
Theorem	fllogbd 42251	A real number is between the base of a logarithm to the power of the floor of the logarithm of the number and the base of the logarithm to the power of the floor of the logarithm of the number plus one. (Contributed by AV, 23-May-2020.)
⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑋 ∈ ℝ+)    &   ⊢ 𝐸 = (⌊‘(𝐵 logb 𝑋))    ⇒   ⊢ (𝜑 → ((𝐵↑𝐸) ≤ 𝑋 ∧ 𝑋 < (𝐵↑(𝐸 + 1))))
Theorem	relogbmulbexp 42252	The logarithm of the product of a positive real number and the base to the power of a real number is the logarithm of the positive real number plus the real number. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ (𝐴 ∈ ℝ+ ∧ 𝐶 ∈ ℝ)) → (𝐵 logb (𝐴 · (𝐵↑𝑐𝐶))) = ((𝐵 logb 𝐴) + 𝐶))
Theorem	relogbdivb 42253	The logarithm of the quotient of a positive real number and the base is the logarithm of the number minus 1. (Contributed by AV, 29-May-2020.)
⊢ ((𝐵 ∈ (ℝ+ ∖ {1}) ∧ 𝐴 ∈ ℝ+) → (𝐵 logb (𝐴 / 𝐵)) = ((𝐵 logb 𝐴) − 1))
Theorem	logbge0b 42254	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → (0 ≤ (𝐵 logb 𝑋) ↔ 1 ≤ 𝑋))
Theorem	logblt1b 42255	The logarithm of a number is less than 1 iff the number is less than the base of the logarithm. (Contributed by AV, 30-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℝ+) → ((𝐵 logb 𝑋) < 1 ↔ 𝑋 < 𝐵))
20.34.15.8  The binary logarithm If the binary logarithm is used more often, a separate symbol/definition could be provided for it, e.g. log2 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (2 logb 𝑋)). Then we can write "( log2 ` x )" (analogous to (log𝑥) for the natural logarithm) instead of (2 logb 𝑥).
Theorem	fldivexpfllog2 42256	The floor of a positive real number divided by 2 to the power of the floor of the logarithm to base 2 of the number is 1. (Contributed by AV, 26-May-2020.)
⊢ (𝑋 ∈ ℝ+ → (⌊‘(𝑋 / (2↑(⌊‘(2 logb 𝑋))))) = 1)
Theorem	nnlog2ge0lt1 42257	A positive integer is 1 iff its binary logarithm is between 0 and 1. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ↔ (0 ≤ (2 logb 𝑁) ∧ (2 logb 𝑁) < 1)))
Theorem	logbpw2m1 42258	The floor of the binary logarithm of 2 to the power of a positive integer minus 1 is equal to the integer minus 1. (Contributed by AV, 31-May-2020.)
⊢ (𝐼 ∈ ℕ → (⌊‘(2 logb ((2↑𝐼) − 1))) = (𝐼 − 1))
Theorem	fllog2 42259	The floor of the binary logarithm of 2 to the power of an element of a half-open integer interval bounded by powers of 2 is equal to the integer. (Contributed by AV, 31-May-2020.)
⊢ ((𝐼 ∈ ℕ0 ∧ 𝑁 ∈ ((2↑𝐼)..^(2↑(𝐼 + 1)))) → (⌊‘(2 logb 𝑁)) = 𝐼)
20.34.15.9  Binary length
Syntax	cblen 42260	Extend class notation with the class of the binary length function.
class #b
Definition	df-blen 42261	Define the binary length of an integer. Definition in section 1.3 of [AhoHopUll] p. 12. Although not restricted to integers, this definition is only meaningful for 𝑛 ∈ ℤ or even for 𝑛 ∈ ℂ. (Contributed by AV, 16-May-2020.)
⊢ #b = (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))
Theorem	blenval 42262	The binary length of an integer. (Contributed by AV, 20-May-2020.)
⊢ (𝑁 ∈ 𝑉 → (#b‘𝑁) = if(𝑁 = 0, 1, ((⌊‘(2 logb (abs‘𝑁))) + 1)))
Theorem	blen0 42263	The binary length of 0. (Contributed by AV, 20-May-2020.)
⊢ (#b‘0) = 1
Theorem	blenn0 42264	The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.)
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 0) → (#b‘𝑁) = ((⌊‘(2 logb (abs‘𝑁))) + 1))
Theorem	blenre 42265	The binary length of a positive real number. (Contributed by AV, 20-May-2020.)
⊢ (𝑁 ∈ ℝ+ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1))
Theorem	blennn 42266	The binary length of a positive integer. (Contributed by AV, 21-May-2020.)
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1))
Theorem	blennnelnn 42267	The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.)
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) ∈ ℕ)
Theorem	blennn0elnn 42268	The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (#b‘𝑁) ∈ ℕ)
Theorem	blenpw2 42269	The binary length of a power of 2 is the exponent plus 1. (Contributed by AV, 30-May-2020.)
⊢ (𝐼 ∈ ℕ0 → (#b‘(2↑𝐼)) = (𝐼 + 1))
Theorem	blenpw2m1 42270	The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.)
⊢ (𝐼 ∈ ℕ → (#b‘((2↑𝐼) − 1)) = 𝐼)
Theorem	nnpw2blen 42271	A positive integer is between 2 to the power of its binary length minus 1 and 2 to the power of its binary length. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ → ((2↑((#b‘𝑁) − 1)) ≤ 𝑁 ∧ 𝑁 < (2↑(#b‘𝑁))))
Theorem	nnpw2blenfzo 42272	A positive integer is between 2 to the power of the binary length of the integer minus 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020.)
⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ((2↑((#b‘𝑁) − 1))..^(2↑(#b‘𝑁))))
Theorem	nnpw2blenfzo2 42273	A positive integer is either 2 to the power of the binary length of the integer minus 1, or between 2 to the power of the binary length of the integer minus 1, increased by 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020.)
⊢ (𝑁 ∈ ℕ → (𝑁 = (2↑((#b‘𝑁) − 1)) ∨ 𝑁 ∈ (((2↑((#b‘𝑁) − 1)) + 1)..^(2↑(#b‘𝑁)))))
Theorem	nnpw2pmod 42274	Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ → 𝑁 = ((2↑((#b‘𝑁) − 1)) + (𝑁 mod (2↑((#b‘𝑁) − 1)))))
Theorem	blen1 42275	The binary length of 1. (Contributed by AV, 21-May-2020.)
⊢ (#b‘1) = 1
Theorem	blen2 42276	The binary length of 2. (Contributed by AV, 21-May-2020.)
⊢ (#b‘2) = 2
Theorem	nnpw2p 42277*	Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ → ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟))
Theorem	nnpw2pb 42278*	A number is a positive integer iff it can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ ↔ ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟))
Theorem	blen1b 42279	The binary length of a nonnegative integer is 1 if the integer is 0 or 1. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ0 → ((#b‘𝑁) = 1 ↔ (𝑁 = 0 ∨ 𝑁 = 1)))
Theorem	blennnt2 42280	The binary length of a positive integer, doubled and increased by 1, is the binary length of the integer plus 1. (Contributed by AV, 30-May-2010.)
⊢ (𝑁 ∈ ℕ → (#b‘(2 · 𝑁)) = ((#b‘𝑁) + 1))
Theorem	nnolog2flm1 42281	The floor of the binary logarithm of an odd integer greater than 1 is the floor of the binary logarithm of the integer decreased by 1. (Contributed by AV, 2-Jun-2020.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ) → (⌊‘(2 logb 𝑁)) = (⌊‘(2 logb (𝑁 − 1))))
Theorem	blennn0em1 42282	The binary length of the half of an even positive integer is the binary length of the integer minus 1. (Contributed by AV, 30-May-2010.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 / 2) ∈ ℕ0) → (#b‘(𝑁 / 2)) = ((#b‘𝑁) − 1))
Theorem	blennngt2o2 42283	The binary length of an odd integer greater than 1 is the binary length of the half of the integer decreased by 1, increased by 1. (Contributed by AV, 3-Jun-2020.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (#b‘𝑁) = ((#b‘((𝑁 − 1) / 2)) + 1))
Theorem	blengt1fldiv2p1 42284	The binary length of an integer greater than 1 is the binary length of the integer divided by 2, increased by one. (Contributed by AV, 3-Jun-2020.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (#b‘𝑁) = ((#b‘(⌊‘(𝑁 / 2))) + 1))
Theorem	blennn0e2 42285	The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 / 2) ∈ ℕ0) → (#b‘𝑁) = ((#b‘(𝑁 / 2)) + 1))
20.34.15.10  Digits Generalisation of df-bits 14857. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 42305: ((𝐾(digit 2 ) N ) = 1 <-> K e. ( bits 𝑁)).
Syntax	cdig 42286	Extend class notation with the class of the digit extraction operation.
class digit
Definition	df-dig 42287*	Definition of an operation to obtain the 𝑘 th digit of a nonnegative real number 𝑟 in the positional system with base 𝑏. 𝑘 = − 1 corresponds to the first digit of the fractional part (for 𝑏 = 10 the first digit after the decimal point), 𝑘 = 0 corresponds to the last digit of the integer part (for 𝑏 = 10 the first digit before the decimal point). See also digit1 12731. Examples (not formal): ( 234.567 ( digit ` 10 ) 0 ) = 4; ( 2.567 ( digit ` 10 ) -2 ) = 6; ( 2345.67 ( digit ` 10 ) 2 ) = 3. (Contributed by AV, 16-May-2020.)
⊢ digit = (𝑏 ∈ ℕ ↦ (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝑏↑-𝑘) · 𝑟)) mod 𝑏)))
Theorem	digfval 42288*	Operation to obtain the 𝑘 th digit of a nonnegative real number 𝑟 in the positional system with base 𝐵. (Contributed by AV, 23-May-2020.)
⊢ (𝐵 ∈ ℕ → (digit‘𝐵) = (𝑘 ∈ ℤ, 𝑟 ∈ (0[,)+∞) ↦ ((⌊‘((𝐵↑-𝑘) · 𝑟)) mod 𝐵)))
Theorem	digval 42289	The 𝐾 th digit of a nonnegative real number 𝑅 in the positional system with base 𝐵. (Contributed by AV, 23-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ (0[,)+∞)) → (𝐾(digit‘𝐵)𝑅) = ((⌊‘((𝐵↑-𝐾) · 𝑅)) mod 𝐵))
Theorem	digvalnn0 42290	The 𝐾 th digit of a nonnegative real number 𝑅 in the positional system with base 𝐵 is a nonnegative integer. (Contributed by AV, 28-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑅 ∈ (0[,)+∞)) → (𝐾(digit‘𝐵)𝑅) ∈ ℕ0)
Theorem	nn0digval 42291	The 𝐾 th digit of a nonnegative real number 𝑅 in the positional system with base 𝐵. (Contributed by AV, 23-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ∧ 𝑅 ∈ (0[,)+∞)) → (𝐾(digit‘𝐵)𝑅) = ((⌊‘(𝑅 / (𝐵↑𝐾))) mod 𝐵))
Theorem	dignn0fr 42292	The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ (ℤ ∖ ℕ0) ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)𝑁) = 0)
Theorem	dignn0ldlem 42293	Lemma for dignnld 42294. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → 𝑁 < (𝐵↑𝐾))
Theorem	dignnld 42294	The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘((⌊‘(𝐵 logb 𝑁)) + 1))) → (𝐾(digit‘𝐵)𝑁) = 0)
Theorem	dig2nn0ld 42295	The leading digits of a positive integer in a binary system are 0. (Contributed by AV, 25-May-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (ℤ≥‘(#b‘𝑁))) → (𝐾(digit‘2)𝑁) = 0)
Theorem	dig2nn1st 42296	The first (relevant) digit of a positive integer in a binary system is 1. (Contributed by AV, 26-May-2020.)
⊢ (𝑁 ∈ ℕ → (((#b‘𝑁) − 1)(digit‘2)𝑁) = 1)
Theorem	dig0 42297	All digits of 0 are 0. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)0) = 0)
Theorem	digexp 42298	The 𝐾 th digit of a power to the base is either 1 or 0. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝐾(digit‘𝐵)(𝐵↑𝑁)) = if(𝐾 = 𝑁, 1, 0))
Theorem	dig1 42299	All but one digits of 1 are 0. (Contributed by AV, 24-May-2020.)
⊢ ((𝐵 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℤ) → (𝐾(digit‘𝐵)1) = if(𝐾 = 0, 1, 0))
Theorem	0dig1 42300	The 0 th digit of 1 is 1 in any positional system. (Contributed by AV, 28-May-2020.)
⊢ (𝐵 ∈ (ℤ≥‘2) → (0(digit‘𝐵)1) = 1)