P. 494 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 49301-49400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lmod1zr 49301	The (smallest) structure representing a zero module over a zero ring. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    &   ⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∈ LMod)
Theorem	lmod1zrnlvec 49302	There is a (left) module (a zero module) which is not a (left) vector space. (Contributed by AV, 29-Apr-2019.)
⊢ 𝑅 = {⟨(Base‘ndx), {𝑍}⟩, ⟨(+g‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩, ⟨(.r‘ndx), {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}⟩}    &   ⊢ 𝑀 = ({⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩, ⟨(Scalar‘ndx), 𝑅⟩} ∪ {⟨( ·𝑠 ‘ndx), {⟨⟨𝑍, 𝐼⟩, 𝐼⟩}⟩})    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑀 ∉ LVec)
Theorem	lmodn0 49303	Left modules exist. (Contributed by AV, 29-Apr-2019.)
⊢ LMod ≠ ∅
Theorem	zlmodzxzequa 49304	Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    &   ⊢ − = (-g‘𝑍)    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ ((2 ∙ 𝐴) − (3 ∙ 𝐵)) = 0
Theorem	zlmodzxznm 49305	Example of a linearly dependent set whose elements are not linear combinations of the others, see note in [Roman] p. 112). (Contributed by AV, 23-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    &   ⊢ − = (-g‘𝑍)    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ ∀𝑖 ∈ ℤ ((𝑖 ∙ 𝐴) ≠ 𝐵 ∧ (𝑖 ∙ 𝐵) ≠ 𝐴)
Theorem	zlmodzxzldeplem 49306	A and B are not equal. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ 𝐴 ≠ 𝐵
Theorem	zlmodzxzequap 49307	Example of an equation within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112 for a linearly dependent set), written as a sum. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 0 = {⟨0, 0⟩, ⟨1, 0⟩}    &   ⊢ + = (+g‘𝑍)    &   ⊢ ∙ = ( ·𝑠 ‘𝑍)    ⇒   ⊢ ((2 ∙ 𝐴) + (-3 ∙ 𝐵)) = 0
Theorem	zlmodzxzldeplem1 49308	Lemma 1 for zlmodzxzldep 49312. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ 𝐹 ∈ (ℤ ↑m {𝐴, 𝐵})
Theorem	zlmodzxzldeplem2 49309	Lemma 2 for zlmodzxzldep 49312. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ 𝐹 finSupp 0
Theorem	zlmodzxzldeplem3 49310	Lemma 3 for zlmodzxzldep 49312. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ (𝐹( linC ‘𝑍){𝐴, 𝐵}) = (0g‘𝑍)
Theorem	zlmodzxzldeplem4 49311*	Lemma 4 for zlmodzxzldep 49312. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    &   ⊢ 𝐹 = {⟨𝐴, 2⟩, ⟨𝐵, -3⟩}    ⇒   ⊢ ∃𝑦 ∈ {𝐴, 𝐵} (𝐹‘𝑦) ≠ 0
Theorem	zlmodzxzldep 49312	{ A , B } is a linearly dependent set within the ℤ-module ℤ × ℤ (see example in [Roman] p. 112). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ {𝐴, 𝐵} linDepS 𝑍
Theorem	ldepsnlinclem1 49313	Lemma 1 for ldepsnlinc 49316. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐵}) → (𝐹( linC ‘𝑍){𝐵}) ≠ 𝐴)
Theorem	ldepsnlinclem2 49314	Lemma 2 for ldepsnlinc 49316. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
⊢ 𝑍 = (ℤring freeLMod {0, 1})    &   ⊢ 𝐴 = {⟨0, 3⟩, ⟨1, 6⟩}    &   ⊢ 𝐵 = {⟨0, 2⟩, ⟨1, 4⟩}    ⇒   ⊢ (𝐹 ∈ ((Base‘ℤring) ↑m {𝐴}) → (𝐹( linC ‘𝑍){𝐴}) ≠ 𝐵)
21.49.21.5  Differences between (left) modules and (left) vector spaces
Theorem	lvecpsslmod 49315	The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod 21238) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec 49302. (Contributed by AV, 29-Apr-2019.)
⊢ LVec ⊊ LMod
Theorem	ldepsnlinc 49316*	The reverse implication of islindeps2 49291 does not hold for arbitrary (left) modules, see note in [Roman] p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combination of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 49304 and zlmodzxznm 49305. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣))
Theorem	ldepslinc 49317*	For (left) vector spaces, isldepslvec2 49293 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 49316 indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
⊢ (∀𝑚 ∈ LVec ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣)) ∧ ¬ ∀𝑚 ∈ LMod ∀𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ↔ ∃𝑣 ∈ 𝑠 ∃𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) ∧ (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣)))
21.49.22  Complexity theory
21.49.22.1  Auxiliary theorems
Theorem	suppdm 49318	If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020.)
⊢ (((Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ 𝑍 ∉ ran 𝐹) → (𝐹 supp 𝑍) = dom 𝐹)
Theorem	eluz2cnn0n1 49319	An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020.)
⊢ (𝐵 ∈ (ℤ≥‘2) → 𝐵 ∈ (ℂ ∖ {0, 1}))
Theorem	divge1b 49320	The ratio of a real number to a positive real number is greater than or equal to 1 iff the divisor (the positive real number) is less than or equal to the dividend (the real number). (Contributed by AV, 26-May-2020.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ 1 ≤ (𝐵 / 𝐴)))
Theorem	divgt1b 49321	The ratio of a real number to a positive real number is greater than 1 iff the divisor (the positive real number) is less than the dividend (the real number). (Contributed by AV, 30-May-2020.)
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 1 < (𝐵 / 𝐴)))
Theorem	ltsubaddb 49322	Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶)))
Theorem	ltsubsubb 49323	Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 − 𝐵) < (𝐶 − 𝐷)))
Theorem	ltsubadd2b 49324	Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐷 − 𝐶) < (𝐵 − 𝐴) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶)))
Theorem	divsub1dir 49325	Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) − 1) = ((𝐴 − 𝐵) / 𝐵))
Theorem	expnegico01 49326	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 49327	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 49328	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 49329	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 49330	An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 − 𝑁)) = ((⌊‘𝐴) − 𝑁))
21.49.22.2  Even and odd integers
Theorem	nn0onn0ex 49331*	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 49332*	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	nnennex 49333*	For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑁 / 2) ∈ ℕ) → ∃𝑚 ∈ ℕ 𝑁 = (2 · 𝑚))
Theorem	nneop 49334	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ))
Theorem	nneom 49335	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	nn0eo 49336	A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.)
⊢ (𝑁 ∈ ℕ0 → ((𝑁 / 2) ∈ ℕ0 ∨ ((𝑁 + 1) / 2) ∈ ℕ0))
Theorem	nnpw2even 49337	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ((2↑𝑁) / 2) ∈ ℕ)
Theorem	zefldiv2 49338	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 49339	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 49340	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 49341	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 49342	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)))
21.49.22.3  The natural logarithm on complex numbers (extension)
Theorem	logcxp0 49343	Logarithm of a complex power. Generalization of logcxp 26845. (Contributed by AV, 22-May-2020.)
⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℂ ∧ (𝐵 · (log‘𝐴)) ∈ ran log) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴)))
Theorem	regt1loggt0 49344	The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.)
⊢ (𝐵 ∈ (1(,)+∞) → 0 < (log‘𝐵))
21.49.22.4  Division of functions
Syntax	cfdiv 49345	Extend class notation with the division operator of two functions.
class /f
Definition	df-fdiv 49346*	Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
⊢ /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘f / 𝑔) ↾ (𝑔 supp 0)))
Theorem	fdivval 49347	The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 /f 𝐺) = ((𝐹 ∘f / 𝐺) ↾ (𝐺 supp 0)))
Theorem	fdivmpt 49348*	The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) = (𝑥 ∈ (𝐺 supp 0) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥))))
Theorem	fdivmptf 49349	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 49350	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 49351	The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℂ ↑pm 𝐴))
Theorem	refdivpm 49352	The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.)
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℝ ↑pm 𝐴))
Theorem	fdivmptfv 49353	The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.)
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋)))
Theorem	refdivmptfv 49354	The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.)
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋)))
21.49.22.5  Upper bounds
Syntax	cbigo 49355	Extend class notation with the class of the "big-O" function.
class Ο
Definition	df-bigo 49356*	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 generalization of "big-O of one", see df-o1 15548 and df-lo1 15549. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 49365. (Contributed by AV, 15-May-2020.)
⊢ Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))})
Theorem	bigoval 49357*	Set of functions of order G(x). (Contributed by AV, 15-May-2020.)
⊢ (𝐺 ∈ (ℝ ↑pm ℝ) → (Ο‘𝐺) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))})
Theorem	elbigofrcl 49358	Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐺 ∈ (ℝ ↑pm ℝ))
Theorem	elbigo 49359*	Properties of a function of order G(x). (Contributed by AV, 16-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
Theorem	elbigo2 49360*	Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.)
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))))
Theorem	elbigo2r 49361*	Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.)
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ (𝑀 · (𝐺‘𝑥))))) → 𝐹 ∈ (Ο‘𝐺))
Theorem	elbigof 49362	A function of order G(x) is a function. (Contributed by AV, 18-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐹:dom 𝐹⟶ℝ)
Theorem	elbigodm 49363	The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.)
⊢ (𝐹 ∈ (Ο‘𝐺) → dom 𝐹 ⊆ ℝ)
Theorem	elbigoimp 49364*	The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.)
⊢ ((𝐹 ∈ (Ο‘𝐺) ∧ 𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ dom 𝐺) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))
Theorem	elbigolo1 49365	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.) (Proof shortened by II, 16-Feb-2023.)
⊢ ((𝐴 ⊆ ℝ ∧ 𝐺:𝐴⟶ℝ+ ∧ 𝐹:𝐴⟶ℝ+) → (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 /f 𝐺) ∈ ≤𝑂(1)))
21.49.22.6  Logarithm to an arbitrary base (extension)
Theorem	rege1logbrege0 49366	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 49367	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 49368	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 49369	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 49370	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 49371	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 49372	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 ↔ 𝑋 < 𝐵))
21.49.22.7  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 49373	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 49374	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 49375	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 49376	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 𝑁)) = 𝐼)
21.49.22.8  Binary length
Syntax	cblen 49377	Extend class notation with the class of the binary length function.
class #b
Definition	df-blen 49378	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 49379	The binary length of an integer. (Contributed by AV, 20-May-2020.)
⊢ (𝑁 ∈ 𝑉 → (#b‘𝑁) = if(𝑁 = 0, 1, ((⌊‘(2 logb (abs‘𝑁))) + 1)))
Theorem	blen0 49380	The binary length of 0. (Contributed by AV, 20-May-2020.)
⊢ (#b‘0) = 1
Theorem	blenn0 49381	The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.)
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 0) → (#b‘𝑁) = ((⌊‘(2 logb (abs‘𝑁))) + 1))
Theorem	blenre 49382	The binary length of a positive real number. (Contributed by AV, 20-May-2020.)
⊢ (𝑁 ∈ ℝ+ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1))
Theorem	blennn 49383	The binary length of a positive integer. (Contributed by AV, 21-May-2020.)
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1))
Theorem	blennnelnn 49384	The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.)
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) ∈ ℕ)
Theorem	blennn0elnn 49385	The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (#b‘𝑁) ∈ ℕ)
Theorem	blenpw2 49386	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 49387	The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.)
⊢ (𝐼 ∈ ℕ → (#b‘((2↑𝐼) − 1)) = 𝐼)
Theorem	nnpw2blen 49388	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 49389	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 49390	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 49391	Every positive integer can be represented as the sum of a power of 2 and a "remainder" less than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ → 𝑁 = ((2↑((#b‘𝑁) − 1)) + (𝑁 mod (2↑((#b‘𝑁) − 1)))))
Theorem	blen1 49392	The binary length of 1. (Contributed by AV, 21-May-2020.)
⊢ (#b‘1) = 1
Theorem	blen2 49393	The binary length of 2. (Contributed by AV, 21-May-2020.)
⊢ (#b‘2) = 2
Theorem	nnpw2p 49394*	Every positive integer can be represented as the sum of a power of 2 and a "remainder" less than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ → ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟))
Theorem	nnpw2pb 49395*	A number is a positive integer iff it can be represented as the sum of a power of 2 and a "remainder" less than the power. (Contributed by AV, 31-May-2020.)
⊢ (𝑁 ∈ ℕ ↔ ∃𝑖 ∈ ℕ0 ∃𝑟 ∈ (0..^(2↑𝑖))𝑁 = ((2↑𝑖) + 𝑟))
Theorem	blen1b 49396	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 49397	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 49398	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 49399	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 49400	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))