P. 133 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mul4sqlem 13201*	Lemma for mul4sq 13202: 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 13202*	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 13201. (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 13203*	Lemma for 4sq 13218. 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 13204*	Lemma for 4sq 13218. 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 13205*	Lemma for 4sq 13218. 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 13206*	Exercise which may help in understanding the proof of 4sqlemsdc 13208. (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 13207*	Exercise which may help in understanding the proof of 4sqlemsdc 13208. (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 13208*	Lemma for 4sq 13218. 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 13206 and 4sqexercise2 13207 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 13209*	Lemma for 4sq 13218. 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 13205 and fin0 7193. (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 13210*	Lemma for 4sq 13218. 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 13211*	Lemma for 4sq 13218. (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 13212*	Lemma for 4sq 13218. (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 13213*	Lemma for 4sq 13218. (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 13214*	Lemma for 4sq 13218. (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 13215*	Lemma for 4sq 13218. (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 13216*	Lemma for 4sq 13218. 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 13217*	Lemma for 4sq 13218. 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 13216. 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 13202 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 13218*	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 13219	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 13220	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 13221	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 13222	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 13223	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 13224	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 13225	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 13226	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	mod2xnegi 13227	Version of mod2xi 13225 where A ^ B does not equal K (mod N) but instead the negative of K (mod N). (Contributed by Mario Carneiro, 21-Feb-2014.)
|- A e. NN   &    |- B e. NN0   &    |- D e. ZZ   &    |- K e. NN   &    |- M e. NN0   &    |- L e. NN0   &    |- ( ( A ^ B ) mod N ) = ( L mod N )   &    |- ( 2 x. B ) = E   &    |- ( L + K ) = N   &    |- ( ( D x. N ) + M ) = ( K x. K )   =>    |- ( ( A ^ E ) mod N ) = ( M mod N )
Theorem	modsubi 13228	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 13229	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 13230	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 13231	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 0 ) = 1
Theorem	numexp1 13232	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 1 ) = A
Theorem	numexpp1 13233	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 13234	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 13235	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 13236	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 13237	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 13238	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 13239	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 9857. (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 13240	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 4 ) = ; 1 6
Theorem	2exp5 13241	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 5 ) = ; 3 2
Theorem	2exp6 13242	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 13243	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 7 ) = ;; 1 2 8
Theorem	2exp8 13244	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 8 ) = ;; 2 5 6
Theorem	2exp11 13245	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^; 1 1 ) = ;;; 2 0 4 8
Theorem	2exp16 13246	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^; 1 6 ) = ;;;; 6 5 5 3 6
Theorem	3exp3 13247	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 3 ^ 3 ) = ; 2 7
Theorem	2expltfac 13248	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.2.14  Specific prime numbers
Theorem	prmlem0 13249*	Lemma for prmlem1a 13250 and prmlem2 13263. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- ( ( -. 2 || M /\ x e. ( ZZ>= ` M ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )   &    |- ( K e. Prime -> -. K || N )   &    |- ( K + 2 ) = M   =>    |- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )
Theorem	prmlem1a 13250*	Lemma for prmlem1 13251 and prmlem2 13263. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   &    |- 1 < N   &    |- -. 2 || N   &    |- -. 3 || N   &    |- ( ( -. 2 || 5 /\ x e. ( ZZ>= ` 5 ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) )   =>    |- N e. Prime
Theorem	prmlem1 13251	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- N e. NN   &    |- 1 < N   &    |- -. 2 || N   &    |- -. 3 || N   &    |- N < ; 2 5   =>    |- N e. Prime
Theorem	5prm 13252	5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- 5 e. Prime
Theorem	6nprm 13253	6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 6 e. Prime
Theorem	7prm 13254	7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- 7 e. Prime
Theorem	8nprm 13255	8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 8 e. Prime
Theorem	9nprm 13256	9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- -. 9 e. Prime
Theorem	10nprm 13257	10 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)
|- -. ; 1 0 e. Prime
Theorem	11prm 13258	11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 1 e. Prime
Theorem	13prm 13259	13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 3 e. Prime
Theorem	17prm 13260	17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 7 e. Prime
Theorem	19prm 13261	19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 1 9 e. Prime
Theorem	23prm 13262	23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- ; 2 3 e. Prime
Theorem	prmlem2 13263	Our last proving session got as far as 25 because we started with the two "bootstrap" primes 2 and 3, and the next prime is 5, so knowing that 2 and 3 are prime and 4 is not allows to cover the numbers less than 5 ^ 2 = 2 5. Additionally, nonprimes are "easy", so we can extend this range of known prime/nonprimes all the way until 29, which is the first prime larger than 25. Thus, in this lemma we extend another blanket out to 2 9 ^ 2 = 8 4 1, from which we can prove even more primes. If we wanted, we could keep doing this, but the goal is Bertrand's postulate, and for that we only need a few large primes - we don't need to find them all, as we have been doing thus far. So after this blanket runs out, we'll have to switch to another method (see 1259prm 13276). As a side note, you can see the pattern of the primes in the indentation pattern of this lemma! (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- N e. NN   &    |- N < ;; 8 4 1   &    |- 1 < N   &    |- -. 2 || N   &    |- -. 3 || N   &    |- -. 5 || N   &    |- -. 7 || N   &    |- -. ; 1 1 || N   &    |- -. ; 1 3 || N   &    |- -. ; 1 7 || N   &    |- -. ; 1 9 || N   &    |- -. ; 2 3 || N   =>    |- N e. Prime
Theorem	37prm 13264	37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ; 3 7 e. Prime
Theorem	43prm 13265	43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ; 4 3 e. Prime
Theorem	83prm 13266	83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ; 8 3 e. Prime
Theorem	139prm 13267	139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 1 3 9 e. Prime
Theorem	163prm 13268	163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 1 6 3 e. Prime
Theorem	317prm 13269	317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 3 1 7 e. Prime
Theorem	631prm 13270	631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- ;; 6 3 1 e. Prime
5.2.15  Very large primes
Theorem	1259lem1 13271	Lemma for 1259prm 13276. Calculate a power mod. In decimal, we calculate 2 ^ 1 6 = 5 2 N + 6 8 == 6 8 and 2 ^ 1 7 == 6 8 x. 2 = 1 3 6 in this lemma. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
|- N = ;;; 1 2 5 9   =>    |- ( ( 2 ^; 1 7 ) mod N ) = (;; 1 3 6 mod N )
Theorem	1259lem2 13272	Lemma for 1259prm 13276. Calculate a power mod. In decimal, we calculate 2 ^ 3 4 = ( 2 ^ 1 7 ) ^ 2 == 1 3 6 ^ 2 == 1 4 N + 8 7 0. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
|- N = ;;; 1 2 5 9   =>    |- ( ( 2 ^; 3 4 ) mod N ) = (;; 8 7 0 mod N )
Theorem	1259lem3 13273	Lemma for 1259prm 13276. Calculate a power mod. In decimal, we calculate 2 ^ 3 8 = 2 ^ 3 4 x. 2 ^ 4 == 8 7 0 x. 1 6 = 1 1 N + 7 1 and 2 ^ 7 6 = ( 2 ^ 3 4 ) ^ 2 == 7 1 ^ 2 = 4 N + 5 == 5. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
|- N = ;;; 1 2 5 9   =>    |- ( ( 2 ^; 7 6 ) mod N ) = ( 5 mod N )
Theorem	1259lem4 13274	Lemma for 1259prm 13276. Calculate a power mod. In decimal, we calculate 2 ^ 3 0 6 = ( 2 ^ 7 6 ) ^ 4 x. 4 == 5 ^ 4 x. 4 = 2 N - 1 8, 2 ^ 6 1 2 = ( 2 ^ 3 0 6 ) ^ 2 == 1 8 ^ 2 = 3 2 4, 2 ^ 6 2 9 = 2 ^ 6 1 2 x. 2 ^ 1 7 == 3 2 4 x. 1 3 6 = 3 5 N - 1 and finally 2 ^ ( N - 1 ) = ( 2 ^ 6 2 9 ) ^ 2 == 1 ^ 2 = 1. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
|- N = ;;; 1 2 5 9   =>    |- ( ( 2 ^ ( N - 1 ) ) mod N ) = ( 1 mod N )
Theorem	1259lem5 13275	Lemma for 1259prm 13276. Calculate the GCD of 2 ^ 3 4 - 1 == 8 6 9 with N = 1 2 5 9. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
|- N = ;;; 1 2 5 9   =>    |- ( ( ( 2 ^; 3 4 ) - 1 ) gcd N ) = 1
Theorem	1259prm 13276	1259 is a prime number. (Contributed by Mario Carneiro, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
|- N = ;;; 1 2 5 9   =>    |- N e. Prime
5.2.16  Bertrand's Ballot Problem
Theorem	ballotfilemofi 13277*	O is finite. (Contributed by Jim Kingdon, 20-May-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   =>    |- O e. Fin
Theorem	ballotfilem1 13278*	The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   =>    |- (♯ ` O ) = ( ( M + N ) _C M )
Theorem	ballotfilemonn 13279*	The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   =>    |- (♯ ` O ) e. NN
Theorem	ballotfilemelo 13280*	Elementhood in O. (Contributed by Thierry Arnoux, 17-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   =>    |- ( C e. O <-> ( C C_ ( 1 ... ( M + N ) ) /\ C e. Fin /\ (♯ ` C ) = M ) )
Theorem	ballotfilemcdc 13281*	Lemma for ballotfi . It is decidable whether a given integer is an element of a particular element of O. (Contributed by Jim Kingdon, 7-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> DECID K e. C )
Theorem	ballotfilemcinfi 13282*	Lemma for ballotfi . The portion of a counting representing votes for A up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( 1 ... J ) i^i C ) e. Fin )
Theorem	ballotfilemdifcfi 13283*	Lemma for ballotfi . The portion of a counting representing votes for B up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( 1 ... J ) \ C ) e. Fin )
Theorem	ballotfilemcinfz 13284*	Lemma for ballotfi . The portion of a counting representing votes for A within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( ( J ... K ) i^i C ) e. Fin )
Theorem	ballotfilemdifcfz 13285*	Lemma for ballotfi . The portion of a counting representing votes for B within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( ( J ... K ) \ C ) e. Fin )
Theorem	ballotfilem2 13286*	The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   =>    |- ( P ` { c e. O | -. 1 e. c } ) = ( N / ( M + N ) )
Theorem	ballotfilemfval 13287*	The value of F. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( F ` C ) ` J ) = ( (♯ ` ( ( 1 ... J ) i^i C ) ) - (♯ ` ( ( 1 ... J ) \ C ) ) ) )
Theorem	ballotfilemfelz 13288*	( F ` C ) has values in ZZ. (Contributed by Thierry Arnoux, 23-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. ZZ )   =>    |- ( ph -> ( ( F ` C ) ` J ) e. ZZ )
Theorem	ballotfilemfp1 13289*	If the J th ballot is for A, ( F ` C ) goes up 1. If the J th ballot is for B, ( F ` C ) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. NN )   =>    |- ( ph -> ( ( -. J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) - 1 ) ) /\ ( J e. C -> ( ( F ` C ) ` J ) = ( ( ( F ` C ) ` ( J - 1 ) ) + 1 ) ) ) )
Theorem	ballotfilemfc0 13290*	F takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. NN )   &    |- ( ph -> E. i e. ( 1 ... J ) ( ( F ` C ) ` i ) <_ 0 )   &    |- ( ph -> 0 < ( ( F ` C ) ` J ) )   =>    |- ( ph -> E. k e. ( 1 ... J ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotfilemfcc 13291*	F takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- ( ph -> C e. O )   &    |- ( ph -> J e. NN )   &    |- ( ph -> E. i e. ( 1 ... J ) 0 <_ ( ( F ` C ) ` i ) )   &    |- ( ph -> ( ( F ` C ) ` J ) < 0 )   =>    |- ( ph -> E. k e. ( 1 ... J ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotfilemfmpn 13292*	( F ` C ) finishes counting at ( M - N ). (Contributed by Thierry Arnoux, 25-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   =>    |- ( C e. O -> ( ( F ` C ) ` ( M + N ) ) = ( M - N ) )
Theorem	ballotfilemfval0 13293*	( F ` C ) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   =>    |- ( C e. O -> ( ( F ` C ) ` 0 ) = 0 )
Theorem	ballotfileme 13294*	Elements of E. (Contributed by Thierry Arnoux, 14-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- ( C e. E <-> ( C e. O /\ A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` C ) ` i ) ) )
Theorem	ballotfilemefi 13295*	E is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- E e. Fin
Theorem	ballotfilemafi 13296*	The set of countings where A got the first vote, but does not stay strictly ahead throughout, is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- { c e. ( O \ E ) | 1 e. c } e. Fin
Theorem	ballotfilembfi 13297*	The set of countings where B got the first vote is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- { c e. ( O \ E ) | -. 1 e. c } e. Fin
Theorem	ballotfilemodife 13298*	Elements of ( O \ E ). (Contributed by Thierry Arnoux, 7-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- ( C e. ( O \ E ) <-> ( C e. O /\ E. i e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` i ) <_ 0 ) )
Theorem	ballotfilem4 13299*	If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   =>    |- ( C e. O -> ( -. 1 e. C -> -. C e. E ) )
Theorem	ballotfilem5 13300*	If A is not ahead throughout, there is a k where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.)
|- M e. NN   &    |- N e. NN   &    |- O = { c e. ( ~P ( 1 ... ( M + N ) ) i^i Fin ) | (♯ ` c ) = M }   &    |- P = ( x e. ( ~P O i^i Fin ) |-> ( (♯ ` x ) / (♯ ` O ) ) )   &    |- F = ( c e. O |-> ( i e. ZZ |-> ( (♯ ` ( ( 1 ... i ) i^i c ) ) - (♯ ` ( ( 1 ... i ) \ c ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   =>    |- ( C e. ( O \ E ) -> E. k e. ( 1 ... ( M + N ) ) ( ( F ` C ) ` k ) = 0 )