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 8-Dec-2025 at 7:14 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
30-Nov-2025nninfnfiinf 15756 An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.)
((𝐴 ∈ ℕ∞ ∧ ¬ ∃𝑛 ∈ ω 𝐴 = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) → 𝐴 = (𝑖 ∈ ω ↦ 1o))
 
25-Nov-2025nninfinfwlpo 7255 The point at infinity in ℕ∞ being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO). By isolated, we mean that the equality of that point with every other element of ℕ∞ is decidable. From an online post by Martin Escardo. By contrast, elements of ℕ∞ corresponding to natural numbers are isolated (nninfisol 7208). (Contributed by Jim Kingdon, 25-Nov-2025.)
(∀𝑥 ∈ ℕ∞ DECID 𝑥 = (𝑖 ∈ ω ↦ 1o) ↔ ω ∈ WOmni)
 
22-Nov-2025df-acnm 7260 Define a local and length-limited version of the axiom of choice. The definition of the predicate 𝑋 ∈ AC 𝐴 is that for all families of inhabited subsets of 𝑋 indexed on 𝐴 (i.e. functions 𝐴⟶{𝑧 ∈ 𝒫 𝑋 ∣ ∃𝑗𝑗 ∈ 𝑧}), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.) Change nonempty to inhabited. (Revised by Jim Kingdon, 22-Nov-2025.)
AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ({𝑧 ∈ 𝒫 𝑥 ∣ ∃𝑗 𝑗 ∈ 𝑧} ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}
 
14-Nov-20252omapen 15729 Equinumerosity of (2o ↑𝑚 𝐴) and the set of decidable subsets of 𝐴. (Contributed by Jim Kingdon, 14-Nov-2025.)
(𝐴 ∈ 𝑉 → (2o ↑𝑚 𝐴) ≈ {𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑦 ∈ 𝐴 DECID 𝑦 ∈ 𝑥})
 
12-Nov-20252omap 15728 Mapping between (2o ↑𝑚 𝐴) and decidable subsets of 𝐴. (Contributed by Jim Kingdon, 12-Nov-2025.)
𝐹 = (𝑠 ∈ (2o ↑𝑚 𝐴) ↦ {𝑧 ∈ 𝐴 ∣ (𝑠‘𝑧) = 1o})    ⇒   (𝐴 ∈ 𝑉 → 𝐹:(2o ↑𝑚 𝐴)–1-1-onto→{𝑥 ∈ 𝒫 𝐴 ∣ ∀𝑦 ∈ 𝐴 DECID 𝑦 ∈ 𝑥})
 
11-Nov-2025domomsubct 15734 A set dominated by ω is subcountable. (Contributed by Jim Kingdon, 11-Nov-2025.)
(𝐴 ≼ ω → ∃𝑠(𝑠 ⊆ ω ∧ ∃𝑓 𝑓:𝑠–onto→𝐴))
 
10-Nov-2025prdsbaslemss 12978 Lemma for prdsbas 12980 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.)
𝑃 = (𝑆Xs𝑅)    &   (𝜑 → 𝑆 ∈ 𝑉)    &   (𝜑 → 𝑅 ∈ 𝑊)    &   𝐴 = (𝐸‘𝑃)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝐸‘ndx) ∈ ℕ    &   (𝜑 → 𝑇 ∈ 𝑋)    &   (𝜑 → {⟨(𝐸‘ndx), 𝑇⟩} ⊆ 𝑃)    ⇒   (𝜑 → 𝐴 = 𝑇)
 
1-Nov-2025ficardon 7269 The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.)
(𝐴 ∈ Fin → (card‘𝐴) ∈ On)
 
31-Oct-2025bitsdc 12131 Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.)
((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → DECID 𝑀 ∈ (bits‘𝑁))
 
28-Oct-2025nn0maxcl 11409 The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → sup({𝐴, 𝐵}, ℝ, < ) ∈ ℕ0)
 
28-Oct-2025qdcle 10355 Rational ≤ is decidable. (Contributed by Jim Kingdon, 28-Oct-2025.)
((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → DECID 𝐴 ≤ 𝐵)
 
17-Oct-2025plycoeid3 15079 Reconstruct a polynomial as an explicit sum of the coefficient function up to an index no smaller than the degree of the polynomial. (Contributed by Jim Kingdon, 17-Oct-2025.)
(𝜑 → 𝐷 ∈ ℕ0)    &   (𝜑 → 𝐴:ℕ0⟶ℂ)    &   (𝜑 → (𝐴 “ (ℤ≥‘(𝐷 + 1))) = {0})    &   (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝐷)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   (𝜑 → 𝑀 ∈ (ℤ≥‘𝐷))    &   (𝜑 → 𝑋 ∈ ℂ)    ⇒   (𝜑 → (𝐹‘𝑋) = Σ𝑗 ∈ (0...𝑀)((𝐴‘𝑗) · (𝑋↑𝑗)))
 
13-Oct-2025tpfidceq 7000 A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
(𝜑 → 𝐴 ∈ 𝐷)    &   (𝜑 → 𝐵 ∈ 𝐷)    &   (𝜑 → 𝐶 ∈ 𝐷)    &   (𝜑 → ∀𝑥 ∈ 𝐷 ∀𝑦 ∈ 𝐷 DECID 𝑥 = 𝑦)    ⇒   (𝜑 → {𝐴, 𝐵, 𝐶} ∈ Fin)
 
13-Oct-2025prfidceq 6998 A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.)
(𝜑 → 𝐴 ∈ 𝐶)    &   (𝜑 → 𝐵 ∈ 𝐶)    &   (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 DECID 𝑥 = 𝑦)    ⇒   (𝜑 → {𝐴, 𝐵} ∈ Fin)
 
13-Oct-2025dcun 3561 The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) (Revised by Jim Kingdon, 13-Oct-2025.)
(𝜑 → DECID 𝐶 ∈ 𝐴)    &   (𝜑 → DECID 𝐶 ∈ 𝐵)    ⇒   (𝜑 → DECID 𝐶 ∈ (𝐴 ∪ 𝐵))
 
9-Oct-2025dvdsfi 12434 A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.)
(𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin)
 
6-Oct-2025dvconstss 15020 Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.)
(𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   𝐽 = (𝐾 ↾t 𝑆)    &   𝐾 = (MetOpen‘(abs ∘ − ))    &   (𝜑 → 𝑋 ∈ 𝐽)    &   (𝜑 → 𝐴 ∈ ℂ)    ⇒   (𝜑 → (𝑆 D (𝑋 × {𝐴})) = (𝑋 × {0}))
 
6-Oct-2025dcfrompeirce 1460 The decidability of a proposition 𝜒 follows from a suitable instance of Peirce's law. Therefore, if we were to introduce Peirce's law as a general principle (without the decidability condition in peircedc 915), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since Perice's law is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
(𝜑 ↔ (𝜒 ∨ ¬ 𝜒))    &   (𝜓 ↔ ⊥)    &   (((𝜑 → 𝜓) → 𝜑) → 𝜑)    ⇒   DECID 𝜒
 
6-Oct-2025dcfromcon 1459 The decidability of a proposition 𝜒 follows from a suitable instance of the principle of contraposition. Therefore, if we were to introduce contraposition as a general principle (without the decidability condition in condc 854), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since the principle of contraposition is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
(𝜑 ↔ (𝜒 ∨ ¬ 𝜒))    &   (𝜓 ↔ ⊤)    &   ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))    ⇒   DECID 𝜒
 
6-Oct-2025dcfromnotnotr 1458 The decidability of a proposition 𝜓 follows from a suitable instance of double negation elimination (DNE). Therefore, if we were to introduce DNE as a general principle (without the decidability condition in notnotrdc 844), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since DNE itself is classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)
(𝜑 ↔ (𝜓 ∨ ¬ 𝜓))    &   (¬ ¬ 𝜑 → 𝜑)    ⇒   DECID 𝜓
 
3-Oct-2025dvidre 15019 Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.)
(ℝ D ( I ↾ ℝ)) = (ℝ × {1})
 
3-Oct-2025dvconstre 15018 Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.)
(𝐴 ∈ ℂ → (ℝ D (ℝ × {𝐴})) = (ℝ × {0}))
 
3-Oct-2025dvidsslem 15015 Lemma for dvconstss 15020. Analogue of dvidlemap 15013 where 𝐹 is defined on an open subset of the real or complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
(𝜑 → 𝑆 ∈ {ℝ, ℂ})    &   𝐽 = (𝐾 ↾t 𝑆)    &   𝐾 = (MetOpen‘(abs ∘ − ))    &   (𝜑 → 𝐹:𝑋⟶ℂ)    &   (𝜑 → 𝑋 ∈ 𝐽)    &   ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   𝐵 ∈ ℂ    ⇒   (𝜑 → (𝑆 D 𝐹) = (𝑋 × {𝐵}))
 
3-Oct-2025dvidrelem 15014 Lemma for dvidre 15019 and dvconstre 15018. Analogue of dvidlemap 15013 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.)
(𝜑 → 𝐹:ℝ⟶ℂ)    &   ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑧 # 𝑥)) → (((𝐹‘𝑧) − (𝐹‘𝑥)) / (𝑧 − 𝑥)) = 𝐵)    &   𝐵 ∈ ℂ    ⇒   (𝜑 → (ℝ D 𝐹) = (ℝ × {𝐵}))
 
28-Sep-2025metuex 14189 Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
(𝐴 ∈ 𝑉 → (metUnif‘𝐴) ∈ V)
 
28-Sep-2025cndsex 14187 The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.)
(abs ∘ − ) ∈ V
 
25-Sep-2025cntopex 14188 The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.)
(MetOpen‘(abs ∘ − )) ∈ V
 
24-Sep-2025mopnset 14186 Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
(𝐷 ∈ 𝑉 → (MetOpen‘𝐷) ∈ V)
 
24-Sep-2025blfn 14185 The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
ball Fn V
 
22-Sep-2025plycjlemc 15082 Lemma for plycj 15083. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.)
(𝜑 → 𝑁 ∈ ℕ0)    &   𝐺 = ((∗ ∘ 𝐹) ∘ ∗)    &   (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))    &   (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑧↑𝑘))))    &   (𝜑 → 𝐹 ∈ (Poly‘𝑆))    ⇒   (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))))
 
20-Sep-2025plycolemc 15080 Lemma for plyco 15081. The result expressed as a sum, with a degree and coefficients for 𝐹 specified as hypotheses. (Contributed by Jim Kingdon, 20-Sep-2025.)
(𝜑 → 𝐹 ∈ (Poly‘𝑆))    &   (𝜑 → 𝐺 ∈ (Poly‘𝑆))    &   ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆)    &   (𝜑 → 𝑁 ∈ ℕ0)    &   (𝜑 → 𝐴:ℕ0⟶(𝑆 ∪ {0}))    &   (𝜑 → (𝐴 “ (ℤ≥‘(𝑁 + 1))) = {0})    &   (𝜑 → 𝐹 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘))))    ⇒   (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))
 
16-Sep-2025lgsquadlemofi 15403 Lemma for lgsquad 15407. There are finitely many members of 𝑆 with odd first part. (Contributed by Jim Kingdon, 16-Sep-2025.)
(𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   (𝜑 → 𝑃 ≠ 𝑄)    &   𝑀 = ((𝑃 − 1) / 2)    &   𝑁 = ((𝑄 − 1) / 2)    &   𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   (𝜑 → {𝑧 ∈ 𝑆 ∣ ¬ 2 ∥ (1st ‘𝑧)} ∈ Fin)
 
16-Sep-2025lgsquadlemsfi 15402 Lemma for lgsquad 15407. 𝑆 is finite. (Contributed by Jim Kingdon, 16-Sep-2025.)
(𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   (𝜑 → 𝑄 ∈ (ℙ ∖ {2}))    &   (𝜑 → 𝑃 ≠ 𝑄)    &   𝑀 = ((𝑃 − 1) / 2)    &   𝑁 = ((𝑄 − 1) / 2)    &   𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (1...𝑀) ∧ 𝑦 ∈ (1...𝑁)) ∧ (𝑦 · 𝑃) < (𝑥 · 𝑄))}    ⇒   (𝜑 → 𝑆 ∈ Fin)
 
16-Sep-2025opabfi 7008 Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.)
𝑆 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜓)}    &   (𝜑 → 𝐴 ∈ Fin)    &   (𝜑 → 𝐵 ∈ Fin)    &   (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 DECID 𝜓)    ⇒   (𝜑 → 𝑆 ∈ Fin)
 
13-Sep-2025uchoice 6204 Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7292 (with the key difference being the change of ∃ to ∃!) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)
((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦𝜑) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑))
 
11-Sep-2025expghmap 14241 Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.)
𝑀 = (mulGrp‘ℂfld)    &   𝑈 = (𝑀 ↾s {𝑧 ∈ ℂ ∣ 𝑧 # 0})    ⇒   ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝑥 ∈ ℤ ↦ (𝐴↑𝑥)) ∈ (ℤring GrpHom 𝑈))
 
11-Sep-2025cnfldui 14223 The invertible complex numbers are exactly those apart from zero. This is recapb 8717 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.)
{𝑧 ∈ ℂ ∣ 𝑧 # 0} = (Unit‘ℂfld)
 
9-Sep-2025gsumfzfsumlemm 14221 Lemma for gsumfzfsum 14222. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.)
(𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐵 ∈ ℂ)    ⇒   (𝜑 → (ℂfld Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐵)) = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
 
9-Sep-2025gsumfzfsumlem0 14220 Lemma for gsumfzfsum 14222. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝑁 < 𝑀)    ⇒   (𝜑 → (ℂfld Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐵)) = Σ𝑘 ∈ (𝑀...𝑁)𝐵)
 
9-Sep-2025gsumfzmhm2 13552 Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐻 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ (𝐺 MndHom 𝐻))    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑋 ∈ 𝐵)    &   (𝑥 = 𝑋 → 𝐶 = 𝐷)    &   (𝑥 = (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝑋)) → 𝐶 = 𝐸)    ⇒   (𝜑 → (𝐻 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝐷)) = 𝐸)
 
8-Sep-2025gsumfzmhm 13551 Apply a monoid homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 8-Sep-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝐻 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻))    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐻 Σg (𝐾 ∘ 𝐹)) = (𝐾‘(𝐺 Σg 𝐹)))
 
8-Sep-20255ndvds6 12119 5 does not divide 6. (Contributed by AV, 8-Sep-2025.)
¬ 5 ∥ 6
 
8-Sep-20255ndvds3 12118 5 does not divide 3. (Contributed by AV, 8-Sep-2025.)
¬ 5 ∥ 3
 
6-Sep-2025gsumfzconst 13549 Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.)
𝐵 = (Base‘𝐺)    &    · = (.g‘𝐺)    ⇒   ((𝐺 ∈ Mnd ∧ 𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 𝑋)) = (((𝑁 − 𝑀) + 1) · 𝑋))
 
31-Aug-2025gsumfzmptfidmadd 13547 The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) (Revised by Jim Kingdon, 31-Aug-2025.)
𝐵 = (Base‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ CMnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐶 ∈ 𝐵)    &   ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐷 ∈ 𝐵)    &   𝐹 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐶)    &   𝐻 = (𝑥 ∈ (𝑀...𝑁) ↦ 𝐷)    ⇒   (𝜑 → (𝐺 Σg (𝑥 ∈ (𝑀...𝑁) ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))
 
30-Aug-2025gsumfzsubmcl 13546 Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 30-Aug-2025.)
(𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝑆)    ⇒   (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆)
 
30-Aug-2025seqm1g 10585 Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 30-Aug-2025.)
(𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))    &   (𝜑 → + ∈ 𝑉)    &   (𝜑 → 𝐹 ∈ 𝑊)    ⇒   (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = ((seq𝑀( + , 𝐹)‘(𝑁 − 1)) + (𝐹‘𝑁)))
 
29-Aug-2025seqf1og 10632 Rearrange a sum via an arbitrary bijection on (𝑀...𝑁). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 29-Aug-2025.)
((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆)    &   ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 𝑦) = (𝑦 + 𝑥))    &   ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   (𝜑 → 𝐶 ⊆ 𝑆)    &   (𝜑 → + ∈ 𝑉)    &   (𝜑 → 𝐹:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))    &   ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝐺‘𝑥) ∈ 𝐶)    &   ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐻‘𝑘) = (𝐺‘(𝐹‘𝑘)))    &   (𝜑 → 𝐺 ∈ 𝑊)    &   (𝜑 → 𝐻 ∈ 𝑋)    ⇒   (𝜑 → (seq𝑀( + , 𝐻)‘𝑁) = (seq𝑀( + , 𝐺)‘𝑁))
 
25-Aug-2025irrmulap 9741 The product of an irrational with a nonzero rational is irrational. By irrational we mean apart from any rational number. For a similar theorem with not rational in place of irrational, see irrmul 9740. (Contributed by Jim Kingdon, 25-Aug-2025.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → ∀𝑞 ∈ ℚ 𝐴 # 𝑞)    &   (𝜑 → 𝐵 ∈ ℚ)    &   (𝜑 → 𝐵 ≠ 0)    &   (𝜑 → 𝑄 ∈ ℚ)    ⇒   (𝜑 → (𝐴 · 𝐵) # 𝑄)
 
19-Aug-2025seqp1g 10577 Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝐹 ∈ 𝑉 ∧ + ∈ 𝑊) → (seq𝑀( + , 𝐹)‘(𝑁 + 1)) = ((seq𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 + 1))))
 
19-Aug-2025seq1g 10574 Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.)
((𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ∧ + ∈ 𝑊) → (seq𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
 
18-Aug-2025iswrdiz 10961 A zero-based sequence is a word. In iswrdinn0 10959 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)
((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℤ) → 𝑊 ∈ Word 𝑆)
 
16-Aug-2025gsumfzcl 13203 Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &   (𝜑 → 𝐺 ∈ Mnd)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
 
16-Aug-2025iswrdinn0 10959 A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)
((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℕ0) → 𝑊 ∈ Word 𝑆)
 
15-Aug-2025gsumfzz 13199 Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 15-Aug-2025.)
0 = (0g‘𝐺)    ⇒   ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = 0 )
 
14-Aug-2025gsumfzval 13095 An expression for Σg when summing over a finite set of sequential integers. (Contributed by Jim Kingdon, 14-Aug-2025.)
𝐵 = (Base‘𝐺)    &    0 = (0g‘𝐺)    &    + = (+g‘𝐺)    &   (𝜑 → 𝐺 ∈ 𝑉)    &   (𝜑 → 𝑀 ∈ ℤ)    &   (𝜑 → 𝑁 ∈ ℤ)    &   (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   (𝜑 → (𝐺 Σg 𝐹) = if(𝑁 < 𝑀, 0 , (seq𝑀( + , 𝐹)‘𝑁)))
 
13-Aug-2025znidom 14291 The ℤ/nℤ structure is an integral domain when 𝑛 is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
𝑌 = (ℤ/nℤ‘𝑁)    ⇒   (𝑁 ∈ ℙ → 𝑌 ∈ IDomn)
 
12-Aug-2025rrgmex 13895 A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.)
𝐸 = (RLReg‘𝑅)    ⇒   (𝐴 ∈ 𝐸 → 𝑅 ∈ V)
 
10-Aug-2025gausslemma2dlem1cl 15386 Lemma for gausslemma2dlem1 15388. Closure of the body of the definition of 𝑅. (Contributed by Jim Kingdon, 10-Aug-2025.)
(𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    &   (𝜑 → 𝐴 ∈ (1...𝐻))    ⇒   (𝜑 → if((𝐴 · 2) < (𝑃 / 2), (𝐴 · 2), (𝑃 − (𝐴 · 2))) ∈ ℤ)
 
9-Aug-2025gausslemma2dlem1f1o 15387 Lemma for gausslemma2dlem1 15388. (Contributed by Jim Kingdon, 9-Aug-2025.)
(𝜑 → 𝑃 ∈ (ℙ ∖ {2}))    &   𝐻 = ((𝑃 − 1) / 2)    &   𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))    ⇒   (𝜑 → 𝑅:(1...𝐻)–1-1-onto→(1...𝐻))
 
7-Aug-2025qdclt 10354 Rational < is decidable. (Contributed by Jim Kingdon, 7-Aug-2025.)
((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℚ) → DECID 𝐴 < 𝐵)
 
22-Jul-2025ivthdich 14975 The intermediate value theorem implies real number dichotomy. Because real number dichotomy (also known as analytic LLPO) is a constructive taboo, this means we will be unable to prove the intermediate value theorem as stated here (although versions with additional conditions, such as ivthinc 14965 for strictly monotonic functions, can be proved).

The proof is via a function which we call the hover function and which is also described in Section 5.1 of [Bauer], p. 493. Consider any real number 𝑧. We want to show that 𝑧 ≤ 0 ∨ 0 ≤ 𝑧. Because of hovercncf 14968, hovera 14969, and hoverb 14970, we are able to apply the intermediate value theorem to get a value 𝑐 such that the hover function at 𝑐 equals 𝑧. By axltwlin 8113, 𝑐 < 1 or 0 < 𝑐, and that leads to 𝑧 ≤ 0 by hoverlt1 14971 or 0 ≤ 𝑧 by hovergt0 14972. (Contributed by Jim Kingdon and Mario Carneiro, 22-Jul-2025.)

(∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))) → ∀𝑟 ∈ ℝ ∀𝑠 ∈ ℝ (𝑟 ≤ 𝑠 ∨ 𝑠 ≤ 𝑟))
 
22-Jul-2025dich0 14974 Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
(∀𝑧 ∈ ℝ (𝑧 ≤ 0 ∨ 0 ≤ 𝑧) ↔ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥))
 
22-Jul-2025ivthdichlem 14973 Lemma for ivthdich 14975. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    &   (𝜑 → 𝑍 ∈ ℝ)    &   (𝜑 → ∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))))    ⇒   (𝜑 → (𝑍 ≤ 0 ∨ 0 ≤ 𝑍))
 
22-Jul-2025hovergt0 14972 The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ((𝐶 ∈ ℝ ∧ 0 < 𝐶) → 0 ≤ (𝐹‘𝐶))
 
22-Jul-2025hoverlt1 14971 The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   ((𝐶 ∈ ℝ ∧ 𝐶 < 1) → (𝐹‘𝐶) ≤ 0)
 
21-Jul-2025hoverb 14970 A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   (𝑍 ∈ ℝ → 𝑍 < (𝐹‘(𝑍 + 2)))
 
21-Jul-2025hovera 14969 A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   (𝑍 ∈ ℝ → (𝐹‘(𝑍 − 1)) < 𝑍)
 
21-Jul-2025rexeqtrrdv 2704 Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐵 = 𝐴)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
 
21-Jul-2025raleqtrrdv 2703 Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐵 = 𝐴)    ⇒   (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
 
21-Jul-2025rexeqtrdv 2702 Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∃𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐴 = 𝐵)    ⇒   (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)
 
21-Jul-2025raleqtrdv 2701 Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.)
(𝜑 → ∀𝑥 ∈ 𝐴 𝜓)    &   (𝜑 → 𝐴 = 𝐵)    ⇒   (𝜑 → ∀𝑥 ∈ 𝐵 𝜓)
 
20-Jul-2025hovercncf 14968 The hover function is continuous. By hover function, we mean a a function which starts out as a line of slope one, is constant at zero from zero to one, and then resumes as a slope of one. (Contributed by Jim Kingdon, 20-Jul-2025.)
𝐹 = (𝑥 ∈ ℝ ↦ sup({inf({𝑥, 0}, ℝ, < ), (𝑥 − 1)}, ℝ, < ))    ⇒   𝐹 ∈ (ℝ–cn→ℝ)
 
19-Jul-2025mincncf 14938 The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.)
(𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   (𝜑 → (𝑥 ∈ 𝑋 ↦ inf({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
 
18-Jul-2025maxcncf 14937 The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.)
(𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℝ))    &   (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℝ))    ⇒   (𝜑 → (𝑥 ∈ 𝑋 ↦ sup({𝐴, 𝐵}, ℝ, < )) ∈ (𝑋–cn→ℝ))
 
14-Jul-2025xnn0nnen 10548 The set of extended nonnegative integers is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 14-Jul-2025.)
ℕ0* ≈ ℕ
 
12-Jul-2025nninfninc 7198 All values beyond a zero in an ℕ∞ sequence are zero. This is another way of stating that elements of ℕ∞ are nonincreasing. (Contributed by Jim Kingdon, 12-Jul-2025.)
(𝜑 → 𝐴 ∈ ℕ∞)    &   (𝜑 → 𝑋 ∈ ω)    &   (𝜑 → 𝑌 ∈ ω)    &   (𝜑 → 𝑋 ⊆ 𝑌)    &   (𝜑 → (𝐴‘𝑋) = ∅)    ⇒   (𝜑 → (𝐴‘𝑌) = ∅)
 
10-Jul-2025nninfctlemfo 12234 Lemma for nninfct 12235. (Contributed by Jim Kingdon, 10-Jul-2025.)
𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))    &   𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {⟨+∞, (ω × {1o})⟩})    ⇒   (ω ∈ Omni → 𝐼:ℕ0*–onto→ℕ∞)
 
8-Jul-2025nnnninfen 15754 Equinumerosity of the natural numbers and ℕ∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.)
(ω ≈ ℕ∞ ↔ ω ∈ Omni)
 
8-Jul-2025nninfct 12235 The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.)
(ω ∈ Omni → ∃𝑓 𝑓:ω–onto→(ℕ∞ ⊔ 1o))
 
8-Jul-2025nninfinf 10554 ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.)
ω ≼ ℕ∞
 
7-Jul-2025ivthreinc 14967 Restating the intermediate value theorem. Given a hypothesis stating the intermediate value theorem (in a strong form which is not provable given our axioms alone), provide a conclusion similar to the theorem as stated in the Metamath Proof Explorer (which is also similar to how we state the theorem for a strictly monotonic function at ivthinc 14965). Being able to have a hypothesis stating the intermediate value theorem will be helpful when it comes time to show that it implies a constructive taboo. This version of the theorem requires that the function 𝐹 is continuous on the entire real line, not just (𝐴[,]𝐵) which may be an unnecessary condition but which is sufficient for the way we want to use it. (Contributed by Jim Kingdon, 7-Jul-2025.)
(𝜑 → 𝐴 ∈ ℝ)    &   (𝜑 → 𝐵 ∈ ℝ)    &   (𝜑 → 𝑈 ∈ ℝ)    &   (𝜑 → 𝐴 < 𝐵)    &   (𝜑 → 𝐹 ∈ (ℝ–cn→ℝ))    &   (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)))    &   (𝜑 → ∀𝑓(𝑓 ∈ (ℝ–cn→ℝ) → ∀𝑎 ∈ ℝ ∀𝑏 ∈ ℝ ((𝑎 < 𝑏 ∧ (𝑓‘𝑎) < 0 ∧ 0 < (𝑓‘𝑏)) → ∃𝑥 ∈ ℝ (𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ∧ (𝑓‘𝑥) = 0))))    ⇒   (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)
 
28-Jun-2025fngsum 13092 Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.)
Σg Fn (V × V)
 
28-Jun-2025iotaexel 5885 Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.)
((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝜑 → 𝑥 ∈ 𝐴)) → (℩𝑥𝜑) ∈ V)
 
27-Jun-2025df-igsum 12963 Define a finite group sum (also called "iterated sum") of a structure.

Given 𝐺 Σg 𝐹 where 𝐹:𝐴⟶(Base‘𝐺), the set of indices is 𝐴 and the values are given by 𝐹 at each index. A group sum over a multiplicative group may be viewed as a product. The definition is meaningful in different contexts, depending on the size of the index set 𝐴 and each demanding different properties of 𝐺.

1. If 𝐴 = ∅ and 𝐺 has an identity element, then the sum equals this identity.

2. If 𝐴 = (𝑀...𝑁) and 𝐺 is any magma, then the sum is the sum of the elements, evaluated left-to-right, i.e., ((𝐹‘1) + (𝐹‘2)) + (𝐹‘3), etc.

3. This definition does not handle other cases.

(Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.)

Σg = (𝑤 ∈ V, 𝑓 ∈ V ↦ (℩𝑥((dom 𝑓 = ∅ ∧ 𝑥 = (0g‘𝑤)) ∨ ∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(dom 𝑓 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚((+g‘𝑤), 𝑓)‘𝑛)))))
 
20-Jun-2025opprnzrbg 13819 The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 13820. (Contributed by SN, 20-Jun-2025.)
𝑂 = (oppr‘𝑅)    ⇒   (𝑅 ∈ 𝑉 → (𝑅 ∈ NzRing ↔ 𝑂 ∈ NzRing))
 
16-Jun-2025fnpsr 14299 The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
mPwSer Fn (V × V)
 
14-Jun-2025basm 12766 A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
𝐵 = (Base‘𝐺)    ⇒   (𝐴 ∈ 𝐵 → ∃𝑗 𝑗 ∈ 𝐺)
 
14-Jun-2025elfvm 5594 If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.)
(𝐴 ∈ (𝐹‘𝐵) → ∃𝑗 𝑗 ∈ 𝐹)
 
6-Jun-2025pcxqcl 12508 The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.)
((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ) → ((𝑃 pCnt 𝑁) ∈ ℤ ∨ (𝑃 pCnt 𝑁) = +∞))
 
5-Jun-2025xqltnle 10376 "Less than" expressed in terms of "less than or equal to", for extended numbers which are rational or +∞. We have not yet had enough usage of such numbers to warrant fully developing the concept, as in ℕ0* or ℝ*, so for now we just have a handful of theorems for what we need. (Contributed by Jim Kingdon, 5-Jun-2025.)
(((𝐴 ∈ ℚ ∨ 𝐴 = +∞) ∧ (𝐵 ∈ ℚ ∨ 𝐵 = +∞)) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
 
5-Jun-2025ceqsexv2d 2803 Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.)
𝐴 ∈ V    &   (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))    &   𝜓    ⇒   ∃𝑥𝜑
 
30-May-20254sqexercise2 12595 Exercise which may help in understanding the proof of 4sqlemsdc 12596. (Contributed by Jim Kingdon, 30-May-2025.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑛 = ((𝑥↑2) + (𝑦↑2))}    ⇒   (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
 
27-May-2025iotaexab 5238 Existence of the ℩ class when all the possible values are contained in a set. (Contributed by Jim Kingdon, 27-May-2025.)
({𝑥 ∣ 𝜑} ∈ 𝑉 → (℩𝑥𝜑) ∈ V)
 
25-May-20254sqlemsdc 12596 Lemma for 4sq 12606. 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 12594 and 4sqexercise2 12595 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 𝐴 ∈ 𝑆)
 
25-May-20254sqexercise1 12594 Exercise which may help in understanding the proof of 4sqlemsdc 12596. (Contributed by Jim Kingdon, 25-May-2025.)
𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ 𝑛 = (𝑥↑2)}    ⇒   (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
 
24-May-20254sqleminfi 12593 Lemma for 4sq 12606. 𝐴 ∩ ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝑃 ∈ ℕ)    &   𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   (𝜑 → (𝐴 ∩ ran 𝐹) ∈ Fin)
 
24-May-20254sqlemffi 12592 Lemma for 4sq 12606. ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝑃 ∈ ℕ)    &   𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   (𝜑 → ran 𝐹 ∈ Fin)
 
24-May-20254sqlemafi 12591 Lemma for 4sq 12606. 𝐴 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
(𝜑 → 𝑁 ∈ ℕ)    &   (𝜑 → 𝑃 ∈ ℕ)    &   𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    ⇒   (𝜑 → 𝐴 ∈ Fin)
 
24-May-2025infidc 7009 The intersection of two sets is finite if one of them is and the other is decidable. (Contributed by Jim Kingdon, 24-May-2025.)
((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 DECID 𝑥 ∈ 𝐵) → (𝐴 ∩ 𝐵) ∈ Fin)
  Copyright terms: Public domain W3C HTML validation [external]