| Metamath
Proof Explorer Theorem List (p. 424 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nnn1suc 42301* | A positive integer that is not 1 is a successor of some other positive integer. (Contributed by Steven Nguyen, 19-Aug-2023.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐴 ≠ 1) → ∃𝑥 ∈ ℕ (𝑥 + 1) = 𝐴) | ||
| Theorem | nnadd1com 42302 | Addition with 1 is commutative for natural numbers. (Contributed by Steven Nguyen, 9-Dec-2022.) |
| ⊢ (𝐴 ∈ ℕ → (𝐴 + 1) = (1 + 𝐴)) | ||
| Theorem | nnaddcom 42303 | Addition is commutative for natural numbers. Uses fewer axioms than addcom 11447. (Contributed by Steven Nguyen, 9-Dec-2022.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) | ||
| Theorem | nnaddcomli 42304 | Version of addcomli 11453 for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ (𝐴 + 𝐵) = 𝐶 ⇒ ⊢ (𝐵 + 𝐴) = 𝐶 | ||
| Theorem | nnadddir 42305 | Right-distributivity for natural numbers without ax-mulcom 11219. (Contributed by SN, 5-Feb-2024.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → ((𝐴 + 𝐵) · 𝐶) = ((𝐴 · 𝐶) + (𝐵 · 𝐶))) | ||
| Theorem | nnmul1com 42306 | Multiplication with 1 is commutative for natural numbers, without ax-mulcom 11219. Since (𝐴 · 1) is 𝐴 by ax-1rid 11225, this is equivalent to remullid 42463 for natural numbers, but using fewer axioms (avoiding ax-resscn 11212, ax-addass 11220, ax-mulass 11221, ax-rnegex 11226, ax-pre-lttri 11229, ax-pre-lttrn 11230, ax-pre-ltadd 11231). (Contributed by SN, 5-Feb-2024.) |
| ⊢ (𝐴 ∈ ℕ → (1 · 𝐴) = (𝐴 · 1)) | ||
| Theorem | nnmulcom 42307 | Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) = (𝐵 · 𝐴)) | ||
| Theorem | readdrcl2d 42308 | Reverse closure for addition: the second addend is real if the first addend is real and the sum is real. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ) ⇒ ⊢ (𝜑 → 𝐵 ∈ ℝ) | ||
| Theorem | mvrrsubd 42309 |
Move a subtraction in the RHS to a right-addition in the LHS. Converse
of mvlraddd 11673.
EDITORIAL: Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.) |
| ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐶) = 𝐵) | ||
| Theorem | laddrotrd 42310 |
Rotate the variables right in an equation with addition on the left,
converting it into a subtraction. Version of mvlladdd 11674 with a commuted
consequent, and of mvrladdd 11676 with a commuted hypothesis.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: ply1dg3rt0irred 33607. (Contributed by SN, 21-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 + 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐶 − 𝐴) = 𝐵) | ||
| Theorem | raddswap12d 42311 |
Swap the first two variables in an equation with addition on the right,
converting it into a subtraction. Version of mvrraddd 11675 with a commuted
consequent, and of mvlraddd 11673 with a commuted hypothesis.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.) |
| ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 + 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = (𝐴 − 𝐶)) | ||
| Theorem | lsubrotld 42312 |
Rotate the variables left in an equation with subtraction on the left,
converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 21-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐵 + 𝐶) = 𝐴) | ||
| Theorem | rsubrotld 42313 |
Rotate the variables left in an equation with subtraction on the right,
converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 4-Jul-2025.) |
| ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐶 ∈ ℂ) & ⊢ (𝜑 → 𝐴 = (𝐵 − 𝐶)) ⇒ ⊢ (𝜑 → 𝐵 = (𝐶 + 𝐴)) | ||
| Theorem | lsubswap23d 42314 |
Swap the second and third variables in an equation with subtraction on
the left, converting it into an addition.
EDITORIAL: The label for this theorem is questionable. Do not move until it would have 7 uses: current additional uses: (none). (Contributed by SN, 23-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → (𝐴 − 𝐵) = 𝐶) ⇒ ⊢ (𝜑 → (𝐴 − 𝐶) = 𝐵) | ||
| Theorem | addsubeq4com 42315 | Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) = (𝐶 + 𝐷) ↔ (𝐴 − 𝐶) = (𝐷 − 𝐵))) | ||
| Theorem | sqsumi 42316 | A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝐵 ∈ ℂ ⇒ ⊢ ((𝐴 + 𝐵) · (𝐴 + 𝐵)) = (((𝐴 · 𝐴) + (𝐵 · 𝐵)) + (2 · (𝐴 · 𝐵))) | ||
| Theorem | negn0nposznnd 42317 | Lemma for dffltz 42644. (Contributed by Steven Nguyen, 27-Feb-2023.) |
| ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → ¬ 0 < 𝐴) & ⊢ (𝜑 → 𝐴 ∈ ℤ) ⇒ ⊢ (𝜑 → -𝐴 ∈ ℕ) | ||
| Theorem | sqmid3api 42318 | Value of the square of the middle term of a 3-term arithmetic progression. (Contributed by Steven Nguyen, 20-Sep-2022.) |
| ⊢ 𝐴 ∈ ℂ & ⊢ 𝑁 ∈ ℂ & ⊢ (𝐴 + 𝑁) = 𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝐵 · 𝐵) = ((𝐴 · 𝐶) + (𝑁 · 𝑁)) | ||
| Theorem | decaddcom 42319 | Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 + 𝐶) = (;𝐴𝐶 + 𝐵) | ||
| Theorem | sqn5i 42320 | The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.) |
| ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (;𝐴5 · ;𝐴5) = ;;(𝐴 · (𝐴 + 1))25 | ||
| Theorem | sqn5ii 42321 | The square of a number ending in 5. This shortcut only works because 5 is half of 10. (Contributed by Steven Nguyen, 16-Sep-2022.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ (𝐴 · 𝐵) = 𝐶 ⇒ ⊢ (;𝐴5 · ;𝐴5) = ;;𝐶25 | ||
| Theorem | decpmulnc 42322 | Partial products algorithm for two digit multiplication, no carry. Compare muladdi 11714. (Contributed by Steven Nguyen, 9-Dec-2022.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = 𝐺 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;;𝐸𝐹𝐺 | ||
| Theorem | decpmul 42323 | Partial products algorithm for two digit multiplication. (Contributed by Steven Nguyen, 10-Dec-2022.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝐶) = 𝐸 & ⊢ ((𝐴 · 𝐷) + (𝐵 · 𝐶)) = 𝐹 & ⊢ (𝐵 · 𝐷) = ;𝐺𝐻 & ⊢ (;𝐸𝐺 + 𝐹) = 𝐼 & ⊢ 𝐺 ∈ ℕ0 & ⊢ 𝐻 ∈ ℕ0 ⇒ ⊢ (;𝐴𝐵 · ;𝐶𝐷) = ;𝐼𝐻 | ||
| Theorem | sqdeccom12 42324 | The square of a number in terms of its digits switched. (Contributed by Steven Nguyen, 3-Jan-2023.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((;𝐴𝐵 · ;𝐴𝐵) − (;𝐵𝐴 · ;𝐵𝐴)) = (;99 · ((𝐴 · 𝐴) − (𝐵 · 𝐵))) | ||
| Theorem | sq3deccom12 42325 | Variant of sqdeccom12 42324 with a three digit square. (Contributed by Steven Nguyen, 3-Jan-2023.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐴 + 𝐶) = 𝐷 ⇒ ⊢ ((;;𝐴𝐵𝐶 · ;;𝐴𝐵𝐶) − (;𝐷𝐵 · ;𝐷𝐵)) = (;99 · ((;𝐴𝐵 · ;𝐴𝐵) − (𝐶 · 𝐶))) | ||
| Theorem | 4t5e20 42326 | 4 times 5 equals 20. (Contributed by SN, 30-Mar-2025.) |
| ⊢ (4 · 5) = ;20 | ||
| Theorem | sq4 42327 | The square of 4 is 16. (Contributed by SN, 26-Aug-2025.) |
| ⊢ (4↑2) = ;16 | ||
| Theorem | sq5 42328 | The square of 5 is 25. (Contributed by SN, 26-Aug-2025.) |
| ⊢ (5↑2) = ;25 | ||
| Theorem | sq6 42329 | The square of 6 is 36. (Contributed by SN, 26-Aug-2025.) |
| ⊢ (6↑2) = ;36 | ||
| Theorem | sq7 42330 | The square of 7 is 49. (Contributed by SN, 26-Aug-2025.) |
| ⊢ (7↑2) = ;49 | ||
| Theorem | sq8 42331 | The square of 8 is 64. (Contributed by SN, 26-Aug-2025.) |
| ⊢ (8↑2) = ;64 | ||
| Theorem | sq9 42332 | The square of 9 is 81. (Contributed by SN, 30-Mar-2025.) |
| ⊢ (9↑2) = ;81 | ||
| Theorem | rpsscn 42333 | The positive reals are a subset of the complex numbers. (Contributed by SN, 1-Oct-2025.) |
| ⊢ ℝ+ ⊆ ℂ | ||
| Theorem | 4rp 42334 | 4 is a positive real. (Contributed by SN, 26-Aug-2025.) |
| ⊢ 4 ∈ ℝ+ | ||
| Theorem | 6rp 42335 | 6 is a positive real. (Contributed by SN, 26-Aug-2025.) |
| ⊢ 6 ∈ ℝ+ | ||
| Theorem | 7rp 42336 | 7 is a positive real. (Contributed by SN, 26-Aug-2025.) |
| ⊢ 7 ∈ ℝ+ | ||
| Theorem | 8rp 42337 | 8 is a positive real. (Contributed by SN, 26-Aug-2025.) |
| ⊢ 8 ∈ ℝ+ | ||
| Theorem | 9rp 42338 | 9 is a positive real. (Contributed by SN, 26-Aug-2025.) |
| ⊢ 9 ∈ ℝ+ | ||
| Theorem | 235t711 42339 |
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 11270 saving the lower level uses of mulcomli 11270 within 235 · 7 since mulcom2 doesn't exist, but if commuted versions of theorems like 7t2e14 12842 are added then this proof would benefit more than ex-decpmul 42340. For practicality, this proof doesn't have "e167085" at the end of its name like 2p2e4 12401 or 8t7e56 12853. (Contributed by Steven Nguyen, 10-Dec-2022.) (New usage is discouraged.) |
| ⊢ (;;235 · ;;711) = ;;;;;167085 | ||
| Theorem | ex-decpmul 42340 | Example usage of decpmul 42323. This proof is significantly longer than 235t711 42339. There is more unnecessary carrying compared to 235t711 42339. Although saving 5 visual steps, using mulcomli 11270 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 42341 | Membership in a successor upper set of integers. (Contributed by SN, 5-Jul-2025.) |
| ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘(𝑀 + 1)) ↔ (𝑁 ∈ ℤ ∧ 𝑀 < 𝑁))) | ||
| Theorem | sn-eluzp1l 42342 | Shorter proof of eluzp1l 12905. (Contributed by NM, 12-Sep-2005.) (Revised by SN, 5-Jul-2025.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → 𝑀 < 𝑁) | ||
| Theorem | fz1sumconst 42343* | The sum of 𝑁 constant terms (𝑘 is not free in 𝐶). (Contributed by SN, 21-Mar-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ ℂ) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (1...𝑁)𝐶 = (𝑁 · 𝐶)) | ||
| Theorem | fz1sump1 42344* | Add one more term to a sum. Special case of fsump1 15792 generalized to 𝑁 ∈ ℕ0. (Contributed by SN, 22-Mar-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 + 1))) → 𝐴 ∈ ℂ) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 + 1))𝐴 = (Σ𝑘 ∈ (1...𝑁)𝐴 + 𝐵)) | ||
| Theorem | oddnumth 42345* | The Odd Number Theorem. The sum of the first 𝑁 odd numbers is 𝑁↑2. A corollary of arisum 15896. (Contributed by SN, 21-Mar-2025.) |
| ⊢ (𝑁 ∈ ℕ0 → Σ𝑘 ∈ (1...𝑁)((2 · 𝑘) − 1) = (𝑁↑2)) | ||
| Theorem | nicomachus 42346* | 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 42347* | 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 42348 | π is nonzero. (Contributed by SN, 25-Apr-2025.) |
| ⊢ π ≠ 0 | ||
| Theorem | ine1 42349 | i is not 1. (Contributed by SN, 25-Apr-2025.) |
| ⊢ i ≠ 1 | ||
| Theorem | 0tie0 42350 | 0 times i equals 0. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (0 · i) = 0 | ||
| Theorem | it1ei 42351 | i times 1 equals i. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (i · 1) = i | ||
| Theorem | 1tiei 42352 | 1 times i equals i. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (1 · i) = i | ||
| Theorem | itrere 42353 | i times a real is real iff the real is zero. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0)) | ||
| Theorem | retire 42354 | A real times i is real iff the real is zero. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0)) | ||
| Theorem | iocioodisjd 42355 | 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 42356 | A positive real is its own absolute value. (Contributed by SN, 1-Oct-2025.) |
| ⊢ (𝑅 ∈ ℝ+ → (abs‘𝑅) = 𝑅) | ||
| Theorem | oexpreposd 42357 | Lemma for dffltz 42644. For a more standard version, see expgt0b 32818. TODO-SN?: This can be used to show exp11d 42361 holds for all integers when the exponent is odd. (Contributed by SN, 4-Mar-2023.) |
| ⊢ (𝜑 → 𝑁 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝑀 / 2) ∈ ℕ) ⇒ ⊢ (𝜑 → (0 < 𝑁 ↔ 0 < (𝑁↑𝑀))) | ||
| Theorem | explt1d 42358 | 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 42359 | 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 42360 | 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 42361 | exp11nnd 14300 for nonzero integer exponents. (Contributed by SN, 14-Sep-2023.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ (𝜑 → (𝐴↑𝑁) = (𝐵↑𝑁)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | 0dvds0 42362 | 0 divides 0. (Contributed by SN, 15-Sep-2024.) |
| ⊢ 0 ∥ 0 | ||
| Theorem | absdvdsabsb 42363 | Divisibility is invariant under taking the absolute value on both sides. (Contributed by SN, 15-Sep-2024.) |
| ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ (abs‘𝑁))) | ||
| Theorem | gcdnn0id 42364 | The gcd of a nonnegative integer and itself is the integer. (Contributed by SN, 25-Aug-2024.) |
| ⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 𝑁) = 𝑁) | ||
| Theorem | gcdle1d 42365 | 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 42366 | 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 42367 | Deduction associated with dvdsexpim 16592. (Contributed by SN, 21-Aug-2024.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ∥ 𝐵) ⇒ ⊢ (𝜑 → (𝐴↑𝑁) ∥ (𝐵↑𝑁)) | ||
| Theorem | dvdsexpnn 42368 | dvdssqlem 16603 generalized to positive integer exponents. (Contributed by SN, 20-Aug-2024.) |
| ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
| Theorem | dvdsexpnn0 42369 | dvdsexpnn 42368 generalized to include zero bases. (Contributed by SN, 15-Sep-2024.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
| Theorem | dvdsexpb 42370 | dvdssq 16604 generalized to positive integer exponents. (Contributed by SN, 15-Sep-2024.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐴 ∥ 𝐵 ↔ (𝐴↑𝑁) ∥ (𝐵↑𝑁))) | ||
| Theorem | posqsqznn 42371 | When a positive rational squared is an integer, the rational is a positive integer. zsqrtelqelz 16795 with all terms squared and positive. (Contributed by SN, 23-Aug-2024.) |
| ⊢ (𝜑 → (𝐴↑2) ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ) | ||
| Theorem | zdivgd 42372* | Two ways to express "𝑁 is an integer multiple of 𝑀". Originally a subproof of zdiv 12688. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝑀 ∈ ℂ) & ⊢ (𝜑 → 𝑁 ∈ ℂ) & ⊢ (𝜑 → 𝑀 ≠ 0) ⇒ ⊢ (𝜑 → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ)) | ||
| Theorem | efne0d 42373 | The exponential of a complex number is nonzero, deduction form. EDITORIAL: Using efne0d 42373 in efne0 16133 is shorter than vice versa. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘𝐴) ≠ 0) | ||
| Theorem | efsubd 42374 | Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → (exp‘(𝐴 − 𝐵)) = ((exp‘𝐴) / (exp‘𝐵))) | ||
| Theorem | ef11d 42375* | General condition for the exponential function to be one-to-one. efper 26521 shows that exponentiation is periodic. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) ⇒ ⊢ (𝜑 → ((exp‘𝐴) = (exp‘𝐵) ↔ ∃𝑛 ∈ ℤ 𝐴 = (𝐵 + ((i · (2 · π)) · 𝑛)))) | ||
| Theorem | logccne0d 42376 | 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 42377* | 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 42378* | 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 42379* | 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 42380 | Deduction form of logne0 26621. See logccne0d 42376 for a more general version. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐴 ≠ 1) ⇒ ⊢ (𝜑 → (log‘𝐴) ≠ 0) | ||
| Theorem | rxp112d 42381 | 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 42382 | The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐵 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 0) & ⊢ (𝜑 → 𝐵 ≠ 0) ⇒ ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | rplog11d 42383 | The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) ⇒ ⊢ (𝜑 → ((log‘𝐴) = (log‘𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | rxp11d 42384 | Real exponentiation is one-to-one with respect to the first argument. (Contributed by SN, 25-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → (𝐴↑𝑐𝐶) = (𝐵↑𝑐𝐶)) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | tanhalfpim 42385 | 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 42386 | The tangent of π / 3 is √3. (Contributed by SN, 2-Sep-2025.) |
| ⊢ (tan‘(π / 3)) = (√‘3) | ||
| Theorem | asin1half 42387 | The arcsine of 1 / 2 is π / 6. (Contributed by SN, 31-Aug-2025.) |
| ⊢ (arcsin‘(1 / 2)) = (π / 6) | ||
| Theorem | acos1half 42388 | The arccosine of 1 / 2 is π / 3. (Contributed by SN, 31-Aug-2024.) |
| ⊢ (arccos‘(1 / 2)) = (π / 3) | ||
| Theorem | dvun 42389 | 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 23090. (Contributed by SN, 30-Sep-2025.) |
| ⊢ 𝐽 = (𝐾 ↾t 𝑆) & ⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐹:𝐴⟶ℂ) & ⊢ (𝜑 → 𝐺:𝐵⟶ℂ) & ⊢ (𝜑 → 𝐴 ⊆ 𝑆) & ⊢ (𝜑 → 𝐵 ⊆ 𝑆) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ (𝜑 → (((int‘𝐽)‘𝐴) ∪ ((int‘𝐽)‘𝐵)) = ((int‘𝐽)‘(𝐴 ∪ 𝐵))) ⇒ ⊢ (𝜑 → ((𝑆 D 𝐹) ∪ (𝑆 D 𝐺)) = (𝑆 D (𝐹 ∪ 𝐺))) | ||
| Theorem | redvmptabs 42390* | The derivative of the absolute value, for real numbers. (Contributed by SN, 30-Sep-2025.) |
| ⊢ 𝐷 = (ℝ ∖ {0}) ⇒ ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (abs‘𝑥))) = (𝑥 ∈ 𝐷 ↦ if(𝑥 < 0, -1, 1)) | ||
| Theorem | readvrec2 42391* | 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 42392* | For real numbers, the antiderivative of 1/x is ln|x|. (Contributed by SN, 30-Sep-2025.) |
| ⊢ 𝐷 = (ℝ ∖ {0}) ⇒ ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘𝑥)))) = (𝑥 ∈ 𝐷 ↦ (1 / 𝑥)) | ||
| Theorem | resuppsinopn 42393 | The support of sin (df-supp 8186) restricted to the reals is an open set. (Contributed by SN, 7-Oct-2025.) |
| ⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0} ⇒ ⊢ 𝐷 ∈ (topGen‘ran (,)) | ||
| Theorem | readvcot 42394* | Real antiderivative of cotangent. (Contributed by SN, 7-Oct-2025.) |
| ⊢ 𝐷 = {𝑦 ∈ ℝ ∣ (sin‘𝑦) ≠ 0} ⇒ ⊢ (ℝ D (𝑥 ∈ 𝐷 ↦ (log‘(abs‘(sin‘𝑥))))) = (𝑥 ∈ 𝐷 ↦ ((cos‘𝑥) / (sin‘𝑥))) | ||
| Syntax | cresub 42395 | Real number subtraction. |
| class −ℝ | ||
| Definition | df-resub 42396* | Define subtraction between real numbers. This operator saves a few axioms over df-sub 11494 in certain situations. Theorem resubval 42397 shows its value, resubadd 42409 relates it to addition, and rersubcl 42408 proves its closure. It is the restriction of df-sub 11494 to the reals: subresre 42460. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ −ℝ = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (℩𝑧 ∈ ℝ (𝑦 + 𝑧) = 𝑥)) | ||
| Theorem | resubval 42397* | Value of real subtraction, which is the (unique) real 𝑥 such that 𝐵 + 𝑥 = 𝐴. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 −ℝ 𝐵) = (℩𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴)) | ||
| Theorem | renegeulemv 42398* | Lemma for renegeu 42400 and similar. Derive existential uniqueness from existence. (Contributed by Steven Nguyen, 28-Jan-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ ℝ (𝐵 + 𝑥) = 𝐴) | ||
| Theorem | renegeulem 42399* | Lemma for renegeu 42400 and similar. Remove a change in bound variables from renegeulemv 42398. (Contributed by Steven Nguyen, 28-Jan-2023.) |
| ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → ∃𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑦 ∈ ℝ (𝐵 + 𝑦) = 𝐴) | ||
| Theorem | renegeu 42400* | Existential uniqueness of real negatives. (Contributed by Steven Nguyen, 7-Jan-2023.) |
| ⊢ (𝐴 ∈ ℝ → ∃!𝑥 ∈ ℝ (𝐴 + 𝑥) = 0) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |