P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fzmaxdif 35801	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 35802	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 35803	Two numbers in the fundamental domain are alternating-congruent iff they are equal. TODO: could be used to shorten jm2.26 35827 (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 35804	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 35805	Partial converse to bezout 14509. 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 35806	Converse of bezout 14509 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 35807	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 35808	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 35809	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 35810	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 35811	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 35810 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 35812	divalgmod 14386 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 35813	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 35814	Lemma for jm2.19 35818. 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 35815	Lemma for jm2.19 35818. (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 35816	Lemma for jm2.19 35818. (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 35817	Lemma for jm2.19 35818. Extend to ZZ by symmetry. TODO: use zindbi 35764. (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 35818	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 35819	Lemma for jm2.20nn 35822. 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 35820*	Lemma for jm2.20nn 35822. 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 35821	Lemma for jm2.20nn 35822. 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 35822	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 35823	Lemma for jm2.26 35827. (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 35824	Lemma for jm2.26 35827. 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 35825	Lemma for jm2.26 35827. 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 35826	Lemma for jm2.26 35827. Use acongrep 35800 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 35827	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 35828	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 35829	Lemma 2.16 of [JonesMatijasevic] p. 695. This may be regarded as a special case of jm2.15nn0 35828 if Yrm is redefined as described in rmyluc 35755. (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 35830	Lemma for jm2.27 35833. 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 35831	Lemma for jm2.27 35833. 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 35832	Lemma for jm2.27 35833. 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 35833*	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 35830 and jm2.27c 35832. 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 35834*	Lemma for rmydioph 35839. 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 35835	Lemma for rmydioph 35839. 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 35836	Lemma for rmydioph 35839. 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 35837	Lemma for rmydioph 35839. 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 35838	Lemma for rmydioph 35839. Used with sselii 3461 to infer membership of midpoints of range; jm2.27dlem2 35835 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 35839	jm2.27 35833 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 35840*	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 35841	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 )
Theorem	jm3.1lem1 35842	Lemma for jm3.1 35845. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ph -> A e. ( ZZ>= ` 2 ) )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( K Yrm ( N + 1 ) ) <_ A )   =>    |- ( ph -> ( K ^ N ) < A )
Theorem	jm3.1lem2 35843	Lemma for jm3.1 35845. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ph -> A e. ( ZZ>= ` 2 ) )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( K Yrm ( N + 1 ) ) <_ A )   =>    |- ( ph -> ( K ^ N ) < ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) )
Theorem	jm3.1lem3 35844	Lemma for jm3.1 35845. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- ( ph -> A e. ( ZZ>= ` 2 ) )   &    |- ( ph -> K e. ( ZZ>= ` 2 ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> ( K Yrm ( N + 1 ) ) <_ A )   =>    |- ( ph -> ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) e. NN )
Theorem	jm3.1 35845	Diophantine expression for exponentiation. Lemma 3.1 of [JonesMatijasevic] p. 698. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( ( A e. ( ZZ>= ` 2 ) /\ K e. ( ZZ>= ` 2 ) /\ N e. NN ) /\ ( K Yrm ( N + 1 ) ) <_ A ) -> ( K ^ N ) = ( ( ( A Xrm N ) - ( ( A - K ) x. ( A Yrm N ) ) ) mod ( ( ( ( 2 x. A ) x. K ) - ( K ^ 2 ) ) - 1 ) ) )
Theorem	expdiophlem1 35846*	Lemma for expdioph 35848. Fully expanded expression for exponential. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- ( C e. NN0 -> ( ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN ) /\ C = ( A ^ B ) ) <-> E. d e. NN0 E. e e. NN0 E. f e. NN0 ( ( A e. ( ZZ>= ` 2 ) /\ B e. NN ) /\ ( ( A e. ( ZZ>= ` 2 ) /\ d = ( A Yrm ( B + 1 ) ) ) /\ ( ( d e. ( ZZ>= ` 2 ) /\ e = ( d Yrm B ) ) /\ ( ( d e. ( ZZ>= ` 2 ) /\ f = ( d Xrm B ) ) /\ ( C < ( ( ( ( 2 x. d ) x. A ) - ( A ^ 2 ) ) - 1 ) /\ ( ( ( ( 2 x. d ) x. A ) - ( A ^ 2 ) ) - 1 ) || ( ( f - ( ( d - A ) x. e ) ) - C ) ) ) ) ) ) ) )
Theorem	expdiophlem2 35847	Lemma for expdioph 35848. Exponentiation on a restricted domain is Diophantine. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( ( ( a ` 1 ) e. ( ZZ>= ` 2 ) /\ ( a ` 2 ) e. NN ) /\ ( a ` 3 ) = ( ( a ` 1 ) ^ ( a ` 2 ) ) ) } e. (Dioph ` 3 )
Theorem	expdioph 35848	The exponential function is Diophantine. This result completes and encapsulates our development using Pell equation solution sequences and is sometimes regarded as Matiyasevich's theorem properly. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- { a e. ( NN0 ^m ( 1 ... 3 ) ) | ( a ` 3 ) = ( ( a ` 1 ) ^ ( a ` 2 ) ) } e. (Dioph ` 3 )
21.23.36  Uncategorized stuff not associated with a major project
Theorem	setindtr 35849*	Epsilon induction for sets contained in a transitive set. If we are allowed to assume Infinity, then all sets have a transitive closure and this reduces to setind 8226; however, this version is useful without Infinity. (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( A. x ( x C_ A -> x e. A ) -> ( E. y ( Tr y /\ B e. y ) -> B e. A ) )
Theorem	setindtrs 35850*	Epsilon induction scheme without Infinity. See comments at setindtr 35849. (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( A. y e. x ps -> ph )   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ( x = B -> ( ph <-> ch ) )   =>    |- ( E. z ( Tr z /\ B e. z ) -> ch )
Theorem	dford3lem1 35851*	Lemma for dford3 35853. (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( ( Tr N /\ A. y e. N Tr y ) -> A. b e. N ( Tr b /\ A. y e. b Tr y ) )
Theorem	dford3lem2 35852*	Lemma for dford3 35853. (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( ( Tr x /\ A. y e. x Tr y ) -> x e. On )
Theorem	dford3 35853*	Ordinals are precisely the hereditarily transitive classes. (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( Ord N <-> ( Tr N /\ A. x e. N Tr x ) )
Theorem	dford4 35854*	dford3 35853 expressed in primitives to demonstrate shortness. (Contributed by Stefan O'Rear, 28-Oct-2014.)
|- ( Ord N <-> A. a A. b A. c ( ( a e. N /\ b e. a ) -> ( b e. N /\ ( c e. b -> c e. a ) ) ) )
Theorem	wopprc 35855	Unrelated: Wiener pairs treat proper classes symmetrically. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( A e. _V /\ B e. _V ) <-> -. 1o e. { { { A } , (/) } , { { B } } } )
Theorem	rpnnen3lem 35856*	Lemma for rpnnen3 35857. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( ( ( a e. RR /\ b e. RR ) /\ a < b ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )
Theorem	rpnnen3 35857	Dedekind cut injection of RR into ~P QQ. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- RR ~<_ ~P QQ
21.23.37  More equivalents of the Axiom of Choice
Theorem	axac10 35858	Characterization of choice similar to dffin1-5 8825. (Contributed by Stefan O'Rear, 6-Jan-2015.)
|- ( ~~ " On ) = _V
Theorem	harinf 35859	The Hartogs number of an infinite set is at least om. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
|- ( ( S e. V /\ -. S e. Fin ) -> om C_ (har ` S ) )
Theorem	wdom2d2 35860*	Deduction for weak dominance by a Cartesian product. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ( ph /\ x e. A ) -> E. y e. B E. z e. C x = X )   =>    |- ( ph -> A ~<_* ( B X. C ) )
Theorem	ttac 35861	Tarski's theorem about choice: infxpidm 8994 is equivalent to ax-ac 8896. (Contributed by Stefan O'Rear, 4-Nov-2014.) (Proof shortened by Stefan O'Rear, 10-Jul-2015.)
|- (CHOICE <-> A. c ( om ~<_ c -> ( c X. c ) ~~ c ) )
Theorem	pw2f1ocnv 35862*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 7688, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 9-Jul-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( A e. V -> ( F : ( 2o ^m A ) -1-1-onto-> ~P A /\ `' F = ( y e. ~P A |-> ( z e. A |-> if ( z e. y , 1o , (/) ) ) ) ) )
Theorem	pw2f1o2 35863*	Define a bijection between characteristic functions and subsets. EDITORIAL: extracted from pw2en 7688, which can be easily reproved in terms of this. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( A e. V -> F : ( 2o ^m A ) -1-1-onto-> ~P A )
Theorem	pw2f1o2val 35864*	Function value of the pw2f1o2 35863 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( X e. ( 2o ^m A ) -> ( F ` X ) = ( `' X " { 1o } ) )
Theorem	pw2f1o2val2 35865*	Membership in a mapped set under the pw2f1o2 35863 bijection. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Stefan O'Rear, 6-May-2015.)
|- F = ( x e. ( 2o ^m A ) |-> ( `' x " { 1o } ) )   =>    |- ( ( X e. ( 2o ^m A ) /\ Y e. A ) -> ( Y e. ( F ` X ) <-> ( X ` Y ) = 1o ) )
Theorem	soeq12d 35866	Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( ph -> R = S )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( R Or A <-> S Or B ) )
Theorem	freq12d 35867	Equality deduction for founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( ph -> R = S )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( R Fr A <-> S Fr B ) )
Theorem	weeq12d 35868	Equality deduction for well-orders. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( ph -> R = S )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( R We A <-> S We B ) )
Theorem	limsuc2 35869	Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- ( ( Ord A /\ A = U. A ) -> ( B e. A <-> suc B e. A ) )
Theorem	wepwsolem 35870*	Transfer an ordering on characteristic functions by isomorphism to the power set. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- T = { <. x , y >. | E. z e. A ( ( z e. y /\ -. z e. x ) /\ A. w e. A ( w R z -> ( w e. x <-> w e. y ) ) ) }   &    |- U = { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }   &    |- F = ( a e. ( 2o ^m A ) |-> ( `' a " { 1o } ) )   =>    |- ( A e. _V -> F Isom U , T ( ( 2o ^m A ) , ~P A ) )
Theorem	wepwso 35871*	A well-ordering induces a strict ordering on the power set. EDITORIAL: when well-orderings are set like, this can be strengthened to remove A e. V. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- T = { <. x , y >. | E. z e. A ( ( z e. y /\ -. z e. x ) /\ A. w e. A ( w R z -> ( w e. x <-> w e. y ) ) ) }   =>    |- ( ( A e. V /\ R We A ) -> T Or ~P A )
Theorem	dnnumch1 35872*	Define an enumeration of a set from a choice function; second part, it restricts to a bijection. EDITORIAL: overlaps dfac8a 8468 (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ph -> E. x e. On ( F |` x ) : x -1-1-onto-> A )
Theorem	dnnumch2 35873*	Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ph -> A C_ ran F )
Theorem	dnnumch3lem 35874*	Value of the ordinal injection function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ( ph /\ w e. A ) -> ( ( x e. A |-> |^| ( `' F " { x } ) ) ` w ) = |^| ( `' F " { w } ) )
Theorem	dnnumch3 35875*	Define an injection from a set into the ordinals using a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   =>    |- ( ph -> ( x e. A |-> |^| ( `' F " { x } ) ) : A -1-1-> On )
Theorem	dnwech 35876*	Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )   &    |- H = { <. v , w >. | |^| ( `' F " { v } ) e. |^| ( `' F " { w } ) }   =>    |- ( ph -> H We A )
Theorem	fnwe2val 35877*	Lemma for fnwe2 35881. Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   =>    |- ( a T b <-> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )
Theorem	fnwe2lem1 35878*	Lemma for fnwe2 35881. Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   =>    |- ( ( ph /\ a e. A ) -> [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } )
Theorem	fnwe2lem2 35879*	Lemma for fnwe2 35881. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus T is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   &    |- ( ph -> ( F |` A ) : A --> B )   &    |- ( ph -> R We B )   &    |- ( ph -> a C_ A )   &    |- ( ph -> a =/= (/) )   =>    |- ( ph -> E. b e. a A. c e. a -. c T b )
Theorem	fnwe2lem3 35880*	Lemma for fnwe2 35881. Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   &    |- ( ph -> ( F |` A ) : A --> B )   &    |- ( ph -> R We B )   &    |- ( ph -> a e. A )   &    |- ( ph -> b e. A )   =>    |- ( ph -> ( a T b \/ a = b \/ b T a ) )
Theorem	fnwe2 35881*	A well-ordering can be constructed on a partitioned set by patching together well-orderings on each partition using a well-ordering on the partitions themselves. Similar to fnwe 6923 but does not require the within-partition ordering to be globally well. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- ( z = ( F ` x ) -> S = U )   &    |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }   &    |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )   &    |- ( ph -> ( F |` A ) : A --> B )   &    |- ( ph -> R We B )   =>    |- ( ph -> T We A )
Theorem	aomclem1 35882*	Lemma for dfac11 35890. This is the beginning of the proof that multiple choice is equivalent to choice. Our goal is to construct, by transfinite recursion, a well-ordering of ( R1 ` A ). In what follows, A is the index of the rank we wish to well-order, z is the collection of well-orderings constructed so far, dom z is the set of ordinal indexes of constructed ranks i.e. the next rank to construct, and y is a postulated multiple-choice function. Successor case 1, define a simple ordering from the well-ordered predecessor. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = suc U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   =>    |- ( ph -> B Or ( R1 ` dom z ) )
Theorem	aomclem2 35883*	Lemma for dfac11 35890. Successor case 2, a choice function for subsets of ( R1 ` dom z ). (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = suc U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> dom z C_ A )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> A. a e. ~P ( R1 ` dom z ) ( a =/= (/) -> ( C ` a ) e. a ) )
Theorem	aomclem3 35884*	Lemma for dfac11 35890. Successor case 3, our required well-ordering. (Contributed by Stefan O'Rear, 19-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = suc U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> dom z C_ A )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> E We ( R1 ` dom z ) )
Theorem	aomclem4 35885*	Lemma for dfac11 35890. Limit case. Patch together well-orderings constructed so far using fnwe2 35881 to cover the limit rank. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- ( ph -> dom z e. On )   &    |- ( ph -> dom z = U. dom z )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   =>    |- ( ph -> F We ( R1 ` dom z ) )
Theorem	aomclem5 35886*	Lemma for dfac11 35890. Combine the successor case with the limit case. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )   &    |- ( ph -> dom z e. On )   &    |- ( ph -> A. a e. dom z ( z ` a ) We ( R1 ` a ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> dom z C_ A )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> G We ( R1 ` dom z ) )
Theorem	aomclem6 35887*	Lemma for dfac11 35890. Transfinite induction, close over z. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )   &    |- H = recs ( ( z e. _V |-> G ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> ( H ` A ) We ( R1 ` A ) )
Theorem	aomclem7 35888*	Lemma for dfac11 35890. ( R1 ` A ) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- B = { <. a , b >. | E. c e. ( R1 ` U. dom z ) ( ( c e. b /\ -. c e. a ) /\ A. d e. ( R1 ` U. dom z ) ( d ( z ` U. dom z ) c -> ( d e. a <-> d e. b ) ) ) }   &    |- C = ( a e. _V |-> sup ( ( y ` a ) , ( R1 ` dom z ) , B ) )   &    |- D = recs ( ( a e. _V |-> ( C ` ( ( R1 ` dom z ) \ ran a ) ) ) )   &    |- E = { <. a , b >. | |^| ( `' D " { a } ) e. |^| ( `' D " { b } ) }   &    |- F = { <. a , b >. | ( ( rank ` a ) _E ( rank ` b ) \/ ( ( rank ` a ) = ( rank ` b ) /\ a ( z ` suc ( rank ` a ) ) b ) ) }   &    |- G = ( if ( dom z = U. dom z , F , E ) i^i ( ( R1 ` dom z ) X. ( R1 ` dom z ) ) )   &    |- H = recs ( ( z e. _V |-> G ) )   &    |- ( ph -> A e. On )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> E. b b We ( R1 ` A ) )
Theorem	aomclem8 35889*	Lemma for dfac11 35890. Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015.)
|- ( ph -> A e. On )   &    |- ( ph -> A. a e. ~P ( R1 ` A ) ( a =/= (/) -> ( y ` a ) e. ( ( ~P a i^i Fin ) \ { (/) } ) ) )   =>    |- ( ph -> E. b b We ( R1 ` A ) )
Theorem	dfac11 35890*	The right-hand side of this theorem (compare with ac4 8912), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg 8116, despite not mentioning the cumulative hierarchy in any way as most consequences of regularity do. This is definition (MC) of [Schechter] p. 141. EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it. A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Stefan O'Rear, 1-Jun-2015.)
|- (CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
Theorem	kelac1 35891*	Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( ph /\ x e. I ) -> S =/= (/) )   &    |- ( ( ph /\ x e. I ) -> J e. Top )   &    |- ( ( ph /\ x e. I ) -> C e. ( Clsd ` J ) )   &    |- ( ( ph /\ x e. I ) -> B : S -1-1-onto-> C )   &    |- ( ( ph /\ x e. I ) -> U e. U. J )   &    |- ( ph -> ( Xt_ ` ( x e. I |-> J ) ) e. Comp )   =>    |- ( ph -> X_ x e. I S =/= (/) )
Theorem	kelac2lem 35892	Lemma for kelac2 35893 and dfac21 35894: knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( S e. V -> ( topGen ` { S , { ~P U. S } } ) e. Comp )
Theorem	kelac2 35893*	Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( ph /\ x e. I ) -> S e. V )   &    |- ( ( ph /\ x e. I ) -> S =/= (/) )   &    |- ( ph -> ( Xt_ ` ( x e. I |-> ( topGen ` { S , { ~P U. S } } ) ) ) e. Comp )   =>    |- ( ph -> X_ x e. I S =/= (/) )
Theorem	dfac21 35894	Tychonoff's theorem is a choice equivalent. Definition AC21 of Schechter p. 461. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 27-Aug-2015.)
|- (CHOICE <-> A. f ( f : dom f --> Comp -> ( Xt_ ` f ) e. Comp ) )
21.23.38  Finitely generated left modules
Syntax	clfig 35895	Extend class notation with the class of finitely generated left modules.
class LFinGen
Definition	df-lfig 35896	Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using ↾s. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- LFinGen = { w e. LMod | ( Base ` w ) e. ( ( LSpan ` w ) " ( ~P ( Base ` w ) i^i Fin ) ) }
Theorem	islmodfg 35897*	Property of a finitely generated left module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- B = ( Base ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> ( W e. LFinGen <-> E. b e. ~P B ( b e. Fin /\ ( N ` b ) = B ) ) )
Theorem	islssfg 35898*	Property of a finitely generated left (sub-)module. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ~P U ( b e. Fin /\ ( N ` b ) = U ) ) )
Theorem	islssfg2 35899*	Property of a finitely generated left (sub-)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- X = ( W ↾s U )   &    |- S = ( LSubSp ` W )   &    |- N = ( LSpan ` W )   &    |- B = ( Base ` W )   =>    |- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ( ~P B i^i Fin ) ( N ` b ) = U ) )
Theorem	islssfgi 35900	Finitely spanned subspaces are finitely generated. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- N = ( LSpan ` W )   &    |- V = ( Base ` W )   &    |- X = ( W ↾s ( N ` B ) )   =>    |- ( ( W e. LMod /\ B C_ V /\ B e. Fin ) -> X e. LFinGen )