Home | Metamath
Proof Explorer Theorem List (p. 395 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rmxneg 39401 | Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 39397, rmxyadd 39398, rmxy0 39400, and rmxy1 39399 via qirropth 39385 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 39402 | 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 39403 | 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 39404 | 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 39405 | Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁)) | ||
Theorem | rmy0 39406 | 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 39407 | 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 39408 | 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 39409 | 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 39410 | 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 39411 | 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 39412 | 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 39413 | 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 39414 | The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 39406 and rmy1 39407. 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 39415 | 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 39416 | "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 39417 | "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 39418* | 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 39419* | 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 39420* | 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 39421* | 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 39422* | 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 39423* | 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 39424 | 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 39425 | The Y-sequence is strictly monotonic on ℕ0. Strengthened by ltrmy 39429. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | ltrmxnn0 39426 | The X-sequence is strictly monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Xrm 𝑀) < (𝐴 Xrm 𝑁))) | ||
Theorem | lermxnn0 39427 | The X-sequence is monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝐴 Xrm 𝑀) ≤ (𝐴 Xrm 𝑁))) | ||
Theorem | rmxnn 39428 | 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 39429 | The Y-sequence is strictly monotonic over ℤ. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁))) | ||
Theorem | rmyeq0 39430 | Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0)) | ||
Theorem | rmyeq 39431 | Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑁))) | ||
Theorem | lermy 39432 | Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝐴 Yrm 𝑀) ≤ (𝐴 Yrm 𝑁))) | ||
Theorem | rmynn 39433 | Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ) | ||
Theorem | rmynn0 39434 | Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 Yrm 𝑁) ∈ ℕ0) | ||
Theorem | rmyabs 39435 | Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (abs‘(𝐴 Yrm 𝐵)) = (𝐴 Yrm (abs‘𝐵))) | ||
Theorem | jm2.24nn 39436 | 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 39437 | 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 39438 | 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 39439 | 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 39440 | Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ℤ. Could be eliminated with a more careful proof of jm2.26lem3 39478. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁)) | ||
Theorem | rmygeid 39441 | 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 39442 | 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 39443 | If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 + 𝐷) − (𝐶 + 𝐸))) | ||
Theorem | congmul 39444 | If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 · 𝐷) − (𝐶 · 𝐸))) | ||
Theorem | congsym 39445 | Congruence mod 𝐴 is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (𝐶 − 𝐵)) | ||
Theorem | congneg 39446 | If two integers are congruent mod 𝐴, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (-𝐵 − -𝐶)) | ||
Theorem | congsub 39447 | If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 − 𝐷) − (𝐶 − 𝐸))) | ||
Theorem | congid 39448 | Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐵 − 𝐵)) | ||
Theorem | mzpcong 39449* | Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.) |
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑m 𝑉) ∧ 𝑌 ∈ (ℤ ↑m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌))) | ||
Theorem | congrep 39450* | Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...(𝐴 − 1))𝐴 ∥ (𝑎 − 𝑁)) | ||
Theorem | congabseq 39451 | 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 39452 |
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 39453 | Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) → (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵))) | ||
Theorem | acongneg2 39454 | Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − -𝐶) ∨ 𝐴 ∥ (𝐵 − --𝐶))) → (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) | ||
Theorem | acongtr 39455 | Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷)))) → (𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷))) | ||
Theorem | acongeq12d 39456 | Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
⊢ (𝜑 → 𝐵 = 𝐶) & ⊢ (𝜑 → 𝐷 = 𝐸) ⇒ ⊢ (𝜑 → ((𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷)) ↔ (𝐴 ∥ (𝐶 − 𝐸) ∨ 𝐴 ∥ (𝐶 − -𝐸)))) | ||
Theorem | acongrep 39457* | 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 39458 | 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 39459 | Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ (𝐵...𝐶) ↔ -𝐴 ∈ (-𝐶...-𝐵))) | ||
Theorem | acongeq 39460 | Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 39479. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 = 𝐶 ↔ ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶)))) | ||
Theorem | dvdsacongtr 39461 | Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐷 ∥ 𝐴 ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)))) → (𝐷 ∥ (𝐵 − 𝐶) ∨ 𝐷 ∥ (𝐵 − -𝐶))) | ||
Theorem | coprmdvdsb 39462 | Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ (𝐾 gcd 𝑀) = 1)) → (𝐾 ∥ 𝑁 ↔ 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | modabsdifz 39463 | 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 39464 | 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 39465 | 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 39466 | Lemma for jm2.19 39470. X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → ((𝐴 Xrm 𝑀) gcd (𝐴 Yrm 𝑀)) = 1) | ||
Theorem | jm2.19lem2 39467 | Lemma for jm2.19 39470. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + 𝑀)))) | ||
Theorem | jm2.19lem3 39468 | Lemma for jm2.19 39470. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))))) | ||
Theorem | jm2.19lem4 39469 | Lemma for jm2.19 39470. Extend to ZZ by symmetry. TODO: use zindbi 39423. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀))))) | ||
Theorem | jm2.19 39470 | 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 39471 | Lemma for jm2.20nn 39474. 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 39472* | Lemma for jm2.20nn 39474. 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 39473 | Lemma for jm2.20nn 39474. Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁))))) | ||
Theorem | jm2.20nn 39474 | 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 39475 | Lemma for jm2.26 39479. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷))) → ((𝐴 ∥ (𝐷 − 𝐵) ∨ 𝐴 ∥ (𝐷 − -𝐵)) ↔ (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵)))) | ||
Theorem | jm2.25 39476 | Lemma for jm2.26 39479. 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 39477 | Lemma for jm2.26 39479. Reverse direction is required to prove forward direction, so do it separately. 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 39478 | Lemma for jm2.26 39479. Use acongrep 39457 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 39479 | 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 39480 | 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 39481 | Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 39480 if Yrm is redefined as described in rmyluc 39414. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁)) | ||
Theorem | jm2.27a 39482 | Lemma for jm2.27 39485. 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 39483 | Lemma for jm2.27 39485. 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 39484 | Lemma for jm2.27 39485. 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 39485* | 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 39482 and jm2.27c 39484. 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 39486* | Lemma for rmydioph 39491. Substitution of a tuple restriction into a projection that doesn't care. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ (1...𝐵) ⇒ ⊢ (𝑎 = (𝑏 ↾ (1...𝐵)) → (𝑎‘𝐴) = (𝑏‘𝐴)) | ||
Theorem | jm2.27dlem2 39487 | Lemma for rmydioph 39491. 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 39488 | Lemma for rmydioph 39491. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ∈ (1...𝐴) | ||
Theorem | jm2.27dlem4 39489 | Lemma for rmydioph 39491. Infer ℕ-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 = (𝐴 + 1) ⇒ ⊢ 𝐵 ∈ ℕ | ||
Theorem | jm2.27dlem5 39490 | Lemma for rmydioph 39491. Used with sselii 3963 to infer membership of midpoints of range; jm2.27dlem2 39487 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
⊢ 𝐵 = (𝐴 + 1) & ⊢ (1...𝐵) ⊆ (1...𝐶) ⇒ ⊢ (1...𝐴) ⊆ (1...𝐶) | ||
Theorem | rmydioph 39491 | jm2.27 39485 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Yrm (𝑎‘2)))} ∈ (Dioph‘3) | ||
Theorem | rmxdiophlem 39492* | 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))) | ||
Theorem | rmxdioph 39493 | X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ ((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘3) = ((𝑎‘1) Xrm (𝑎‘2)))} ∈ (Dioph‘3) | ||
Theorem | jm3.1lem1 39494 | Lemma for jm3.1 39497. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐾↑𝑁) < 𝐴) | ||
Theorem | jm3.1lem2 39495 | Lemma for jm3.1 39497. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝐾↑𝑁) < ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1)) | ||
Theorem | jm3.1lem3 39496 | Lemma for jm3.1 39497. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) ⇒ ⊢ (𝜑 → ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1) ∈ ℕ) | ||
Theorem | jm3.1 39497 | Diophantine expression for exponentiation. Lemma 3.1 of [JonesMatijasevic] p. 698. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
⊢ (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐾 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) ∧ (𝐾 Yrm (𝑁 + 1)) ≤ 𝐴) → (𝐾↑𝑁) = (((𝐴 Xrm 𝑁) − ((𝐴 − 𝐾) · (𝐴 Yrm 𝑁))) mod ((((2 · 𝐴) · 𝐾) − (𝐾↑2)) − 1))) | ||
Theorem | expdiophlem1 39498* | Lemma for expdioph 39500. Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ (𝐶 ∈ ℕ0 → (((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ) ∧ 𝐶 = (𝐴↑𝐵)) ↔ ∃𝑑 ∈ ℕ0 ∃𝑒 ∈ ℕ0 ∃𝑓 ∈ ℕ0 ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℕ) ∧ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑑 = (𝐴 Yrm (𝐵 + 1))) ∧ ((𝑑 ∈ (ℤ≥‘2) ∧ 𝑒 = (𝑑 Yrm 𝐵)) ∧ ((𝑑 ∈ (ℤ≥‘2) ∧ 𝑓 = (𝑑 Xrm 𝐵)) ∧ (𝐶 < ((((2 · 𝑑) · 𝐴) − (𝐴↑2)) − 1) ∧ ((((2 · 𝑑) · 𝐴) − (𝐴↑2)) − 1) ∥ ((𝑓 − ((𝑑 − 𝐴) · 𝑒)) − 𝐶)))))))) | ||
Theorem | expdiophlem2 39499 | Lemma for expdioph 39500. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (((𝑎‘1) ∈ (ℤ≥‘2) ∧ (𝑎‘2) ∈ ℕ) ∧ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2)))} ∈ (Dioph‘3) | ||
Theorem | expdioph 39500 | The exponential function is Diophantine. This result completes and encapsulates our development using Pell equation solution sequences and is sometimes regarded as Matiyasevich's theorem properly. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
⊢ {𝑎 ∈ (ℕ0 ↑m (1...3)) ∣ (𝑎‘3) = ((𝑎‘1)↑(𝑎‘2))} ∈ (Dioph‘3) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |