P. 435 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 43401-43500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pell14qrgapw 43401	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 43402	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.33.23  Pell equations 3: characterizing fundamental solution
Theorem	infmrgelbi 43403*	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 43404*	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 43405*	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 43406	The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ)
Theorem	pellfundge 43407	Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (PellFund‘𝐷))
Theorem	pellfundgt1 43408	Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷))
Theorem	pellfundlb 43409	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 43410*	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 43411	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 43401. (Contributed by Stefan O'Rear, 18-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷))
Theorem	pellfund14gap 43412	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 43413	The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+)
Theorem	pellfundne1 43414	The fundamental Pell solution is never 1. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ≠ 1)
21.33.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 43415	General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 26808 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) → ((log‘𝐴) / (log‘𝐵)) ∈ ℝ)
Theorem	reglogltb 43416	General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 26819 instead.
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 < 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) < ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogleb 43417	General logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 26818 instead.
⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) ≤ ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogmul 43418	Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 26812 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴 · 𝐵)) / (log‘𝐶)) = (((log‘𝐴) / (log‘𝐶)) + ((log‘𝐵) / (log‘𝐶))))
Theorem	reglogexp 43419	Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 26811 instead.
⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴↑𝑁)) / (log‘𝐶)) = (𝑁 · ((log‘𝐴) / (log‘𝐶))))
Theorem	reglogbas 43420	General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 26803 instead.
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘𝐶) / (log‘𝐶)) = 1)
Theorem	reglog1 43421	General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 26804 instead.
⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘1) / (log‘𝐶)) = 0)
Theorem	reglogexpbas 43422	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 26815 instead.
⊢ ((𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐶↑𝑁)) / (log‘𝐶)) = 𝑁)
21.33.25  Pell equations 4: the positive solution group is infinite cyclic
Theorem	pellfund14 43423*	Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥))
Theorem	pellfund14b 43424*	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.33.26  X and Y sequences 1: Definition and recurrence laws
Syntax	crmx 43425	Extend class notation to include the Robertson-Matiyasevich X sequence.
class Xrm
Syntax	crmy 43426	Extend class notation to include the Robertson-Matiyasevich Y sequence.
class Yrm
Definition	df-rmx 43427*	Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 43438 and rmxyval 43440 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 43428*	Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 43439 and rmxyval 43440 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 43429*	Value of the X sequence. Not used after rmxyval 43440 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) = (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))))
Theorem	rmyfval 43430*	Value of the Y sequence. Not used after rmxyval 43440 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) = (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁))))
Theorem	rmspecsqrtnq 43431	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 43432	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 43433	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 43434	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 43435*	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 43436*	The function used to extract rational and irrational parts in df-rmx 43427 and df-rmy 43428 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 43437*	Lemma for frmx 43438 and frmy 43439. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) ∈ (ℕ0 × ℤ))
Theorem	frmx 43438	The X sequence is a nonnegative integer. See rmxnn 43476 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0
Theorem	frmy 43439	The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ
Theorem	rmxyval 43440	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 43441	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 43442*	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 43443	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 43444	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 43445	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 43446	Addition formula for X and Y sequences. See rmxadd 43452 and rmyadd 43456 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 43447	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 43448	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 43449	Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 43445, rmxyadd 43446, rmxy0 43448, and rmxy1 43447 via qirropth 43433 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 43450	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 43451	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 43452	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 43453	Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁))
Theorem	rmy0 43454	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 43455	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 43456	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 43457	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 43458	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 43459	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 43460	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 43461	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 43462	The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 43454 and rmy1 43455. 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 43463	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 43464	"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 43465	"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 43466*	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 43467*	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 43468*	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 43469*	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 43470*	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 43471*	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 43472	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 43473	The Y-sequence is strictly monotonic on ℕ0. Strengthened by ltrmy 43477. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁)))
Theorem	ltrmxnn0 43474	The X-sequence is strictly monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 < 𝑁 ↔ (𝐴 Xrm 𝑀) < (𝐴 Xrm 𝑁)))
Theorem	lermxnn0 43475	The X-sequence is monotonic on ℕ0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ≤ 𝑁 ↔ (𝐴 Xrm 𝑀) ≤ (𝐴 Xrm 𝑁)))
Theorem	rmxnn 43476	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 43477	The Y-sequence is strictly monotonic over ℤ. (Contributed by Stefan O'Rear, 25-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝐴 Yrm 𝑀) < (𝐴 Yrm 𝑁)))
Theorem	rmyeq0 43478	Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ↔ (𝐴 Yrm 𝑁) = 0))
Theorem	rmyeq 43479	Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 = 𝑁 ↔ (𝐴 Yrm 𝑀) = (𝐴 Yrm 𝑁)))
Theorem	lermy 43480	Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ≤ 𝑁 ↔ (𝐴 Yrm 𝑀) ≤ (𝐴 Yrm 𝑁)))
Theorem	rmynn 43481	Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ) → (𝐴 Yrm 𝑁) ∈ ℕ)
Theorem	rmynn0 43482	Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 Yrm 𝑁) ∈ ℕ0)
Theorem	rmyabs 43483	Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (abs‘(𝐴 Yrm 𝐵)) = (𝐴 Yrm (abs‘𝐵)))
Theorem	jm2.24nn 43484	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 43485	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 43486	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 43487	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 43488	Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ℤ. Could be eliminated with a more careful proof of jm2.26lem3 43526. (Contributed by Stefan O'Rear, 3-Oct-2014.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Yrm (𝑁 − 1)) + (𝐴 Yrm 𝑁)) < (𝐴 Xrm 𝑁))
Theorem	rmygeid 43489	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 43490	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 43491	If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 + 𝐷) − (𝐶 + 𝐸)))
Theorem	congmul 43492	If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 · 𝐷) − (𝐶 · 𝐸)))
Theorem	congsym 43493	Congruence mod 𝐴 is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (𝐶 − 𝐵))
Theorem	congneg 43494	If two integers are congruent mod 𝐴, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ (𝐵 − 𝐶))) → 𝐴 ∥ (-𝐵 − -𝐶))
Theorem	congsub 43495	If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝐷 ∈ ℤ ∧ 𝐸 ∈ ℤ) ∧ (𝐴 ∥ (𝐵 − 𝐶) ∧ 𝐴 ∥ (𝐷 − 𝐸))) → 𝐴 ∥ ((𝐵 − 𝐷) − (𝐶 − 𝐸)))
Theorem	congid 43496	Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐵 − 𝐵))
Theorem	mzpcong 43497*	Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.)
⊢ ((𝐹 ∈ (mzPoly‘𝑉) ∧ (𝑋 ∈ (ℤ ↑m 𝑉) ∧ 𝑌 ∈ (ℤ ↑m 𝑉)) ∧ (𝑁 ∈ ℤ ∧ ∀𝑘 ∈ 𝑉 𝑁 ∥ ((𝑋‘𝑘) − (𝑌‘𝑘)))) → 𝑁 ∥ ((𝐹‘𝑋) − (𝐹‘𝑌)))
Theorem	congrep 43498*	Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝑁 ∈ ℤ) → ∃𝑎 ∈ (0...(𝐴 − 1))𝐴 ∥ (𝑎 − 𝑁))
Theorem	congabseq 43499	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 43500	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.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ (𝐵 − 𝐵) ∨ 𝐴 ∥ (𝐵 − -𝐵)))