![]() |
Metamath
Proof Explorer Theorem List (p. 424 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 | decpmul 42301 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = ;𝐺𝐻 & ⊢ (;𝐸𝐺 + 𝐹) = 𝐼 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻 | ||
Theorem | sqdeccom12 42302 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) | ||
Theorem | sq3deccom12 42303 | Variant of sqdeccom12 42302 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐴 + 𝐶) = 𝐷 ⇒ ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶))) | ||
Theorem | 4t5e20 42304 | 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.) |
⊢ (4 · 5) = ;20 | ||
Theorem | sq4 42305 | The square of 4 is 16. (Contributed by SN, 26-Aug-2025.) |
⊢ (4↑2) = ;16 | ||
Theorem | sq5 42306 | The square of 5 is 25. (Contributed by SN, 26-Aug-2025.) |
⊢ (5↑2) = ;25 | ||
Theorem | sq6 42307 | The square of 6 is 36. (Contributed by SN, 26-Aug-2025.) |
⊢ (6↑2) = ;36 | ||
Theorem | sq7 42308 | The square of 7 is 49. (Contributed by SN, 26-Aug-2025.) |
⊢ (7↑2) = ;49 | ||
Theorem | sq8 42309 | The square of 8 is 64. (Contributed by SN, 26-Aug-2025.) |
⊢ (8↑2) = ;64 | ||
Theorem | sq9 42310 | The square of 9 is 81. (Contributed by SN, 30-Mar-2025.) |
⊢ (9↑2) = ;81 | ||
Theorem | rpsscn 42311 | The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025.) |
⊢ ℝ+ ⊆ ℂ | ||
Theorem | 4rp 42312 | 4 is a positive real. (Contributed by SN, 26-Aug-2025.) |
⊢ 4 ∈ ℝ+ | ||
Theorem | 6rp 42313 | 6 is a positive real. (Contributed by SN, 26-Aug-2025.) |
⊢ 6 ∈ ℝ+ | ||
Theorem | 7rp 42314 | 7 is a positive real. (Contributed by SN, 26-Aug-2025.) |
⊢ 7 ∈ ℝ+ | ||
Theorem | 8rp 42315 | 8 is a positive real. (Contributed by SN, 26-Aug-2025.) |
⊢ 8 ∈ ℝ+ | ||
Theorem | 9rp 42316 | 9 is a positive real. (Contributed by SN, 26-Aug-2025.) |
⊢ 9 ∈ ℝ+ | ||
Theorem | 235t711 42317 |
Calculate a product by long multiplication as a base comparison with other
multiplication algorithms.
Conveniently, 711 has two ones which greatly simplifies calculations like 235 · 1. There isn't a higher level mulcomli 11267 saving the lower level uses of mulcomli 11267 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12839 are added then this proof would benefit more than ex-decpmul 42318. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12398 or 8t7e56 12850. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 | ||
Theorem | ex-decpmul 42318 | Example usage of decpmul 42301. This proof is significantly longer than 235t711 42317. There is more unnecessary carrying compared to 235t711 42317. Although saving 5 visual steps, using mulcomli 11267 early on increases the compressed proof length. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (;;235 · ;;711) = ;;;;;167085 | ||
Theorem | eluzp1 42319 | Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025.) |
⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ↔ (𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))) | ||
Theorem | sn-eluzp1l 42320 | Shorter proof of eluzp1l 12902. (Contributed by NM, 12-Sep-2005.) (Revised by SN, 5-Jul-2025.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) | ||
Theorem | fz1sumconst 42321* | The sum of 𝑁 constant terms (𝑘 is not free in 𝐶). (Contributed by SN, 21-Mar-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (1...𝑁)𝐶 = (𝑁 · 𝐶)) | ||
Theorem | fz1sump1 42322* | Add one more term to a sum. Special case of fsump1 15788 generalized to 𝑁 ∈ ℕ0. (Contributed by SN, 22-Mar-2025.) |
⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (1...𝑁)𝐴 + 𝐵)) | ||
Theorem | oddnumth 42323* | The Odd Number Theorem. The sum of the first 𝑁 odd numbers is 𝑁↑2. A corollary of arisum 15892. (Contributed by SN, 21-Mar-2025.) |
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)((2 · 𝑘) − 1) = (𝑁↑2)) | ||
Theorem | nicomachus 42324* | Nicomachus's Theorem. The sum of the odd numbers from 𝑁↑2 − 𝑁 + 1 to 𝑁↑2 + 𝑁 − 1 is 𝑁↑3. Proof 2 from https://proofwiki.org/wiki/Nicomachus%27s_Theorem. (Contributed by SN, 21-Mar-2025.) |
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(((𝑁↑2) − 𝑁) + ((2 · 𝑘) − 1)) = (𝑁↑3)) | ||
Theorem | sumcubes 42325* | The sum of the first 𝑁 perfect cubes is the sum of the first 𝑁 nonnegative integers, squared. This is the Proof by Nicomachus from https://proofwiki.org/wiki/Sum_of_Sequence_of_Cubes using induction and index shifting to collect all the odd numbers. (Contributed by SN, 22-Mar-2025.) |
⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)(𝑘↑3) = (Σ𝑘 ∈ (1...𝑁)𝑘↑2)) | ||
Theorem | pine0 42326 | π is nonzero. (Contributed by SN, 25-Apr-2025.) |
⊢ π ≠ 0 | ||
Theorem | ine1 42327 | i is not 1. (Contributed by SN, 25-Apr-2025.) |
⊢ i ≠ 1 | ||
Theorem | 0tie0 42328 | 0 times i equals 0. (Contributed by SN, 25-Apr-2025.) |
⊢ (0 · i) = 0 | ||
Theorem | it1ei 42329 | i times 1 equals i. (Contributed by SN, 25-Apr-2025.) |
⊢ (i · 1) = i | ||
Theorem | 1tiei 42330 | 1 times i equals i. (Contributed by SN, 25-Apr-2025.) |
⊢ (1 · i) = i | ||
Theorem | itrere 42331 | i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0)) | ||
Theorem | retire 42332 | A real times i is real iff the real is zero. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0)) | ||
Theorem | iocioodisjd 42333 | Adjacent intervals where the lower interval is right-closed and the upper interval is open are disjoint. (Contributed by SN, 1-Oct-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 𝐵 ∈ ℝ*) & ⊢ (𝜑 → 𝐶 ∈ ℝ*) ⇒ ⊢ (𝜑 → ((𝐴(,]𝐵) ∩ (𝐵(,)𝐶)) = ∅) | ||
Theorem | rpabsid 42334 | A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025.) |
⊢ (𝑅 ∈ ℝ+ → (abs‘𝑅) = 𝑅) | ||
Theorem | oexpreposd 42335 | Lemma for dffltz 42620. TODO-SN?: This can be used to show exp11d 42339 holds for all integers when the exponent is odd. The more standard ¬ 2 ∥ 𝑀 should be used. (Contributed by SN, 4-Mar-2023.) |
⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ) ⇒ ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀))) | ||
Theorem | explt1d 42336 | A nonnegative real number less than one raised to a positive integer is less than one. (Contributed by SN, 3-Jul-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 0 ≤ 𝐴) & ⊢ (𝜑 → 𝐴 < 1) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) < 1) | ||
Theorem | expeq1d 42337 | A nonnegative real number is one if and only if it is one when raised to a positive integer. (Contributed by SN, 3-Jul-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → ((𝐴↑𝑁) = 1 ↔ 𝐴 = 1)) | ||
Theorem | expeqidd 42338 | A nonnegative real number is zero or one if and only if it is itself when raised to an integer greater than one. (Contributed by SN, 3-Jul-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 0 ≤ 𝐴) ⇒ ⊢ (𝜑 → ((𝐴↑𝑁) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1))) | ||
Theorem | exp11d 42339 | exp11nnd 14296 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | 0dvds0 42340 | 0 divides 0. (Contributed by SN, 15-Sep-2024.) |
⊢ 0 ∥ 0 | ||
Theorem | absdvdsabsb 42341 | Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁))) | ||
Theorem | gcdnn0id 42342 | The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁) | ||
Theorem | gcdle1d 42343 | The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ≤ 𝑀) | ||
Theorem | gcdle2d 42344 | The greatest common divisor of a positive integer and another integer is less than or equal to the positive integer. (Contributed by SN, 25-Aug-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ≤ 𝑁) | ||
Theorem | dvdsexpad 42345 | Deduction associated with dvdsexpim 16588. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∥ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁)) | ||
Theorem | dvdsexpnn 42346 | dvdssqlem 16599 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | dvdsexpnn0 42347 | dvdsexpnn 42346 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | dvdsexpb 42348 | dvdssq 16600 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
Theorem | posqsqznn 42349 | When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16791 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.) |
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ) | ||
Theorem | zdivgd 42350* | Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12685. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝑀 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ≠ 0) ⇒ ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ)) | ||
Theorem | efne0d 42351 | The exponential of a complex number is nonzero, deduction form. EDITORIAL: Using efne0d 42351 in efne0 16129 is shorter than vice versa. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ≠ 0) | ||
Theorem | efsubd 42352 | Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) | ||
Theorem | ef11d 42353* | General condition for the exponential function to be one-to-one. efper 26535 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛)))) | ||
Theorem | logccne0d 42354 | The logarithm isn't 0 if its argument isn't 0 or 1, deduction form. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐴 ≠ 1) ⇒ ⊢ (𝜑 → (log‘𝐴) ≠ 0) | ||
Theorem | cxp112d 42355* | General condition for complex exponentiation to be one-to-one with respect to the second argument. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 1) ⇒ ⊢ (𝜑 → ((𝐶↑𝑐𝐴) = (𝐶↑𝑐𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + (((i · (2 · π)) · 𝑛) / (log‘𝐶))))) | ||
Theorem | cxp111d 42356* | General condition for complex exponentiation to be one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝐶 ≠ 0) ⇒ ⊢ (𝜑 → ((𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶) ↔ ∃𝑛 ∈ ℤ (log‘𝐴) = ((log‘𝐵) + (((i · (2 · π)) · 𝑛) / 𝐶)))) | ||
Theorem | cxpi11d 42357* | i to the powers of 𝐴 and 𝐵 are equal iff 𝐴 and 𝐵 are a multiple of 4 apart. EDITORIAL: This theorem may be revised to a more convenient form. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((i↑𝑐𝐴) = (i↑𝑐𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + (4 · 𝑛)))) | ||
Theorem | logne0d 42358 | Deduction form of logne0 26635. See logccne0d 42354 for a more general version. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≠ 1) ⇒ ⊢ (𝜑 → (log‘𝐴) ≠ 0) | ||
Theorem | rxp112d 42359 | Real exponentiation is one-to-one with respect to the second argument. (TODO: Note that the base 𝐶 must be positive since -𝐶↑𝐴 is 𝐶↑𝐴 · e↑iπ𝐴, so in the negative case 𝐴 = 𝐵 + 2𝑘). (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 1) & ⊢ (𝜑 → (𝐶↑𝑐𝐴) = (𝐶↑𝑐𝐵)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | log11d 42360 | The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | rplog11d 42361 | The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | rxp11d 42362 | Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
Theorem | tanhalfpim 42363 | The tangent of π / 2 minus a number is the cotangent, here represented by cos𝐴 / sin𝐴. (Contributed by SN, 2-Sep-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → (sin‘𝐴) ≠ 0) ⇒ ⊢ (𝜑 → (tan‘((π / 2) − 𝐴)) = ((cos‘𝐴) / (sin‘𝐴))) | ||
Theorem | tan3rdpi 42364 | The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.) |
⊢ (tan‘(π / 3)) = (√‘3) | ||
Theorem | asin1half 42365 | The arcsine of 1 / 2 is π / 6. (Contributed by SN, 31-Aug-2025.) |
⊢ (arcsin‘(1 / 2)) = (π / 6) | ||
Theorem | acos1half 42366 | The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.) |
⊢ (arccos‘(1 / 2)) = (π / 3) | ||
Theorem | dvun 42367 | Condition for the union of the derivatives of two disjoint functions to be equal to the derivative of the union of the two functions. If 𝐴 and 𝐵 are open sets, this condition (dvun.n) is satisfied by isopn3i 23105. (Contributed by SN, 30-Sep-2025.) |
⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐺:𝐵⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐵 ⊆ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → (((int‘𝐽)‘𝐴) ∪ ((int‘𝐽)‘𝐵)) = ((int‘𝐽)‘(𝐴 ∪ 𝐵))) ⇒ ⊢ (𝜑 → ((𝑆 D 𝐹) ∪ (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∪ 𝐺))) | ||
Theorem | redvmptabs 42368* | The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025.) |
⊢ 𝐷 = (ℝ ∖ {0}) ⇒ ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1)) | ||
Theorem | readvrec2 42369* | The antiderivative of 1/x in real numbers, without using the absolute value function. (Contributed by SN, 1-Oct-2025.) |
⊢ 𝐷 = (ℝ ∖ {0}) ⇒ ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ ((log‘(𝑥↑2)) / 2))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) | ||
Theorem | readvrec 42370* | For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025.) |
⊢ 𝐷 = (ℝ ∖ {0}) ⇒ ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) | ||
Syntax | cresub 42371 | Real number subtraction. |
class −ℝ | ||
Definition | df-resub 42372* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 11491 in certain situations. Theorem resubval 42373 shows its value, resubadd 42385 relates it to addition, and rersubcl 42384 proves its closure. It is the restriction of df-sub 11491 to the reals: subresre 42436. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥)) | ||
Theorem | resubval 42373* | Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)) | ||
Theorem | renegeulemv 42374* | Lemma for renegeu 42376 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴) | ||
Theorem | renegeulem 42375* | Lemma for renegeu 42376 and similar. Remove a change in bound variables from renegeulemv 42374. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) | ||
Theorem | renegeu 42376* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
Theorem | rernegcl 42377 | Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (0 −ℝ 𝐴) ∈ ℝ) | ||
Theorem | renegadd 42378 | Relationship between real negation and addition. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 −ℝ 𝐴) = 𝐵 ↔ (𝐴 + 𝐵) = 0)) | ||
Theorem | renegid 42379 | Addition of a real number and its negative. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (𝐴 + (0 −ℝ 𝐴)) = 0) | ||
Theorem | reneg0addlid 42380 | Negative zero is a left additive identity. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → ((0 −ℝ 0) + 𝐴) = 𝐴) | ||
Theorem | resubeulem1 42381 | Lemma for resubeu 42383. A value which when added to zero, results in negative zero. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ (𝐴 ∈ ℝ → (0 + (0 −ℝ (0 + 0))) = (0 −ℝ 0)) | ||
Theorem | resubeulem2 42382 | Lemma for resubeu 42383. A value which when added to 𝐴, results in 𝐵. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + ((0 −ℝ 𝐴) + ((0 −ℝ (0 + 0)) + 𝐵))) = 𝐵) | ||
Theorem | resubeu 42383* | Existential uniqueness of real differences. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 𝐵) | ||
Theorem | rersubcl 42384 | Closure for real subtraction. Based on subcl 11504. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) ∈ ℝ) | ||
Theorem | resubadd 42385 | Relation between real subtraction and addition. Based on subadd 11508. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubaddd 42386 | Relationship between subtraction and addition. Based on subaddd 11635. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) = 𝐶 ↔ (𝐵 + 𝐶) = 𝐴)) | ||
Theorem | resubf 42387 | Real subtraction is an operation on the real numbers. Based on subf 11507. (Contributed by Steven Nguyen, 7-Jan-2023.) |
⊢ −ℝ :(ℝ × ℝ)⟶ℝ | ||
Theorem | repncan2 42388 | Addition and subtraction of equals. Compare pncan2 11512. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐴) = 𝐵) | ||
Theorem | repncan3 42389 | Addition and subtraction of equals. Based on pncan3 11513. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + (𝐵 −ℝ 𝐴)) = 𝐵) | ||
Theorem | readdsub 42390 | Law for addition and subtraction. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ 𝐶) = ((𝐴 −ℝ 𝐶) + 𝐵)) | ||
Theorem | reladdrsub 42391 | Move LHS of a sum into RHS of a (real) difference. Version of mvlladdd 11671 with real subtraction. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 −ℝ 𝐴)) | ||
Theorem | reltsub1 42392 | Subtraction from both sides of 'less than'. Compare ltsub1 11756. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 −ℝ 𝐶) < (𝐵 −ℝ 𝐶))) | ||
Theorem | reltsubadd2 42393 | 'Less than' relationship between addition and subtraction. Compare ltsubadd2 11731. (Contributed by SN, 13-Feb-2024.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) < 𝐶 ↔ 𝐴 < (𝐵 + 𝐶))) | ||
Theorem | resubcan2 42394 | Cancellation law for real subtraction. Compare subcan2 11531. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) = (𝐵 −ℝ 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | resubsub4 42395 | Law for double subtraction. Compare subsub4 11539. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) −ℝ 𝐶) = (𝐴 −ℝ (𝐵 + 𝐶))) | ||
Theorem | rennncan2 42396 | Cancellation law for real subtraction. Compare nnncan2 11543. (Contributed by Steven Nguyen, 14-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐶) −ℝ (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐵)) | ||
Theorem | renpncan3 42397 | Cancellation law for real subtraction. Compare npncan3 11544. (Contributed by Steven Nguyen, 28-Jan-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 −ℝ 𝐵) + (𝐶 −ℝ 𝐴)) = (𝐶 −ℝ 𝐵)) | ||
Theorem | repnpcan 42398 | Cancellation law for addition and real subtraction. Compare pnpcan 11545. (Contributed by Steven Nguyen, 19-May-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐵) −ℝ (𝐴 + 𝐶)) = (𝐵 −ℝ 𝐶)) | ||
Theorem | reppncan 42399 | Cancellation law for mixed addition and real subtraction. Compare ppncan 11548. (Contributed by SN, 3-Sep-2023.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 + 𝐶) + (𝐵 −ℝ 𝐶)) = (𝐴 + 𝐵)) | ||
Theorem | resubidaddlidlem 42400 | Lemma for resubidaddlid 42401. A special case of npncan 11527. (Contributed by Steven Nguyen, 8-Jan-2023.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → (𝐴 −ℝ 𝐵) = (𝐵 −ℝ 𝐶)) ⇒ ⊢ (𝜑 → ((𝐴 −ℝ 𝐵) + (𝐵 −ℝ 𝐶)) = (𝐴 −ℝ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |