Home | Metamath
Proof Explorer Theorem List (p. 447 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | zlmodzxznm 44601 | 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 44602 | 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 44603 | 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 44604 | Lemma 1 for zlmodzxzldep 44608. (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 44605 | Lemma 2 for zlmodzxzldep 44608. (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 44606 | Lemma 3 for zlmodzxzldep 44608. (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 44607* | Lemma 4 for zlmodzxzldep 44608. (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 44608 | { 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 44609 | Lemma 1 for ldepsnlinc 44612. (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 44610 | Lemma 2 for ldepsnlinc 44612. (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 | lvecpsslmod 44611 | 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 19878) 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 44598. (Contributed by AV, 29-Apr-2019.) |
⊢ LVec ⊊ LMod | ||
Theorem | ldepsnlinc 44612* | The reverse implication of islindeps2 44587 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 combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 44600 and zlmodzxznm 44601. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.) |
⊢ ∃𝑚 ∈ LMod ∃𝑠 ∈ 𝒫 (Base‘𝑚)(𝑠 linDepS 𝑚 ∧ ∀𝑣 ∈ 𝑠 ∀𝑓 ∈ ((Base‘(Scalar‘𝑚)) ↑m (𝑠 ∖ {𝑣}))(𝑓 finSupp (0g‘(Scalar‘𝑚)) → (𝑓( linC ‘𝑚)(𝑠 ∖ {𝑣})) ≠ 𝑣)) | ||
Theorem | ldepslinc 44613* | For (left) vector spaces, isldepslvec2 44589 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 44612 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 ‘𝑚)(𝑠 ∖ {𝑣})) = 𝑣))) | ||
Theorem | suppdm 44614 | 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 44615 | 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 44616 | 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 44617 | 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 44618 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | ltsubsubb 44619 | Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 − 𝐶) < (𝐵 − 𝐷) ↔ (𝐴 − 𝐵) < (𝐶 − 𝐷))) | ||
Theorem | ltsubadd2b 44620 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐷 − 𝐶) < (𝐵 − 𝐴) ↔ (𝐴 + 𝐷) < (𝐵 + 𝐶))) | ||
Theorem | divsub1dir 44621 | Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → ((𝐴 / 𝐵) − 1) = ((𝐴 − 𝐵) / 𝐵)) | ||
Theorem | expnegico01 44622 | 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 44623 | 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 44624 | 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 44625 | 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 44626 | An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ) → (⌊‘(𝐴 − 𝑁)) = ((⌊‘𝐴) − 𝑁)) | ||
Theorem | fldivmod 44627 | Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵)) | ||
Theorem | mod0mul 44628* | 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 44629* | 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 44630 | 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 44631 | 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)) | ||
Theorem | nn0onn0ex 44632* | 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 44633* | 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 44634* | 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 44635 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ)) | ||
Theorem | nneom 44636 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 − 1) / 2) ∈ ℕ0)) | ||
Theorem | nn0eo 44637 | A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → ((𝑁 / 2) ∈ ℕ0 ∨ ((𝑁 + 1) / 2) ∈ ℕ0)) | ||
Theorem | nnpw2even 44638 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → ((2↑𝑁) / 2) ∈ ℕ) | ||
Theorem | zefldiv2 44639 | 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 44640 | 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 44641 | 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 44642 | 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 44643 | 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))) | ||
Theorem | logcxp0 44644 | Logarithm of a complex power. Generalization of logcxp 25252. (Contributed by AV, 22-May-2020.) |
⊢ ((𝐴 ∈ (ℂ ∖ {0}) ∧ 𝐵 ∈ ℂ ∧ (𝐵 · (log‘𝐴)) ∈ ran log) → (log‘(𝐴↑𝑐𝐵)) = (𝐵 · (log‘𝐴))) | ||
Theorem | regt1loggt0 44645 | The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.) |
⊢ (𝐵 ∈ (1(,)+∞) → 0 < (log‘𝐵)) | ||
Syntax | cfdiv 44646 | Extend class notation with the division operator of two functions. |
class /f | ||
Definition | df-fdiv 44647* | Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
⊢ /f = (𝑓 ∈ V, 𝑔 ∈ V ↦ ((𝑓 ∘f / 𝑔) ↾ (𝑔 supp 0))) | ||
Theorem | fdivval 44648 | The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐺 ∈ 𝑊) → (𝐹 /f 𝐺) = ((𝐹 ∘f / 𝐺) ↾ (𝐺 supp 0))) | ||
Theorem | fdivmpt 44649* | The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) = (𝑥 ∈ (𝐺 supp 0) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥)))) | ||
Theorem | fdivmptf 44650 | 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 44651 | 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 44652 | The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℂ ↑pm 𝐴)) | ||
Theorem | refdivpm 44653 | The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.) |
⊢ ((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) → (𝐹 /f 𝐺) ∈ (ℝ ↑pm 𝐴)) | ||
Theorem | fdivmptfv 44654 | The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.) |
⊢ (((𝐹:𝐴⟶ℂ ∧ 𝐺:𝐴⟶ℂ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
Theorem | refdivmptfv 44655 | The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.) |
⊢ (((𝐹:𝐴⟶ℝ ∧ 𝐺:𝐴⟶ℝ ∧ 𝐴 ∈ 𝑉) ∧ 𝑋 ∈ (𝐺 supp 0)) → ((𝐹 /f 𝐺)‘𝑋) = ((𝐹‘𝑋) / (𝐺‘𝑋))) | ||
Syntax | cbigo 44656 | Extend class notation with the class of the "big-O" function. |
class Ο | ||
Definition | df-bigo 44657* | 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 14847 and df-lo1 14848. As explained in the comment of df-o1 , any big-O can be represented in terms of 𝑂(1) and division, see elbigolo1 44666. (Contributed by AV, 15-May-2020.) |
⊢ Ο = (𝑔 ∈ (ℝ ↑pm ℝ) ↦ {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝑔‘𝑦))}) | ||
Theorem | bigoval 44658* | Set of functions of order G(x). (Contributed by AV, 15-May-2020.) |
⊢ (𝐺 ∈ (ℝ ↑pm ℝ) → (Ο‘𝐺) = {𝑓 ∈ (ℝ ↑pm ℝ) ∣ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝑓 ∩ (𝑥[,)+∞))(𝑓‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))}) | ||
Theorem | elbigofrcl 44659 | Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐺 ∈ (ℝ ↑pm ℝ)) | ||
Theorem | elbigo 44660* | Properties of a function of order G(x). (Contributed by AV, 16-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) ↔ (𝐹 ∈ (ℝ ↑pm ℝ) ∧ 𝐺 ∈ (ℝ ↑pm ℝ) ∧ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ (dom 𝐹 ∩ (𝑥[,)+∞))(𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) | ||
Theorem | elbigo2 44661* | Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.) |
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴)) → (𝐹 ∈ (Ο‘𝐺) ↔ ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦))))) | ||
Theorem | elbigo2r 44662* | Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.) |
⊢ (((𝐺:𝐴⟶ℝ ∧ 𝐴 ⊆ ℝ) ∧ (𝐹:𝐵⟶ℝ ∧ 𝐵 ⊆ 𝐴) ∧ (𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝐶 ≤ 𝑥 → (𝐹‘𝑥) ≤ (𝑀 · (𝐺‘𝑥))))) → 𝐹 ∈ (Ο‘𝐺)) | ||
Theorem | elbigof 44663 | A function of order G(x) is a function. (Contributed by AV, 18-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) → 𝐹:dom 𝐹⟶ℝ) | ||
Theorem | elbigodm 44664 | The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.) |
⊢ (𝐹 ∈ (Ο‘𝐺) → dom 𝐹 ⊆ ℝ) | ||
Theorem | elbigoimp 44665* | The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.) |
⊢ ((𝐹 ∈ (Ο‘𝐺) ∧ 𝐹:𝐴⟶ℝ ∧ 𝐴 ⊆ dom 𝐺) → ∃𝑥 ∈ ℝ ∃𝑚 ∈ ℝ ∀𝑦 ∈ 𝐴 (𝑥 ≤ 𝑦 → (𝐹‘𝑦) ≤ (𝑚 · (𝐺‘𝑦)))) | ||
Theorem | elbigolo1 44666 | 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))) | ||
Theorem | rege1logbrege0 44667 | 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 44668 | 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 44669 | 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 44670 | 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 44671 | 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 44672 | 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 44673 | 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 ↔ 𝑋 < 𝐵)) | ||
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 44674 | 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 44675 | 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 44676 | 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 44677 | 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 𝑁)) = 𝐼) | ||
Syntax | cblen 44678 | Extend class notation with the class of the binary length function. |
class #b | ||
Definition | df-blen 44679 | 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 44680 | The binary length of an integer. (Contributed by AV, 20-May-2020.) |
⊢ (𝑁 ∈ 𝑉 → (#b‘𝑁) = if(𝑁 = 0, 1, ((⌊‘(2 logb (abs‘𝑁))) + 1))) | ||
Theorem | blen0 44681 | The binary length of 0. (Contributed by AV, 20-May-2020.) |
⊢ (#b‘0) = 1 | ||
Theorem | blenn0 44682 | The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.) |
⊢ ((𝑁 ∈ 𝑉 ∧ 𝑁 ≠ 0) → (#b‘𝑁) = ((⌊‘(2 logb (abs‘𝑁))) + 1)) | ||
Theorem | blenre 44683 | The binary length of a positive real number. (Contributed by AV, 20-May-2020.) |
⊢ (𝑁 ∈ ℝ+ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1)) | ||
Theorem | blennn 44684 | The binary length of a positive integer. (Contributed by AV, 21-May-2020.) |
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) = ((⌊‘(2 logb 𝑁)) + 1)) | ||
Theorem | blennnelnn 44685 | The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.) |
⊢ (𝑁 ∈ ℕ → (#b‘𝑁) ∈ ℕ) | ||
Theorem | blennn0elnn 44686 | The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.) |
⊢ (𝑁 ∈ ℕ0 → (#b‘𝑁) ∈ ℕ) | ||
Theorem | blenpw2 44687 | 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 44688 | The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.) |
⊢ (𝐼 ∈ ℕ → (#b‘((2↑𝐼) − 1)) = 𝐼) | ||
Theorem | nnpw2blen 44689 | 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 44690 | 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 44691 | 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 44692 | 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 44693 | The binary length of 1. (Contributed by AV, 21-May-2020.) |
⊢ (#b‘1) = 1 | ||
Theorem | blen2 44694 | The binary length of 2. (Contributed by AV, 21-May-2020.) |
⊢ (#b‘2) = 2 | ||
Theorem | nnpw2p 44695* | 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 44696* | 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 44697 | 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 44698 | 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 44699 | 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 44700 | 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |