![]() |
Metamath
Proof Explorer Theorem List (p. 385 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pellqrexplicit 38401 | Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1) → (𝐴 + ((√‘𝐷) · 𝐵)) ∈ (Pell1QR‘𝐷)) | ||
Theorem | infmrgelbi 38402* | Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013.) (Revised by AV, 17-Sep-2020.) |
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥) → 𝐵 ≤ inf(𝐴, ℝ, < )) | ||
Theorem | pellqrex 38403* | There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ∃𝑥 ∈ (Pell1QR‘𝐷)1 < 𝑥) | ||
Theorem | pellfundval 38404* | Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) = inf({𝑥 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑥}, ℝ, < )) | ||
Theorem | pellfundre 38405 | The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ) | ||
Theorem | pellfundge 38406 | Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (PellFund‘𝐷)) | ||
Theorem | pellfundgt1 38407 | Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷)) | ||
Theorem | pellfundlb 38408 | A nontrivial first quadrant solution is at least as large as the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Proof shortened by AV, 15-Sep-2020.) |
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (PellFund‘𝐷) ≤ 𝐴) | ||
Theorem | pellfundglb 38409* | If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴)) | ||
Theorem | pellfundex 38410 |
The fundamental solution as an infimum is itself a solution, showing
that the solution set is discrete.
Since the fundamental solution is an infimum, there must be an element ge to Fund and lt 2*Fund. If this element is equal to the fundamental solution we're done, otherwise use the infimum again to find another element which must be ge Fund and lt the first element; their ratio is a group element in (1,2), contradicting pell14qrgapw 38400. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) | ||
Theorem | pellfund14gap 38411 | There are no solutions between 1 and the fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ (1 ≤ 𝐴 ∧ 𝐴 < (PellFund‘𝐷))) → 𝐴 = 1) | ||
Theorem | pellfundrp 38412 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+) | ||
Theorem | pellfundne1 38413 | The fundamental Pell solution is never 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ≠ 1) | ||
Section should be obsolete because its contents are covered by section "Logarithms to an arbitrary base" now. | ||
Theorem | reglogcl 38414 | General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 24951 instead. |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) → ((log‘𝐴) / (log‘𝐵)) ∈ ℝ) | ||
Theorem | reglogltb 38415 | General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 24962 instead. |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 < 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) < ((log‘𝐵) / (log‘𝐶)))) | ||
Theorem | reglogleb 38416 | General logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 24961 instead. |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) ≤ ((log‘𝐵) / (log‘𝐶)))) | ||
Theorem | reglogmul 38417 | Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 24955 instead. |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴 · 𝐵)) / (log‘𝐶)) = (((log‘𝐴) / (log‘𝐶)) + ((log‘𝐵) / (log‘𝐶)))) | ||
Theorem | reglogexp 38418 | Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 24954 instead. |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴↑𝑁)) / (log‘𝐶)) = (𝑁 · ((log‘𝐴) / (log‘𝐶)))) | ||
Theorem | reglogbas 38419 | General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 24946 instead. |
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘𝐶) / (log‘𝐶)) = 1) | ||
Theorem | reglog1 38420 | General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 24947 instead. |
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘1) / (log‘𝐶)) = 0) | ||
Theorem | reglogexpbas 38421 | General log of a power of the base is the exponent. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbexp 24958 instead. |
⊢ ((𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐶↑𝑁)) / (log‘𝐶)) = 𝑁) | ||
Theorem | pellfund14 38422* | Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥)) | ||
Theorem | pellfund14b 38423* | The positive Pell solutions are precisely the integer powers of the fundamental solution. To get the general solution set (which we will not be using), throw in a copy of Z/2Z. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥))) | ||
Syntax | crmx 38424 | Extend class notation to include the Robertson-Matiyasevich X sequence. |
class Xrm | ||
Syntax | crmy 38425 | Extend class notation to include the Robertson-Matiyasevich Y sequence. |
class Yrm | ||
Definition | df-rmx 38426* | Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 38437 and rmxyval 38439 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ Xrm = (𝑎 ∈ (ℤ≥‘2), 𝑛 ∈ ℤ ↦ (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)))) | ||
Definition | df-rmy 38427* | Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 38438 and rmxyval 38439 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ Yrm = (𝑎 ∈ (ℤ≥‘2), 𝑛 ∈ ℤ ↦ (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)))) | ||
Theorem | rmxfval 38428* | Value of the X sequence. Not used after rmxyval 38439 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) = (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
Theorem | rmyfval 38429* | Value of the Y sequence. Not used after rmxyval 38439 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) = (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
Theorem | rmspecsqrtnq 38430 | The discriminant used to define the X and Y sequences has an irrational square root. (Contributed by Stefan O'Rear, 21-Sep-2014.) (Proof shortened by AV, 2-Aug-2021.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖ ℚ)) | ||
Theorem | rmspecnonsq 38431 | The discriminant used to define the X and Y sequences is a nonsquare positive integer and thus a valid Pell equation discriminant. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴↑2) − 1) ∈ (ℕ ∖ ◻NN)) | ||
Theorem | qirropth 38432 | This lemma implements the concept of "equate rational and irrational parts", used to prove many arithmetical properties of the X and Y sequences. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ ((𝐴 ∈ (ℂ ∖ ℚ) ∧ (𝐵 ∈ ℚ ∧ 𝐶 ∈ ℚ) ∧ (𝐷 ∈ ℚ ∧ 𝐸 ∈ ℚ)) → ((𝐵 + (𝐴 · 𝐶)) = (𝐷 + (𝐴 · 𝐸)) ↔ (𝐵 = 𝐷 ∧ 𝐶 = 𝐸))) | ||
Theorem | rmspecfund 38433 | The base of exponent used to define the X and Y sequences is the fundamental solution of the corresponding Pell equation. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (PellFund‘((𝐴↑2) − 1)) = (𝐴 + (√‘((𝐴↑2) − 1)))) | ||
Theorem | rmxyelqirr 38434* | The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁) ∈ {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) | ||
Theorem | rmxypairf1o 38435* | The function used to extract rational and irrational parts in df-rmx 38426 and df-rmy 38427 in fact achieves a one-to-one mapping from the quadratic irrationals to pairs of integers. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏)))):(ℕ0 × ℤ)–1-1-onto→{𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) | ||
Theorem | rmxyelxp 38436* | Lemma for frmx 38437 and frmy 38438. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) ∈ (ℕ0 × ℤ)) | ||
Theorem | frmx 38437 | The X sequence is a nonnegative integer. See rmxnn 38477 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0 | ||
Theorem | frmy 38438 | The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ | ||
Theorem | rmxyval 38439 | Main definition of the X and Y sequences. Compare definition 2.3 of [JonesMatijasevic] p. 694. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) | ||
Theorem | rmspecpos 38440 | The discriminant used to define the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴↑2) − 1) ∈ ℝ+) | ||
Theorem | rmxycomplete 38441* | The X and Y sequences taken together enumerate all solutions to the corresponding Pell equation in the right half-plane. This is Metamath 100 proof #39. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → (((𝑋↑2) − (((𝐴↑2) − 1) · (𝑌↑2))) = 1 ↔ ∃𝑛 ∈ ℤ (𝑋 = (𝐴 Xrm 𝑛) ∧ 𝑌 = (𝐴 Yrm 𝑛)))) | ||
Theorem | rmxynorm 38442 | The X and Y sequences define a solution to the corresponding Pell equation. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑁)↑2))) = 1) | ||
Theorem | rmbaserp 38443 | The base of exponentiation for the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 + (√‘((𝐴↑2) − 1))) ∈ ℝ+) | ||
Theorem | rmxyneg 38444 | Negation law for X and Y sequences. JonesMatijasevic is inconsistent on whether the X and Y sequences have domain ℕ0 or ℤ; we use ℤ consistently to avoid the need for a separate subtraction law. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁) ∧ (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁))) | ||
Theorem | rmxyadd 38445 | Addition formula for X and Y sequences. See rmxadd 38451 and rmyadd 38455 for most uses. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm (𝑀 + 𝑁)) = (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∧ (𝐴 Yrm (𝑀 + 𝑁)) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))))) | ||
Theorem | rmxy1 38446 | Value of the X and Y sequences at 1. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴 Xrm 1) = 𝐴 ∧ (𝐴 Yrm 1) = 1)) | ||
Theorem | rmxy0 38447 | Value of the X and Y sequences at 0. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴 Xrm 0) = 1 ∧ (𝐴 Yrm 0) = 0)) | ||
Theorem | rmxneg 38448 | Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 38444, rmxyadd 38445, rmxy0 38447, and rmxy1 38446 via qirropth 38432 results in two theorems at once, but typical use requires only one, so this group of theorems serves to separate the cases. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁)) | ||
Theorem | rmx0 38449 | Value of X sequence at 0. Part 1 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 Xrm 0) = 1) | ||
Theorem | rmx1 38450 | Value of X sequence at 1. Part 2 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 Xrm 1) = 𝐴) | ||
Theorem | rmxadd 38451 | Addition formula for X sequence. Equation 2.7 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (𝑀 + 𝑁)) = (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁))))) | ||
Theorem | rmyneg 38452 | Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)) | ||
Theorem | rmy0 38453 | Value of Y sequence at 0. Part 1 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 Yrm 0) = 0) | ||
Theorem | rmy1 38454 | Value of Y sequence at 1. Part 2 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 Yrm 1) = 1) | ||
Theorem | rmyadd 38455 | Addition formula for Y sequence. Equation 2.8 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (𝑀 + 𝑁)) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁)))) | ||
Theorem | rmxp1 38456 | Special addition-of-1 formula for X sequence. Part 1 of equation 2.9 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (𝑁 + 1)) = (((𝐴 Xrm 𝑁) · 𝐴) + (((𝐴↑2) − 1) · (𝐴 Yrm 𝑁)))) | ||
Theorem | rmyp1 38457 | Special addition of 1 formula for Y sequence. Part 2 of equation 2.9 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (𝑁 + 1)) = (((𝐴 Yrm 𝑁) · 𝐴) + (𝐴 Xrm 𝑁))) | ||
Theorem | rmxm1 38458 | Subtraction of 1 formula for X sequence. Part 1 of equation 2.10 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (𝑁 − 1)) = ((𝐴 · (𝐴 Xrm 𝑁)) − (((𝐴↑2) − 1) · (𝐴 Yrm 𝑁)))) | ||
Theorem | rmym1 38459 | Subtraction of 1 formula for Y sequence. Part 2 of equation 2.10 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (𝑁 − 1)) = (((𝐴 Yrm 𝑁) · 𝐴) − (𝐴 Xrm 𝑁))) | ||
Theorem | rmxluc 38460 | The X sequence is a Lucas (second-order integer recurrence) sequence. Part 3 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (𝑁 + 1)) = (((2 · 𝐴) · (𝐴 Xrm 𝑁)) − (𝐴 Xrm (𝑁 − 1)))) | ||
Theorem | rmyluc 38461 | The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 38453 and rmy1 38454. Part 3 of equation 2.12 of [JonesMatijasevic] p. 695. JonesMatijasevic uses this theorem to redefine the X and Y sequences to have domain (ℤ × ℤ), which simplifies some later theorems. It may shorten the derivation to use this as our initial definition. Incidentally, the X sequence satisfies the exact same recurrence. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (𝑁 + 1)) = ((2 · ((𝐴 Yrm 𝑁) · 𝐴)) − (𝐴 Yrm (𝑁 − 1)))) | ||
Theorem | rmyluc2 38462 | Lucas sequence property of Y with better output ordering. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (𝑁 + 1)) = (((2 · 𝐴) · (𝐴 Yrm 𝑁)) − (𝐴 Yrm (𝑁 − 1)))) | ||
Theorem | rmxdbl 38463 | "Double-angle formula" for X-values. Equation 2.13 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (2 · 𝑁)) = ((2 · ((𝐴 Xrm 𝑁)↑2)) − 1)) | ||
Theorem | rmydbl 38464 | "Double-angle formula" for Y-values. Equation 2.14 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm (2 · 𝑁)) = ((2 · (𝐴 Xrm 𝑁)) · (𝐴 Yrm 𝑁))) | ||
Theorem | monotuz 38465* | A function defined on an upper set of integers which increases at every adjacent pair is globally strictly monotonic by induction. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐻) → 𝐹 < 𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐻) → 𝐶 ∈ ℝ) & ⊢ 𝐻 = (ℤ≥‘𝐼) & ⊢ (𝑥 = (𝑦 + 1) → 𝐶 = 𝐺) & ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐹) & ⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) & ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻)) → (𝐴 < 𝐵 ↔ 𝐷 < 𝐸)) | ||
Theorem | monotoddzzfi 38466* | A function which is odd and monotonic on ℕ0 is monotonic on ℤ. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝐹‘𝑥) ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝐹‘-𝑥) = -(𝐹‘𝑥)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ (𝐹‘𝐴) < (𝐹‘𝐵))) | ||
Theorem | monotoddzz 38467* | A function (given implicitly) which is odd and monotonic on ℕ0 is monotonic on ℤ. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0) → (𝑥 < 𝑦 → 𝐸 < 𝐹)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐸 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐺 = -𝐹) & ⊢ (𝑥 = 𝐴 → 𝐸 = 𝐶) & ⊢ (𝑥 = 𝐵 → 𝐸 = 𝐷) & ⊢ (𝑥 = 𝑦 → 𝐸 = 𝐹) & ⊢ (𝑥 = -𝑦 → 𝐸 = 𝐺) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ 𝐶 < 𝐷)) | ||
Theorem | oddcomabszz 38468* | An odd function which takes nonnegative values on nonnegative arguments commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝐴 ∈ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ ∧ 0 ≤ 𝑥) → 0 ≤ 𝐴) & ⊢ ((𝜑 ∧ 𝑦 ∈ ℤ) → 𝐶 = -𝐵) & ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ (𝑥 = -𝑦 → 𝐴 = 𝐶) & ⊢ (𝑥 = 𝐷 → 𝐴 = 𝐸) & ⊢ (𝑥 = (abs‘𝐷) → 𝐴 = 𝐹) ⇒ ⊢ ((𝜑 ∧ 𝐷 ∈ ℤ) → (abs‘𝐸) = 𝐹) | ||
Theorem | 2nn0ind 38469* | Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝑦 ∈ ℕ → ((𝜃 ∧ 𝜏) → 𝜂)) & ⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 − 1) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜏)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜂)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜌)) ⇒ ⊢ (𝐴 ∈ ℕ0 → 𝜌) | ||
Theorem | zindbi 38470* | Inductively transfer a property to the integers if it holds for zero and passes between adjacent integers in either direction. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (𝑦 ∈ ℤ → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 0 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) ⇒ ⊢ (𝐴 ∈ ℤ → (𝜃 ↔ 𝜏)) | ||
Theorem | expmordi 38471 | Mantissa ordering relationship for exponentiation. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵) ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
Theorem | rpexpmord 38472 | Mantissa ordering relationship for exponentiation of positive reals. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
Theorem | rmxypos 38473 | For all nonnegative indices, X is positive and Y is nonnegative. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (0 < (𝐴 Xrm 𝑁) ∧ 0 ≤ (𝐴 Yrm 𝑁))) | ||
Theorem | ltrmynn0 38474 | The Y-sequence is strictly monotonic on ℕ0. Strengthened by ltrmy 38478. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | ltrmxnn0 38475 | The X-sequence is strictly monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Xrm 𝑀) < (𝐴 Xrm 𝑁))) | ||
Theorem | lermxnn0 38476 | The X-sequence is monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝐴 Xrm 𝑀) ≤ (𝐴 Xrm 𝑁))) | ||
Theorem | rmxnn 38477 | The X-sequence is defined to range over ℕ0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) ∈ ℕ) | ||
Theorem | ltrmy 38478 | The Y-sequence is strictly monotonic over ℤ. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | rmyeq0 38479 | Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0)) | ||
Theorem | rmyeq 38480 | Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑁))) | ||
Theorem | lermy 38481 | Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝐴 Yrm 𝑀) ≤ (𝐴 Yrm 𝑁))) | ||
Theorem | rmynn 38482 | Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ) | ||
Theorem | rmynn0 38483 | Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 Yrm 𝑁) ∈ ℕ0) | ||
Theorem | rmyabs 38484 | Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (abs‘(𝐴 Yrm 𝐵)) = (𝐴 Yrm (abs‘𝐵))) | ||
Theorem | jm2.24nn 38485 | X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of [JonesMatijasevic] p. 697 restricted to ℕ. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) | ||
Theorem | jm2.17a 38486 | First half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (((2 · 𝐴) − 1)↑𝑁) ≤ (𝐴 Yrm (𝑁 + 1))) | ||
Theorem | jm2.17b 38487 | Weak form of the second half of lemma 2.17 of [JonesMatijasevic] p. 696, allowing induction to start lower. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 Yrm (𝑁 + 1)) ≤ ((2 · 𝐴)↑𝑁)) | ||
Theorem | jm2.17c 38488 | Second half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm ((𝑁 + 1) + 1)) < ((2 · 𝐴)↑(𝑁 + 1))) | ||
Theorem | jm2.24 38489 | Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ℤ. Could be eliminated with a more careful proof of jm2.26lem3 38527. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) | ||
Theorem | rmygeid 38490 | Y(n) increases faster than n. Used implicitly without proof or comment in lemma 2.27 of [JonesMatijasevic] p. 697. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (𝐴 Yrm 𝑁)) | ||
Theorem | congtr 38491 | A wff of the form 𝐴 ∥ (𝐵 − 𝐶) is interpreted as a congruential equation. This is similar to (𝐵 mod 𝐴) = (𝐶 mod 𝐴), but is defined such that behavior is regular for zero and negative values of 𝐴. To use this concept effectively, we need to show that congruential equations behave similarly to normal equations; first a transitivity law. Idea for the future: If there was a congruential equation symbol, it could incorporate type constraints, so that most of these would not need them. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐶 − 𝐷))) → 𝐴 ∥ (𝐵 − 𝐷)) | ||
Theorem | congadd 38492 | If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 + 𝐷) − (𝐶 + 𝐸))) | ||
Theorem | congmul 38493 | If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 · 𝐷) − (𝐶 · 𝐸))) | ||
Theorem | congsym 38494 | Congruence mod 𝐴 is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (𝐶 − 𝐵)) | ||
Theorem | congneg 38495 | If two integers are congruent mod 𝐴, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (-𝐵 − -𝐶)) | ||
Theorem | congsub 38496 | If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 − 𝐷) − (𝐶 − 𝐸))) | ||
Theorem | congid 38497 | Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐵 − 𝐵)) | ||
Theorem | mzpcong 38498* | Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))) | ||
Theorem | congrep 38499* | Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...(𝐴 − 1))𝐴 ∥ (𝑎 − 𝑁)) | ||
Theorem | congabseq 38500 | If two integers are congruent, they are either equal or separated by at least the congruence base. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ 𝐴 ∥ (𝐵 − 𝐶)) → ((abs‘(𝐵 − 𝐶)) < 𝐴 ↔ 𝐵 = 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |