P. 439 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43801-43900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pell14qrss1234 43801	A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) ⊆ (Pell1234QR‘𝐷))
Theorem	pell14qrre 43802	A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ)
Theorem	pell14qrne0 43803	A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ≠ 0)
Theorem	pell14qrgt0 43804	A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴)
Theorem	pell14qrrp 43805	A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ+)
Theorem	pell1234qrdich 43806	A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷)))
Theorem	elpell14qr2 43807	A number is a positive Pell solution iff it is positive and a Pell solution, justifying our name choice. (Contributed by Stefan O'Rear, 19-Oct-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ (Pell1234QR‘𝐷) ∧ 0 < 𝐴)))
Theorem	pell14qrmulcl 43808	Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrreccl 43809	Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 / 𝐴) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrdivcl 43810	Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 / 𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrexpclnn0 43811	Lemma for pell14qrexpcl 43812. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell14qrexpcl 43812	Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷))
Theorem	pell1qrss14 43813	First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷))
Theorem	pell14qrdich 43814	A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (𝐴 ∈ (Pell1QR‘𝐷) ∨ (1 / 𝐴) ∈ (Pell1QR‘𝐷)))
Theorem	pell1qrge1 43815	A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴)
Theorem	pell1qr1 43816	1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 ∈ (Pell1QR‘𝐷))
Theorem	elpell1qr2 43817	The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝐴)))
Theorem	pell1qrgaplem 43818	Lemma for pell1qrgap 43819. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (𝐴 + ((√‘𝐷) · 𝐵)))
Theorem	pell1qrgap 43819	First-quadrant Pell solutions are bounded away from 1. (This particular bound allows to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴)
Theorem	pell14qrgap 43820	Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴)
Theorem	pell14qrgapw 43821	Positive Pell solutions are bounded away from 1, with a friendlier bound. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < 𝐴)
Theorem	pellqrexplicit 43822	Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1) → (𝐴 + ((√‘𝐷) · 𝐵)) ∈ (Pell1QR‘𝐷))
21.35.23  Pell equations 3: characterizing fundamental solution
Theorem	infmrgelbi 43823*	Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013.) (Revised by AV, 17-Sep-2020.)
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥) → 𝐵 ≤ inf(𝐴, ℝ, < ))
Theorem	pellqrex 43824*	There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ∃𝑥 ∈ (Pell1QR‘𝐷)1 < 𝑥)
Theorem	pellfundval 43825*	Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) = inf({𝑥 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑥}, ℝ, < ))
Theorem	pellfundre 43826	The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ)
Theorem	pellfundge 43827	Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (PellFund‘𝐷))
Theorem	pellfundgt1 43828	Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷))
Theorem	pellfundlb 43829	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 43830*	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 43831	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 43821. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
Theorem	pellfund14gap 43832	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 43833	The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+)
Theorem	pellfundne1 43834	The fundamental Pell solution is never 1. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ≠ 1)
21.35.24  Logarithm laws generalized to an arbitrary base Section should be obsolete because its contents are covered by section "Logarithms to an arbitrary base" now.
Theorem	reglogcl 43835	General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 27065 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) → ((log‘𝐴) / (log‘𝐵)) ∈ ℝ)
Theorem	reglogltb 43836	General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 27076 instead.
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 < 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) < ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogleb 43837	General logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 27075 instead.
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) ≤ ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogmul 43838	Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 27069 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴 · 𝐵)) / (log‘𝐶)) = (((log‘𝐴) / (log‘𝐶)) + ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogexp 43839	Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 27068 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴↑𝑁)) / (log‘𝐶)) = (𝑁 · ((log‘𝐴) / (log‘𝐶))))
Theorem	reglogbas 43840	General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 27060 instead.
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘𝐶) / (log‘𝐶)) = 1)
Theorem	reglog1 43841	General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 27061 instead.
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘1) / (log‘𝐶)) = 0)
Theorem	reglogexpbas 43842	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 27072 instead.
⊢ ((𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐶↑𝑁)) / (log‘𝐶)) = 𝑁)
21.35.25  Pell equations 4: the positive solution group is infinite cyclic
Theorem	pellfund14 43843*	Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥))
Theorem	pellfund14b 43844*	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‘𝐷)↑𝑥)))
21.35.26  X and Y sequences 1: Definition and recurrence laws
Syntax	crmx 43845	Extend class notation to include the Robertson-Matiyasevich X sequence.
class Xrm
Syntax	crmy 43846	Extend class notation to include the Robertson-Matiyasevich Y sequence.
class Yrm
Definition	df-rmx 43847*	Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 43858 and rmxyval 43860 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 43848*	Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 43859 and rmxyval 43860 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 43849*	Value of the X sequence. Not used after rmxyval 43860 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) = (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))))
Theorem	rmyfval 43850*	Value of the Y sequence. Not used after rmxyval 43860 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) = (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))))
Theorem	rmspecsqrtnq 43851	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 43852	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 43853	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 43854	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 43855*	The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014.) (Proof shortened by SN, 23-Dec-2024.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁) ∈ {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))})
Theorem	rmxypairf1o 43856*	The function used to extract rational and irrational parts in df-rmx 43847 and df-rmy 43848 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 43857*	Lemma for frmx 43858 and frmy 43859. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) ∈ (ℕ0 × ℤ))
Theorem	frmx 43858	The X sequence is a nonnegative integer. See rmxnn 43896 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0
Theorem	frmy 43859	The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
Theorem	rmxyval 43860	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 43861	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 43862*	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 43863	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 43864	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 43865	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 43866	Addition formula for X and Y sequences. See rmxadd 43872 and rmyadd 43876 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 43867	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 43868	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 43869	Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 43865, rmxyadd 43866, rmxy0 43868, and rmxy1 43867 via qirropth 43853 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 43870	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 43871	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 43872	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 43873	Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁))
Theorem	rmy0 43874	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 43875	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 43876	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 43877	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 43878	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 43879	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 43880	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 43881	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 43882	The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 43874 and rmy1 43875. 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 43883	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 43884	"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 43885	"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.35.27  Ordering and induction lemmas for the integers
Theorem	monotuz 43886*	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 43887*	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 43888*	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 43889*	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 43890*	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 43891*	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.35.28  X and Y sequences 2: Order properties
Theorem	rmxypos 43892	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 43893	The Y-sequence is strictly monotonic on ℕ0. Strengthened by ltrmy 43897. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁)))
Theorem	ltrmxnn0 43894	The X-sequence is strictly monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Xrm 𝑀) < (𝐴 Xrm 𝑁)))
Theorem	lermxnn0 43895	The X-sequence is monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝐴 Xrm 𝑀) ≤ (𝐴 Xrm 𝑁)))
Theorem	rmxnn 43896	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 43897	The Y-sequence is strictly monotonic over ℤ. (Contributed by Stefan O'Rear, 25-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁)))
Theorem	rmyeq0 43898	Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0))
Theorem	rmyeq 43899	Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑁)))
Theorem	lermy 43900	Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝐴 Yrm 𝑀) ≤ (𝐴 Yrm 𝑁)))