Home | Metamath
Proof Explorer Theorem List (p. 396 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pellfundlb 39501 | 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 39502* | 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 39503 |
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 39493. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) | ||
Theorem | pellfund14gap 39504 | 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 39505 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+) | ||
Theorem | pellfundne1 39506 | 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 39507 | General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 25351 instead. |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) → ((log‘𝐴) / (log‘𝐵)) ∈ ℝ) | ||
Theorem | reglogltb 39508 | General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 25362 instead. |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 < 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) < ((log‘𝐵) / (log‘𝐶)))) | ||
Theorem | reglogleb 39509 | General logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 25361 instead. |
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) ≤ ((log‘𝐵) / (log‘𝐶)))) | ||
Theorem | reglogmul 39510 | Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 25355 instead. |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴 · 𝐵)) / (log‘𝐶)) = (((log‘𝐴) / (log‘𝐶)) + ((log‘𝐵) / (log‘𝐶)))) | ||
Theorem | reglogexp 39511 | Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 25354 instead. |
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴↑𝑁)) / (log‘𝐶)) = (𝑁 · ((log‘𝐴) / (log‘𝐶)))) | ||
Theorem | reglogbas 39512 | General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 25346 instead. |
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘𝐶) / (log‘𝐶)) = 1) | ||
Theorem | reglog1 39513 | General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 25347 instead. |
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘1) / (log‘𝐶)) = 0) | ||
Theorem | reglogexpbas 39514 | 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 25358 instead. |
⊢ ((𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐶↑𝑁)) / (log‘𝐶)) = 𝑁) | ||
Theorem | pellfund14 39515* | Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥)) | ||
Theorem | pellfund14b 39516* | 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 39517 | Extend class notation to include the Robertson-Matiyasevich X sequence. |
class Xrm | ||
Syntax | crmy 39518 | Extend class notation to include the Robertson-Matiyasevich Y sequence. |
class Yrm | ||
Definition | df-rmx 39519* | Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 39530 and rmxyval 39532 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 39520* | Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 39531 and rmxyval 39532 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 39521* | Value of the X sequence. Not used after rmxyval 39532 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) = (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
Theorem | rmyfval 39522* | Value of the Y sequence. Not used after rmxyval 39532 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) = (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
Theorem | rmspecsqrtnq 39523 | 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 39524 | 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 39525 | 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 39526 | 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 39527* | 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 39528* | The function used to extract rational and irrational parts in df-rmx 39519 and df-rmy 39520 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 39529* | Lemma for frmx 39530 and frmy 39531. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) ∈ (ℕ0 × ℤ)) | ||
Theorem | frmx 39530 | The X sequence is a nonnegative integer. See rmxnn 39568 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0 | ||
Theorem | frmy 39531 | The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ | ||
Theorem | rmxyval 39532 | 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 39533 | 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 39534* | 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 39535 | 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 39536 | 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 39537 | 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 39538 | Addition formula for X and Y sequences. See rmxadd 39544 and rmyadd 39548 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 39539 | 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 39540 | 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 39541 | Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 39537, rmxyadd 39538, rmxy0 39540, and rmxy1 39539 via qirropth 39525 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 39542 | 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 39543 | 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 39544 | 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 39545 | Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)) | ||
Theorem | rmy0 39546 | 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 39547 | 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 39548 | 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 39549 | 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 39550 | 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 39551 | 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 39552 | 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 39553 | 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 39554 | The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 39546 and rmy1 39547. 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 39555 | 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 39556 | "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 39557 | "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 39558* | 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 39559* | 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 39560* | 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 39561* | 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 39562* | 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 39563* | 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 | rmxypos 39564 | 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 39565 | The Y-sequence is strictly monotonic on ℕ0. Strengthened by ltrmy 39569. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | ltrmxnn0 39566 | The X-sequence is strictly monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Xrm 𝑀) < (𝐴 Xrm 𝑁))) | ||
Theorem | lermxnn0 39567 | The X-sequence is monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝐴 Xrm 𝑀) ≤ (𝐴 Xrm 𝑁))) | ||
Theorem | rmxnn 39568 | 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 39569 | The Y-sequence is strictly monotonic over ℤ. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | rmyeq0 39570 | Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0)) | ||
Theorem | rmyeq 39571 | Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑁))) | ||
Theorem | lermy 39572 | Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝐴 Yrm 𝑀) ≤ (𝐴 Yrm 𝑁))) | ||
Theorem | rmynn 39573 | Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ) | ||
Theorem | rmynn0 39574 | Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 Yrm 𝑁) ∈ ℕ0) | ||
Theorem | rmyabs 39575 | Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (abs‘(𝐴 Yrm 𝐵)) = (𝐴 Yrm (abs‘𝐵))) | ||
Theorem | jm2.24nn 39576 | 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 39577 | 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 39578 | 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 39579 | 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 39580 | Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ℤ. Could be eliminated with a more careful proof of jm2.26lem3 39618. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) | ||
Theorem | rmygeid 39581 | 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 39582 | 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 39583 | If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 + 𝐷) − (𝐶 + 𝐸))) | ||
Theorem | congmul 39584 | If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 · 𝐷) − (𝐶 · 𝐸))) | ||
Theorem | congsym 39585 | Congruence mod 𝐴 is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (𝐶 − 𝐵)) | ||
Theorem | congneg 39586 | If two integers are congruent mod 𝐴, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (-𝐵 − -𝐶)) | ||
Theorem | congsub 39587 | If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 − 𝐷) − (𝐶 − 𝐸))) | ||
Theorem | congid 39588 | Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐵 − 𝐵)) | ||
Theorem | mzpcong 39589* | Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑m 𝑉) ∧ 𝑌 ∈ (ℤ ↑m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))) | ||
Theorem | congrep 39590* | Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...(𝐴 − 1))𝐴 ∥ (𝑎 − 𝑁)) | ||
Theorem | congabseq 39591 | 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‘(𝐵 − 𝐶)) < 𝐴 ↔ 𝐵 = 𝐶)) | ||
Theorem | acongid 39592 |
A wff like that in this theorem will be known as an "alternating
congruence". A special symbol might be considered if more uses come
up.
They have many of the same properties as normal congruences, starting with
reflexivity.
JonesMatijasevic uses "a ≡ ± b (mod c)" for this construction. The disjunction of divisibility constraints seems to adequately capture the concept, but it's rather verbose and somewhat inelegant. Use of an explicit equivalence relation might also work. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ (𝐵 − 𝐵) ∨ 𝐴 ∥ (𝐵 − -𝐵))) | ||
Theorem | acongsym 39593 | Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) → (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵))) | ||
Theorem | acongneg2 39594 | Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − -𝐶) ∨ 𝐴 ∥ (𝐵 − --𝐶))) → (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) | ||
Theorem | acongtr 39595 | Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷)))) → (𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷))) | ||
Theorem | acongeq12d 39596 | Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ (𝜑 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐷 = 𝐸) ⇒ ⊢ (𝜑 → ((𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷)) ↔ (𝐴 ∥ (𝐶 − 𝐸) ∨ 𝐴 ∥ (𝐶 − -𝐸)))) | ||
Theorem | acongrep 39597* | Every integer is alternating-congruent to some number in the first half of the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...𝐴)((2 · 𝐴) ∥ (𝑎 − 𝑁) ∨ (2 · 𝐴) ∥ (𝑎 − -𝑁))) | ||
Theorem | fzmaxdif 39598 | Bound on the difference between two integers constrained to two possibly overlapping finite ranges. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (((𝐶 ∈ ℤ ∧ 𝐴 ∈ (𝐵...𝐶)) ∧ (𝐹 ∈ ℤ ∧ 𝐷 ∈ (𝐸...𝐹)) ∧ (𝐶 − 𝐸) ≤ (𝐹 − 𝐵)) → (abs‘(𝐴 − 𝐷)) ≤ (𝐹 − 𝐵)) | ||
Theorem | fzneg 39599 | Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ (𝐵...𝐶) ↔ -𝐴 ∈ (-𝐶...-𝐵))) | ||
Theorem | acongeq 39600 | Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 39619. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 = 𝐶 ↔ ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |