Home | Metamath
Proof Explorer Theorem List (p. 366 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rmxynorm 36501 | 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 36502 | 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 36503 | 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 36504 | Addition formula for X and Y sequences. See rmxadd 36510 and rmyadd 36514 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 36505 | 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 36506 | 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 36507 | Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 36503, rmxyadd 36504, rmxy0 36506, and rmxy1 36505 via qirropth 36491 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 36508 | 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 36509 | 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 36510 | 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 36511 | Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)) | ||
Theorem | rmy0 36512 | 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 36513 | 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 36514 | 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 36515 | 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 36516 | 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 36517 | 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 36518 | 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 36519 | 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 36520 | The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 36512 and rmy1 36513. 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 36521 | 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 36522 | "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 36523 | "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 36524* | 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 36525* | 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 36526* | 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 36527* | 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 36528* | 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 36529* | 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 36530 | Mantissa ordering relationship for exponentiation. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤ 𝐴 ∧ 𝐴 < 𝐵) ∧ 𝑁 ∈ ℕ) → (𝐴↑𝑁) < (𝐵↑𝑁)) | ||
Theorem | rpexpmord 36531 | Mantissa ordering relationship for exponentiation of positive reals. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → (𝐴 < 𝐵 ↔ (𝐴↑𝑁) < (𝐵↑𝑁))) | ||
Theorem | rmxypos 36532 | 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 36533 | The Y-sequence is strictly monotonic on ℕ0. Strengthened by ltrmy 36537. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | ltrmxnn0 36534 | The X-sequence is strictly monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Xrm 𝑀) < (𝐴 Xrm 𝑁))) | ||
Theorem | lermxnn0 36535 | The X-sequence is monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝐴 Xrm 𝑀) ≤ (𝐴 Xrm 𝑁))) | ||
Theorem | rmxnn 36536 | 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 36537 | The Y-sequence is strictly monotonic over ℤ. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | rmyeq0 36538 | Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0)) | ||
Theorem | rmyeq 36539 | Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑁))) | ||
Theorem | lermy 36540 | Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝐴 Yrm 𝑀) ≤ (𝐴 Yrm 𝑁))) | ||
Theorem | rmynn 36541 | Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ) | ||
Theorem | rmynn0 36542 | Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 Yrm 𝑁) ∈ ℕ0) | ||
Theorem | rmyabs 36543 | Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (abs‘(𝐴 Yrm 𝐵)) = (𝐴 Yrm (abs‘𝐵))) | ||
Theorem | jm2.24nn 36544 | 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 36545 | 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 36546 | 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 36547 | 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 36548 | Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ℤ. Could be eliminated with a more careful proof of jm2.26lem3 36586. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) | ||
Theorem | rmygeid 36549 | 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 36550 | 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 36551 | If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 + 𝐷) − (𝐶 + 𝐸))) | ||
Theorem | congmul 36552 | If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 · 𝐷) − (𝐶 · 𝐸))) | ||
Theorem | congsym 36553 | Congruence mod 𝐴 is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (𝐶 − 𝐵)) | ||
Theorem | congneg 36554 | If two integers are congruent mod 𝐴, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (-𝐵 − -𝐶)) | ||
Theorem | congsub 36555 | If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 − 𝐷) − (𝐶 − 𝐸))) | ||
Theorem | congid 36556 | Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐵 − 𝐵)) | ||
Theorem | mzpcong 36557* | Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑𝑚 𝑉) ∧ 𝑌 ∈ (ℤ ↑𝑚 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))) | ||
Theorem | congrep 36558* | Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...(𝐴 − 1))𝐴 ∥ (𝑎 − 𝑁)) | ||
Theorem | congabseq 36559 | 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 36560 |
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 36561 | Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) → (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵))) | ||
Theorem | acongneg2 36562 | Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − -𝐶) ∨ 𝐴 ∥ (𝐵 − --𝐶))) → (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) | ||
Theorem | acongtr 36563 | Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷)))) → (𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷))) | ||
Theorem | acongeq12d 36564 | Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ (𝜑 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐷 = 𝐸) ⇒ ⊢ (𝜑 → ((𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷)) ↔ (𝐴 ∥ (𝐶 − 𝐸) ∨ 𝐴 ∥ (𝐶 − -𝐸)))) | ||
Theorem | acongrep 36565* | 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 36566 | 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 36567 | Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ (𝐵...𝐶) ↔ -𝐴 ∈ (-𝐶...-𝐵))) | ||
Theorem | acongeq 36568 | Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 36587. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 = 𝐶 ↔ ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶)))) | ||
Theorem | dvdsacongtr 36569 | Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐷 ∥ 𝐴 ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)))) → (𝐷 ∥ (𝐵 − 𝐶) ∨ 𝐷 ∥ (𝐵 − -𝐶))) | ||
Theorem | coprmdvdsb 36570 | Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ (𝐾 gcd 𝑀) = 1)) → (𝐾 ∥ 𝑁 ↔ 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | modabsdifz 36571 | Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≠ 0) → ((𝑁 − (𝑁 mod (abs‘𝑀))) / 𝑀) ∈ ℤ) | ||
Theorem | dvdsabsmod0 36572 | Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 24-Sep-2014.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≠ 0) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod (abs‘𝑀)) = 0)) | ||
Theorem | jm2.18 36573 | Theorem 2.18 of [JonesMatijasevic] p. 696. Direct relationship of the exponential function to X and Y sequences. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∥ (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) − (𝐾↑𝑁))) | ||
Theorem | jm2.19lem1 36574 | Lemma for jm2.19 36578. X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → ((𝐴 Xrm 𝑀) gcd (𝐴 Yrm 𝑀)) = 1) | ||
Theorem | jm2.19lem2 36575 | Lemma for jm2.19 36578. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + 𝑀)))) | ||
Theorem | jm2.19lem3 36576 | Lemma for jm2.19 36578. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))))) | ||
Theorem | jm2.19lem4 36577 | Lemma for jm2.19 36578. Extend to ZZ by symmetry. TODO: use zindbi 36529. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))))) | ||
Theorem | jm2.19 36578 | Lemma 2.19 of [JonesMatijasevic] p. 696. Transfer divisibility constraints between Y-values and their indices. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁))) | ||
Theorem | jm2.21 36579 | Lemma for jm2.20nn 36582. Express X and Y values as a binomial. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ) → ((𝐴 Xrm (𝑁 · 𝐽)) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm (𝑁 · 𝐽)))) = (((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁)))↑𝐽)) | ||
Theorem | jm2.22 36580* | Lemma for jm2.20nn 36582. Applying binomial theorem and taking irrational part. (Contributed by Stefan O'Rear, 26-Sep-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ0) → (𝐴 Yrm (𝑁 · 𝐽)) = Σ𝑖 ∈ {𝑥 ∈ (0...𝐽) ∣ ¬ 2 ∥ 𝑥} ((𝐽C𝑖) · (((𝐴 Xrm 𝑁)↑(𝐽 − 𝑖)) · (((𝐴 Yrm 𝑁)↑𝑖) · (((𝐴↑2) − 1)↑((𝑖 − 1) / 2)))))) | ||
Theorem | jm2.23 36581 | Lemma for jm2.20nn 36582. Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))))) | ||
Theorem | jm2.20nn 36582 | Lemma 2.20 of [JonesMatijasevic] p. 696, the "first step down lemma". (Contributed by Stefan O'Rear, 27-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (((𝐴 Yrm 𝑁)↑2) ∥ (𝐴 Yrm 𝑀) ↔ (𝑁 · (𝐴 Yrm 𝑁)) ∥ 𝑀)) | ||
Theorem | jm2.25lem1 36583 | Lemma for jm2.26 36587. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷))) → ((𝐴 ∥ (𝐷 − 𝐵) ∨ 𝐴 ∥ (𝐷 − -𝐵)) ↔ (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵)))) | ||
Theorem | jm2.25 36584 | Lemma for jm2.26 36587. Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm (𝑀 + (𝐼 · (2 · 𝑁)))) − -(𝐴 Yrm 𝑀)))) | ||
Theorem | jm2.26a 36585 | Lemma for jm2.26 36587. Reverse direction is required to prove forward direction, so do it separatly. Induction on difference between K and M, together with the addition formula fact that adding 2N only inverts sign. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)) → ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))))) | ||
Theorem | jm2.26lem3 36586 | Lemma for jm2.26 36587. Use acongrep 36565 to find K', M' ~ K, M in [ 0,N ]. Thus Y(K') ~ Y(M') and both are small; K' = M' on pain of contradicting 2.24, so K ~ M. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ (0...𝑁) ∧ 𝑀 ∈ (0...𝑁)) ∧ ((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀)))) → 𝐾 = 𝑀) | ||
Theorem | jm2.26 36587 | Lemma 2.26 of [JonesMatijasevic] p. 697, the "second step down lemma". (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → (((𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − (𝐴 Yrm 𝑀)) ∨ (𝐴 Xrm 𝑁) ∥ ((𝐴 Yrm 𝐾) − -(𝐴 Yrm 𝑀))) ↔ ((2 · 𝑁) ∥ (𝐾 − 𝑀) ∨ (2 · 𝑁) ∥ (𝐾 − -𝑀)))) | ||
Theorem | jm2.15nn0 36588 | Lemma 2.15 of [JonesMatijasevic] p. 695. Yrm is a polynomial for fixed N, so has the expected congruence property. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 𝐵) ∥ ((𝐴 Yrm 𝑁) − (𝐵 Yrm 𝑁))) | ||
Theorem | jm2.16nn0 36589 | Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 36588 if Yrm is redefined as described in rmyluc 36520. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁)) | ||
Theorem | jm2.27a 36590 | Lemma for jm2.27 36593. Reverse direction after existential quantifiers are expanded. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐸 ∈ ℕ0) & ⊢ (𝜑 → 𝐹 ∈ ℕ0) & ⊢ (𝜑 → 𝐺 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ ℕ0) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1) & ⊢ (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1) & ⊢ (𝜑 → 𝐺 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1) & ⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2)))) & ⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴)) & ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1)) & ⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶)) & ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) & ⊢ (𝜑 → 𝑃 ∈ ℤ) & ⊢ (𝜑 → 𝐷 = (𝐴 Xrm 𝑃)) & ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝑃)) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝐹 = (𝐴 Xrm 𝑄)) & ⊢ (𝜑 → 𝐸 = (𝐴 Yrm 𝑄)) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝐼 = (𝐺 Xrm 𝑅)) & ⊢ (𝜑 → 𝐻 = (𝐺 Yrm 𝑅)) ⇒ ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) | ||
Theorem | jm2.27b 36591 | Lemma for jm2.27 36593. Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → 𝐸 ∈ ℕ0) & ⊢ (𝜑 → 𝐹 ∈ ℕ0) & ⊢ (𝜑 → 𝐺 ∈ ℕ0) & ⊢ (𝜑 → 𝐻 ∈ ℕ0) & ⊢ (𝜑 → 𝐼 ∈ ℕ0) & ⊢ (𝜑 → 𝐽 ∈ ℕ0) & ⊢ (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1) & ⊢ (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1) & ⊢ (𝜑 → 𝐺 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1) & ⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2)))) & ⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴)) & ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1)) & ⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶)) & ⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) ⇒ ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) | ||
Theorem | jm2.27c 36592 | Lemma for jm2.27 36593. Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℕ) & ⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) & ⊢ 𝐷 = (𝐴 Xrm 𝐵) & ⊢ 𝑄 = (𝐵 · (𝐴 Yrm 𝐵)) & ⊢ 𝐸 = (𝐴 Yrm (2 · 𝑄)) & ⊢ 𝐹 = (𝐴 Xrm (2 · 𝑄)) & ⊢ 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) & ⊢ 𝐻 = (𝐺 Yrm 𝐵) & ⊢ 𝐼 = (𝐺 Xrm 𝐵) & ⊢ 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1) ⇒ ⊢ (𝜑 → (((𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0 ∧ 𝐹 ∈ ℕ0) ∧ (𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0)) ∧ (𝐽 ∈ ℕ0 ∧ (((((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ∧ 𝐺 ∈ (ℤ≥‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻 − 𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶)))))) | ||
Theorem | jm2.27 36593* | Lemma 2.27 of [JonesMatijasevic] p. 697; rmY is a diophantine relation. 0 was excluded from the range of B and the lower limit of G was imposed because the source proof does not seem to work otherwise; quite possible I'm just missing something. The source proof uses both i and I; i has been changed to j to avoid collision. This theorem is basically nothing but substitution instances, all the work is done in jm2.27a 36590 and jm2.27c 36592. Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine" (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (𝐶 = (𝐴 Yrm 𝐵) ↔ ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ∃𝑔 ∈ ℕ0 ∃ℎ ∈ ℕ0 ∃𝑖 ∈ ℕ0 ∃𝑗 ∈ ℕ0 (((((𝑑↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝑓↑2) − (((𝐴↑2) − 1) · (𝑒↑2))) = 1 ∧ 𝑔 ∈ (ℤ≥‘2)) ∧ (((𝑖↑2) − (((𝑔↑2) − 1) · (ℎ↑2))) = 1 ∧ 𝑒 = ((𝑗 + 1) · (2 · (𝐶↑2))) ∧ 𝑓 ∥ (𝑔 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝑔 − 1) ∧ 𝑓 ∥ (ℎ − 𝐶)) ∧ ((2 · 𝐶) ∥ (ℎ − 𝐵) ∧ 𝐵 ≤ 𝐶))))) | ||
Theorem | jm2.27dlem1 36594* | Lemma for rmydioph 36599. Subsitution of a tuple restriction into a projection that doesn't care. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ (1...𝐵) ⇒ ⊢ (𝑎 = (𝑏 ↾ (1...𝐵)) → (𝑎‘𝐴) = (𝑏‘𝐴)) | ||
Theorem | jm2.27dlem2 36595 | Lemma for rmydioph 36599. This theorem is used along with the next three to efficiently infer steps like 7 ∈ (1...;10). (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ (1...𝐵) & ⊢ 𝐶 = (𝐵 + 1) & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ 𝐴 ∈ (1...𝐶) | ||
Theorem | jm2.27dlem3 36596 | Lemma for rmydioph 36599. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ (1...𝐴) | ||
Theorem | jm2.27dlem4 36597 | Lemma for rmydioph 36599. Infer ℕ-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 = (𝐴 + 1) ⇒ ⊢ 𝐵 ∈ ℕ | ||
Theorem | jm2.27dlem5 36598 | Lemma for rmydioph 36599. Used with sselii 3565 to infer membership of midpoints of range; jm2.27dlem2 36595 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐵 = (𝐴 + 1) & ⊢ (1...𝐵) ⊆ (1...𝐶) ⇒ ⊢ (1...𝐴) ⊆ (1...𝐶) | ||
Theorem | rmydioph 36599 | jm2.27 36593 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ {𝑎 ∈ (ℕ0 ↑𝑚 (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3) | ||
Theorem | rmxdiophlem 36600* | X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ ℕ0) → (𝑋 = (𝐴 Xrm 𝑁) ↔ ∃𝑦 ∈ ℕ0 (𝑦 = (𝐴 Yrm 𝑁) ∧ ((𝑋↑2) − (((𝐴↑2) − 1) · (𝑦↑2))) = 1))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |