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	mul4sq 13201*	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 13200. (For the curious, the explicit formula that is used is ( ∣ 𝑎 ∣ ↑2 + ∣ 𝑏 ∣ ↑2)( ∣ 𝑐 ∣ ↑2 + ∣ 𝑑 ∣ ↑2) = ∣ 𝑎∗ · 𝑐 + 𝑏 · 𝑑∗ ∣ ↑2 + ∣ 𝑎∗ · 𝑑 − 𝑏 · 𝑐∗ ∣ ↑2.) (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆)
Theorem	4sqlemafi 13202*	Lemma for 4sq 13217. 𝐴 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    ⇒   ⊢ (𝜑 → 𝐴 ∈ Fin)
Theorem	4sqlemffi 13203*	Lemma for 4sq 13217. ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ Fin)
Theorem	4sqleminfi 13204*	Lemma for 4sq 13217. 𝐴 ∩ ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ∈ Fin)
Theorem	4sqexercise1 13205*	Exercise which may help in understanding the proof of 4sqlemsdc 13207. (Contributed by Jim Kingdon, 25-May-2025.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ 𝑛 = (𝑥↑2)}    ⇒   ⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
Theorem	4sqexercise2 13206*	Exercise which may help in understanding the proof of 4sqlemsdc 13207. (Contributed by Jim Kingdon, 30-May-2025.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑛 = ((𝑥↑2) + (𝑦↑2))}    ⇒   ⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
Theorem	4sqlemsdc 13207*	Lemma for 4sq 13217. The property of being the sum of four squares is decidable. The proof involves showing that (for a particular 𝐴) 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 13205 and 4sqexercise2 13206 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.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
Theorem	4sqlem11 13208*	Lemma for 4sq 13217. Use the pigeonhole principle to show that the sets {𝑚↑2 ∣ 𝑚 ∈ (0...𝑁)} and { -1 − 𝑛↑2 ∣ 𝑛 ∈ (0...𝑁)} have a common element, mod 𝑃. Note that although the conclusion is stated in terms of 𝐴 ∩ ran 𝐹 being nonempty, it is also inhabited by 4sqleminfi 13204 and fin0 7195. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
Theorem	4sqlem12 13209*	Lemma for 4sq 13217. For any odd prime 𝑃, there is a 𝑘 < 𝑃 such that 𝑘𝑃 − 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃))
Theorem	4sqlem13m 13210*	Lemma for 4sq 13217. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃))
Theorem	4sqlem14 13211*	Lemma for 4sq 13217. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ (𝜑 → 𝑅 ∈ ℕ0)
Theorem	4sqlem15 13212*	Lemma for 4sq 13217. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((((𝑀↑2) / 2) / 2) − (𝐸↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) − (𝐹↑2)) = 0) ∧ (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) − (𝐻↑2)) = 0)))
Theorem	4sqlem16 13213*	Lemma for 4sq 13217. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ (𝜑 → (𝑅 ≤ 𝑀 ∧ ((𝑅 = 0 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃))))
Theorem	4sqlem17 13214*	Lemma for 4sq 13217. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀)    &   ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))))    ⇒   ⊢ ¬ 𝜑
Theorem	4sqlem18 13215*	Lemma for 4sq 13217. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑆)
Theorem	4sqlem19 13216*	Lemma for 4sq 13217. The proof is by strong induction - we show that if all the integers less than 𝑘 are in 𝑆, then 𝑘 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 13215. If 𝑘 is 0, 1, 2, we show 𝑘 ∈ 𝑆 directly; otherwise if 𝑘 is composite, 𝑘 is the product of two numbers less than it (and hence in 𝑆 by assumption), so by mul4sq 13201 𝑘 ∈ 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ℕ0 = 𝑆
Theorem	4sq 13217*	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.)
⊢ (𝐴 ∈ ℕ0 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
5.2.13  Decimal arithmetic (cont.)
Theorem	dec2dvds 13218	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    &   ⊢ 𝐷 = (𝐶 + 1)    ⇒   ⊢ ¬ 2 ∥ ;𝐴𝐷
Theorem	dec5dvds 13219	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐵
Theorem	dec5dvds2 13220	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    &   ⊢ (5 + 𝐵) = 𝐶    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐶
Theorem	dec5nprm 13221	A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ¬ ;𝐴5 ∈ ℙ
Theorem	dec2nprm 13222	A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    ⇒   ⊢ ¬ ;𝐴𝐶 ∈ ℙ
Theorem	modxai 13223	Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ ((𝐴↑𝐶) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (𝐵 + 𝐶) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐿)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	mod2xi 13224	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modxp1i 13225	Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝐵 + 1) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐴)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	mod2xnegi 13226	Version of mod2xi 13224 where 𝐴↑𝐵 does not equal 𝐾 (mod 𝑁) but instead the negative of 𝐾 (mod 𝑁). (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ (𝐿 + 𝐾) = 𝑁    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modsubi 13227	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝑀 + 𝐵) = 𝐾    ⇒   ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	gcdi 13228	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    &   ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀    ⇒   ⊢ (𝑀 gcd 𝑁) = 𝐺
Theorem	gcdmodi 13229	Calculate a GCD via Euclid's algorithm. Theorem 5.6 in [ApostolNT] p. 109. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ (𝐾 mod 𝑁) = (𝑅 mod 𝑁)    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    ⇒   ⊢ (𝐾 gcd 𝑁) = 𝐺
Theorem	numexp0 13230	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑0) = 1
Theorem	numexp1 13231	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑1) = 𝐴
Theorem	numexpp1 13232	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴↑𝑀) · 𝐴) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	numexp2x 13233	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (2 · 𝑀) = 𝑁    &   ⊢ (𝐴↑𝑀) = 𝐷    &   ⊢ (𝐷 · 𝐷) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	decsplit0b 13234	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 𝐵) = (𝐴 + 𝐵)
Theorem	decsplit0 13235	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 0) = 𝐴
Theorem	decsplit1 13236	Split a decimal number into two parts. Base case: 𝑁 = 1. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑1)) + 𝐵) = ;𝐴𝐵
Theorem	decsplit 13237	Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝐶    ⇒   ⊢ ((𝐴 · (;10↑𝑁)) + ;𝐵𝐷) = ;𝐶𝐷
Theorem	karatsuba 13238	The Karatsuba multiplication algorithm. If 𝑋 and 𝑌 are decomposed into two groups of digits of length 𝑀 (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 𝑋𝑌 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 9856. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑆 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝑅    &   ⊢ (𝐵 · 𝐷) = 𝑇    &   ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = ((𝑅 + 𝑆) + 𝑇)    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝑋    &   ⊢ ((𝐶 · (;10↑𝑀)) + 𝐷) = 𝑌    &   ⊢ ((𝑅 · (;10↑𝑀)) + 𝑆) = 𝑊    &   ⊢ ((𝑊 · (;10↑𝑀)) + 𝑇) = 𝑍    ⇒   ⊢ (𝑋 · 𝑌) = 𝑍
Theorem	2exp4 13239	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑4) = ;16
Theorem	2exp5 13240	Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑5) = ;32
Theorem	2exp6 13241	Two to the sixth power is 64. (Contributed by Mario Carneiro, 20-Apr-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
⊢ (2↑6) = ;64
Theorem	2exp7 13242	Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑7) = ;;128
Theorem	2exp8 13243	Two to the eighth power is 256. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑8) = ;;256
Theorem	2exp11 13244	Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.)
⊢ (2↑;11) = ;;;2048
Theorem	2exp16 13245	Two to the sixteenth power is 65536. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑;16) = ;;;;65536
Theorem	3exp3 13246	Three to the third power is 27. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (3↑3) = ;27
Theorem	2expltfac 13247	The factorial grows faster than two to the power 𝑁. (Contributed by Mario Carneiro, 15-Sep-2016.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (2↑𝑁) < (!‘𝑁))
5.2.14  Specific prime numbers
Theorem	prmlem0 13248*	Lemma for prmlem1a 13249 and prmlem2 13262. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((¬ 2 ∥ 𝑀 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))    &   ⊢ (𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁)    &   ⊢ (𝐾 + 2) = 𝑀    ⇒   ⊢ ((¬ 2 ∥ 𝐾 ∧ 𝑥 ∈ (ℤ≥‘𝐾)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))
Theorem	prmlem1a 13249*	Lemma for prmlem1 13250 and prmlem2 13262. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ ((¬ 2 ∥ 5 ∧ 𝑥 ∈ (ℤ≥‘5)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	prmlem1 13250	A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ 𝑁 < ;25    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	5prm 13251	5 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 5 ∈ ℙ
Theorem	6nprm 13252	6 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 6 ∈ ℙ
Theorem	7prm 13253	7 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 7 ∈ ℙ
Theorem	8nprm 13254	8 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 8 ∈ ℙ
Theorem	9nprm 13255	9 is not a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 9 ∈ ℙ
Theorem	10nprm 13256	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.)
⊢ ¬ ;10 ∈ ℙ
Theorem	11prm 13257	11 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;11 ∈ ℙ
Theorem	13prm 13258	13 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;13 ∈ ℙ
Theorem	17prm 13259	17 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;17 ∈ ℙ
Theorem	19prm 13260	19 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;19 ∈ ℙ
Theorem	23prm 13261	23 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ ;23 ∈ ℙ
Theorem	prmlem2 13262	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 = 25. 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 29↑2 = 841, 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 13275). 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.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑁 < ;;841    &   ⊢ 1 < 𝑁    &   ⊢ ¬ 2 ∥ 𝑁    &   ⊢ ¬ 3 ∥ 𝑁    &   ⊢ ¬ 5 ∥ 𝑁    &   ⊢ ¬ 7 ∥ 𝑁    &   ⊢ ¬ ;11 ∥ 𝑁    &   ⊢ ¬ ;13 ∥ 𝑁    &   ⊢ ¬ ;17 ∥ 𝑁    &   ⊢ ¬ ;19 ∥ 𝑁    &   ⊢ ¬ ;23 ∥ 𝑁    ⇒   ⊢ 𝑁 ∈ ℙ
Theorem	37prm 13263	37 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;37 ∈ ℙ
Theorem	43prm 13264	43 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;43 ∈ ℙ
Theorem	83prm 13265	83 is a prime number. (Contributed by Mario Carneiro, 18-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;83 ∈ ℙ
Theorem	139prm 13266	139 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;139 ∈ ℙ
Theorem	163prm 13267	163 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;163 ∈ ℙ
Theorem	317prm 13268	317 is a prime number. (Contributed by Mario Carneiro, 19-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;317 ∈ ℙ
Theorem	631prm 13269	631 is a prime number. (Contributed by Mario Carneiro, 1-Mar-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ ;;631 ∈ ℙ
5.2.15  Very large primes
Theorem	1259lem1 13270	Lemma for 1259prm 13275. Calculate a power mod. In decimal, we calculate 2↑16 = 52𝑁 + 68≡68 and 2↑17≡68 · 2 = 136 in this lemma. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;17) mod 𝑁) = (;;136 mod 𝑁)
Theorem	1259lem2 13271	Lemma for 1259prm 13275. Calculate a power mod. In decimal, we calculate 2↑34 = (2↑17)↑2≡136↑2≡14𝑁 + 870. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;34) mod 𝑁) = (;;870 mod 𝑁)
Theorem	1259lem3 13272	Lemma for 1259prm 13275. Calculate a power mod. In decimal, we calculate 2↑38 = 2↑34 · 2↑4≡870 · 16 = 11𝑁 + 71 and 2↑76 = (2↑34)↑2≡71↑2 = 4𝑁 + 5≡5. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑;76) mod 𝑁) = (5 mod 𝑁)
Theorem	1259lem4 13273	Lemma for 1259prm 13275. Calculate a power mod. In decimal, we calculate 2↑306 = (2↑76)↑4 · 4≡5↑4 · 4 = 2𝑁 − 18, 2↑612 = (2↑306)↑2≡18↑2 = 324, 2↑629 = 2↑612 · 2↑17≡324 · 136 = 35𝑁 − 1 and finally 2↑(𝑁 − 1) = (2↑629)↑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.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Theorem	1259lem5 13274	Lemma for 1259prm 13275. Calculate the GCD of 2↑34 − 1≡869 with 𝑁 = 1259. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ (((2↑;34) − 1) gcd 𝑁) = 1
Theorem	1259prm 13275	1259 is a prime number. (Contributed by Mario Carneiro, 22-Feb-2014.) (Proof shortened by Mario Carneiro, 20-Apr-2015.)
⊢ 𝑁 = ;;;1259    ⇒   ⊢ 𝑁 ∈ ℙ
5.2.16  Bertrand's Ballot Problem
Theorem	ballotfilemofi 13276*	𝑂 is finite. (Contributed by Jim Kingdon, 20-May-2026.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ 𝑂 ∈ Fin
Theorem	ballotfilem1 13277*	The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀)
Theorem	ballotfilemonn 13278*	The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ (♯‘𝑂) ∈ ℕ
Theorem	ballotfilemelo 13279*	Elementhood in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   ⊢ (𝐶 ∈ 𝑂 ↔ (𝐶 ⊆ (1...(𝑀 + 𝑁)) ∧ 𝐶 ∈ Fin ∧ (♯‘𝐶) = 𝑀))
Theorem	ballotfilemcdc 13280*	Lemma for ballotfi . It is decidable whether a given integer is an element of a particular element of 𝑂. (Contributed by Jim Kingdon, 7-Jun-2026.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → DECID 𝐾 ∈ 𝐶)
Theorem	ballotfilemcinfi 13281*	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.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((1...𝐽) ∩ 𝐶) ∈ Fin)
Theorem	ballotfilemdifcfi 13282*	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.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((1...𝐽) ∖ 𝐶) ∈ Fin)
Theorem	ballotfilemcinfz 13283*	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.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐽...𝐾) ∩ 𝐶) ∈ Fin)
Theorem	ballotfilemdifcfz 13284*	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.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐽...𝐾) ∖ 𝐶) ∈ Fin)
Theorem	ballotfilem2 13285*	The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    ⇒   ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁))
Theorem	ballotfilemfval 13286*	The value of 𝐹. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶))))
Theorem	ballotfilemfelz 13287*	(𝐹‘𝐶) has values in ℤ. (Contributed by Thierry Arnoux, 23-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℤ)    ⇒   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ)
Theorem	ballotfilemfp1 13288*	If the 𝐽 th ballot is for A, (𝐹‘𝐶) goes up 1. If the 𝐽 th ballot is for B, (𝐹‘𝐶) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((¬ 𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1)) ∧ (𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1))))
Theorem	ballotfilemfc0 13289*	𝐹 takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0)    &   ⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽))    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
Theorem	ballotfilemfcc 13290*	𝐹 takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ (𝜑 → 𝐶 ∈ 𝑂)    &   ⊢ (𝜑 → 𝐽 ∈ ℕ)    &   ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖))    &   ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) < 0)    ⇒   ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0)
Theorem	ballotfilemfmpn 13291*	(𝐹‘𝐶) finishes counting at (𝑀 − 𝑁). (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    ⇒   ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘(𝑀 + 𝑁)) = (𝑀 − 𝑁))
Theorem	ballotfilemfval0 13292*	(𝐹‘𝐶) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    ⇒   ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0)
Theorem	ballotfileme 13293*	Elements of 𝐸. (Contributed by Thierry Arnoux, 14-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖)))
Theorem	ballotfilemefi 13294*	𝐸 is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ 𝐸 ∈ Fin
Theorem	ballotfilemafi 13295*	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.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ 1 ∈ 𝑐} ∈ Fin
Theorem	ballotfilembfi 13296*	The set of countings where B got the first vote is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ {𝑐 ∈ (𝑂 ∖ 𝐸) ∣ ¬ 1 ∈ 𝑐} ∈ Fin
Theorem	ballotfilemodife 13297*	Elements of (𝑂 ∖ 𝐸). (Contributed by Thierry Arnoux, 7-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0))
Theorem	ballotfilem4 13298*	If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   ⊢ (𝐶 ∈ 𝑂 → (¬ 1 ∈ 𝐶 → ¬ 𝐶 ∈ 𝐸))
Theorem	ballotfilem5 13299*	If A is not ahead throughout, there is a 𝑘 where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑘 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑘) = 0)
Theorem	ballotfilemi 13300*	Value of 𝐼 for a given counting 𝐶. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.)
⊢ 𝑀 ∈ ℕ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   ⊢ 𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   ⊢ 𝑁 < 𝑀    &   ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    ⇒   ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) = inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < ))