P. 353 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35201-35300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rmxneg 35201	Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 35197, rmxyadd 35198, rmxy0 35200, and rmxy1 35199 via qirropth 35185 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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm -u N ) = ( A Xrm N ) )
Theorem	rmx0 35202	Value of X sequence at 0. Part 1 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Xrm 0 ) = 1 )
Theorem	rmx1 35203	Value of X sequence at 1. Part 2 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Xrm 1 ) = A )
Theorem	rmxadd 35204	Addition formula for X sequence. Equation 2.7 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A Xrm ( M + N ) ) = ( ( ( A Xrm M ) x. ( A Xrm N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A Yrm M ) x. ( A Yrm N ) ) ) ) )
Theorem	rmyneg 35205	Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm -u N ) = -u ( A Yrm N ) )
Theorem	rmy0 35206	Value of Y sequence at 0. Part 1 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Yrm 0 ) = 0 )
Theorem	rmy1 35207	Value of Y sequence at 1. Part 2 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Yrm 1 ) = 1 )
Theorem	rmyadd 35208	Addition formula for Y sequence. Equation 2.8 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A Yrm ( M + N ) ) = ( ( ( A Yrm M ) x. ( A Xrm N ) ) + ( ( A Xrm M ) x. ( A Yrm N ) ) ) )
Theorem	rmxp1 35209	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( N + 1 ) ) = ( ( ( A Xrm N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A Yrm N ) ) ) )
Theorem	rmyp1 35210	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N + 1 ) ) = ( ( ( A Yrm N ) x. A ) + ( A Xrm N ) ) )
Theorem	rmxm1 35211	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( N - 1 ) ) = ( ( A x. ( A Xrm N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A Yrm N ) ) ) )
Theorem	rmym1 35212	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N - 1 ) ) = ( ( ( A Yrm N ) x. A ) - ( A Xrm N ) ) )
Theorem	rmxluc 35213	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( N + 1 ) ) = ( ( ( 2 x. A ) x. ( A Xrm N ) ) - ( A Xrm ( N - 1 ) ) ) )
Theorem	rmyluc 35214	The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 35206 and rmy1 35207. Part 3 of equation 2.12 of [JonesMatijasevic] p. 695. JonesMatijasevic uses this theorem to redefine the X and Y sequences to have domain ( ZZ X. ZZ ), 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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N + 1 ) ) = ( ( 2 x. ( ( A Yrm N ) x. A ) ) - ( A Yrm ( N - 1 ) ) ) )
Theorem	rmyluc2 35215	Lucas sequence property of Y with better output ordering. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N + 1 ) ) = ( ( ( 2 x. A ) x. ( A Yrm N ) ) - ( A Yrm ( N - 1 ) ) ) )
Theorem	rmxdbl 35216	"Double-angle formula" for X-values. Equation 2.13 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( 2 x. N ) ) = ( ( 2 x. ( ( A Xrm N ) ^ 2 ) ) - 1 ) )
Theorem	rmydbl 35217	"Double-angle formula" for Y-values. Equation 2.14 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( 2 x. N ) ) = ( ( 2 x. ( A Xrm N ) ) x. ( A Yrm N ) ) )
21.23.28  Ordering and induction lemmas for the integers
Theorem	monotuz 35218*	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.)
|- ( ( ph /\ y e. H ) -> F < G )   &    |- ( ( ph /\ x e. H ) -> C e. RR )   &    |- H = ( ZZ>= ` I )   &    |- ( x = ( y + 1 ) -> C = G )   &    |- ( x = y -> C = F )   &    |- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( ph /\ ( A e. H /\ B e. H ) ) -> ( A < B <-> D < E ) )
Theorem	monotoddzzfi 35219*	A function which is odd and monotonic on NN0 is monotonic on ZZ. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.)
|- ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR )   &    |- ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) )   &    |- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) )   =>    |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )
Theorem	monotoddzz 35220*	A function (given implicitly) which is odd and monotonic on NN0 is monotonic on ZZ. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.)
|- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> E < F ) )   &    |- ( ( ph /\ x e. ZZ ) -> E e. RR )   &    |- ( ( ph /\ y e. ZZ ) -> G = -u F )   &    |- ( x = A -> E = C )   &    |- ( x = B -> E = D )   &    |- ( x = y -> E = F )   &    |- ( x = -u y -> E = G )   =>    |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> C < D ) )
Theorem	oddcomabszz 35221*	An odd function which takes nonnegative values on nonnegative arguments commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( ph /\ x e. ZZ ) -> A e. RR )   &    |- ( ( ph /\ x e. ZZ /\ 0 <_ x ) -> 0 <_ A )   &    |- ( ( ph /\ y e. ZZ ) -> C = -u B )   &    |- ( x = y -> A = B )   &    |- ( x = -u y -> A = C )   &    |- ( x = D -> A = E )   &    |- ( x = ( abs ` D ) -> A = F )   =>    |- ( ( ph /\ D e. ZZ ) -> ( abs ` E ) = F )
Theorem	2nn0ind 35222*	Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ps   &    |- ch   &    |- ( y e. NN -> ( ( th /\ ta ) -> et ) )   &    |- ( x = 0 -> ( ph <-> ps ) )   &    |- ( x = 1 -> ( ph <-> ch ) )   &    |- ( x = ( y - 1 ) -> ( ph <-> th ) )   &    |- ( x = y -> ( ph <-> ta ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> et ) )   &    |- ( x = A -> ( ph <-> rh ) )   =>    |- ( A e. NN0 -> rh )
Theorem	zindbi 35223*	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.)
|- ( y e. ZZ -> ( ps <-> ch ) )   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> ch ) )   &    |- ( x = 0 -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   =>    |- ( A e. ZZ -> ( th <-> ta ) )
Theorem	expmordi 35224	Mantissa ordering relationship for exponentiation. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) /\ N e. NN ) -> ( A ^ N ) < ( B ^ N ) )
Theorem	rpexpmord 35225	Mantissa ordering relationship for exponentiation of positive reals. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( N e. NN /\ A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) )
21.23.29  X and Y sequences 2: Order properties
Theorem	rmxypos 35226	For all nonnegative indices, X is positive and Y is nonnegative. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( 0 < ( A Xrm N ) /\ 0 <_ ( A Yrm N ) ) )
Theorem	ltrmynn0 35227	The Y-sequence is strictly monotonic on NN0. Strengthened by ltrmy 35231. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( A Yrm M ) < ( A Yrm N ) ) )
Theorem	ltrmxnn0 35228	The X-sequence is strictly monotonic on NN0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( A Xrm M ) < ( A Xrm N ) ) )
Theorem	lermxnn0 35229	The X-sequence is monotonic on NN0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( A Xrm M ) <_ ( A Xrm N ) ) )
Theorem	rmxnn 35230	The X-sequence is defined to range over NN0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm N ) e. NN )
Theorem	ltrmy 35231	The Y-sequence is strictly monotonic over ZZ. (Contributed by Stefan O'Rear, 25-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( A Yrm M ) < ( A Yrm N ) ) )
Theorem	rmyeq0 35232	Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N = 0 <-> ( A Yrm N ) = 0 ) )
Theorem	rmyeq 35233	Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M = N <-> ( A Yrm M ) = ( A Yrm N ) ) )
Theorem	lermy 35234	Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( A Yrm M ) <_ ( A Yrm N ) ) )
Theorem	rmynn 35235	Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A Yrm N ) e. NN )
Theorem	rmynn0 35236	Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A Yrm N ) e. NN0 )
Theorem	rmyabs 35237	Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( abs ` ( A Yrm B ) ) = ( A Yrm ( abs ` B ) ) )
Theorem	jm2.24nn 35238	X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of [JonesMatijasevic] p. 697 restricted to NN. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) < ( A Xrm N ) )
Theorem	jm2.17a 35239	First half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 14-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( ( 2 x. A ) - 1 ) ^ N ) <_ ( A Yrm ( N + 1 ) ) )
Theorem	jm2.17b 35240	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A Yrm ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) )
Theorem	jm2.17c 35241	Second half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 15-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A Yrm ( ( N + 1 ) + 1 ) ) < ( ( 2 x. A ) ^ ( N + 1 ) ) )
Theorem	jm2.24 35242	Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ZZ. Could be eliminated with a more careful proof of jm2.26lem3 35285. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) < ( A Xrm N ) )
Theorem	rmygeid 35243	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N <_ ( A Yrm N ) )
21.23.30  Congruential equations
Theorem	congtr 35244	A wff of the form A || ( B - C ) is interpreted as a congruential equation. This is similar to ( B mod A ) = ( C mod A ), but is defined such that behavior is regular for zero and negative values of A. 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.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( B - D ) )
Theorem	congadd 35245	If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B + D ) - ( C + E ) ) )
Theorem	congmul 35246	If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B x. D ) - ( C x. E ) ) )
Theorem	congsym 35247	Congruence mod A is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( C - B ) )
Theorem	congneg 35248	If two integers are congruent mod A, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( -u B - -u C ) )
Theorem	congsub 35249	If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B - D ) - ( C - E ) ) )
Theorem	congid 35250	Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> A || ( B - B ) )
Theorem	mzpcong 35251*	Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( F e. (mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) -> N || ( ( F ` X ) - ( F ` Y ) ) )
Theorem	congrep 35252*	Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... ( A - 1 ) ) A || ( a - N ) )
Theorem	congabseq 35253	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.)
|- ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) -> ( ( abs ` ( B - C ) ) < A <-> B = C ) )
21.23.31  Alternating congruential equations
Theorem	acongid 35254	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.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A || ( B - B ) \/ A || ( B - -u B ) ) )
Theorem	acongsym 35255	Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( A || ( B - C ) \/ A || ( B - -u C ) ) ) -> ( A || ( C - B ) \/ A || ( C - -u B ) ) )
Theorem	acongneg2 35256	Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( A || ( B - -u C ) \/ A || ( B - -u -u C ) ) ) -> ( A || ( B - C ) \/ A || ( B - -u C ) ) )
Theorem	acongtr 35257	Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( ( A || ( B - C ) \/ A || ( B - -u C ) ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) )
Theorem	acongeq12d 35258	Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ph -> B = C )   &    |- ( ph -> D = E )   =>    |- ( ph -> ( ( A || ( B - D ) \/ A || ( B - -u D ) ) <-> ( A || ( C - E ) \/ A || ( C - -u E ) ) ) )
Theorem	acongrep 35259*	Every integer is alternating-congruent to some number in the first half of the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
Theorem	fzmaxdif 35260	Bound on the difference between two integers constrained to two possibly overlapping finite ranges. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( ( C e. ZZ /\ A e. ( B ... C ) ) /\ ( F e. ZZ /\ D e. ( E ... F ) ) /\ ( C - E ) <_ ( F - B ) ) -> ( abs ` ( A - D ) ) <_ ( F - B ) )
Theorem	fzneg 35261	Reflection of a finite range of integers about 0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A e. ( B ... C ) <-> -u A e. ( -u C ... -u B ) ) )
Theorem	acongeq 35262	Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 35286 (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. NN /\ B e. ( 0 ... A ) /\ C e. ( 0 ... A ) ) -> ( B = C <-> ( ( 2 x. A ) || ( B - C ) \/ ( 2 x. A ) || ( B - -u C ) ) ) )
Theorem	dvdsacongtr 35263	Alternating congruence passes from a base to a dividing base. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( D || A /\ ( A || ( B - C ) \/ A || ( B - -u C ) ) ) ) -> ( D || ( B - C ) \/ D || ( B - -u C ) ) )
21.23.32  Additional theorems on integer divisibility
Theorem	bezoutr 35264	Partial converse to bezout 14387. Existence of a linear combination does not set the GCD, but it does upper bound it. (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( A gcd B ) || ( ( A x. X ) + ( B x. Y ) ) )
Theorem	bezoutr1 35265	Converse of bezout 14387 for the gcd = 1 case, sufficient condition for relative primality. (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( X e. ZZ /\ Y e. ZZ ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = 1 -> ( A gcd B ) = 1 ) )
Theorem	coprmdvdsb 35266	Multiplication by a coprime number does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( K e. ZZ /\ N e. ZZ /\ ( M e. ZZ /\ ( K gcd M ) = 1 ) ) -> ( K || N <-> K || ( M x. N ) ) )
Theorem	dvdsleabs2 35267	Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N -> ( abs ` M ) <_ ( abs ` N ) ) )
Theorem	modabsdifz 35268	Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. ZZ )
Theorem	dvdsabsmod0 35269	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.)
|- ( ( M e. ZZ /\ N e. ZZ /\ M =/= 0 ) -> ( M || N <-> ( N mod ( abs ` M ) ) = 0 ) )
Theorem	dvdsabsmod0OLD 35270	Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 24-Sep-2014.) Obsolete version of dvdsabsmod0 35269 as of 3-Jul-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( M e. ZZ /\ N e. ZZ /\ M =/= 0 ) -> ( M || N <-> ( N mod ( abs ` M ) ) = 0 ) )
Theorem	divalgmodcl 35271	divalgmod 14271 using a class variable. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- ( ( N e. ZZ /\ D e. NN /\ R e. NN0 ) -> ( R = ( N mod D ) <-> ( R < D /\ D || ( N - R ) ) ) )
21.23.33  X and Y sequences 3: Divisibility properties
Theorem	jm2.18 35272	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ K e. NN0 /\ N e. NN0 ) -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) || ( ( ( A Xrm N ) - ( ( A - K ) x. ( A Yrm N ) ) ) - ( K ^ N ) ) )
Theorem	jm2.19lem1 35273	Lemma for jm2.19 35277. X and Y values are coprime. (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( ( A Xrm M ) gcd ( A Yrm M ) ) = 1 )
Theorem	jm2.19lem2 35274	Lemma for jm2.19 35277. (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A Yrm M ) || ( A Yrm N ) <-> ( A Yrm M ) || ( A Yrm ( N + M ) ) ) )
Theorem	jm2.19lem3 35275	Lemma for jm2.19 35277. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. NN0 ) -> ( ( A Yrm M ) || ( A Yrm N ) <-> ( A Yrm M ) || ( A Yrm ( N + ( I x. M ) ) ) ) )
Theorem	jm2.19lem4 35276	Lemma for jm2.19 35277. Extend to ZZ by symmetry. TODO: use zindbi 35223. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. ZZ ) -> ( ( A Yrm M ) || ( A Yrm N ) <-> ( A Yrm M ) || ( A Yrm ( N + ( I x. M ) ) ) ) )
Theorem	jm2.19 35277	Lemma 2.19 of [JonesMatijasevic] p. 696. Transfer divisibility constraints between Y-values and their indices. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( A Yrm M ) || ( A Yrm N ) ) )
Theorem	jm2.21 35278	Lemma for jm2.20nn 35281. Express X and Y values as a binomial. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. ZZ ) -> ( ( A Xrm ( N x. J ) ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm ( N x. J ) ) ) ) = ( ( ( A Xrm N ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ) ^ J ) )
Theorem	jm2.22 35279*	Lemma for jm2.20nn 35281. Applying binomial theorem and taking irrational part. (Contributed by Stefan O'Rear, 26-Sep-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN0 ) -> ( A Yrm ( N x. J ) ) = sum_ i e. { x e. ( 0 ... J ) | -. 2 || x } ( ( J _C i ) x. ( ( ( A Xrm N ) ^ ( J - i ) ) x. ( ( ( A Yrm N ) ^ i ) x. ( ( ( A ^ 2 ) - 1 ) ^ ( ( i - 1 ) / 2 ) ) ) ) ) )
Theorem	jm2.23 35280	Lemma for jm2.20nn 35281. Truncate binomial expansion p-adicly. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ J e. NN ) -> ( ( A Yrm N ) ^ 3 ) || ( ( A Yrm ( N x. J ) ) - ( J x. ( ( ( A Xrm N ) ^ ( J - 1 ) ) x. ( A Yrm N ) ) ) ) )
Theorem	jm2.20nn 35281	Lemma 2.20 of [JonesMatijasevic] p. 696, the "first step down lemma". (Contributed by Stefan O'Rear, 27-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN /\ N e. NN ) -> ( ( ( A Yrm N ) ^ 2 ) || ( A Yrm M ) <-> ( N x. ( A Yrm N ) ) || M ) )
Theorem	jm2.25lem1 35282	Lemma for jm2.26 35286. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) -> ( ( A || ( D - B ) \/ A || ( D - -u B ) ) <-> ( A || ( C - B ) \/ A || ( C - -u B ) ) ) )
Theorem	jm2.25 35283	Lemma for jm2.26 35286. Remainders mod X(2n) are negaperiodic mod 2n. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ ( M e. ZZ /\ N e. ZZ ) /\ I e. ZZ ) -> ( ( A Xrm N ) || ( ( A Yrm ( M + ( I x. ( 2 x. N ) ) ) ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm ( M + ( I x. ( 2 x. N ) ) ) ) - -u ( A Yrm M ) ) ) )
Theorem	jm2.26a 35284	Lemma for jm2.26 35286. Reverse direction is required to prove forward direction, so do it separatly. Induction on difference between K and M, together with the addition formula fact that adding 2N only inverts sign. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) -> ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) )
Theorem	jm2.26lem3 35285	Lemma for jm2.26 35286. Use acongrep 35259 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.)
|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ( 0 ... N ) /\ M e. ( 0 ... N ) ) /\ ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) ) -> K = M )
Theorem	jm2.26 35286	Lemma 2.26 of [JonesMatijasevic] p. 697, the "second step down lemma". (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K e. ZZ /\ M e. ZZ ) ) -> ( ( ( A Xrm N ) || ( ( A Yrm K ) - ( A Yrm M ) ) \/ ( A Xrm N ) || ( ( A Yrm K ) - -u ( A Yrm M ) ) ) <-> ( ( 2 x. N ) || ( K - M ) \/ ( 2 x. N ) || ( K - -u M ) ) ) )
Theorem	jm2.15nn0 35287	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A - B ) || ( ( A Yrm N ) - ( B Yrm N ) ) )
Theorem	jm2.16nn0 35288	Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 35287 if Yrm is redefined as described in rmyluc 35214. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A - 1 ) || ( ( A Yrm N ) - N ) )
21.23.34  X and Y sequences 4: Diophantine representability of Y
Theorem	jm2.27a 35289	Lemma for jm2.27 35292. Reverse direction after existential quantifiers are expanded. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ph -> A e. ( ZZ>= ` 2 ) )   &    |- ( ph -> B e. NN )   &    |- ( ph -> C e. NN )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> E e. NN0 )   &    |- ( ph -> F e. NN0 )   &    |- ( ph -> G e. NN0 )   &    |- ( ph -> H e. NN0 )   &    |- ( ph -> I e. NN0 )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )   &    |- ( ph -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )   &    |- ( ph -> G e. ( ZZ>= ` 2 ) )   &    |- ( ph -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )   &    |- ( ph -> E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )   &    |- ( ph -> F || ( G - A ) )   &    |- ( ph -> ( 2 x. C ) || ( G - 1 ) )   &    |- ( ph -> F || ( H - C ) )   &    |- ( ph -> ( 2 x. C ) || ( H - B ) )   &    |- ( ph -> B <_ C )   &    |- ( ph -> P e. ZZ )   &    |- ( ph -> D = ( A Xrm P ) )   &    |- ( ph -> C = ( A Yrm P ) )   &    |- ( ph -> Q e. ZZ )   &    |- ( ph -> F = ( A Xrm Q ) )   &    |- ( ph -> E = ( A Yrm Q ) )   &    |- ( ph -> R e. ZZ )   &    |- ( ph -> I = ( G Xrm R ) )   &    |- ( ph -> H = ( G Yrm R ) )   =>    |- ( ph -> C = ( A Yrm B ) )
Theorem	jm2.27b 35290	Lemma for jm2.27 35292. Expand existential quantifiers for reverse direction. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ph -> A e. ( ZZ>= ` 2 ) )   &    |- ( ph -> B e. NN )   &    |- ( ph -> C e. NN )   &    |- ( ph -> D e. NN0 )   &    |- ( ph -> E e. NN0 )   &    |- ( ph -> F e. NN0 )   &    |- ( ph -> G e. NN0 )   &    |- ( ph -> H e. NN0 )   &    |- ( ph -> I e. NN0 )   &    |- ( ph -> J e. NN0 )   &    |- ( ph -> ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 )   &    |- ( ph -> ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 )   &    |- ( ph -> G e. ( ZZ>= ` 2 ) )   &    |- ( ph -> ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 )   &    |- ( ph -> E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) )   &    |- ( ph -> F || ( G - A ) )   &    |- ( ph -> ( 2 x. C ) || ( G - 1 ) )   &    |- ( ph -> F || ( H - C ) )   &    |- ( ph -> ( 2 x. C ) || ( H - B ) )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> C = ( A Yrm B ) )
Theorem	jm2.27c 35291	Lemma for jm2.27 35292. Forward direction with substitutions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ph -> A e. ( ZZ>= ` 2 ) )   &    |- ( ph -> B e. NN )   &    |- ( ph -> C e. NN )   &    |- ( ph -> C = ( A Yrm B ) )   &    |- D = ( A Xrm B )   &    |- Q = ( B x. ( A Yrm B ) )   &    |- E = ( A Yrm ( 2 x. Q ) )   &    |- F = ( A Xrm ( 2 x. Q ) )   &    |- G = ( A + ( ( F ^ 2 ) x. ( ( F ^ 2 ) - A ) ) )   &    |- H = ( G Yrm B )   &    |- I = ( G Xrm B )   &    |- J = ( ( E / ( 2 x. ( C ^ 2 ) ) ) - 1 )   =>    |- ( ph -> ( ( ( D e. NN0 /\ E e. NN0 /\ F e. NN0 ) /\ ( G e. NN0 /\ H e. NN0 /\ I e. NN0 ) ) /\ ( J e. NN0 /\ ( ( ( ( ( D ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( F ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( E ^ 2 ) ) ) = 1 /\ G e. ( ZZ>= ` 2 ) ) /\ ( ( ( I ^ 2 ) - ( ( ( G ^ 2 ) - 1 ) x. ( H ^ 2 ) ) ) = 1 /\ E = ( ( J + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ F || ( G - A ) ) ) /\ ( ( ( 2 x. C ) || ( G - 1 ) /\ F || ( H - C ) ) /\ ( ( 2 x. C ) || ( H - B ) /\ B <_ C ) ) ) ) ) )
Theorem	jm2.27 35292*	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 35289 and jm2.27c 35291. Once Diophantine relations have been defined, the content of the theorem is "rmY is Diophantine" (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN /\ C e. NN ) -> ( C = ( A Yrm B ) <-> E. d e. NN0 E. e e. NN0 E. f e. NN0 E. g e. NN0 E. h e. NN0 E. i e. NN0 E. j e. NN0 ( ( ( ( ( d ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( C ^ 2 ) ) ) = 1 /\ ( ( f ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( e ^ 2 ) ) ) = 1 /\ g e. ( ZZ>= ` 2 ) ) /\ ( ( ( i ^ 2 ) - ( ( ( g ^ 2 ) - 1 ) x. ( h ^ 2 ) ) ) = 1 /\ e = ( ( j + 1 ) x. ( 2 x. ( C ^ 2 ) ) ) /\ f || ( g - A ) ) ) /\ ( ( ( 2 x. C ) || ( g - 1 ) /\ f || ( h - C ) ) /\ ( ( 2 x. C ) || ( h - B ) /\ B <_ C ) ) ) ) )
Theorem	jm2.27dlem1 35293*	Lemma for rmydioph 35298. Subsitution of a tuple restriction into a projection that doesn't care. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- A e. ( 1 ... B )   =>    |- ( a = ( b |` ( 1 ... B ) ) -> ( a ` A ) = ( b ` A ) )
Theorem	jm2.27dlem2 35294	Lemma for rmydioph 35298. This theorem is used along with the next three to efficiently infer steps like 7 e. ( 1 ... 10 ). (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- A e. ( 1 ... B )   &    |- C = ( B + 1 )   &    |- B e. NN   =>    |- A e. ( 1 ... C )
Theorem	jm2.27dlem3 35295	Lemma for rmydioph 35298. Infer membership of the endpoint of a range. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- A e. NN   =>    |- A e. ( 1 ... A )
Theorem	jm2.27dlem4 35296	Lemma for rmydioph 35298. Infer NN-hood of large numbers. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- A e. NN   &    |- B = ( A + 1 )   =>    |- B e. NN
Theorem	jm2.27dlem5 35297	Lemma for rmydioph 35298. Used with sselii 3438 to infer membership of midpoints of range; jm2.27dlem2 35294 is deprecated. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- B = ( A + 1 )   &    |- ( 1 ... B ) C_ ( 1 ... C )   =>    |- ( 1 ... A ) C_ ( 1 ... C )
Theorem	rmydioph 35298	jm2.27 35292 restated in terms of Diophantine sets. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) Yrm ( a ` 2 ) ) ) } e. (Dioph ` 3 )
21.23.35  X and Y sequences 5: Diophantine representability of X, ^, _C
Theorem	rmxdiophlem 35299*	X can be expressed in terms of Y, so it is also Diophantine. (Contributed by Stefan O'Rear, 15-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 /\ X e. NN0 ) -> ( X = ( A Xrm N ) <-> E. y e. NN0 ( y = ( A Yrm N ) /\ ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( y ^ 2 ) ) ) = 1 ) ) )
Theorem	rmxdioph 35300	X is a Diophantine function. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 3 ) = ( ( a ` 1 ) Xrm ( a ` 2 ) ) ) } e. (Dioph ` 3 )