![]() |
Metamath
Proof Explorer Theorem List (p. 473 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfatsnafv2 47201 | Singleton of function value, analogous to fnsnfv 6987. (Contributed by AV, 7-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → {(𝐹''''𝐴)} = (𝐹 “ {𝐴})) | ||
Theorem | dfafv23 47202* | A definition of function value in terms of iota, analogous to dffv3 6902. (Contributed by AV, 6-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (℩𝑥𝑥 ∈ (𝐹 “ {𝐴}))) | ||
Theorem | dfatdmfcoafv2 47203 | Domain of a function composition, analogous to dmfco 7004. (Contributed by AV, 7-Sep-2022.) |
⊢ (𝐺 defAt 𝐴 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺''''𝐴) ∈ dom 𝐹)) | ||
Theorem | dfatcolem 47204* | Lemma for dfatco 47205. (Contributed by AV, 8-Sep-2022.) |
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃!𝑦 𝑋(𝐹 ∘ 𝐺)𝑦) | ||
Theorem | dfatco 47205 | The predicate "defined at" for a function composition. (Contributed by AV, 8-Sep-2022.) |
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝐹 ∘ 𝐺) defAt 𝑋) | ||
Theorem | afv2co2 47206 | Value of a function composition, analogous to fvco2 7005. (Contributed by AV, 8-Sep-2022.) |
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝐹 ∘ 𝐺)''''𝑋) = (𝐹''''(𝐺''''𝑋))) | ||
Theorem | rlimdmafv2 47207 | Two ways to express that a function has a limit, analogous to rlimdm 15583. (Contributed by AV, 5-Sep-2022.) |
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → sup(𝐴, ℝ*, < ) = +∞) ⇒ ⊢ (𝜑 → (𝐹 ∈ dom ⇝𝑟 ↔ 𝐹 ⇝𝑟 ( ⇝𝑟 ''''𝐹))) | ||
Theorem | dfafv22 47208 | Alternate definition of (𝐹''''𝐴) using (𝐹‘𝐴) directly. (Contributed by AV, 3-Sep-2022.) |
⊢ (𝐹''''𝐴) = if(𝐹 defAt 𝐴, (𝐹‘𝐴), 𝒫 ∪ ran 𝐹) | ||
Theorem | afv2ndeffv0 47209 | If the alternate function value at an argument is undefined, i.e., not in the range of the function, the function's value at this argument is the empty set. (Contributed by AV, 3-Sep-2022.) |
⊢ ((𝐹''''𝐴) ∉ ran 𝐹 → (𝐹‘𝐴) = ∅) | ||
Theorem | dfatafv2eqfv 47210 | If a function is defined at a class 𝐴, the alternate function value equals the function's value at 𝐴. (Contributed by AV, 3-Sep-2022.) |
⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afv2rnfveq 47211 | If the alternate function value is defined, i.e., in the range of the function, the alternate function value equals the function's value. (Contributed by AV, 3-Sep-2022.) |
⊢ ((𝐹''''𝐴) ∈ ran 𝐹 → (𝐹''''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afv20fv0 47212 | If the alternate function value at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by AV, 3-Sep-2022.) |
⊢ ((𝐹''''𝐴) = ∅ → (𝐹‘𝐴) = ∅) | ||
Theorem | afv2fvn0fveq 47213 | If the function's value at an argument is not the empty set, it equals the alternate function value at this argument. (Contributed by AV, 3-Sep-2022.) |
⊢ ((𝐹‘𝐴) ≠ ∅ → (𝐹''''𝐴) = (𝐹‘𝐴)) | ||
Theorem | afv2fv0 47214 | If the function's value at an argument is the empty set, then the alternate function value at this argument is the empty set or undefined. (Contributed by AV, 3-Sep-2022.) |
⊢ ((𝐹‘𝐴) = ∅ → ((𝐹''''𝐴) = ∅ ∨ (𝐹''''𝐴) ∉ ran 𝐹)) | ||
Theorem | afv2fv0b 47215 | The function's value at an argument is the empty set if and only if the alternate function value at this argument is the empty set or undefined. (Contributed by AV, 3-Sep-2022.) |
⊢ ((𝐹‘𝐴) = ∅ ↔ ((𝐹''''𝐴) = ∅ ∨ (𝐹''''𝐴) ∉ ran 𝐹)) | ||
Theorem | afv2fv0xorb 47216 | If a set is in the range of a function, the function's value at an argument is the empty set if and only if the alternate function value at this argument is either the empty set or undefined. (Contributed by AV, 11-Sep-2022.) |
⊢ (∅ ∈ ran 𝐹 → ((𝐹‘𝐴) = ∅ ↔ ((𝐹''''𝐴) = ∅ ⊻ (𝐹''''𝐴) ∉ ran 𝐹))) | ||
Theorem | an4com24 47217 | Rearrangement of 4 conjuncts: second and forth positions interchanged. (Contributed by AV, 18-Feb-2022.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜒 ∧ 𝜓))) | ||
Theorem | 3an4ancom24 47218 | Commutative law for a conjunction with a triple conjunction: second and forth positions interchanged. (Contributed by AV, 18-Feb-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ↔ ((𝜑 ∧ 𝜃 ∧ 𝜒) ∧ 𝜓)) | ||
Theorem | 4an21 47219 | Rearrangement of 4 conjuncts with a triple conjunction. (Contributed by AV, 4-Mar-2022.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒 ∧ 𝜃))) | ||
Syntax | cnelbr 47220 | Extend wff notation to include the 'not element of' relation. |
class _∉ | ||
Definition | df-nelbr 47221* | Define negated membership as binary relation. Analogous to df-eprel 5588 (the membership relation). (Contributed by AV, 26-Dec-2021.) |
⊢ _∉ = {〈𝑥, 𝑦〉 ∣ ¬ 𝑥 ∈ 𝑦} | ||
Theorem | dfnelbr2 47222 | Alternate definition of the negated membership as binary relation. (Proposed by BJ, 27-Dec-2021.) (Contributed by AV, 27-Dec-2021.) |
⊢ _∉ = ((V × V) ∖ E ) | ||
Theorem | nelbr 47223 | The binary relation of a set not being a member of another set. (Contributed by AV, 26-Dec-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 _∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵)) | ||
Theorem | nelbrim 47224 | If a set is related to another set by the negated membership relation, then it is not a member of the other set. The other direction of the implication is not generally true, because if 𝐴 is a proper class, then ¬ 𝐴 ∈ 𝐵 would be true, but not 𝐴 _∉ 𝐵. (Contributed by AV, 26-Dec-2021.) |
⊢ (𝐴 _∉ 𝐵 → ¬ 𝐴 ∈ 𝐵) | ||
Theorem | nelbrnel 47225 | A set is related to another set by the negated membership relation iff it is not a member of the other set. (Contributed by AV, 26-Dec-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 _∉ 𝐵 ↔ 𝐴 ∉ 𝐵)) | ||
Theorem | nelbrnelim 47226 | If a set is related to another set by the negated membership relation, then it is not a member of the other set. (Contributed by AV, 26-Dec-2021.) |
⊢ (𝐴 _∉ 𝐵 → 𝐴 ∉ 𝐵) | ||
Theorem | ralralimp 47227* | Selecting one of two alternatives within a restricted generalization if one of the alternatives is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.) |
⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → (∀𝑥 ∈ 𝐴 ((𝜑 → (𝜃 ∨ 𝜏)) ∧ ¬ 𝜃) → 𝜏)) | ||
Theorem | otiunsndisjX 47228* | The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.) |
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉}) | ||
Theorem | fvifeq 47229 | Equality of function values with conditional arguments, see also fvif 6922. (Contributed by Alexander van der Vekens, 21-May-2018.) |
⊢ (𝐴 = if(𝜑, 𝐵, 𝐶) → (𝐹‘𝐴) = if(𝜑, (𝐹‘𝐵), (𝐹‘𝐶))) | ||
Theorem | rnfdmpr 47230 | The range of a one-to-one function 𝐹 of an unordered pair into a set is the unordered pair of the function values. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝐹 Fn {𝑋, 𝑌} → ran 𝐹 = {(𝐹‘𝑋), (𝐹‘𝑌)})) | ||
Theorem | imarnf1pr 47231 | The image of the range of a function 𝐹 under a function 𝐸 if 𝐹 is a function from a pair into the domain of 𝐸. (Contributed by Alexander van der Vekens, 2-Feb-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (((𝐹:{𝑋, 𝑌}⟶dom 𝐸 ∧ 𝐸:dom 𝐸⟶𝑅) ∧ ((𝐸‘(𝐹‘𝑋)) = 𝐴 ∧ (𝐸‘(𝐹‘𝑌)) = 𝐵)) → (𝐸 “ ran 𝐹) = {𝐴, 𝐵})) | ||
Theorem | funop1 47232* | A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) (Avoid depending on this detail.) |
⊢ (∃𝑥∃𝑦 𝐹 = 〈𝑥, 𝑦〉 → (Fun 𝐹 ↔ ∃𝑥∃𝑦 𝐹 = {〈𝑥, 𝑦〉})) | ||
Theorem | fun2dmnopgexmpl 47233 | A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Avoid depending on this detail.) |
⊢ (𝐺 = {〈0, 1〉, 〈1, 1〉} → ¬ 𝐺 ∈ (V × V)) | ||
Theorem | opabresex0d 47234* | A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 1-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V) | ||
Theorem | opabbrfex0d 47235* | A collection of ordered pairs, the class of all possible second components being a set, is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ∈ V) | ||
Theorem | opabresexd 47236* | A collection of ordered pairs, the second component being a function, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V) | ||
Theorem | opabbrfexd 47237* | A collection of ordered pairs, the second component being a function, is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶) & ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} ∈ V) | ||
Theorem | f1oresf1orab 47238* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 1-Aug-2022.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝑥 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | f1oresf1o 47239* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦 ↔ (𝑦 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | f1oresf1o2 47240* | Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.) |
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝑥 ∈ 𝐷 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) | ||
Theorem | fvmptrab 47241* | Value of a function mapping a set to a class abstraction restricting a class depending on the argument of the function. More general version of fvmptrabfv 7047, but relying on the fact that out-of-domain arguments evaluate to the empty set, which relies on set.mm's particular encoding. (Contributed by AV, 14-Feb-2022.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑀 ∣ 𝜑}) & ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑋 → 𝑀 = 𝑁) & ⊢ (𝑋 ∈ 𝑉 → 𝑁 ∈ V) & ⊢ (𝑋 ∉ 𝑉 → 𝑁 = ∅) ⇒ ⊢ (𝐹‘𝑋) = {𝑦 ∈ 𝑁 ∣ 𝜓} | ||
Theorem | fvmptrabdm 47242* | Value of a function mapping a set to a class abstraction restricting the value of another function. See also fvmptrabfv 7047. (Suggested by BJ, 18-Feb-2022.) (Contributed by AV, 18-Feb-2022.) |
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜑}) & ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓)) & ⊢ (𝑌 ∈ dom 𝐺 → 𝑋 ∈ dom 𝐹) ⇒ ⊢ (𝐹‘𝑋) = {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜓} | ||
Theorem | cnambpcma 47243 | ((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) − 𝐴) = (𝐶 − 𝐵)) | ||
Theorem | cnapbmcpd 47244 | ((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) − 𝐶) + 𝐷) = (((𝐴 + 𝐷) + 𝐵) − 𝐶)) | ||
Theorem | addsubeq0 47245 | The sum of two complex numbers is equal to the difference of these two complex numbers iff the subtrahend is 0. (Contributed by AV, 8-May-2023.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 − 𝐵) ↔ 𝐵 = 0)) | ||
Theorem | leaddsuble 47246 | Addition and subtraction on one side of "less than or equal to". (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ ((𝐴 + 𝐵) − 𝐶) ≤ 𝐴)) | ||
Theorem | 2leaddle2 47247 | If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐶) → (𝐴 + 𝐵) < (2 · 𝐶))) | ||
Theorem | ltnltne 47248 | Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴))) | ||
Theorem | p1lep2 47249 | A real number increasd by 1 is less than or equal to the number increased by 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ≤ (𝑁 + 2)) | ||
Theorem | ltsubsubaddltsub 47250 | If the result of subtracting two numbers is greater than a number, the result of adding one of these subtracted numbers to the number is less than the result of subtracting the other subtracted number only. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
⊢ ((𝐽 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → (𝐽 < ((𝐿 − 𝑀) − 𝑁) ↔ (𝐽 + 𝑀) < (𝐿 − 𝑁))) | ||
Theorem | zm1nn 47251 | An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈ ℕ)) | ||
Theorem | readdcnnred 47252 | The sum of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∉ ℝ) | ||
Theorem | resubcnnred 47253 | The difference of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) ⇒ ⊢ (𝜑 → (𝐴 − 𝐵) ∉ ℝ) | ||
Theorem | recnmulnred 47254 | The product of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∉ ℝ) | ||
Theorem | cndivrenred 47255 | The quotient of an imaginary number and a real number is not a real number. (Contributed by AV, 23-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ)) & ⊢ (𝜑 → 𝐴 ≠ 0) ⇒ ⊢ (𝜑 → (𝐵 / 𝐴) ∉ ℝ) | ||
Theorem | sqrtnegnre 47256 | The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023.) |
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → (√‘𝑋) ∉ ℝ) | ||
Theorem | nn0resubcl 47257 | Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 − 𝐵) ∈ ℝ) | ||
Theorem | zgeltp1eq 47258 | If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020.) |
⊢ ((𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 ≤ 𝐼 ∧ 𝐼 < (𝐴 + 1)) → 𝐼 = 𝐴)) | ||
Theorem | 1t10e1p1e11 47259 | 11 is 1 times 10 to the power of 1, plus 1. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
⊢ ;11 = ((1 · (;10↑1)) + 1) | ||
Theorem | deccarry 47260 | Add 1 to a 2 digit number with carry. This is a special case of decsucc 12771, but in closed form. As observed by ML, this theorem allows for carrying the 1 down multiple decimal constructors, so we can carry the 1 multiple times down a multi-digit number, e.g., by applying this theorem three times we get (;;999 + 1) = ;;;1000. (Contributed by AV, 4-Aug-2020.) (Revised by ML, 8-Aug-2020.) (Proof shortened by AV, 10-Sep-2021.) |
⊢ (𝐴 ∈ ℕ → (;𝐴9 + 1) = ;(𝐴 + 1)0) | ||
Theorem | eluzge0nn0 47261 | If an integer is greater than or equal to a nonnegative integer, then it is a nonnegative integer. (Contributed by Alexander van der Vekens, 27-Aug-2018.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (0 ≤ 𝑀 → 𝑁 ∈ ℕ0)) | ||
Theorem | nltle2tri 47262 | Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.) |
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴)) | ||
Theorem | ssfz12 47263 | Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁))) | ||
Theorem | elfz2z 47264 | Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁))) | ||
Theorem | 2elfz3nn0 47265 | If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.) |
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) | ||
Theorem | fz0addcom 47266 | The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.) |
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
Theorem | 2elfz2melfz 47267 | If the sum of two integers of a 0-based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0-based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈ (0...𝐴))) | ||
Theorem | fz0addge0 47268 | The sum of two integers in 0-based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
⊢ ((𝐴 ∈ (0...𝑀) ∧ 𝐵 ∈ (0...𝑁)) → 0 ≤ (𝐴 + 𝐵)) | ||
Theorem | elfzlble 47269 | Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ((𝑁 − 𝑀)...𝑁)) | ||
Theorem | elfzelfzlble 47270 | Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less than the upper bound. (Contributed by AV, 21-Oct-2018.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → 𝐾 ∈ ((𝑁 − 𝑀)...𝑁)) | ||
Theorem | fzopred 47271 | Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 13790. (Contributed by AV, 14-Jul-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁))) | ||
Theorem | fzopredsuc 47272 | Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if 𝑁 = 𝑀 (then (𝑀...𝑁) = {𝑀} = ({𝑀} ∪ ∅) ∪ {𝑀}). (Contributed by AV, 14-Jul-2020.) |
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁})) | ||
Theorem | 1fzopredsuc 47273 | Join 0 and a successor to the beginning and the end of an open integer interval starting at 1. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝑁 ∈ ℕ0 → (0...𝑁) = (({0} ∪ (1..^𝑁)) ∪ {𝑁})) | ||
Theorem | el1fzopredsuc 47274 | An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020.) |
⊢ (𝑁 ∈ ℕ0 → (𝐼 ∈ (0...𝑁) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁))) | ||
Theorem | subsubelfzo0 47275 | Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐼 ∈ (0..^𝑁) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) ∈ (0..^𝐴)) | ||
Theorem | 2ffzoeq 47276* | Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖)))) | ||
Theorem | fldivmod 47277 | Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵)) | ||
Theorem | ceildivmod 47278 | Expressing the ceiling of a division by the modulo operator. (Contributed by AV, 7-Sep-2025.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌈‘(𝐴 / 𝐵)) = ((𝐴 + ((𝐵 − 𝐴) mod 𝐵)) / 𝐵)) | ||
Theorem | ceil5half3 47279 | The ceiling of half of 5 is 3. (Contributed by AV, 7-Sep-2025.) |
⊢ (⌈‘(5 / 2)) = 3 | ||
Theorem | submodaddmod 47280 | Subtraction and addition modulo a positive integer. (Contributed by AV, 7-Sep-2025.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (((𝐴 + 𝐵) mod 𝑁) = ((𝐴 − 𝐶) mod 𝑁) ↔ ((𝐴 + (𝐵 + 𝐶)) mod 𝑁) = (𝐴 mod 𝑁))) | ||
Theorem | difltmodne 47281 | Two nonnegative integers are not equal modulo a positive modulus if their difference is greater than 0 and less then the modulus. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (1 ≤ (𝐴 − 𝐵) ∧ (𝐴 − 𝐵) < 𝑁)) → (𝐴 mod 𝑁) ≠ (𝐵 mod 𝑁)) | ||
Theorem | zplusmodne 47282 | A nonnegative integer is not itself plus a positive integer modulo an integer greater than 1 and the positive integer. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐴 + 𝐾) mod 𝑁) ≠ (𝐴 mod 𝑁)) | ||
Theorem | addmodne 47283 | The sum of a nonnegative integer and a positive integer modulo a number greater than both integers is not equal to the nonnegative integer. (Contributed by AV, 27-Aug-2025.) (Proof shortened by AV, 6-Sep-2025.) |
⊢ ((𝑀 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀) ∧ (𝐵 ∈ ℕ ∧ 𝐵 < 𝑀)) → ((𝐴 + 𝐵) mod 𝑀) ≠ 𝐴) | ||
Theorem | plusmod5ne 47284 | A nonnegative integer is not itself plus a positive integer less than 5 modulo 5. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝐴 ∈ (0..^5) ∧ 𝐾 ∈ (1..^5)) → ((𝐴 + 𝐾) mod 5) ≠ 𝐴) | ||
Theorem | zp1modne 47285 | An integer is not itself plus 1 modulo an integer greater than 1. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ) → ((𝐴 + 1) mod 𝑁) ≠ (𝐴 mod 𝑁)) | ||
Theorem | p1modne 47286 | A nonnegative integer is not itself plus 1 modulo an integer greater than 1 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ (0..^𝑁)) → ((𝐴 + 1) mod 𝑁) ≠ 𝐴) | ||
Theorem | m1modne 47287 | A nonnegative integer is not itself minus 1 modulo an integer greater than 1 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ (0..^𝑁)) → ((𝐴 − 1) mod 𝑁) ≠ 𝐴) | ||
Theorem | minusmod5ne 47288 | A nonnegative integer is not itself minus a positive integer less than 5 modulo 5. (Contributed by AV, 7-Sep-2025.) |
⊢ ((𝐴 ∈ (0..^5) ∧ 𝐾 ∈ (1..^5)) → ((𝐴 − 𝐾) mod 5) ≠ 𝐴) | ||
Theorem | submodlt 47289 | The difference of an element of a half-open range of nonnegative integers and the upper bound of this range modulo an integer greater than the upper bound. (Contributed by AV, 1-Sep-2025.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (0..^𝐵) ∧ 𝐵 < 𝑁) → ((𝐴 − 𝐵) mod 𝑁) = ((𝑁 + 𝐴) − 𝐵)) | ||
Theorem | submodneaddmod 47290 | An integer minus 𝐵 is not itself plus 𝐶 modulo an integer greater than the sum of 𝐵 and 𝐶. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (1 ≤ (𝐵 + 𝐶) ∧ (𝐵 + 𝐶) < 𝑁)) → ((𝐴 + 𝐵) mod 𝑁) ≠ ((𝐴 − 𝐶) mod 𝑁)) | ||
Theorem | m1modnep2mod 47291 | A nonnegative integer minus 1 is not itself plus 2 modulo an integer greater than 3 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.) |
⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝐴 ∈ ℤ) → ((𝐴 − 1) mod 𝑁) ≠ ((𝐴 + 2) mod 𝑁)) | ||
Theorem | minusmodnep2tmod 47292 | A nonnegative integer minus a positive integer 1 or 2 is not itself plus 2 times the positive integer modulo 5. (Contributed by AV, 8-Sep-2025.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (1..^3)) → ((𝐴 − 𝐵) mod 5) ≠ ((𝐴 + (2 · 𝐵)) mod 5)) | ||
Theorem | m1mod0mod1 47293 | An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 < 𝑁) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1)) | ||
Theorem | elmod2 47294 | An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (𝑁 ∈ ℤ → (𝑁 mod 2) ∈ {0, 1}) | ||
Theorem | smonoord 47295* | Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 14069 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 45247? (Contributed by AV, 12-Jul-2020.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁)) | ||
Theorem | fsummsndifre 47296* | A finite sum with one of its integer summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 ∈ ℝ) | ||
Theorem | fsumsplitsndif 47297* | Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐵 = (Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 + ⦋𝑋 / 𝑘⦌𝐵)) | ||
Theorem | fsummmodsndifre 47298* | A finite sum of summands modulo a positive number with one of its summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})(𝐵 mod 𝑁) ∈ ℝ) | ||
Theorem | fsummmodsnunz 47299* | A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.) |
⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑧})(𝐵 mod 𝑁) ∈ ℤ) | ||
Theorem | setsidel 47300 | The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.) |
⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑊) & ⊢ 𝑅 = (𝑆 sSet 〈𝐴, 𝐵〉) ⇒ ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |