Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs 		 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100
Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 10-Jul-2026 at 7:15 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
29-Jun-2026dichmul0or 16643 Real number dichotomy is equivalent to the zero product principle for complex numbers: if a product is zero, one of its factors must be zero. (Contributed by Matthew House, 29-Jun-2026.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥) ↔ ∀𝑧 ∈ ℂ ∀𝑤 ∈ ℂ ((𝑧 · 𝑤) = 0 → (𝑧 = 0 ∨ 𝑤 = 0)))
 
29-Jun-2026dichmul0orlem5 16640 Lemma for dichmul0or 16643. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → ((abs‘𝐴) + 𝐴) = 0)    ⇒   (𝜑 → 𝐴 ≤ 0)
 
29-Jun-2026dichmul0orlem4 16639 Lemma for dichmul0or 16643. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    ⇒   (𝜑 → (((abs‘𝐴) + 𝐴) · ((abs‘𝐴) − 𝐴)) = 0)
 
29-Jun-2026dichmul0orlem3 16638 Lemma for dichmul0or 16643. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))    &   (𝜑 → 𝐴 ∈ ℂ)    &   (𝜑 → 𝐵 ∈ ℂ)    &   (𝜑 → (𝐴 · 𝐵) = 0)    ⇒   (𝜑 → (𝐴 = 0 ∨ 𝐵 = 0))
 
29-Jun-2026dichmul0orlem2 16637 Lemma for dichmul0or 16643. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℂ)    &   (𝜑 → 𝐵 ∈ ℂ)    &   (𝜑 → (𝐴 · 𝐵) = 0)    &   (𝜑 → (abs‘𝐴) ≤ (abs‘𝐵))    ⇒   (𝜑 → 𝐴 = 0)
 
29-Jun-2026dichmul0orlem1 16636 Lemma for dichmul0or 16643. (Contributed by Matthew House, 29-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → (𝐴 · 𝐵) = 0)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑 → 𝐴 ≤ 𝐵)    ⇒   (𝜑 → 𝐴 = 0)
 
29-Jun-2026lealltlt2 16635 Alternative definition for ≤ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ (𝐵 < 𝑥 → 𝐴 < 𝑥)))
 
29-Jun-2026lealltlt1 16634 Alternative definition for ≤ on real numbers. (Contributed by Matthew House, 29-Jun-2026.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ∀𝑥 ∈ ℝ (𝑥 < 𝐴 → 𝑥 < 𝐵)))
 
28-Jun-2026dichmul0orlem7 16642 Lemma for dichmul0or 16643. (Contributed by Matthew House, 28-Jun-2026.)
(𝜑 → ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ ((𝑥 · 𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0)))    &   (𝜑 → 𝐴 ∈ ℝ)    ⇒   (𝜑 → (𝐴 ≤ 0 ∨ 0 ≤ 𝐴))
 
28-Jun-2026dichmul0orlem6 16641 Lemma for dichmul0or 16643. (Contributed by Matthew House, 28-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → ((abs‘𝐴) − 𝐴) = 0)    ⇒   (𝜑 → 0 ≤ 𝐴)
 
28-Jun-2026msq0 8961 A number is zero iff its square is zero. (Contributed by Matthew House, 28-Jun-2026.)
(𝐴 ∈ ℂ → ((𝐴 · 𝐴) = 0 ↔ 𝐴 = 0))
 
28-Jun-2026msqap0 8960 A number is apart from zero iff its square is apart from zero. (Contributed by Matthew House, 28-Jun-2026.)
(𝐴 ∈ ℂ → ((𝐴 · 𝐴) # 0 ↔ 𝐴 # 0))
 
28-Jun-2026letrid 8406 Tightness of real apartness. (Contributed by Matthew House, 28-Jun-2026.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝐴 ≤ 𝐵)    &   (𝜑 → 𝐵 ≤ 𝐴)    ⇒   (𝜑 → 𝐴 = 𝐵)
 
19-Jun-2026ringen1zr0 14563 The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 14204, and semirings, see srgen1zr0 14234. (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    &   𝑍 = (0g‘𝑅)    ⇒   ((𝑅 ∈ Ring ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
19-Jun-2026srg1zr 14233 The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ SRing ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
18-Jun-2026rngen1zr0 14204 The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    &    0 = (0g‘𝑅)    ⇒   ((𝑅 ∈ Rng ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨ 0 , 0 ⟩, 0 ⟩} ∧ ∗ = {⟨⟨ 0 , 0 ⟩, 0 ⟩})))
 
18-Jun-2026rngen1zr 14203 The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ Rng ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 ≈ 1o ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
18-Jun-2026rng1zr 14202 The only ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ Rng ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
18-Jun-2026rng1zrlem 14201 Lemma for rng1zr 14202 and srg1zr 14233. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.)
𝐵 = (Base‘𝑅)    &    + = (+g‘𝑅)    &    ∗ = (.r‘𝑅)    ⇒   (((𝑅 ∈ Mgm ∧ (mulGrp‘𝑅) ∈ Mgm) ∧ ( + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩} ∧ ∗ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩})))
 
17-Jun-2026ballotfi 13229 Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) (Revised by Jim Kingdon, 17-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    ⇒   (𝑃‘𝐸) = ((𝑀 − 𝑁) / (𝑀 + 𝑁))
 
17-Jun-2026ballotfilembfi 13186 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
 
17-Jun-2026ballotfilemafi 13185 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
 
17-Jun-2026ballotfilemefi 13184 𝐸 is finite. (Contributed by Jim Kingdon, 17-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    ⇒   𝐸 ∈ Fin
 
17-Jun-2026rabxmdc 3544 Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Jim Kingdon, 17-Jun-2026.)
(∀𝑥 ∈ 𝐴 DECID 𝜑 → 𝐴 = ({𝑥 ∈ 𝐴 ∣ 𝜑} ∪ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}))
 
15-Jun-2026ballotfilemgun 13215 A property of the defined ↑ operator. (Contributed by Thierry Arnoux, 26-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    &   𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &    ↑ = (𝑢 ∈ 𝑂, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    &   (𝜑 → 𝑈 ∈ 𝑂)    &   (𝜑 → 𝐿 ∈ (𝐽...𝐾))    ⇒   (𝜑 → (𝑈 ↑ (𝐽...𝐾)) = ((𝑈 ↑ (𝐽...(𝐿 − 1))) + (𝑈 ↑ (𝐿...𝐾))))
 
15-Jun-2026ballotfilemgval 13214 Expand the value of ↑. (Contributed by Thierry Arnoux, 21-Apr-2017.) (Revised by Jim Kingdon, 15-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    &   𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖)))    &   𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐))    &    ↑ = (𝑢 ∈ 𝑂, 𝑣 ∈ Fin ↦ ((♯‘(𝑣 ∩ 𝑢)) − (♯‘(𝑣 ∖ 𝑢))))    &   (𝜑 → 𝑈 ∈ 𝑂)    &   (𝜑 → 𝐽 ∈ ℤ)    &   (𝜑 → 𝐾 ∈ ℤ)    &   (𝜑 → 𝑉 = (𝐽...𝐾))    ⇒   (𝜑 → (𝑈 ↑ 𝑉) = ((♯‘(𝑉 ∩ 𝑈)) − (♯‘(𝑉 ∖ 𝑈))))
 
15-Jun-2026ballotfilemdifcfz 13174 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)
 
15-Jun-2026ballotfilemcinfz 13173 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)
 
12-Jun-2026ballotfilemsle 13195 The infimum of the set of zeroes of 𝐹 is a lower bound. (Contributed by Jim Kingdon, 12-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    &   𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   𝑆 = {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}    ⇒   ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝑋 ∈ 𝑆) → inf(𝑆, ℝ, < ) ≤ 𝑋)
 
12-Jun-2026ballotfilemscl 13194 The set of zeroes of 𝐹 has an infimum. (Contributed by Jim Kingdon, 12-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    &   𝑃 = (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↦ ((♯‘𝑥) / (♯‘𝑂)))    &   𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐)))))    &   𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)}    &   𝑁 < 𝑀    &   𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < ))    &   𝑆 = {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}    ⇒   (𝐶 ∈ (𝑂 ∖ 𝐸) → inf(𝑆, ℝ, < ) ∈ 𝑆)
 
12-Jun-2026infssfzledc 10622 The infimum of a decidable inhabited subset of an integer range is a lower bound for that set. (Contributed by Jim Kingdon, 12-Jun-2026.)
𝑆 = {𝑛 ∈ (𝑀...𝑁) ∣ 𝜓}    &   (𝜑 → 𝐴 ∈ 𝑆)    &   ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   (𝜑 → inf(𝑆, ℝ, < ) ≤ 𝐴)
 
12-Jun-2026infssfzcldc 10621 The infimum of a decidable inhabited subset of an integer range is a member of the set. (Contributed by Jim Kingdon, 12-Jun-2026.)
𝑆 = {𝑛 ∈ (𝑀...𝑁) ∣ 𝜓}    &   (𝜑 → 𝐴 ∈ 𝑆)    &   ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   (𝜑 → inf(𝑆, ℝ, < ) ∈ 𝑆)
 
8-Jun-2026ballotfilemdifcfi 13172 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)
 
8-Jun-2026ballotfilemcinfi 13171 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)
 
8-Jun-2026zfidc 9676 Whether an integer is an element of a finite set of integers is decidable. (Contributed by Jim Kingdon, 8-Jun-2026.)
((𝑆 ⊆ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑆 ∈ Fin) → DECID 𝐴 ∈ 𝑆)
 
7-Jun-2026ballotfilemcdc 13170 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 𝐾 ∈ 𝐶)
 
5-Jun-2026hashpwfi 11221 The number of finite subsets of a finite set is two raised to the power of the size of the set. For a similar theorem with set size expressed using equinumerosity, see 2omapfi 7284. For the number of subsets (which need not be finite) of a set, see pw1mapen 16909. (Contributed by Jim Kingdon, 5-Jun-2026.)
(𝐴 ∈ Fin → (♯‘(𝒫 𝐴 ∩ Fin)) = (2↑(♯‘𝐴)))
 
4-Jun-2026ballotfilemonn 13168 The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   (♯‘𝑂) ∈ ℕ
 
3-Jun-2026papeq2 7574 Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
(𝐴 = 𝐵 → (𝑅 Ap 𝐴 ↔ 𝑅 Ap 𝐵))
 
3-Jun-2026papeq1 7573 Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.)
(𝑅 = 𝑆 → (𝑅 Ap 𝐴 ↔ 𝑆 Ap 𝐴))
 
2-Jun-2026resq01 11047 If a real number equals its square, it must be 0 or 1. (Contributed by Jim Kingdon, 2-Jun-2026.)
(𝐴 ∈ ℝ → ((𝐴↑2) = 𝐴 ↔ (𝐴 = 0 ∨ 𝐴 = 1)))
 
31-May-2026aprprop 14542 If two structures have the same ring components (properties), df-apr 14531 generates the same relation for both of them. (Contributed by Jim Kingdon, 31-May-2026.)
(Base‘𝐾) = (Base‘𝐿)    &   (+g‘𝐾) = (+g‘𝐿)    &   (.r‘𝐾) = (.r‘𝐿)    ⇒   (𝐾 ∈ Ring → (#r‘𝐾) = (#r‘𝐿))
 
31-May-2026ringunitsap0 14535 The set of units of a ring. If 𝑅 is a local ring, # is an apartness and this theorem states that the units of a ring are those elements apart from zero (see aprlring 14541). Given the definition of #r this theorem holds even if # is not an apartness, however. (Contributed by Jim Kingdon, 31-May-2026.)
𝐵 = (Base‘𝑅)    &    0 = (0g‘𝑅)    &    # = (#r‘𝑅)    ⇒   (𝑅 ∈ Ring → {𝑥 ∈ 𝐵 ∣ 𝑥 # 0 } = (Unit‘𝑅))
 
30-May-2026ringunitap 14534 Elementhood in the set of units. (Contributed by Jim Kingdon, 30-May-2026.)
𝐵 = (Base‘𝑅)    &   𝑈 = (Unit‘𝑅)    &    0 = (0g‘𝑅)    &    # = (#r‘𝑅)    ⇒   (𝑅 ∈ Ring → (𝑋 ∈ 𝑈 ↔ (𝑋 ∈ 𝐵 ∧ 𝑋 # 0 )))
 
29-May-2026drnglring 14548 A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.)
(𝑅 ∈ DivRing → 𝑅 ∈ LRing)
 
29-May-2026isdrngtap 14547 The predicate "is a division ring". (Contributed by Jim Kingdon, 29-May-2026.)
𝐵 = (Base‘𝑅)    &    # = (#r‘𝑅)    ⇒   (𝑅 ∈ DivRing ↔ (𝑅 ∈ Ring ∧ # TAp 𝐵))
 
29-May-2026df-drngap 14545 Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14531 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.)
DivRing = {𝑟 ∈ Ring ∣ (#r‘𝑟) TAp (Base‘𝑟)}
 
29-May-2026aprunit 14533 The df-apr 14531 relation with zero expresses whether a ring element is a unit. That is, the difference of an element of a ring and zero is invertible iff the element is a unit. (Contributed by Jim Kingdon, 29-May-2026.)
𝐵 = (Base‘𝑅)    &    0 = (0g‘𝑅)    &   𝑈 = (Unit‘𝑅)    &    # = (#r‘𝑅)    &   (𝜑 → 𝑅 ∈ Ring)    &   (𝜑 → 𝑋 ∈ 𝐵)    ⇒   (𝜑 → (𝑋 # 0 ↔ 𝑋 ∈ 𝑈))
 
29-May-2026tapap 7580 A tight apartness is an apartness. (Contributed by Jim Kingdon, 29-May-2026.)
(𝑅 TAp 𝐴 → 𝑅 Ap 𝐴)
 
28-May-2026aprlring 14541 A ring is a local ring if and only if the relation given by df-apr 14531 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.)
(𝑅 ∈ Ring → (𝑅 ∈ LRing ↔ (#r‘𝑅) Ap (Base‘𝑅)))
 
28-May-2026papcotr 7577 An apartness is cotransitive. (Contributed by Jim Kingdon, 28-May-2026.)
(𝜑 → 𝑅 Ap 𝐴)    &   (𝜑 → 𝑋 ∈ 𝐴)    &   (𝜑 → 𝑌 ∈ 𝐴)    &   (𝜑 → 𝑋𝑅𝑌)    &   (𝜑 → 𝑍 ∈ 𝐴)    ⇒   (𝜑 → (𝑋𝑅𝑍 ∨ 𝑌𝑅𝑍))
 
27-May-2026trimul0or 16984 Real number trichotomy implies that if a product is zero, one of its factors must be zero. (Contributed by Jim Kingdon, 27-May-2026.)
(∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 < 𝑥) → ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ ((𝑢 · 𝑣) = 0 → (𝑢 = 0 ∨ 𝑣 = 0)))
 
27-May-2026aprnzr 14540 If the relation given by df-apr 14531 on a ring is an apartness relation, then the ring is a nonzero ring. (Contributed by Jim Kingdon, 27-May-2026.)
((𝑅 ∈ Ring ∧ (#r‘𝑅) Ap (Base‘𝑅)) → 𝑅 ∈ NzRing)
 
27-May-2026papsym 7576 An apartness is symmetric. (Contributed by Jim Kingdon, 27-May-2026.)
(𝜑 → 𝑅 Ap 𝐴)    &   (𝜑 → 𝑋 ∈ 𝐴)    &   (𝜑 → 𝑌 ∈ 𝐴)    &   (𝜑 → 𝑋𝑅𝑌)    ⇒   (𝜑 → 𝑌𝑅𝑋)
 
27-May-2026papirr 7575 An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.)
((𝑅 Ap 𝐴 ∧ 𝑋 ∈ 𝐴) → ¬ 𝑋𝑅𝑋)
 
24-May-2026gfsumz 14112 Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.)
0 = (0g‘𝐺)    ⇒   ((𝐺 ∈ CMnd ∧ 𝐴 ∈ Fin) → (𝐺 Σgf (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
 
22-May-2026sshashneg 11233 Subsets of a class of a negative size (a degenerate case). Together with ssenneg 11232 this shows that sseqn 11231 could not be extended beyond 𝑁 ∈ ℕ0. (Contributed by Jim Kingdon, 22-May-2026.)
((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁} = ∅)
 
22-May-2026ssenneg 11232 Subsets of a class of a negative size (a degenerate case). Together with sshashneg 11233 this shows that sseqn 11231 could not be extended beyond 𝑁 ∈ ℕ0. (Contributed by Jim Kingdon, 22-May-2026.)
((𝑁 ∈ ℤ ∧ 𝑁 < 0) → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {∅})
 
22-May-2026sseqn 11231 Two ways to express the subsets of a class of a given size. It might seem that {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑁} would suffice, but that would require the converse of hashcl 11172 or something similar. Although each side of the equality would be well defined if we changed 𝑁 ∈ ℕ0 to 𝑁 ∈ ℤ, they would give different results for the (degenerate) case of a negative size, as shown at ssenneg 11232 and sshashneg 11233. (Contributed by Jim Kingdon, 22-May-2026.)
(𝑁 ∈ ℕ0 → {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≈ (1...𝑁)} = {𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∣ (♯‘𝑥) = 𝑁})
 
20-May-2026ballotfilemofi 13166 𝑂 is finite. (Contributed by Jim Kingdon, 20-May-2026.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝑂 = {𝑐 ∈ (𝒫 (1...(𝑀 + 𝑁)) ∩ Fin) ∣ (♯‘𝑐) = 𝑀}    ⇒   𝑂 ∈ Fin
 
19-May-2026fipwfi 7285 The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.)
(𝐴 ∈ Fin → (𝒫 𝐴 ∩ Fin) ∈ Fin)
 
18-May-20262omapfi 7284 The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11167), see hashpwfi 11221. (Contributed by Jim Kingdon, 18-May-2026.)
(𝐴 ∈ Fin → (2o ↑𝑚 𝐴) ≈ (𝒫 𝐴 ∩ Fin))
 
18-May-2026fissfi 7229 A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.)
((𝑆 ⊆ 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝑆 ∈ Fin) → ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝑆)
 
18-May-2026fresaunres1disj 5551 From the union of two functions with disjoint domains, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015.) (Revised by Jim Kingdon, 18-May-2026.)
((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹)
 
18-May-2026fresaunres2disj 5550 From the union of two functions with disjoint domains, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Jim Kingdon, 18-May-2026.)
((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐹 ∪ 𝐺) ↾ 𝐵) = 𝐺)
 
15-May-2026fsuppcorn 7267 The composition of a 1-1 function with a finitely supported function is finitely supported. The purpose of the (𝐹 supp 𝑍) ⊆ ran 𝐺 condition is to ensure we don't subset the support of the function in such a way as to fun afoul of exmidssfi 7212. (Other alternative conditions might also be sufficient). (Contributed by AV, 28-May-2019.) (Revised by Jim Kingdon, 15-May-2026.)
(𝜑 → 𝐹 finSupp 𝑍)    &   (𝜑 → 𝐺:𝑋–1-1→𝑌)    &   (𝜑 → 𝑍 ∈ 𝑊)    &   (𝜑 → 𝐹 ∈ 𝑉)    &   (𝜑 → 𝐺 ∈ 𝑈)    &   (𝜑 → (𝐹 supp 𝑍) ⊆ ran 𝐺)    ⇒   (𝜑 → (𝐹 ∘ 𝐺) finSupp 𝑍)
 
13-May-2026lincmble 10359 A linear combination of two reals which lies in the interval between them. Like lincmb01cmp 10358 but generalized to require merely 𝐴 ≤ 𝐵 not 𝐴 < 𝐵. (Contributed by Jim Kingdon, 13-May-2026.)
(((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐴) + (𝑇 · 𝐵)) ∈ (𝐴[,]𝐵))
 
5-May-2026fmelpw1o 7570 With a formula 𝜑 one can associate an element of 𝒫 1o, which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than ⊤ and ⊥, by nndc 859, which translate to 1o and ∅ respectively by iftrue 3631 and iffalse 3634, giving pwtrufal 16910).

As proved in if0ab 3627, the associated element of 𝒫 1o is the extension, in 𝒫 1o, of the formula 𝜑. (Contributed by BJ, 15-Aug-2024.) (Proof shortened by BJ, 5-May-2026.)

if(𝜑, 1o, ∅) ∈ 𝒫 1o
 
5-May-2026if0elpw 4276 A conditional class with the False alternative being sent to the empty class is an element of the powerset of the class corresponding to the True alternative when that class is a set. This statement requires fewer axioms than the general case ifelpwung 4607. (Contributed by BJ, 5-May-2026.)
(𝐴 ∈ 𝑉 → if(𝜑, 𝐴, ∅) ∈ 𝒫 𝐴)
 
5-May-2026if0ss 3628 A conditional class with the False alternative being sent to the empty class is included in the class corresponding to the True alternative. (Contributed by BJ, 5-May-2026.)
if(𝜑, 𝐴, ∅) ⊆ 𝐴
 
27-Apr-2026repiecef 16951 Piecewise definition on the reals yields a function. The function agrees with 𝐹 and 𝐺 on their respective parts of the real line; see repiecele0 16949 and repiecege0 16950. From an online post by James E Hanson. The construction was published in Martín Hötzel Escardó, "Effective and sequential definition by cases on the reals via infinite signed-digit numerals", Electronic Notes in Theoretical Computer Science 10 (1998), page 2, https://martinescardo.github.io/papers/lexnew.pdf. 16950 (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   (𝜑 → 𝐻:ℝ⟶ℝ)
 
27-Apr-2026repiecege0 16950 Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 16951 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ((𝜑 ∧ 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐻‘𝐴) = (𝐺‘𝐴))
 
27-Apr-2026repiecele0 16949 Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 16951 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ((𝜑 ∧ 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0) → (𝐻‘𝐴) = (𝐹‘𝐴))
 
27-Apr-2026repiecelem 16948 Lemma for repiecele0 16949, repiecege0 16950, and repiecef 16951. The function 𝐻 is defined everywhere. (Contributed by Jim Kingdon, 27-Apr-2026.)
(𝜑 → 𝐹:(-∞(,]0)⟶ℝ)    &   (𝜑 → 𝐺:(0[,)+∞)⟶ℝ)    &   (𝜑 → (𝐹‘0) = (𝐺‘0))    &   𝐻 = (𝑥 ∈ ℝ ↦ (((𝐹‘inf({𝑥, 0}, ℝ, < )) + (𝐺‘sup({𝑥, 0}, ℝ, < ))) − (𝐹‘0)))    ⇒   ((𝜑 ∧ 𝐴 ∈ ℝ) → (((𝐹‘inf({𝐴, 0}, ℝ, < )) + (𝐺‘sup({𝐴, 0}, ℝ, < ))) − (𝐹‘0)) ∈ ℝ)
 
24-Apr-2026qdiff 16972 The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to apdiff 16971 but by stating the result positively we can completely sidestep the issue of not equal versus apart in the statement of the result. From an online post by Ingo Blechschmidt. (Contributed by Jim Kingdon, 24-Apr-2026.)
(𝐴 ∈ ℝ → (𝐴 ∈ ℚ ↔ ∃𝑞 ∈ ℚ ∃𝑟 ∈ ℚ (𝑞 ≠ 𝑟 ∧ (abs‘(𝐴 − 𝑞)) = (abs‘(𝐴 − 𝑟)))))
 
23-Apr-2026exmidpeirce 16920 Excluded middle is equivalent to Peirce's law. Read an element of 𝒫 1o as being a truth value and 𝑥 = 1o being that 𝑥 is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfrompeirce 1495. (Contributed by Jim Kingdon, 23-Apr-2026.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1o∀𝑦 ∈ 𝒫 1o(((𝑥 = 1o → 𝑦 = 1o) → 𝑥 = 1o) → 𝑥 = 1o))
 
22-Apr-2026exmidcon 16919 Excluded middle is equivalent to the form of contraposition which removes negation. Read an element of 𝒫 1o as being a truth value and 𝑥 = 1o being that 𝑥 is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromcon 1494. (Contributed by Jim Kingdon, 22-Apr-2026.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1o∀𝑦 ∈ 𝒫 1o((¬ 𝑦 = 1o → ¬ 𝑥 = 1o) → (𝑥 = 1o → 𝑦 = 1o)))
 
22-Apr-2026exmidnotnotr 16918 Excluded middle is equivalent to double negation elimination. Read an element of 𝒫 1o as being a truth value and 𝑥 = 1o being that 𝑥 is true. For a similar theorem, but expressed in terms of formulas rather than subsets of 1o, see dcfromnotnotr 1493. (Contributed by Jim Kingdon, 22-Apr-2026.)
(EXMID ↔ ∀𝑥 ∈ 𝒫 1o(¬ ¬ 𝑥 = 1o → 𝑥 = 1o))
 
18-Apr-2026hashtpglem 11246 Lemma for hashtpg 11247. This is one of the three not-equal conclusions required for the reverse direction. (Contributed by Jim Kingdon, 18-Apr-2026.)
(𝜑 → 𝐴 ∈ 𝑈)    &   (𝜑 → 𝐵 ∈ 𝑉)    &   (𝜑 → 𝐶 ∈ 𝑊)    &   (𝜑 → (♯‘{𝐴, 𝐵, 𝐶}) = 3)    ⇒   (𝜑 → 𝐵 ≠ 𝐶)
 
17-Apr-2026hashtpgim 11245 The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.) (Revised by Jim Kingdon, 17-Apr-2026.)
((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴) → (♯‘{𝐴, 𝐵, 𝐶}) = 3))
 
14-Apr-2026depind 16633 Theorem related to a dependently typed induction principle in type theory. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    ⇒   (𝜑 → ∃!𝑓 ∈ X 𝑛 ∈ ℕ0 (𝑃‘𝑛)((𝑓‘0) = 𝐴 ∧ ∀𝑛 ∈ ℕ0 (𝑓‘(𝑛 + 1)) = ((𝐻‘𝑛)‘(𝑓‘𝑛))))
 
14-Apr-2026depindlem3 16632 Lemma for depind 16633. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → ∀𝑓 ∈ X 𝑛 ∈ ℕ0 (𝑃‘𝑛)(((𝑓‘0) = 𝐴 ∧ ∀𝑛 ∈ ℕ0 (𝑓‘(𝑛 + 1)) = ((𝐻‘𝑛)‘(𝑓‘𝑛))) → 𝑓 = 𝐹))
 
14-Apr-2026depindlem2 16631 Lemma for depind 16633. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → 𝐹 ∈ X𝑛 ∈ ℕ0 (𝑃‘𝑛))
 
14-Apr-2026depindlem1 16630 Lemma for depind 16633. (Contributed by Matthew House, 14-Apr-2026.)
(𝜑 → 𝑃:ℕ0⟶V)    &   (𝜑 → 𝐴 ∈ (𝑃‘0))    &   (𝜑 → ∀𝑛 ∈ ℕ0 (𝐻‘𝑛):(𝑃‘𝑛)⟶(𝑃‘(𝑛 + 1)))    &   𝐹 = seq0((𝑥 ∈ V, ℎ ∈ V ↦ (ℎ‘𝑥)), (𝑚 ∈ ℕ0 ↦ if(𝑚 = 0, 𝐴, (𝐻‘(𝑚 − 1)))))    ⇒   (𝜑 → (𝐹:ℕ0⟶V ∧ (𝐹‘0) = 𝐴 ∧ ∀𝑛 ∈ ℕ0 (𝐹‘(𝑛 + 1)) = ((𝐻‘𝑛)‘(𝐹‘𝑛))))
 
8-Apr-2026gfsumcl 14113 Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   (𝜑 → (𝐺 Σgf 𝐹) ∈ 𝐵)
 
4-Apr-2026gsumsplit0 14102 Splitting off the rightmost summand of a group sum (even if it is the only summand). Similar to gsumsplit1r 13664 except that 𝑁 can equal 𝑀 − 1. (Contributed by Jim Kingdon, 4-Apr-2026.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 − 1)))    &   (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ (𝑀...𝑁))) + (𝐹‘(𝑁 + 1))))
 
4-Apr-2026fzf1o 12089 A finite set can be enumerated by integers starting at one. (Contributed by Jim Kingdon, 4-Apr-2026.)
(𝐴 ∈ Fin → ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
 
3-Apr-2026gfsump1 14111 Splitting off one element from a finite group sum. This would typically used in a proof by induction. (Contributed by Jim Kingdon, 3-Apr-2026.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐹:(𝑌 ∪ {𝑍})⟶𝐵)    &   (𝜑 → 𝑌 ∈ Fin)    &   (𝜑 → 𝑍 ∈ 𝑉)    &   (𝜑 → ¬ 𝑍 ∈ 𝑌)    ⇒   (𝜑 → (𝐺 Σgf 𝐹) = ((𝐺 Σgf (𝐹 ↾ 𝑌)) + (𝐹‘𝑍)))
 
2-Apr-2026gfsumsn 14110 Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.)
𝐵 = (Base‘𝐺)    &   (𝑘 = 𝑀 → 𝐴 = 𝐶)    ⇒   ((𝐺 ∈ CMnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σgf (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶)
 
31-Mar-2026sspw1or2 7508 The set of subsets of a given set with one or two elements can be expressed as elements of the power set or as inhabited elements of the power set. (Contributed by Jim Kingdon, 31-Mar-2026.)
{𝑥 ∈ {𝑠 ∈ 𝒫 𝑉 ∣ ∃𝑗 𝑗 ∈ 𝑠} ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)} = {𝑥 ∈ 𝒫 𝑉 ∣ (𝑥 ≈ 1o ∨ 𝑥 ≈ 2o)}
 
28-Mar-2026imaf1fi 7206 The image of a finite set under a one-to-one mapping is finite. (Contributed by Jim Kingdon, 28-Mar-2026.)
((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝐹 “ 𝑋) ∈ Fin)
 
26-Mar-2026gsumshift 14108 Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    &   𝑆 = (𝑗 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑗 − (1 − 𝑀)))    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝑆)))
 
26-Mar-2026gfsum0 14107 An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.)
(𝐺 ∈ CMnd → (𝐺 Σgf ∅) = (0g‘𝐺))
 
25-Mar-2026gsumgfsum 14109 On an integer range, Σg and Σgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σgf 𝐹))
 
25-Mar-2026gsumgfsum1 14106 On an integer range starting at one, Σg and Σgf agree. (Contributed by Jim Kingdon, 25-Mar-2026.)
𝐵 = (Base‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑁 ∈ ℕ0)    &   (𝜑 → 𝐹:(1...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σgf 𝐹))
 
24-Mar-2026gfsumval 14105 Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.)
𝐵 = (Base‘𝑊)    &   (𝜑 → 𝑊 ∈ CMnd)    &   (𝜑 → 𝐹:𝐴⟶𝐵)    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐺:(1...(♯‘𝐴))–1-1-onto→𝐴)    ⇒   (𝜑 → (𝑊 Σgf 𝐹) = (𝑊 Σg (𝐹 ∘ 𝐺)))
 
23-Mar-2026df-gfsum 14104 Define the finite group sum (iterated sum) over an unordered finite set.

Given 𝐺 Σgf 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. For this notation, 𝐴 is a finite set and 𝐺 is a commutative monoid, and the sum adds up these elements in some order (the sum does not depend on the order).

For a sum indexed by consecutive integers (and thus defining an order for the sum), see df-igsum 13559. (Contributed by Jim Kingdon, 23-Mar-2026.)

Σgf = (𝑤 ∈ CMnd, 𝑓 ∈ V ↦ (℩𝑥(dom 𝑓 ∈ Fin ∧ ∃𝑔(𝑔:(1...(♯‘dom 𝑓))–1-1-onto→dom 𝑓 ∧ 𝑥 = (𝑤 Σg (𝑓 ∘ 𝑔))))))
 
20-Mar-2026exmidssfi 7212 Excluded middle is equivalent to any subset of a finite set being finite. Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 20-Mar-2026.)
(EXMID ↔ ∀𝑥∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin))
 
18-Mar-2026umgr1een 16249 A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UMGraph)
 
18-Mar-2026upgr1een 16248 A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16245 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.)
(𝜑 → 𝐾 ∈ 𝑋)    &   (𝜑 → 𝑉 ∈ 𝑌)    &   (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   (𝜑 → 𝐸 ≈ 2o)    ⇒   (𝜑 → ⟨𝑉, {⟨𝐾, 𝐸⟩}⟩ ∈ UPGraph)
  Copyright terms: Public domain W3C HTML validation [external]