P. 130 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12901-13000   *Has distinct variable group(s)

Type	Label	Description
Statement
5.2.11  Fundamental theorem of arithmetic
Theorem	1arithlem1 12901*	Lemma for 1arith 12905. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   =>    |- ( N e. NN -> ( M ` N ) = ( p e. Prime |-> ( p pCnt N ) ) )
Theorem	1arithlem2 12902*	Lemma for 1arith 12905. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   =>    |- ( ( N e. NN /\ P e. Prime ) -> ( ( M ` N ) ` P ) = ( P pCnt N ) )
Theorem	1arithlem3 12903*	Lemma for 1arith 12905. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   =>    |- ( N e. NN -> ( M ` N ) : Prime --> NN0 )
Theorem	1arithlem4 12904*	Lemma for 1arith 12905. (Contributed by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   &    |- G = ( y e. NN |-> if ( y e. Prime , ( y ^ ( F ` y ) ) , 1 ) )   &    |- ( ph -> F : Prime --> NN0 )   &    |- ( ph -> N e. NN )   &    |- ( ( ph /\ ( q e. Prime /\ N <_ q ) ) -> ( F ` q ) = 0 )   =>    |- ( ph -> E. x e. NN F = ( M ` x ) )
Theorem	1arith 12905*	Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function M maps the set of positive integers one-to-one onto the set of prime factorizations R. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   &    |- R = { e e. ( NN0 ^m Prime ) | ( `' e " NN ) e. Fin }   =>    |- M : NN -1-1-onto-> R
Theorem	1arith2 12906*	Fundamental theorem of arithmetic, where a prime factorization is represented as a finite monotonic 1-based sequence of primes. Every positive integer has a unique prime factorization. Theorem 1.10 in [ApostolNT] p. 17. This is Metamath 100 proof #80. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 30-May-2014.)
|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )   &    |- R = { e e. ( NN0 ^m Prime ) | ( `' e " NN ) e. Fin }   =>    |- A. z e. NN E! g e. R ( M ` z ) = g
5.2.12  Lagrange's four-square theorem
Syntax	cgz 12907	Extend class notation with the set of gaussian integers.
class ZZ[_i]
Definition	df-gz 12908	Define the set of gaussian integers, which are complex numbers whose real and imaginary parts are integers. (Note that the [ _i ] is actually part of the symbol token and has no independent meaning.) (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ZZ[_i] = { x e. CC | ( ( Re ` x ) e. ZZ /\ ( Im ` x ) e. ZZ ) }
Theorem	elgz 12909	Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] <-> ( A e. CC /\ ( Re ` A ) e. ZZ /\ ( Im ` A ) e. ZZ ) )
Theorem	gzcn 12910	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> A e. CC )
Theorem	zgz 12911	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ -> A e. ZZ[_i] )
Theorem	igz 12912	_i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- _i e. ZZ[_i]
Theorem	gznegcl 12913	The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> -u A e. ZZ[_i] )
Theorem	gzcjcl 12914	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( A e. ZZ[_i] -> ( * ` A ) e. ZZ[_i] )
Theorem	gzaddcl 12915	The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. ZZ[_i] /\ B e. ZZ[_i] ) -> ( A + B ) e. ZZ[_i] )
Theorem	gzmulcl 12916	The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. ZZ[_i] /\ B e. ZZ[_i] ) -> ( A x. B ) e. ZZ[_i] )
Theorem	gzreim 12917	Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A + ( _i x. B ) ) e. ZZ[_i] )
Theorem	gzsubcl 12918	The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- ( ( A e. ZZ[_i] /\ B e. ZZ[_i] ) -> ( A - B ) e. ZZ[_i] )
Theorem	gzabssqcl 12919	The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( A e. ZZ[_i] -> ( ( abs ` A ) ^ 2 ) e. NN0 )
Theorem	4sqlem5 12920	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( B e. ZZ /\ ( ( A - B ) / M ) e. ZZ ) )
Theorem	4sqlem6 12921	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( -u ( M / 2 ) <_ B /\ B < ( M / 2 ) ) )
Theorem	4sqlem7 12922	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> ( B ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
Theorem	4sqlem8 12923	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   =>    |- ( ph -> M || ( ( A ^ 2 ) - ( B ^ 2 ) ) )
Theorem	4sqlem9 12924	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- ( ( ph /\ ps ) -> ( B ^ 2 ) = 0 )   =>    |- ( ( ph /\ ps ) -> ( M ^ 2 ) || ( A ^ 2 ) )
Theorem	4sqlem10 12925	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> M e. NN )   &    |- B = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- ( ( ph /\ ps ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( B ^ 2 ) ) = 0 )   =>    |- ( ( ph /\ ps ) -> ( M ^ 2 ) || ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
Theorem	4sqlem1 12926*	Lemma for 4sq 12948. The set S is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that S = NN0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- S C_ NN0
Theorem	4sqlem2 12927*	Lemma for 4sq 12948. Change bound variables in S. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( A e. S <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
Theorem	4sqlem3 12928*	Lemma for 4sq 12948. Sufficient condition to be in S. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. S )
Theorem	4sqlem4a 12929*	Lemma for 4sqlem4 12930. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( ( A e. ZZ[_i] /\ B e. ZZ[_i] ) -> ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) ) e. S )
Theorem	4sqlem4 12930*	Lemma for 4sq 12948. We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( A e. S <-> E. u e. ZZ[_i] E. v e. ZZ[_i] A = ( ( ( abs ` u ) ^ 2 ) + ( ( abs ` v ) ^ 2 ) ) )
Theorem	mul4sqlem 12931*	Lemma for mul4sq 12932: algebraic manipulations. The extra assumptions involving M would let us know not just that the product is a sum of squares, but also that it preserves divisibility by M. (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> A e. ZZ[_i] )   &    |- ( ph -> B e. ZZ[_i] )   &    |- ( ph -> C e. ZZ[_i] )   &    |- ( ph -> D e. ZZ[_i] )   &    |- X = ( ( ( abs ` A ) ^ 2 ) + ( ( abs ` B ) ^ 2 ) )   &    |- Y = ( ( ( abs ` C ) ^ 2 ) + ( ( abs ` D ) ^ 2 ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> ( ( A - C ) / M ) e. ZZ[_i] )   &    |- ( ph -> ( ( B - D ) / M ) e. ZZ[_i] )   &    |- ( ph -> ( X / M ) e. NN0 )   =>    |- ( ph -> ( ( X / M ) x. ( Y / M ) ) e. S )
Theorem	mul4sq 12932*	Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 12931. (For the curious, the explicit formula that is used is ( | a | ^ 2 + | b | ^ 2 ) ( | c | ^ 2 + | d | ^ 2 ) = | a * x. c + b x. d * | ^ 2 + | a * x. d - b x. c * | ^ 2.) (Contributed by Mario Carneiro, 14-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( ( A e. S /\ B e. S ) -> ( A x. B ) e. S )
Theorem	4sqlemafi 12933*	Lemma for 4sq 12948. A is finite. (Contributed by Jim Kingdon, 24-May-2025.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. NN )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   =>    |- ( ph -> A e. Fin )
Theorem	4sqlemffi 12934*	Lemma for 4sq 12948. ran F is finite. (Contributed by Jim Kingdon, 24-May-2025.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. NN )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   &    |- F = ( v e. A |-> ( ( P - 1 ) - v ) )   =>    |- ( ph -> ran F e. Fin )
Theorem	4sqleminfi 12935*	Lemma for 4sq 12948. A i^i ran F is finite. (Contributed by Jim Kingdon, 24-May-2025.)
|- ( ph -> N e. NN )   &    |- ( ph -> P e. NN )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   &    |- F = ( v e. A |-> ( ( P - 1 ) - v ) )   =>    |- ( ph -> ( A i^i ran F ) e. Fin )
Theorem	4sqexercise1 12936*	Exercise which may help in understanding the proof of 4sqlemsdc 12938. (Contributed by Jim Kingdon, 25-May-2025.)
|- S = { n | E. x e. ZZ n = ( x ^ 2 ) }   =>    |- ( A e. NN0 -> DECID A e. S )
Theorem	4sqexercise2 12937*	Exercise which may help in understanding the proof of 4sqlemsdc 12938. (Contributed by Jim Kingdon, 30-May-2025.)
|- S = { n | E. x e. ZZ E. y e. ZZ n = ( ( x ^ 2 ) + ( y ^ 2 ) ) }   =>    |- ( A e. NN0 -> DECID A e. S )
Theorem	4sqlemsdc 12938*	Lemma for 4sq 12948. The property of being the sum of four squares is decidable. The proof involves showing that (for a particular A) there are only a finite number of possible ways that it could be the sum of four squares, so checking each of those possibilities in turn decides whether the number is the sum of four squares. If this proof is hard to follow, especially because of its length, the simplified versions at 4sqexercise1 12936 and 4sqexercise2 12937 may help clarify, as they are using very much the same techniques on simplified versions of this lemma. (Contributed by Jim Kingdon, 25-May-2025.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- ( A e. NN0 -> DECID A e. S )
Theorem	4sqlem11 12939*	Lemma for 4sq 12948. Use the pigeonhole principle to show that the sets { m ^ 2 | m e. ( 0 ... N ) } and { -u 1 - n ^ 2 | n e. ( 0 ... N ) } have a common element, mod P. Note that although the conclusion is stated in terms of A i^i ran F being nonempty, it is also inhabited by 4sqleminfi 12935 and fin0 7055. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   &    |- F = ( v e. A |-> ( ( P - 1 ) - v ) )   =>    |- ( ph -> ( A i^i ran F ) =/= (/) )
Theorem	4sqlem12 12940*	Lemma for 4sq 12948. For any odd prime P, there is a k < P such that k P - 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- A = { u | E. m e. ( 0 ... N ) u = ( ( m ^ 2 ) mod P ) }   &    |- F = ( v e. A |-> ( ( P - 1 ) - v ) )   =>    |- ( ph -> E. k e. ( 1 ... ( P - 1 ) ) E. u e. ZZ[_i] ( ( ( abs ` u ) ^ 2 ) + 1 ) = ( k x. P ) )
Theorem	4sqlem13m 12941*	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   =>    |- ( ph -> ( E. j j e. T /\ M < P ) )
Theorem	4sqlem14 12942*	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ph -> R e. NN0 )
Theorem	4sqlem15 12943*	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ( ph /\ R = M ) -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) ) )
Theorem	4sqlem16 12944*	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- ( ph -> ( R <_ M /\ ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) ) )
Theorem	4sqlem17 12945*	Lemma for 4sq 12948. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   &    |- ( ph -> M e. ( ZZ>= ` 2 ) )   &    |- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. ZZ )   &    |- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )   &    |- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )   &    |- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )   =>    |- -. ph
Theorem	4sqlem18 12946*	Lemma for 4sq 12948. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   &    |- ( ph -> N e. NN )   &    |- ( ph -> P = ( ( 2 x. N ) + 1 ) )   &    |- ( ph -> P e. Prime )   &    |- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )   &    |- T = { i e. NN | ( i x. P ) e. S }   &    |- M = inf ( T , RR , < )   =>    |- ( ph -> P e. S )
Theorem	4sqlem19 12947*	Lemma for 4sq 12948. The proof is by strong induction - we show that if all the integers less than k are in S, then k is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 12946. If k is 0 , 1 , 2, we show k e. S directly; otherwise if k is composite, k is the product of two numbers less than it (and hence in S by assumption), so by mul4sq 12932 k e. S. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
|- S = { n | E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }   =>    |- NN0 = S
Theorem	4sq 12948*	Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. This is Metamath 100 proof #19. (Contributed by Mario Carneiro, 16-Jul-2014.)
|- ( A e. NN0 <-> E. a e. ZZ E. b e. ZZ E. c e. ZZ E. d e. ZZ A = ( ( ( a ^ 2 ) + ( b ^ 2 ) ) + ( ( c ^ 2 ) + ( d ^ 2 ) ) ) )
5.2.13  Decimal arithmetic (cont.)
Theorem	dec2dvds 12949	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN0   &    |- ( B x. 2 ) = C   &    |- D = ( C + 1 )   =>    |- -. 2 || ; A D
Theorem	dec5dvds 12950	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN   &    |- B < 5   =>    |- -. 5 || ; A B
Theorem	dec5dvds2 12951	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN   &    |- B < 5   &    |- ( 5 + B ) = C   =>    |- -. 5 || ; A C
Theorem	dec5nprm 12952	A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN   =>    |- -. ; A 5 e. Prime
Theorem	dec2nprm 12953	A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN   &    |- B e. NN0   &    |- ( B x. 2 ) = C   =>    |- -. ; A C e. Prime
Theorem	modxai 12954	Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- C e. NN0   &    |- L e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( ( A ^ C ) mod N ) = ( L mod N )   &    |- ( B + C ) = E   &    |- ( ( D x. N ) + M ) = ( K x. L )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	mod2xi 12955	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( 2 x. B ) = E   &    |- ( ( D x. N ) + M ) = ( K x. K )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	modxp1i 12956	Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN0   &    |- M e. NN0   &    |- ( ( A ^ B ) mod N ) = ( K mod N )   &    |- ( B + 1 ) = E   &    |- ( ( D x. N ) + M ) = ( K x. A )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	modsubi 12957	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- M e. NN0   &    |- ( A mod N ) = ( K mod N )   &    |- ( M + B ) = K   =>    |- ( ( A - B ) mod N ) = ( M mod N )
Theorem	gcdi 12958	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
|- K e. NN0   &    |- R e. NN0   &    |- N e. NN0   &    |- ( N gcd R ) = G   &    |- ( ( K x. N ) + R ) = M   =>    |- ( M gcd N ) = G
Theorem	gcdmodi 12959	Calculate a GCD via Euclid's algorithm. Theorem 5.6 in [ApostolNT] p. 109. (Contributed by Mario Carneiro, 19-Feb-2014.)
|- K e. NN0   &    |- R e. NN0   &    |- N e. NN   &    |- ( K mod N ) = ( R mod N )   &    |- ( N gcd R ) = G   =>    |- ( K gcd N ) = G
Theorem	numexp0 12960	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 0 ) = 1
Theorem	numexp1 12961	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 1 ) = A
Theorem	numexpp1 12962	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   &    |- M e. NN0   &    |- ( M + 1 ) = N   &    |- ( ( A ^ M ) x. A ) = C   =>    |- ( A ^ N ) = C
Theorem	numexp2x 12963	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   &    |- M e. NN0   &    |- ( 2 x. M ) = N   &    |- ( A ^ M ) = D   &    |- ( D x. D ) = C   =>    |- ( A ^ N ) = C
Theorem	decsplit0b 12964	Split a decimal number into two parts. Base case: N = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   =>    |- ( ( A x. (; 1 0 ^ 0 ) ) + B ) = ( A + B )
Theorem	decsplit0 12965	Split a decimal number into two parts. Base case: N = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   =>    |- ( ( A x. (; 1 0 ^ 0 ) ) + 0 ) = A
Theorem	decsplit1 12966	Split a decimal number into two parts. Base case: N = 1. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   =>    |- ( ( A x. (; 1 0 ^ 1 ) ) + B ) = ; A B
Theorem	decsplit 12967	Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- D e. NN0   &    |- M e. NN0   &    |- ( M + 1 ) = N   &    |- ( ( A x. (; 1 0 ^ M ) ) + B ) = C   =>    |- ( ( A x. (; 1 0 ^ N ) ) + ; B D ) = ; C D
Theorem	karatsuba 12968	The Karatsuba multiplication algorithm. If X and Y are decomposed into two groups of digits of length M (only the lower group is known to be this size but the algorithm is most efficient when the partition is chosen near the middle of the digit string), then X Y can be written in three groups of digits, where each group needs only one multiplication. Thus, we can halve both inputs with only three multiplications on the smaller operands, yielding an asymptotic improvement of n^(log2 3) instead of n^2 for the "naive" algorithm decmul1c 9653. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 9-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- S e. NN0   &    |- M e. NN0   &    |- ( A x. C ) = R   &    |- ( B x. D ) = T   &    |- ( ( A + B ) x. ( C + D ) ) = ( ( R + S ) + T )   &    |- ( ( A x. (; 1 0 ^ M ) ) + B ) = X   &    |- ( ( C x. (; 1 0 ^ M ) ) + D ) = Y   &    |- ( ( R x. (; 1 0 ^ M ) ) + S ) = W   &    |- ( ( W x. (; 1 0 ^ M ) ) + T ) = Z   =>    |- ( X x. Y ) = Z
Theorem	2exp4 12969	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 4 ) = ; 1 6
Theorem	2exp5 12970	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 5 ) = ; 3 2
Theorem	2exp6 12971	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- ( 2 ^ 6 ) = ; 6 4
Theorem	2exp7 12972	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 7 ) = ;; 1 2 8
Theorem	2exp8 12973	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 8 ) = ;; 2 5 6
Theorem	2exp11 12974	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^; 1 1 ) = ;;; 2 0 4 8
Theorem	2exp16 12975	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^; 1 6 ) = ;;;; 6 5 5 3 6
Theorem	3exp3 12976	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 3 ^ 3 ) = ; 2 7
Theorem	2expltfac 12977	The factorial grows faster than two to the power N. (Contributed by Mario Carneiro, 15-Sep-2016.)
|- ( N e. ( ZZ>= ` 4 ) -> ( 2 ^ N ) < ( ! ` N ) )
5.3  Cardinality of real and complex number subsets
5.3.1  Countability of integers and rationals
Theorem	oddennn 12978	There are as many odd positive integers as there are positive integers. (Contributed by Jim Kingdon, 11-May-2022.)
|- { z e. NN | -. 2 || z } ~~ NN
Theorem	evenennn 12979	There are as many even positive integers as there are positive integers. (Contributed by Jim Kingdon, 12-May-2022.)
|- { z e. NN | 2 || z } ~~ NN
Theorem	xpnnen 12980	The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.)
|- ( NN X. NN ) ~~ NN
Theorem	xpomen 12981	The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.)
|- ( om X. om ) ~~ om
Theorem	xpct 12982	The cartesian product of two sets dominated by om is dominated by om. (Contributed by Thierry Arnoux, 24-Sep-2017.)
|- ( ( A ~<_ om /\ B ~<_ om ) -> ( A X. B ) ~<_ om )
Theorem	unennn 12983	The union of two disjoint countably infinite sets is countably infinite. (Contributed by Jim Kingdon, 13-May-2022.)
|- ( ( A ~~ NN /\ B ~~ NN /\ ( A i^i B ) = (/) ) -> ( A u. B ) ~~ NN )
Theorem	znnen 12984	The set of integers and the set of positive integers are equinumerous. Corollary 8.1.23 of [AczelRathjen], p. 75. (Contributed by NM, 31-Jul-2004.)
|- ZZ ~~ NN
Theorem	ennnfonelemdc 12985*	Lemma for ennnfone 13011. A direct consequence of fidcenumlemrk 7132. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> P e. om )   =>    |- ( ph -> DECID ( F ` P ) e. ( F " P ) )
Theorem	ennnfonelemk 12986*	Lemma for ennnfone 13011. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> F : om -onto-> A )   &    |- ( ph -> K e. om )   &    |- ( ph -> N e. om )   &    |- ( ph -> A. j e. suc N ( F ` K ) =/= ( F ` j ) )   =>    |- ( ph -> N e. K )
Theorem	ennnfonelemj0 12987*	Lemma for ennnfone 13011. Initial state for J. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> ( J ` 0 ) e. { g e. ( A ^pm om ) | dom g e. om } )
Theorem	ennnfonelemjn 12988*	Lemma for ennnfone 13011. Non-initial state for J. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ( ph /\ f e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( J ` f ) e. om )
Theorem	ennnfonelemg 12989*	Lemma for ennnfone 13011. Closure for G. (Contributed by Jim Kingdon, 20-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ( ph /\ ( f e. { g e. ( A ^pm om ) | dom g e. om } /\ j e. om ) ) -> ( f G j ) e. { g e. ( A ^pm om ) | dom g e. om } )
Theorem	ennnfonelemh 12990*	Lemma for ennnfone 13011. (Contributed by Jim Kingdon, 8-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> H : NN0 --> ( A ^pm om ) )
Theorem	ennnfonelem0 12991*	Lemma for ennnfone 13011. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> ( H ` 0 ) = (/) )
Theorem	ennnfonelemp1 12992*	Lemma for ennnfone 13011. Value of H at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> ( H ` ( P + 1 ) ) = if ( ( F ` ( `' N ` P ) ) e. ( F " ( `' N ` P ) ) , ( H ` P ) , ( ( H ` P ) u. { <. dom ( H ` P ) , ( F ` ( `' N ` P ) ) >. } ) ) )
Theorem	ennnfonelem1 12993*	Lemma for ennnfone 13011. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   =>    |- ( ph -> ( H ` 1 ) = { <. (/) , ( F ` (/) ) >. } )
Theorem	ennnfonelemom 12994*	Lemma for ennnfone 13011. H yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> dom ( H ` P ) e. om )
Theorem	ennnfonelemhdmp1 12995*	Lemma for ennnfone 13011. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   &    |- ( ph -> -. ( F ` ( `' N ` P ) ) e. ( F " ( `' N ` P ) ) )   =>    |- ( ph -> dom ( H ` ( P + 1 ) ) = suc dom ( H ` P ) )
Theorem	ennnfonelemss 12996*	Lemma for ennnfone 13011. We only add elements to H as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> ( H ` P ) C_ ( H ` ( P + 1 ) ) )
Theorem	ennnfoneleminc 12997*	Lemma for ennnfone 13011. We only add elements to H as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   &    |- ( ph -> Q e. NN0 )   &    |- ( ph -> P <_ Q )   =>    |- ( ph -> ( H ` P ) C_ ( H ` Q ) )
Theorem	ennnfonelemkh 12998*	Lemma for ennnfone 13011. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> dom ( H ` P ) C_ ( `' N ` P ) )
Theorem	ennnfonelemhf1o 12999*	Lemma for ennnfone 13011. Each of the functions in H is one to one and onto an image of F. (Contributed by Jim Kingdon, 17-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> ( H ` P ) : dom ( H ` P ) -1-1-onto-> ( F " ( `' N ` P ) ) )
Theorem	ennnfonelemex 13000*	Lemma for ennnfone 13011. Extending the sequence ( H ` P ) to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.)
|- ( ph -> A. x e. A A. y e. A DECID x = y )   &    |- ( ph -> F : om -onto-> A )   &    |- ( ph -> A. n e. om E. k e. om A. j e. suc n ( F ` k ) =/= ( F ` j ) )   &    |- G = ( x e. ( A ^pm om ) , y e. om |-> if ( ( F ` y ) e. ( F " y ) , x , ( x u. { <. dom x , ( F ` y ) >. } ) ) )   &    |- N = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   &    |- J = ( x e. NN0 |-> if ( x = 0 , (/) , ( `' N ` ( x - 1 ) ) ) )   &    |- H = seq 0 ( G , J )   &    |- ( ph -> P e. NN0 )   =>    |- ( ph -> E. i e. NN0 dom ( H ` P ) e. dom ( H ` i ) )