P. 132 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13101-13200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gzmulcl 13101	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 13102	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 13103	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 13104	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 13105	Lemma for 4sq 13133. (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 13106	Lemma for 4sq 13133. (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 13107	Lemma for 4sq 13133. (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 13108	Lemma for 4sq 13133. (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 13109	Lemma for 4sq 13133. (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 13110	Lemma for 4sq 13133. (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 13111*	Lemma for 4sq 13133. 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 13112*	Lemma for 4sq 13133. 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 13113*	Lemma for 4sq 13133. 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 13114*	Lemma for 4sqlem4 13115. (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 13115*	Lemma for 4sq 13133. 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 13116*	Lemma for mul4sq 13117: 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 13117*	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 13116. (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 13118*	Lemma for 4sq 13133. 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 13119*	Lemma for 4sq 13133. 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 13120*	Lemma for 4sq 13133. 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 13121*	Exercise which may help in understanding the proof of 4sqlemsdc 13123. (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 13122*	Exercise which may help in understanding the proof of 4sqlemsdc 13123. (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 13123*	Lemma for 4sq 13133. 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 13121 and 4sqexercise2 13122 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 13124*	Lemma for 4sq 13133. 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 13120 and fin0 7155. (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 13125*	Lemma for 4sq 13133. 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 13126*	Lemma for 4sq 13133. (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 13127*	Lemma for 4sq 13133. (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 13128*	Lemma for 4sq 13133. (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 13129*	Lemma for 4sq 13133. (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 13130*	Lemma for 4sq 13133. (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 13131*	Lemma for 4sq 13133. 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 13132*	Lemma for 4sq 13133. 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 13131. 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 13117 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 13133*	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 13134	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 13135	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 13136	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 13137	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 13138	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 13139	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 13140	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 13141	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 13142	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 13143	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 13144	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 13145	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 0 ) = 1
Theorem	numexp1 13146	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A e. NN0   =>    |- ( A ^ 1 ) = A
Theorem	numexpp1 13147	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 13148	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 13149	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 13150	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 13151	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 13152	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 13153	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 9791. (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 13154	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 4 ) = ; 1 6
Theorem	2exp5 13155	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 5 ) = ; 3 2
Theorem	2exp6 13156	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 13157	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^ 7 ) = ;; 1 2 8
Theorem	2exp8 13158	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^ 8 ) = ;; 2 5 6
Theorem	2exp11 13159	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
|- ( 2 ^; 1 1 ) = ;;; 2 0 4 8
Theorem	2exp16 13160	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 2 ^; 1 6 ) = ;;;; 6 5 5 3 6
Theorem	3exp3 13161	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
|- ( 3 ^ 3 ) = ; 2 7
Theorem	2expltfac 13162	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  Bertrand's Ballot Problem
Theorem	ballotfilemofi 13163*	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 13164*	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 13165*	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 13166*	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 13167*	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 13168*	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 13169*	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 13170*	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 13171*	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 13172*	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 13173*	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 13174*	( 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 13175*	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 13176*	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 13177*	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 13178*	( 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 13179*	( 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 13180*	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 13181*	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 13182*	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 13183*	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 13184*	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 13185*	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 13186*	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 )
Theorem	ballotfilemi 13187*	Value of I for a given counting C. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- 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   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> ( I ` C ) = inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 } , RR , < ) )
Theorem	ballotfilemiex 13188*	Properties of ( I ` C ). (Contributed by Thierry Arnoux, 12-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- 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   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> ( ( I ` C ) e. ( 1 ... ( M + N ) ) /\ ( ( F ` C ) ` ( I ` C ) ) = 0 ) )
Theorem	ballotfilemi1 13189*	The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) =/= 1 )
Theorem	ballotfilemii 13190*	The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ 1 e. C ) -> ( I ` C ) =/= 1 )
Theorem	ballotfilemscl 13191*	The set of zeroes of F has an infimum. (Contributed by Jim Kingdon, 12-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 ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 }   =>    |- ( C e. ( O \ E ) -> inf ( S , RR , < ) e. S )
Theorem	ballotfilemsle 13192*	The infimum of the set of zeroes of F is a lower bound. (Contributed by Jim Kingdon, 12-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 ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = { k e. ( 1 ... ( M + N ) ) | ( ( F ` C ) ` k ) = 0 }   =>    |- ( ( C e. ( O \ E ) /\ X e. S ) -> inf ( S , RR , < ) <_ X )
Theorem	ballotfilemimin 13193*	( I ` C ) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
|- 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   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( C e. ( O \ E ) -> -. E. k e. ( 1 ... ( ( I ` C ) - 1 ) ) ( ( F ` C ) ` k ) = 0 )
Theorem	ballotfilemic 13194*	If the first vote is for B, the vote on the first tie is for A. (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   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ -. 1 e. C ) -> ( I ` C ) e. C )
Theorem	ballotfilem1c 13195*	If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   =>    |- ( ( C e. ( O \ E ) /\ 1 e. C ) -> -. ( I ` C ) e. C )
Theorem	ballotfilemsval 13196*	Value of S. (Contributed by Thierry Arnoux, 12-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( C e. ( O \ E ) -> ( S ` C ) = ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - i ) , i ) ) )
Theorem	ballotfilemsv 13197*	Value of S evaluated at J for a given counting C. (Contributed by Thierry Arnoux, 12-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` J ) = if ( J <_ ( I ` C ) , ( ( ( I ` C ) + 1 ) - J ) , J ) )
Theorem	ballotfilemsgt1 13198*	S maps values less than ( I ` C ) to values greater than 1. (Contributed by Thierry Arnoux, 28-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) /\ J < ( I ` C ) ) -> 1 < ( ( S ` C ) ` J ) )
Theorem	ballotfilemsdom 13199*	Domain of S for a given counting C. (Contributed by Thierry Arnoux, 12-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( M + N ) ) ) -> ( ( S ` C ) ` J ) e. ( 1 ... ( M + N ) ) )
Theorem	ballotfilemsel1i 13200*	The range ( 1 ... ( I ` C ) ) is invariant under ( S ` C ). (Contributed by Thierry Arnoux, 28-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 ) ) ) ) )   &    |- E = { c e. O | A. i e. ( 1 ... ( M + N ) ) 0 < ( ( F ` c ) ` i ) }   &    |- N < M   &    |- I = ( c e. ( O \ E ) |-> inf ( { k e. ( 1 ... ( M + N ) ) | ( ( F ` c ) ` k ) = 0 } , RR , < ) )   &    |- S = ( c e. ( O \ E ) |-> ( i e. ( 1 ... ( M + N ) ) |-> if ( i <_ ( I ` c ) , ( ( ( I ` c ) + 1 ) - i ) , i ) ) )   =>    |- ( ( C e. ( O \ E ) /\ J e. ( 1 ... ( I ` C ) ) ) -> ( ( S ` C ) ` J ) e. ( 1 ... ( I ` C ) ) )