P. 436 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43501-43600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rmxyelxp 43501*	Lemma for frmx 43502 and frmy 43503. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) ∈ (ℕ0 × ℤ))
Theorem	frmx 43502	The X sequence is a nonnegative integer. See rmxnn 43540 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0
Theorem	frmy 43503	The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
Theorem	rmxyval 43504	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 43505	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 43506*	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 43507	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 43508	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 43509	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 43510	Addition formula for X and Y sequences. See rmxadd 43516 and rmyadd 43520 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 43511	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 43512	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 43513	Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 43509, rmxyadd 43510, rmxy0 43512, and rmxy1 43511 via qirropth 43497 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 43514	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 43515	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 43516	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 43517	Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁))
Theorem	rmy0 43518	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 43519	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 43520	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 43521	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 43522	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 43523	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 43524	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 43525	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 43526	The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 43518 and rmy1 43519. 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 43527	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 43528	"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 43529	"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 𝑁)))
21.33.27  Ordering and induction lemmas for the integers
Theorem	monotuz 43530*	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 43531*	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 43532*	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 43533*	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 43534*	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 43535*	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 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    ⇒   ⊢ (𝐴 ∈ ℤ → (𝜃 ↔ 𝜏))
21.33.28  X and Y sequences 2: Order properties
Theorem	rmxypos 43536	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 43537	The Y-sequence is strictly monotonic on ℕ0. Strengthened by ltrmy 43541. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁)))
Theorem	ltrmxnn0 43538	The X-sequence is strictly monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Xrm 𝑀) < (𝐴 Xrm 𝑁)))
Theorem	lermxnn0 43539	The X-sequence is monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝐴 Xrm 𝑀) ≤ (𝐴 Xrm 𝑁)))
Theorem	rmxnn 43540	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 43541	The Y-sequence is strictly monotonic over ℤ. (Contributed by Stefan O'Rear, 25-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁)))
Theorem	rmyeq0 43542	Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0))
Theorem	rmyeq 43543	Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑁)))
Theorem	lermy 43544	Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝐴 Yrm 𝑀) ≤ (𝐴 Yrm 𝑁)))
Theorem	rmynn 43545	Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ)
Theorem	rmynn0 43546	Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 Yrm 𝑁) ∈ ℕ0)
Theorem	rmyabs 43547	Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (abs‘(𝐴 Yrm 𝐵)) = (𝐴 Yrm (abs‘𝐵)))
Theorem	jm2.24nn 43548	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 43549	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 43550	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 43551	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 43552	Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ℤ. Could be eliminated with a more careful proof of jm2.26lem3 43590. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁))
Theorem	rmygeid 43553	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 𝑁))
21.33.29  Congruential equations
Theorem	congtr 43554	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 43555	If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 + 𝐷) − (𝐶 + 𝐸)))
Theorem	congmul 43556	If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 · 𝐷) − (𝐶 · 𝐸)))
Theorem	congsym 43557	Congruence mod 𝐴 is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (𝐶 − 𝐵))
Theorem	congneg 43558	If two integers are congruent mod 𝐴, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (-𝐵 − -𝐶))
Theorem	congsub 43559	If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 − 𝐷) − (𝐶 − 𝐸)))
Theorem	congid 43560	Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐵 − 𝐵))
Theorem	mzpcong 43561*	Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑m 𝑉) ∧ 𝑌 ∈ (ℤ ↑m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))
Theorem	congrep 43562*	Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...(𝐴 − 1))𝐴 ∥ (𝑎 − 𝑁))
Theorem	congabseq 43563	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‘(𝐵 − 𝐶)) < 𝐴 ↔ 𝐵 = 𝐶))
21.33.30  Alternating congruential equations
Theorem	acongid 43564	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 43565	Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶))) → (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵)))
Theorem	acongneg2 43566	Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − -𝐶) ∨ 𝐴 ∥ (𝐵 − --𝐶))) → (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)))
Theorem	acongtr 43567	Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ ((𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷)))) → (𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷)))
Theorem	acongeq12d 43568	Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ (𝜑 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐷 = 𝐸)    ⇒   ⊢ (𝜑 → ((𝐴 ∥ (𝐵 − 𝐷) ∨ 𝐴 ∥ (𝐵 − -𝐷)) ↔ (𝐴 ∥ (𝐶 − 𝐸) ∨ 𝐴 ∥ (𝐶 − -𝐸))))
Theorem	acongrep 43569*	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 43570	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 43571	Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∈ (𝐵...𝐶) ↔ -𝐴 ∈ (-𝐶...-𝐵)))
Theorem	acongeq 43572	Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 43591. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ (0...𝐴) ∧ 𝐶 ∈ (0...𝐴)) → (𝐵 = 𝐶 ↔ ((2 · 𝐴) ∥ (𝐵 − 𝐶) ∨ (2 · 𝐴) ∥ (𝐵 − -𝐶))))
Theorem	dvdsacongtr 43573	Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐷 ∥ 𝐴 ∧ (𝐴 ∥ (𝐵 − 𝐶) ∨ 𝐴 ∥ (𝐵 − -𝐶)))) → (𝐷 ∥ (𝐵 − 𝐶) ∨ 𝐷 ∥ (𝐵 − -𝐶)))
21.33.31  Additional theorems on integer divisibility
Theorem	coprmdvdsb 43574	Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ (𝐾 gcd 𝑀) = 1)) → (𝐾 ∥ 𝑁 ↔ 𝐾 ∥ (𝑀 · 𝑁)))
Theorem	modabsdifz 43575	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 43576	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))
21.33.32  X and Y sequences 3: Divisibility properties
Theorem	jm2.18 43577	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 43578	Lemma for jm2.19 43582. X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ) → ((𝐴 Xrm 𝑀) gcd (𝐴 Yrm 𝑀)) = 1)
Theorem	jm2.19lem2 43579	Lemma for jm2.19 43582. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + 𝑀))))
Theorem	jm2.19lem3 43580	Lemma for jm2.19 43582. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℕ0) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))
Theorem	jm2.19lem4 43581	Lemma for jm2.19 43582. Extend to ZZ by symmetry. TODO: use zindbi 43535. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐼 ∈ ℤ) → ((𝐴 Yrm 𝑀) ∥ (𝐴 Yrm 𝑁) ↔ (𝐴 Yrm 𝑀) ∥ (𝐴 Yrm (𝑁 + (𝐼 · 𝑀)))))
Theorem	jm2.19 43582	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 43583	Lemma for jm2.20nn 43586. 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 43584*	Lemma for jm2.20nn 43586. 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 43585	Lemma for jm2.20nn 43586. Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℕ) → ((𝐴 Yrm 𝑁)↑3) ∥ ((𝐴 Yrm (𝑁 · 𝐽)) − (𝐽 · (((𝐴 Xrm 𝑁)↑(𝐽 − 1)) · (𝐴 Yrm 𝑁)))))
Theorem	jm2.20nn 43586	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 43587	Lemma for jm2.26 43591. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝐴 ∥ (𝐶 − 𝐷) ∨ 𝐴 ∥ (𝐶 − -𝐷))) → ((𝐴 ∥ (𝐷 − 𝐵) ∨ 𝐴 ∥ (𝐷 − -𝐵)) ↔ (𝐴 ∥ (𝐶 − 𝐵) ∨ 𝐴 ∥ (𝐶 − -𝐵))))
Theorem	jm2.25 43588	Lemma for jm2.26 43591. 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 43589	Lemma for jm2.26 43591. 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 43590	Lemma for jm2.26 43591. Use acongrep 43569 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 43591	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 43592	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 43593	Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 43592 if Yrm is redefined as described in rmyluc 43526. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 − 1) ∥ ((𝐴 Yrm 𝑁) − 𝑁))
21.33.33  X and Y sequences 4: Diophantine representability of Y
Theorem	jm2.27a 43594	Lemma for jm2.27 43597. 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 43595	Lemma for jm2.27 43597. 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 43596	Lemma for jm2.27 43597. 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 43597*	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 43594 and jm2.27c 43596. 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 43598*	Lemma for rmydioph 43603. 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 43599	Lemma for rmydioph 43603. 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 43600	Lemma for rmydioph 43603. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ 𝐴 ∈ (1...𝐴)