Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent ILE Most Recent             Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 212ee7d9, also available here: set.mm (43MB) or set.mm.bz2 (compressed, 13MB).

The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43. The "OLD" versions are usually deleted after a year.

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 7-Dec-2021 .    Contributing: How can I contribute to Metamath?    Syndication: RSS feed (courtesy of Dan Getz)    Related wikis: Ghilbert site; Ghilbert Google Group.

Recent news items    (7-Aug-2021) Version 0.198 of the metamath program fixes a bug in "write source ... /rewrap" that prevented end-of-sentence punctuation from appearing in column 79, causing some rewrapped lines to be shorter than necessary. Because this affects about 2000 lines in set.mm, you should use version 0.198 or later for rewrapping before submitting to GitHub.

(7-May-2021) Mario Carneiro has written a Metamath verifier in Lean.

(5-May-2021) Marnix Klooster has written a Metamath verifier in Zig.

(24-Mar-2021) Metamath was mentioned in a couple of articles about OpenAI: Researchers find that large language models struggle with math and What Is GPT-F?.

(26-Dec-2020) Version 0.194 of the metamath program adds the keyword "htmlexturl" to the $t comment to specify external versions of theorem pages. This keyward has been added to set.mm, and you must update your local copy of set.mm for "verify markup" to pass with the new program version.

(19-Dec-2020) Aleksandr A. Adamov has translated the Wikipedia Metamath page into Russian.

(19-Nov-2020) Eric Schmidt's checkmm.cpp was used as a test case for C'est, "a non-standard version of the C++20 standard library, with enhanced support for compile-time evaluation." See C++20 Compile-time Metamath Proof Verification using C'est.

(10-Nov-2020) Filip Cernatescu has updated the XPuzzle (Android app) to version 1.2. XPuzzle is a puzzle with math formulas derived from the Metamath system. At the bottom of the web page is a link to the Google Play Store, where the app can be found.

(7-Nov-2020) Richard Penner created a cross-reference guide between Frege's logic notation and the notation used by set.mm.

(4-Sep-2020) Version 0.192 of the metamath program adds the qualifier '/extract' to 'write source'. See 'help write source' and also this Google Group post.

(23-Aug-2020) Version 0.188 of the metamath program adds keywords Conclusion, Fact, Introduction, Paragraph, Scolia, Scolion, Subsection, and Table to bibliographic references. See 'help write bibliography' for the complete current list.

   Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 22-Jul-2024 at 5:08 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 7-Dec-2020 )
DateLabelDescription
Theorem
 
21-Jul-2024wl-ifp-ncond2 34879 If one case of an if- condition is false, the other automatically follows. (Contributed by Wolf Lammen, 21-Jul-2024.)
𝜒 → (if-(𝜑, 𝜓, 𝜒) ↔ (𝜑𝜓)))
 
21-Jul-2024wl-ifp-ncond1 34878 If one case of an if- condition is false, the other automatically follows. (Contributed by Wolf Lammen, 21-Jul-2024.)
𝜓 → (if-(𝜑, 𝜓, 𝜒) ↔ (¬ 𝜑𝜒)))
 
18-Jul-2024metakunt34 39378 𝐷 is a permutation. (Contributed by metakunt, 18-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀𝐼)), 1, 0)), ((𝑤𝐼) + if(𝐼 ≤ (𝑤𝐼), 1, 0)))))       (𝜑𝐷:(1...𝑀)–1-1-onto→(1...𝑀))
 
18-Jul-2024metakunt33 39377 Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀𝐼)), (𝑧 + (1 − 𝐼)))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   𝐷 = (𝑤 ∈ (1...𝑀) ↦ if(𝑤 = 𝐼, 𝑤, if(𝑤 < 𝐼, ((𝑤 + (𝑀𝐼)) + if(𝐼 ≤ (𝑤 + (𝑀𝐼)), 1, 0)), ((𝑤𝐼) + if(𝐼 ≤ (𝑤𝐼), 1, 0)))))       (𝜑 → (𝐶 ∘ (𝐵𝐴)) = 𝐷)
 
18-Jul-2024metakunt32 39376 Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   (𝜑𝑋 ∈ (1...𝑀))    &   𝐷 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑥, if(𝑥 < 𝐼, ((𝑥 + (𝑀𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀𝐼)), 1, 0)), ((𝑥𝐼) + if(𝐼 ≤ (𝑥𝐼), 1, 0)))))    &   𝐺 = if(𝐼 ≤ (𝑋 + (𝑀𝐼)), 1, 0)    &   𝐻 = if(𝐼 ≤ (𝑋𝐼), 1, 0)    &   𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀𝐼)) + 𝐺), ((𝑋𝐼) + 𝐻)))       (𝜑 → (𝐷𝑋) = 𝑅)
 
18-Jul-2024metakunt31 39375 Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   (𝜑𝑋 ∈ (1...𝑀))    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀𝐼)), (𝑧 + (1 − 𝐼)))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   𝐺 = if(𝐼 ≤ (𝑋 + (𝑀𝐼)), 1, 0)    &   𝐻 = if(𝐼 ≤ (𝑋𝐼), 1, 0)    &   𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀𝐼)) + 𝐺), ((𝑋𝐼) + 𝐻)))       (𝜑 → (𝐶‘(𝐵‘(𝐴𝑋))) = 𝑅)
 
16-Jul-2024unexd 39400 The union of two sets is a set. (Contributed by SN, 16-Jul-2024.)
(𝜑𝐴𝑉)    &   (𝜑𝐵𝑊)       (𝜑 → (𝐴𝐵) ∈ V)
 
16-Jul-2024difexd 39399 Existence of a difference. (Contributed by SN, 16-Jul-2024.)
(𝜑𝐴𝑉)       (𝜑 → (𝐴𝐵) ∈ V)
 
16-Jul-2024sylibda 39386 A syllogism deduction. (Contributed by SN, 16-Jul-2024.)
(𝜑 → (𝜓𝜒))    &   ((𝜑𝜒) → 𝜃)       ((𝜑𝜓) → 𝜃)
 
15-Jul-2024fsuppssindlem2 39453 Lemma for fsuppssind 39454. Write a function as a union. (Contributed by SN, 15-Jul-2024.)
(𝜑𝐵𝑊)    &   (𝜑𝐼𝑉)    &   (𝜑𝑆𝐼)       (𝜑 → (𝐹 ∈ {𝑓 ∈ (𝐵m 𝑆) ∣ (𝑥𝐼 ↦ if(𝑥𝑆, (𝑓𝑥), 0 )) ∈ 𝐻} ↔ (𝐹:𝑆𝐵 ∧ (𝐹 ∪ ((𝐼𝑆) × { 0 })) ∈ 𝐻)))
 
15-Jul-2024fsuppssindlem1 39452 Lemma for fsuppssind 39454. Functions are zero outside of their support. (Contributed by SN, 15-Jul-2024.)
(𝜑0𝑊)    &   (𝜑𝐼𝑉)    &   (𝜑𝐹:𝐼𝐵)    &   (𝜑 → (𝐹 supp 0 ) ⊆ 𝑆)       (𝜑𝐹 = (𝑥𝐼 ↦ if(𝑥𝑆, ((𝐹𝑆)‘𝑥), 0 )))
 
13-Jul-2024rtrclind 14416 Principle of transitive induction. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction step. (Contributed by Drahflow, 12-Nov-2015.) (Revised by AV, 13-Jul-2024.)
(𝜂 → Rel 𝑅)    &   (𝜂𝑆𝑉)    &   (𝜂𝑋𝑊)    &   (𝑖 = 𝑆 → (𝜑𝜒))    &   (𝑖 = 𝑥 → (𝜑𝜓))    &   (𝑖 = 𝑗 → (𝜑𝜃))    &   (𝑥 = 𝑋 → (𝜓𝜏))    &   (𝜂𝜒)    &   (𝜂 → (𝑗𝑅𝑥 → (𝜃𝜓)))       (𝜂 → (𝑆(t*‘𝑅)𝑋𝜏))
 
13-Jul-2024relexpind 14415 Principle of transitive induction, finite version. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
(𝜂 → Rel 𝑅)    &   (𝜂𝑆𝑉)    &   (𝜂𝑋𝑊)    &   (𝑖 = 𝑆 → (𝜑𝜒))    &   (𝑖 = 𝑥 → (𝜑𝜓))    &   (𝑖 = 𝑗 → (𝜑𝜃))    &   (𝑥 = 𝑋 → (𝜓𝜏))    &   (𝜂𝜒)    &   (𝜂 → (𝑗𝑅𝑥 → (𝜃𝜓)))       (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅𝑟𝑛)𝑋𝜏)))
 
13-Jul-2024relexpindlem 14414 Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (Revised by AV, 13-Jul-2024.)
(𝜂 → Rel 𝑅)    &   (𝜂𝑆𝑉)    &   (𝑖 = 𝑆 → (𝜑𝜒))    &   (𝑖 = 𝑥 → (𝜑𝜓))    &   (𝑖 = 𝑗 → (𝜑𝜃))    &   (𝜂𝜒)    &   (𝜂 → (𝑗𝑅𝑥 → (𝜃𝜓)))       (𝜂 → (𝑛 ∈ ℕ0 → (𝑆(𝑅𝑟𝑛)𝑥𝜓)))
 
13-Jul-2024dfrtrcl2 14413 The two definitions t* and t*rec of the reflexive, transitive closure coincide if 𝑅 is indeed a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
(𝜑 → Rel 𝑅)       (𝜑 → (t*‘𝑅) = (t*rec‘𝑅))
 
13-Jul-2024rtrclreclem4 14412 The reflexive, transitive closure of 𝑅 is the smallest reflexive, transitive relation which contains 𝑅 and the identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
(𝜑 → Rel 𝑅)       (𝜑 → ∀𝑠((( I ↾ (dom 𝑅 ∪ ran 𝑅)) ⊆ 𝑠𝑅𝑠 ∧ (𝑠𝑠) ⊆ 𝑠) → (t*rec‘𝑅) ⊆ 𝑠))
 
13-Jul-2024rtrclreclem3 14411 The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
(𝜑 → Rel 𝑅)       (𝜑 → ((t*rec‘𝑅) ∘ (t*rec‘𝑅)) ⊆ (t*rec‘𝑅))
 
13-Jul-2024rtrclreclem2 14410 The reflexive, transitive closure is indeed reflexive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 13-Jul-2024.)
(𝜑 → Rel 𝑅)    &   (𝜑𝑅𝑉)       (𝜑 → ( I ↾ 𝑅) ⊆ (t*rec‘𝑅))
 
13-Jul-2024dfrtrclrec2 14409 If two elements are connected by a reflexive, transitive closure, then they are connected via 𝑛 instances the relation, for some 𝑛. (Contributed by Drahflow, 12-Nov-2015.) (Revised by AV, 13-Jul-2024.)
(𝜑 → Rel 𝑅)       (𝜑 → (𝐴(t*rec‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅𝑟𝑛)𝐵))
 
12-Jul-2024erlecpbl 16815 Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
(𝜑 Er 𝑉)    &   (𝜑𝑉𝑊)    &   𝐹 = (𝑥𝑉 ↦ [𝑥] )    &   (𝜑 → ((𝐴 𝐶𝐵 𝐷) → (𝐴𝑁𝐵𝐶𝑁𝐷)))       ((𝜑 ∧ (𝐴𝑉𝐵𝑉) ∧ (𝐶𝑉𝐷𝑉)) → (((𝐹𝐴) = (𝐹𝐶) ∧ (𝐹𝐵) = (𝐹𝐷)) → (𝐴𝑁𝐵𝐶𝑁𝐷)))
 
12-Jul-2024ercpbl 16814 Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
(𝜑 Er 𝑉)    &   (𝜑𝑉𝑊)    &   𝐹 = (𝑥𝑉 ↦ [𝑥] )    &   ((𝜑 ∧ (𝑎𝑉𝑏𝑉)) → (𝑎 + 𝑏) ∈ 𝑉)    &   (𝜑 → ((𝐴 𝐶𝐵 𝐷) → (𝐴 + 𝐵) (𝐶 + 𝐷)))       ((𝜑 ∧ (𝐴𝑉𝐵𝑉) ∧ (𝐶𝑉𝐷𝑉)) → (((𝐹𝐴) = (𝐹𝐶) ∧ (𝐹𝐵) = (𝐹𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷))))
 
12-Jul-2024ercpbllem 16813 Lemma for ercpbl 16814. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.)
(𝜑 Er 𝑉)    &   (𝜑𝑉𝑊)    &   𝐹 = (𝑥𝑉 ↦ [𝑥] )    &   (𝜑𝐴𝑉)       (𝜑 → ((𝐹𝐴) = (𝐹𝐵) ↔ 𝐴 𝐵))
 
12-Jul-2024divsfval 16812 Value of the function in qusval 16807. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)
(𝜑 Er 𝑉)    &   (𝜑𝑉𝑊)    &   𝐹 = (𝑥𝑉 ↦ [𝑥] )       (𝜑 → (𝐹𝐴) = [𝐴] )
 
12-Jul-2024prdsvallem 16719 Lemma for prdsbas 16722 and similar theorems. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 12-Jul-2024.)
(𝜑𝑈 = (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩})))    &   𝐴 = (𝐸𝑈)    &   𝐸 = Slot (𝐸‘ndx)    &   (𝜑𝑇𝑉)    &   {⟨(𝐸‘ndx), 𝑇⟩} ⊆ (({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), × ⟩} ∪ {⟨(Scalar‘ndx), 𝑆⟩, ⟨( ·𝑠 ‘ndx), · ⟩, ⟨(·𝑖‘ndx), , ⟩}) ∪ ({⟨(TopSet‘ndx), 𝑂⟩, ⟨(le‘ndx), 𝐿⟩, ⟨(dist‘ndx), 𝐷⟩} ∪ {⟨(Hom ‘ndx), 𝐻⟩, ⟨(comp‘ndx), ⟩}))       (𝜑𝐴 = 𝑇)
 
12-Jul-2024rtrclreclem1 14408 The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑𝑅𝑉)       (𝜑𝑅 ⊆ (t*rec‘𝑅))
 
12-Jul-2024relexpaddd 14405 Relation composition becomes addition under exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑 → Rel 𝑅)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑀 ∈ ℕ0)       (𝜑 → ((𝑅𝑟𝑁) ∘ (𝑅𝑟𝑀)) = (𝑅𝑟(𝑁 + 𝑀)))
 
12-Jul-2024relexpfldd 14401 The field of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑𝑁 ∈ ℕ0)       (𝜑 (𝑅𝑟𝑁) ⊆ 𝑅)
 
12-Jul-2024relexprnd 14399 The range of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑𝑁 ∈ ℕ0)       (𝜑 → ran (𝑅𝑟𝑁) ⊆ 𝑅)
 
12-Jul-2024relexpdmd 14395 The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑𝑁 ∈ ℕ0)       (𝜑 → dom (𝑅𝑟𝑁) ⊆ 𝑅)
 
12-Jul-2024relexpreld 14391 The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑 → Rel 𝑅)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → Rel (𝑅𝑟𝑁))
 
12-Jul-2024relexpcnvd 14387 Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑𝑅𝑉)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑(𝑅𝑟𝑁) = (𝑅𝑟𝑁))
 
12-Jul-2024relexpsucld 14385 A reduction for relation exponentiation to the left. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑 → Rel 𝑅)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝑅𝑟(𝑁 + 1)) = (𝑅 ∘ (𝑅𝑟𝑁)))
 
12-Jul-2024relexpsucrd 14384 A reduction for relation exponentiation to the right. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑 → Rel 𝑅)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → (𝑅𝑟(𝑁 + 1)) = ((𝑅𝑟𝑁) ∘ 𝑅))
 
12-Jul-2024relexp1d 14380 A relation composed once is itself. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑𝑅𝑉)       (𝜑 → (𝑅𝑟1) = 𝑅)
 
12-Jul-2024relexp0d 14375 A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.) (Revised by AV, 12-Jul-2024.)
(𝜑 → Rel 𝑅)    &   (𝜑𝑅𝑉)       (𝜑 → (𝑅𝑟0) = ( I ↾ 𝑅))
 
12-Jul-2024reldmrelexp 14372 The domain of the repeated composition of a relation is a relation. (Contributed by AV, 12-Jul-2024.)
Rel dom ↑𝑟
 
8-Jul-2024rhmpreimacn 31238 The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map 𝐺 is reverse: the original ring homomorphism 𝐹 goes from 𝑅 to 𝑆, but the continuous map 𝐺 goes from 𝐵 to 𝐴. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.)
𝑇 = (Spec‘𝑅)    &   𝑈 = (Spec‘𝑆)    &   𝐴 = (PrmIdeal‘𝑅)    &   𝐵 = (PrmIdeal‘𝑆)    &   𝐽 = (TopOpen‘𝑇)    &   𝐾 = (TopOpen‘𝑈)    &   𝐺 = (𝑖𝐵 ↦ (𝐹𝑖))    &   (𝜑𝑅 ∈ CRing)    &   (𝜑𝑆 ∈ CRing)    &   (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))    &   (𝜑 → ran 𝐹 = (Base‘𝑆))       (𝜑𝐺 ∈ (𝐾 Cn 𝐽))
 
7-Jul-2024metakunt30 39374 Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   (𝜑𝑋 ∈ (1...𝑀))    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀𝐼)), (𝑧 + (1 − 𝐼)))))    &   (𝜑 → ¬ 𝑋 = 𝐼)    &   (𝜑 → ¬ 𝑋 < 𝐼)    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   𝐻 = if(𝐼 ≤ (𝑋𝐼), 1, 0)       (𝜑 → (𝐶‘(𝐵‘(𝐴𝑋))) = ((𝑋𝐼) + 𝐻))
 
7-Jul-2024metakunt29 39373 Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   (𝜑𝑋 ∈ (1...𝑀))    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀𝐼)), (𝑧 + (1 − 𝐼)))))    &   (𝜑 → ¬ 𝑋 = 𝐼)    &   (𝜑𝑋 < 𝐼)    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   𝐻 = if(𝐼 ≤ (𝑋 + (𝑀𝐼)), 1, 0)       (𝜑 → (𝐶‘(𝐵‘(𝐴𝑋))) = ((𝑋 + (𝑀𝐼)) + 𝐻))
 
7-Jul-2024metakunt28 39372 Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   (𝜑𝑋 ∈ (1...𝑀))    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀𝐼)), (𝑧 + (1 − 𝐼)))))    &   (𝜑 → ¬ 𝑋 = 𝐼)    &   (𝜑 → ¬ 𝑋 < 𝐼)       (𝜑 → (𝐵‘(𝐴𝑋)) = (𝑋𝐼))
 
7-Jul-2024metakunt27 39371 Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   (𝜑𝑋 ∈ (1...𝑀))    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀𝐼)), (𝑧 + (1 − 𝐼)))))    &   (𝜑 → ¬ 𝑋 = 𝐼)    &   (𝜑𝑋 < 𝐼)       (𝜑 → (𝐵‘(𝐴𝑋)) = (𝑋 + (𝑀𝐼)))
 
7-Jul-2024metakunt26 39370 Construction of one solution of the increment equation system. (Contributed by metakunt, 7-Jul-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   𝐵 = (𝑧 ∈ (1...𝑀) ↦ if(𝑧 = 𝑀, 𝑀, if(𝑧 < 𝐼, (𝑧 + (𝑀𝐼)), (𝑧 + (1 − 𝐼)))))    &   (𝜑𝑋 = 𝐼)       (𝜑 → (𝐶‘(𝐵‘(𝐴𝑋))) = 𝑋)
 
7-Jul-2024rhmpreimacnlem 31237 Lemma for rhmpreimacn 31238. (Contributed by Thierry Arnoux, 7-Jul-2024.)
𝑇 = (Spec‘𝑅)    &   𝑈 = (Spec‘𝑆)    &   𝐴 = (PrmIdeal‘𝑅)    &   𝐵 = (PrmIdeal‘𝑆)    &   𝐽 = (TopOpen‘𝑇)    &   𝐾 = (TopOpen‘𝑈)    &   𝐺 = (𝑖𝐵 ↦ (𝐹𝑖))    &   (𝜑𝑅 ∈ CRing)    &   (𝜑𝑆 ∈ CRing)    &   (𝜑𝐹 ∈ (𝑅 RingHom 𝑆))    &   (𝜑 → ran 𝐹 = (Base‘𝑆))    &   (𝜑𝐼 ∈ (LIdeal‘𝑅))    &   𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘𝐴𝑗𝑘})    &   𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘𝐵𝑗𝑘})       (𝜑 → (𝑊‘(𝐹𝐼)) = (𝐺 “ (𝑉𝐼)))
 
6-Jul-2024rhmimaidl 31017 The image of an ideal 𝐼 by a surjective ring homomorphism 𝐹 is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024.)
𝐵 = (Base‘𝑆)    &   𝑇 = (LIdeal‘𝑅)    &   𝑈 = (LIdeal‘𝑆)       ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵𝐼𝑇) → (𝐹𝐼) ∈ 𝑈)
 
6-Jul-2024idlinsubrg 31016 The intersection between an ideal and a subring is an ideal of the subring. (Contributed by Thierry Arnoux, 6-Jul-2024.)
𝑆 = (𝑅s 𝐴)    &   𝑈 = (LIdeal‘𝑅)    &   𝑉 = (LIdeal‘𝑆)       ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼𝑈) → (𝐼𝐴) ∈ 𝑉)
 
5-Jul-2024lidlincl 31015 Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.)
𝑈 = (LIdeal‘𝑅)       ((𝑅 ∈ Ring ∧ 𝐼𝑈𝐽𝑈) → (𝐼𝐽) ∈ 𝑈)
 
3-Jul-2024ficardun2 9613 The cardinality of the union of finite sets is at most the ordinal sum of their cardinalities. (Contributed by Mario Carneiro, 5-Feb-2013.) Avoid ax-rep 5154. (Revised by BTernaryTau, 3-Jul-2024.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (card‘(𝐴𝐵)) ⊆ ((card‘𝐴) +o (card‘𝐵)))
 
3-Jul-2024ficardun 9611 The cardinality of the union of disjoint, finite sets is the ordinal sum of their cardinalities. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Mario Carneiro, 28-Apr-2015.) Avoid ax-rep 5154. (Revised by BTernaryTau, 3-Jul-2024.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴𝐵) = ∅) → (card‘(𝐴𝐵)) = ((card‘𝐴) +o (card‘𝐵)))
 
3-Jul-2024ficardadju 9610 The disjoint union of finite sets is equinumerous to the ordinal sum of the cardinalities of those sets. (Contributed by BTernaryTau, 3-Jul-2024.)
((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴𝐵) ≈ ((card‘𝐴) +o (card‘𝐵)))
 
2-Jul-2024zarcmp 31235 The Zariski topology is compact. Proposition 1.1.10(ii) of [EGA], p. 82. (Contributed by Thierry Arnoux, 2-Jul-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)       (𝑅 ∈ CRing → 𝐽 ∈ Comp)
 
2-Jul-2024zarcmplem 31234 Lemma for zarcmp 31235. (Contributed by Thierry Arnoux, 2-Jul-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)    &   𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})       (𝑅 ∈ CRing → 𝐽 ∈ Comp)
 
2-Jul-2024nnadju 9608 The cardinal and ordinal sums of finite ordinals are equal. For a shorter proof using ax-rep 5154, see nnadjuALT 9609. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 6-Feb-2013.) Avoid ax-rep 5154. (Revised by BTernaryTau, 2-Jul-2024.)
((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (card‘(𝐴𝐵)) = (𝐴 +o 𝐵))
 
1-Jul-2024zar0ring 31231 The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)    &   𝐵 = (Base‘𝑅)       ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐽 = {∅})
 
1-Jul-2024isrprm 31073 Property for 𝑃 to be a prime element in the ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
𝐵 = (Base‘𝑅)    &   𝑈 = (Unit‘𝑅)    &    0 = (0g𝑅)    &    = (∥r𝑅)    &    · = (.r𝑅)       (𝑅𝑉 → (𝑃 ∈ (RPrime‘𝑅) ↔ (𝑃 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∧ ∀𝑥𝐵𝑦𝐵 (𝑃 (𝑥 · 𝑦) → (𝑃 𝑥𝑃 𝑦)))))
 
1-Jul-2024rprmval 31072 The prime elements of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jul-2024.)
𝐵 = (Base‘𝑅)    &   𝑈 = (Unit‘𝑅)    &    0 = (0g𝑅)    &    · = (.r𝑅)    &    = (∥r𝑅)       (𝑅𝑉 → (RPrime‘𝑅) = {𝑝 ∈ (𝐵 ∖ (𝑈 ∪ { 0 })) ∣ ∀𝑥𝐵𝑦𝐵 (𝑝 (𝑥 · 𝑦) → (𝑝 𝑥𝑝 𝑦))})
 
1-Jul-20240ringidl 31013 The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.)
𝐵 = (Base‘𝑅)    &    0 = (0g𝑅)       ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (LIdeal‘𝑅) = {{ 0 }})
 
1-Jul-2024kerlidl 31012 The kernel of a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 1-Jul-2024.)
𝐼 = (LIdeal‘𝑅)    &    0 = (0g𝑆)       (𝐹 ∈ (𝑅 RingHom 𝑆) → (𝐹 “ { 0 }) ∈ 𝐼)
 
30-Jun-2024sn-mul02 39572 mul02 10807 without ax-mulcom 10590. See https://github.com/icecream17/Stuff/blob/main/math/0A%3D0.md 10590 for an outline. (Contributed by SN, 30-Jun-2024.)
(𝐴 ∈ ℂ → (0 · 𝐴) = 0)
 
30-Jun-2024sn-0tie0 39571 Lemma for sn-mul02 39572. Commuted version of sn-it0e0 39547. (Contributed by SN, 30-Jun-2024.)
(0 · i) = 0
 
30-Jun-2024ipiiie0 39569 The multiplicative inverse of i (per i4 13563) is also its additive inverse. (Contributed by SN, 30-Jun-2024.)
(i + (i · (i · i))) = 0
 
30-Jun-2024prmidl0 31034 The zero ideal of a commutative ring 𝑅 is a prime ideal if and only if 𝑅 is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024.)
0 = (0g𝑅)       ((𝑅 ∈ CRing ∧ { 0 } ∈ (PrmIdeal‘𝑅)) ↔ 𝑅 ∈ IDomn)
 
30-Jun-20240ringprmidl 31033 The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.)
𝐵 = (Base‘𝑅)       ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (PrmIdeal‘𝑅) = ∅)
 
30-Jun-2024elrspunidl 31014 Elementhood to the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024.)
𝑁 = (RSpan‘𝑅)    &   𝐵 = (Base‘𝑅)    &    0 = (0g𝑅)    &    · = (.r𝑅)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝑆 ⊆ (LIdeal‘𝑅))       (𝜑 → (𝑋 ∈ (𝑁 𝑆) ↔ ∃𝑎 ∈ (𝐵m 𝑆)(𝑎 finSupp 0𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘𝑆 (𝑎𝑘) ∈ 𝑘)))
 
30-Jun-2024rhmpreimaidl 31011 The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.)
𝐼 = (LIdeal‘𝑅)       ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ 𝐽 ∈ (LIdeal‘𝑆)) → (𝐹𝐽) ∈ 𝐼)
 
30-Jun-2024abf 4310 A class abstraction determined by a false formula is empty. (Contributed by NM, 20-Jan-2012.) Avoid ax-8 2113, ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 30-Jun-2024.)
¬ 𝜑       {𝑥𝜑} = ∅
 
29-Jun-2024rhmpreimaprmidl 31035 The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024.)
𝑃 = (PrmIdeal‘𝑅)       (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝐽 ∈ (PrmIdeal‘𝑆)) → (𝐹𝐽) ∈ 𝑃)
 
28-Jun-2024reldisj 4359 Two ways of saying that two classes are disjoint, using the complement of 𝐵 relative to a universe 𝐶. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
(𝐴𝐶 → ((𝐴𝐵) = ∅ ↔ 𝐴 ⊆ (𝐶𝐵)))
 
28-Jun-2024disj 4355 Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
((𝐴𝐵) = ∅ ↔ ∀𝑥𝐴 ¬ 𝑥𝐵)
 
28-Jun-2024csb0 4314 The proper substitution of a class into the empty set is the empty set. (Contributed by NM, 18-Aug-2018.) Avoid ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
𝐴 / 𝑥∅ = ∅
 
28-Jun-2024rspn0 4266 Specialization for restricted generalization with a nonempty class. (Contributed by Alexander van der Vekens, 6-Sep-2018.) Avoid ax-10 2142, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
(𝐴 ≠ ∅ → (∀𝑥𝐴 𝜑𝜑))
 
28-Jun-2024n0 4260 A class is nonempty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 29-Sep-2006.) Avoid ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
(𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
 
28-Jun-2024neq0 4259 A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) Avoid ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
𝐴 = ∅ ↔ ∃𝑥 𝑥𝐴)
 
28-Jun-2024eq0 4258 A class is equal to the empty set if and only if it has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.) Avoid ax-11 2158, ax-12 2175. (Revised by Gino Giotto and Steven Nguyen, 28-Jun-2024.)
(𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥𝐴)
 
28-Jun-2024ss2abi 3994 Inference of abstraction subclass from implication. (Contributed by NM, 31-Mar-1995.) Avoid ax-8 2113, ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
(𝜑𝜓)       {𝑥𝜑} ⊆ {𝑥𝜓}
 
28-Jun-2024ss2abdvALT 3992 Alternate proof of ss2abdv 3991. Shorter, but requiring ax-8 2113. (Contributed by Steven Nguyen, 28-Jun-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝜑 → (𝜓𝜒))       (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
 
28-Jun-2024ss2abdv 3991 Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2113, ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
(𝜑 → (𝜓𝜒))       (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
 
28-Jun-2024cgsex4g 3486 An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.) Avoid ax-10 2142, ax-11 2158. (Revised by Gino Giotto, 28-Jun-2024.)
(((𝑥 = 𝐴𝑦 = 𝐵) ∧ (𝑧 = 𝐶𝑤 = 𝐷)) → 𝜒)    &   (𝜒 → (𝜑𝜓))       (((𝐴𝑅𝐵𝑆) ∧ (𝐶𝑅𝐷𝑆)) → (∃𝑥𝑦𝑧𝑤(𝜒𝜑) ↔ 𝜓))
 
27-Jun-2024cnreeu 39588 The reals in the expression given by cnre 10627 uniquely define a complex number. (Contributed by SN, 27-Jun-2024.)
(𝜑𝑟 ∈ ℝ)    &   (𝜑𝑠 ∈ ℝ)    &   (𝜑𝑡 ∈ ℝ)    &   (𝜑𝑢 ∈ ℝ)       (𝜑 → ((𝑟 + (i · 𝑠)) = (𝑡 + (i · 𝑢)) ↔ (𝑟 = 𝑡𝑠 = 𝑢)))
 
27-Jun-2024retire 39587 Commuted version of itrere 39586. (Contributed by SN, 27-Jun-2024.)
(𝑅 ∈ ℝ → ((𝑅 · i) ∈ ℝ ↔ 𝑅 = 0))
 
27-Jun-2024itrere 39586 i times a real is real iff the real is zero. (Contributed by SN, 27-Jun-2024.)
(𝑅 ∈ ℝ → ((i · 𝑅) ∈ ℝ ↔ 𝑅 = 0))
 
27-Jun-2024diffib 30293 Case where diffi 8734 is a biconditional. (Contributed by Thierry Arnoux, 27-Jun-2024.)
(𝐵 ∈ Fin → (𝐴 ∈ Fin ↔ (𝐴𝐵) ∈ Fin))
 
26-Jun-2024sn-sup2 39589 sup2 11584 with exactly the same proof except for using sn-ltp1 39583 instead of ltp1 11469, saving ax-mulcom 10590. (Contributed by SN, 26-Jun-2024.)
((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦𝐴 (𝑦 < 𝑥𝑦 = 𝑥)) → ∃𝑥 ∈ ℝ (∀𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧𝐴 𝑦 < 𝑧)))
 
26-Jun-2024sn-ltmul2d 39581 ltmul2d 12461 without ax-mulcom 10590. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝐶 ∈ ℝ)    &   (𝜑 → 0 < 𝐶)       (𝜑 → ((𝐶 · 𝐴) < (𝐶 · 𝐵) ↔ 𝐴 < 𝐵))
 
26-Jun-2024mulgt0b2d 39580 Biconditional, deductive form of mulgt0 10707. The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi 39529 does not have a commuted form. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)       (𝜑 → (0 < 𝐵 ↔ 0 < (𝐴 · 𝐵)))
 
26-Jun-2024mulgt0con2d 39579 Lemma for mulgt0b2d 39580 and contrapositive of mulgt0 10707. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐴)    &   (𝜑 → (𝐴 · 𝐵) < 0)       (𝜑𝐵 < 0)
 
26-Jun-2024mulgt0con1d 39578 Counterpart to mulgt0con2d 39579, though not a lemma of anything. This is the first use of ax-pre-mulgt0 10603. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐵)    &   (𝜑 → (𝐴 · 𝐵) < 0)       (𝜑𝐴 < 0)
 
26-Jun-2024mulgt0con1dlem 39577 Lemma for mulgt0con1d 39578. Contraposes a positive deduction to a negative deduction. (Contributed by SN, 26-Jun-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑 → (0 < 𝐴 → 0 < 𝐵))    &   (𝜑 → (𝐴 = 0 → 𝐵 = 0))       (𝜑 → (𝐵 < 0 → 𝐴 < 0))
 
26-Jun-2024undif5 30291 An equality involving class union and class difference. (Contributed by Thierry Arnoux, 26-Jun-2024.)
((𝐴𝐵) = ∅ → ((𝐴𝐵) ∖ 𝐵) = 𝐴)
 
25-Jun-2024ressupprn 30450 The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.)
((Fun 𝐹𝐹𝑉0𝑊) → ran (𝐹 ↾ (𝐹 supp 0 )) = (ran 𝐹 ∖ { 0 }))
 
25-Jun-2024fressupp 30448 The restriction of a function to its support. (Contributed by Thierry Arnoux, 25-Jun-2024.)
((Fun 𝐹𝐹𝑉𝑍𝑊) → (𝐹 ↾ (𝐹 supp 𝑍)) = (𝐹 ∖ (V × {𝑍})))
 
25-Jun-2024suppiniseg 30446 Relation between the support (𝐹 supp 𝑍) and the initial segment (𝐹 “ {𝑍}). (Contributed by Thierry Arnoux, 25-Jun-2024.)
((Fun 𝐹𝐹𝑉𝑍𝑊) → (dom 𝐹 ∖ (𝐹 supp 𝑍)) = (𝐹 “ {𝑍}))
 
24-Jun-2024fsupprnfi 30452 Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024.)
(((Fun 𝐹𝐹𝑉) ∧ ( 0𝑊𝐹 finSupp 0 )) → ran 𝐹 ∈ Fin)
 
24-Jun-2024supppreima 30451 Express the support of a function as the preimage of its range except zero. (Contributed by Thierry Arnoux, 24-Jun-2024.)
((Fun 𝐹𝐹𝑉𝑍𝑊) → (𝐹 supp 𝑍) = (𝐹 “ (ran 𝐹 ∖ {𝑍})))
 
23-Jun-2024wl-df3maxtru1 34906 Assuming "(n+1)-maxtru1" ↔ ¬ "(n+1)-mintru-2", we can deduce from the recursion formula given in wl-df-3mintru2 34898, that a similiar one

"(n+1)-maxtru1" ↔ if-(𝜑,-. "n-mintru-1" , "n-maxtru1" )

is valid for expressing 'at most one input is true'. This can also be rephrased as a mutual exclusivity of propositional expressions (no two of a sequence of inputs can simultaniously be true). Of course, this suggests that all inputs depend on variables 𝜂, 𝜁... Whatever wellformed expression we plugin for these variables, it will render at most one of the inputs true.

The here introduced mutual exclusivity is possibly useful for case studies, where we want the cases be sort of 'disjoint'. One can further imagine that a complete case scenario demands that the 'at most' is sharpened to 'exactly one'. This does not impose any difficulty here, as one of the inputs will then be the negation of all others be or'ed. As one input is determined, 'at most one' is sufficient to describe the general form here.

Since cadd is an alias for 'at least 2 out of three are true', its negation is under focus here. (Contributed by Wolf Lammen, 23-Jun-2024.)

(¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 𝜒), (𝜓𝜒)))
 
23-Jun-20242ndresdjuf1o 30412 The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst 7779. (Contributed by Thierry Arnoux, 23-Jun-2024.)
𝑈 = 𝑥𝑋 ({𝑥} × 𝐶)    &   (𝜑𝐴𝑉)    &   (𝜑𝑋𝑊)    &   (𝜑Disj 𝑥𝑋 𝐶)    &   (𝜑 𝑥𝑋 𝐶 = 𝐴)       (𝜑 → (2nd𝑈):𝑈1-1-onto𝐴)
 
23-Jun-20242ndresdju 30411 The 2nd function restricted to a disjoint union is injective. (Contributed by Thierry Arnoux, 23-Jun-2024.)
𝑈 = 𝑥𝑋 ({𝑥} × 𝐶)    &   (𝜑𝐴𝑉)    &   (𝜑𝑋𝑊)    &   (𝜑Disj 𝑥𝑋 𝐶)    &   (𝜑 𝑥𝑋 𝐶 = 𝐴)       (𝜑 → (2nd𝑈):𝑈1-1𝐴)
 
23-Jun-2024djussxp2 30410 Stronger version of djussxp 5680 (Contributed by Thierry Arnoux, 23-Jun-2024.)
𝑘𝐴 ({𝑘} × 𝐵) ⊆ (𝐴 × 𝑘𝐴 𝐵)
 
23-Jun-20242ndimaxp 30409 Image of a cartesian product by 2nd. (Contributed by Thierry Arnoux, 23-Jun-2024.)
(𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵)
 
23-Jun-2024indifbi 30292 Two ways to express equality relative to a class 𝐴. (Contributed by Thierry Arnoux, 23-Jun-2024.)
((𝐴𝐵) = (𝐴𝐶) ↔ (𝐴𝐵) = (𝐴𝐶))
 
22-Jun-2024gsumhashmul 30741 Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    · = (.g𝐺)    &   (𝜑𝐺 ∈ CMnd)    &   (𝜑𝐹:𝐴𝐵)    &   (𝜑𝐹 finSupp 0 )       (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((♯‘(𝐹 “ {𝑥})) · 𝑥))))
 
22-Jun-2024gsumpart 30740 Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &   (𝜑𝐺 ∈ CMnd)    &   (𝜑𝐴𝑉)    &   (𝜑𝑋𝑊)    &   (𝜑𝐹:𝐴𝐵)    &   (𝜑𝐹 finSupp 0 )    &   (𝜑Disj 𝑥𝑋 𝐶)    &   (𝜑 𝑥𝑋 𝐶 = 𝐴)       (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝑋 ↦ (𝐺 Σg (𝐹𝐶)))))
 
22-Jun-2024gsummptres2 30738 Extend a finite group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 22-Jun-2024.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &   (𝜑𝐺 ∈ CMnd)    &   (𝜑𝐴𝑉)    &   ((𝜑𝑥 ∈ (𝐴𝑆)) → 𝑌 = 0 )    &   (𝜑𝑆 ∈ Fin)    &   ((𝜑𝑥𝐴) → 𝑌𝐵)    &   (𝜑𝑆𝐴)       (𝜑 → (𝐺 Σg (𝑥𝐴𝑌)) = (𝐺 Σg (𝑥𝑆𝑌)))
 
22-Jun-2024fdifsuppconst 30449 A function is a zero constant outside of its support. (Contributed by Thierry Arnoux, 22-Jun-2024.)
𝐴 = (dom 𝐹 ∖ (𝐹 supp 𝑍))       ((Fun 𝐹𝐹𝑉𝑍𝑊) → (𝐹𝐴) = (𝐴 × {𝑍}))
 
22-Jun-2024iunsnima2 30383 Version of iunsnima 30382 with different variables. (Contributed by Thierry Arnoux, 22-Jun-2024.)
(𝜑𝐴𝑉)    &   ((𝜑𝑥𝐴) → 𝐵𝑊)    &   𝑥𝐶    &   (𝑥 = 𝑌𝐵 = 𝐶)       ((𝜑𝑌𝐴) → ( 𝑥𝐴 ({𝑥} × 𝐵) “ {𝑌}) = 𝐶)
 
21-Jun-2024fsuppinisegfi 30447 The initial segment (𝐹 “ {𝑌}) of a nonzero 𝑌 is finite if 𝐹 has finite support. (Contributed by Thierry Arnoux, 21-Jun-2024.)
(𝜑𝐹𝑉)    &   (𝜑0𝑊)    &   (𝜑𝑌 ∈ (V ∖ { 0 }))    &   (𝜑𝐹 finSupp 0 )       (𝜑 → (𝐹 “ {𝑌}) ∈ Fin)
 
19-Jun-2024wl-df4-3mintru2 34901 An alternative definition of the adder carry. Copy of df-cad 1609. (Contributed by Mario Carneiro, 4-Sep-2016.) df-cad redefined. (Revised by Wolf Lammen, 19-Jun-2024.)
(cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (𝜒 ∧ (𝜑𝜓))))
 
18-Jun-2024wl-df3-3mintru2 34900 The adder carry in conjunctive normal form. An alternative highly symmetric definition emphasizing the independance of order of the inputs 𝜑, 𝜓 and 𝜒. Copy of cadan 1611. (Contributed by Mario Carneiro, 4-Sep-2016.) df-cad redefined. (Revised by Wolf Lammen, 18-Jun-2024.)
(cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∧ (𝜑𝜒) ∧ (𝜓𝜒)))
 
18-Jun-2024wl-ifp4impr 34881 If one case of an if- condition is a consequence of the other, the expression in dfifp4 1062 can be shortened. (Contributed by Wolf Lammen, 18-Jun-2024.)
((𝜒𝜓) → (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜒) ∧ 𝜓)))
 
17-Jun-2024idlsrgmulrssin 31066 In a commutative ring, the product of two ideals is a subset of their intersection. (Contributed by Thierry Arnoux, 17-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐵 = (LIdeal‘𝑅)    &    = (.r𝑆)    &   (𝜑𝑅 ∈ CRing)    &   (𝜑𝐼𝐵)    &   (𝜑𝐽𝐵)       (𝜑 → (𝐼 𝐽) ⊆ (𝐼𝐽))
 
16-Jun-2024ofun 39411 A function operation of unions of disjoint functions is a union of function operations. (Contributed by SN, 16-Jun-2024.)
(𝜑𝐴 Fn 𝑀)    &   (𝜑𝐵 Fn 𝑀)    &   (𝜑𝐶 Fn 𝑁)    &   (𝜑𝐷 Fn 𝑁)    &   (𝜑𝑀𝑉)    &   (𝜑𝑁𝑊)    &   (𝜑 → (𝑀𝑁) = ∅)       (𝜑 → ((𝐴𝐶) ∘f 𝑅(𝐵𝐷)) = ((𝐴f 𝑅𝐵) ∪ (𝐶f 𝑅𝐷)))
 
16-Jun-2024rspectps 31236 The spectrum of a ring 𝑅 is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (Spec‘𝑅)       (𝑅 ∈ CRing → 𝑆 ∈ TopSp)
 
16-Jun-2024zarmxt1 31233 The Zariski topology restricted to maximal ideals is T1 . (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)    &   𝑀 = (MaxIdeal‘𝑅)    &   𝑇 = (𝐽t 𝑀)       (𝑅 ∈ CRing → 𝑇 ∈ Fre)
 
16-Jun-2024zart0 31232 The Zariski topology is T0 . Corollary 1.1.8 of [EGA] p. 81. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)       (𝑅 ∈ CRing → 𝐽 ∈ Kol2)
 
16-Jun-2024zartopon 31230 The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)    &   𝑃 = (PrmIdeal‘𝑅)       (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝑃))
 
16-Jun-2024zartop 31229 The Zariski topology is a topology. Proposition 1.1.2 of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)       (𝑅 ∈ CRing → 𝐽 ∈ Top)
 
16-Jun-2024zartopn 31228 The Zariski topology is a topology, and its closed sets are images by 𝑉 of the ideals of 𝑅. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)    &   𝑃 = (PrmIdeal‘𝑅)    &   𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗𝑃𝑖𝑗})       (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘𝐽)))
 
16-Jun-2024zarcls 31227 The open sets of the Zariski topology are the complements of the closed sets. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐽 = (TopOpen‘𝑆)    &   𝑃 = (PrmIdeal‘𝑅)    &   𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗𝑃𝑖𝑗})       (𝑅 ∈ Ring → 𝐽 = {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃𝑠) ∈ ran 𝑉})
 
16-Jun-2024zarclssn 31226 The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})    &   𝐵 = (LIdeal‘𝑅)       ((𝑅 ∈ CRing ∧ 𝑀𝐵) → ({𝑀} = (𝑉𝑀) ↔ 𝑀 ∈ (MaxIdeal‘𝑅)))
 
16-Jun-2024zarclsint 31225 The intersection of a family of closed sets is closed in the Zariski topology. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})       ((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉𝑆 ≠ ∅) → 𝑆 ∈ ran 𝑉)
 
16-Jun-2024zarclsiin 31224 In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})    &   𝐾 = (RSpan‘𝑅)       ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → 𝑙𝑇 (𝑉𝑙) = (𝑉‘(𝐾 𝑇)))
 
16-Jun-2024zarclsun 31223 The union of two closed sets of the Zariski topology is closed. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})       ((𝑅 ∈ CRing ∧ 𝑋 ∈ ran 𝑉𝑌 ∈ ran 𝑉) → (𝑋𝑌) ∈ ran 𝑉)
 
16-Jun-2024zarcls1 31222 The unit ideal 𝐵 is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})    &   𝐵 = (Base‘𝑅)       ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ((𝑉𝐼) = ∅ ↔ 𝐼 = 𝐵))
 
16-Jun-2024zarcls0 31221 The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖𝑗})    &   𝑃 = (PrmIdeal‘𝑅)    &    0 = (0g𝑅)       (𝑅 ∈ Ring → (𝑉‘{ 0 }) = 𝑃)
 
16-Jun-2024idlsrgmulrss1 31064 In a commutative ring, the product of two ideals is a subset of the first one. (Contributed by Thierry Arnoux, 16-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐵 = (LIdeal‘𝑅)    &    = (.r𝑆)    &    · = (.r𝑅)    &   (𝜑𝑅 ∈ CRing)    &   (𝜑𝐼𝐵)    &   (𝜑𝐽𝐵)       (𝜑 → (𝐼 𝐽) ⊆ 𝐼)
 
16-Jun-2024biadanid 30236 Deduction associated with biadani 819. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.)
((𝜑𝜓) → 𝜒)    &   ((𝜑𝜒) → (𝜓𝜃))       (𝜑 → (𝜓 ↔ (𝜒𝜃)))
 
16-Jun-2024pmatassa 21299 The set of polynomial matrices over a commutative ring is an associative algebra. (Contributed by AV, 16-Jun-2024.)
𝑃 = (Poly1𝑅)    &   𝐶 = (𝑁 Mat 𝑃)       ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐶 ∈ AssAlg)
 
15-Jun-2024fsuppssind 39454 Induction on functions 𝐹:𝐴𝐵 with finite support (see fsuppind 39451) whose supports are subsets of 𝑆. (Contributed by SN, 15-Jun-2024.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    + = (+g𝐺)    &   (𝜑𝐺 ∈ Grp)    &   (𝜑𝐼𝑉)    &   (𝜑𝑆𝐼)    &   (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)    &   ((𝜑 ∧ (𝑎𝑆𝑏𝐵)) → (𝑠𝐼 ↦ if(𝑠 = 𝑎, 𝑏, 0 )) ∈ 𝐻)    &   ((𝜑 ∧ (𝑥𝐻𝑦𝐻)) → (𝑥f + 𝑦) ∈ 𝐻)    &   (𝜑𝑋:𝐼𝐵)    &   (𝜑𝑋 finSupp 0 )    &   (𝜑 → (𝑋 supp 0 ) ⊆ 𝑆)       (𝜑𝑋𝐻)
 
15-Jun-2024intimafv 30470 The intersection of an image set, as an indexed intersection of function values. (Contributed by Thierry Arnoux, 15-Jun-2024.)
((Fun 𝐹𝐴 ⊆ dom 𝐹) → (𝐹𝐴) = 𝑥𝐴 (𝐹𝑥))
 
15-Jun-2024iinabrex 30332 Rewriting an indexed intersection into an intersection of its image set. (Contributed by Thierry Arnoux, 15-Jun-2024.)
(∀𝑥𝐴 𝐵𝑉 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦 = 𝐵})
 
12-Jun-2024wl-df2-3mintru2 34899 The adder carry in disjunctive normal form. An alternative highly symmetric definition emphasizing the independance of order of the inputs 𝜑, 𝜓 and 𝜒. Copy of cador 1610. (Contributed by Mario Carneiro, 4-Sep-2016.) df-cad redefined. (Revised by Wolf Lammen, 12-Jun-2024.)
(cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ (𝜑𝜒) ∨ (𝜓𝜒)))
 
12-Jun-2024wl-ifpimpr 34880 If one case of an if- condition is a consequence of the other, the expression in df-ifp 1059 can be shortened. (Contributed by Wolf Lammen, 12-Jun-2024.)
((𝜒𝜓) → (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ∨ 𝜒)))
 
9-Jun-2024preiman0 30469 The preimage of a nonempty set is nonempty. (Contributed by Thierry Arnoux, 9-Jun-2024.)
((Fun 𝐹𝐴 ⊆ ran 𝐹𝐴 ≠ ∅) → (𝐹𝐴) ≠ ∅)
 
8-Jun-20242ap1caineq 39344 Inequality for Theorem 6.6 for AKS. (Contributed by metakunt, 8-Jun-2024.)
(𝜑𝑁 ∈ ℤ)    &   (𝜑 → 2 ≤ 𝑁)       (𝜑 → (2↑(𝑁 + 1)) < (((2 · 𝑁) + 1)C𝑁))
 
8-Jun-20242np3bcnp1 39343 Part of induction step for 2ap1caineq 39344. (Contributed by metakunt, 8-Jun-2024.)
(𝜑𝑁 ∈ ℕ0)       (𝜑 → (((2 · (𝑁 + 1)) + 1)C(𝑁 + 1)) = ((((2 · 𝑁) + 1)C𝑁) · (2 · (((2 · 𝑁) + 3) / (𝑁 + 2)))))
 
8-Jun-20245bc2eq10 39341 The value of 5 choose 2. (Contributed by metakunt, 8-Jun-2024.)
(5C2) = 10
 
8-Jun-2024uzindd 39261 Induction on the upper integers that start at 𝑀. The first four hypotheses give us the substitution instances we need; the following two are the basis and the induction step, a deduction version. (Contributed by metakunt, 8-Jun-2024.)
(𝑗 = 𝑀 → (𝜓𝜒))    &   (𝑗 = 𝑘 → (𝜓𝜃))    &   (𝑗 = (𝑘 + 1) → (𝜓𝜏))    &   (𝑗 = 𝑁 → (𝜓𝜂))    &   (𝜑𝜒)    &   ((𝜑𝜃 ∧ (𝑘 ∈ ℤ ∧ 𝑀𝑘)) → 𝜏)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝑀𝑁)       (𝜑𝜂)
 
8-Jun-2024intlidl 31010 The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.)
((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → 𝐶 ∈ (LIdeal‘𝑅))
 
8-Jun-2024ringlsmss1 31003 The product of an ideal 𝐼 of a commutative ring 𝑅 with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.)
𝐵 = (Base‘𝑅)    &   𝐺 = (mulGrp‘𝑅)    &    × = (LSSum‘𝐺)    &   (𝜑𝑅 ∈ CRing)    &   (𝜑𝐸𝐵)    &   (𝜑𝐼 ∈ (LIdeal‘𝑅))       (𝜑 → (𝐼 × 𝐸) ⊆ 𝐼)
 
7-Jun-2024df-naryf 45036 Define the n-ary (endo)functions. (Contributed by AV, 11-May-2024.) (Revised by TA and SN, 7-Jun-2024.)
-aryF = (𝑛 ∈ ℕ0, 𝑥 ∈ V ↦ (𝑥m (𝑥m (0..^𝑛))))
 
4-Jun-2024naryfvalelwrdf 45042 An n-ary (endo)function on a set 𝑋 expressed as a function over the set of words on 𝑋 of length 𝑛. (Contributed by AV, 4-Jun-2024.)
((𝑁 ∈ ℕ0𝑋𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:{𝑤 ∈ Word 𝑋 ∣ (♯‘𝑤) = 𝑁}⟶𝑋))
 
4-Jun-2024iccioo01 34738 The closed unit interval is equinumerous to the open unit interval. Based on a Mastodon post by Michael Kinyon. (Contributed by Jim Kingdon, 4-Jun-2024.)
(0[,]1) ≈ (0(,)1)
 
4-Jun-2024rspectopn 31220 The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐼 = (LIdeal‘𝑅)    &   𝑃 = (PrmIdeal‘𝑅)    &   𝐽 = ran (𝑖𝐼 ↦ {𝑗𝑃 ∣ ¬ 𝑖𝑗})       (𝑅 ∈ Ring → 𝐽 = (TopOpen‘𝑆))
 
3-Jun-2024rabeqi 3429 Equality theorem for restricted class abstractions. Inference form of rabeqf 3428. (Contributed by Glauco Siliprandi, 26-Jun-2021.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 3-Jun-2024.)
𝐴 = 𝐵       {𝑥𝐴𝜑} = {𝑥𝐵𝜑}
 
3-Jun-2024nfcri 2943 Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2142, ax-11 2158. (Revised by Gino Giotto, 23-May-2024.) Avoid ax-12 2175 (adopting Wolf Lammen's 13-May-2023 proof). (Revised by SN, 3-Jun-2024.)
𝑥𝐴       𝑥 𝑦𝐴
 
3-Jun-2024nfcr 2941 Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Drop ax-12 2175 but use ax-8 2113, and avoid a DV condition on 𝑦, 𝐴. (Revised by SN, 3-Jun-2024.)
(𝑥𝐴 → Ⅎ𝑥 𝑦𝐴)
 
2-Jun-2024mapprop 44743 An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019.) (Proof shortened by AV, 2-Jun-2024.)
𝐹 = {⟨𝑋, 𝐴⟩, ⟨𝑌, 𝐵⟩}       (((𝑋𝑉𝐴𝑅) ∧ (𝑌𝑉𝐵𝑅) ∧ (𝑋𝑌𝑅𝑊)) → 𝐹 ∈ (𝑅m {𝑋, 𝑌}))
 
2-Jun-2024rspectset 31219 Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.)
𝑆 = (Spec‘𝑅)    &   𝐼 = (LIdeal‘𝑅)    &   𝐽 = ran (𝑖𝐼 ↦ {𝑗𝐼 ∣ ¬ 𝑖𝑗})       (𝑅 ∈ Ring → 𝐽 = (TopSet‘𝑆))
 
2-Jun-2024rspecbas 31218 The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.)
𝑆 = (Spec‘𝑅)       (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = (Base‘𝑆))
 
2-Jun-2024rspecval 31217 Value of the spectrum of the ring 𝑅. Notation 1.1.1 of [EGA] p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024.)
(𝑅 ∈ Ring → (Spec‘𝑅) = ((IDLsrg‘𝑅) ↾s (PrmIdeal‘𝑅)))
 
2-Jun-2024idlsrgmulrss2 31065 The product of two ideals is a subset of the second one. (Contributed by Thierry Arnoux, 2-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐵 = (LIdeal‘𝑅)    &    = (.r𝑆)    &    · = (.r𝑅)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝐼𝐵)    &   (𝜑𝐽𝐵)       (𝜑 → (𝐼 𝐽) ⊆ 𝐽)
 
2-Jun-2024prmidlssidl 31028 Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.)
(𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅))
 
2-Jun-2024ringlsmss2 31004 The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024.)
𝐵 = (Base‘𝑅)    &   𝐺 = (mulGrp‘𝑅)    &    × = (LSSum‘𝐺)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝐸𝐵)    &   (𝜑𝐼 ∈ (LIdeal‘𝑅))       (𝜑 → (𝐸 × 𝐼) ⊆ 𝐼)
 
1-Jun-2024sn-inelr 39585 inelr 11615 without ax-mulcom 10590. (Contributed by SN, 1-Jun-2024.)
¬ i ∈ ℝ
 
1-Jun-2024reneg1lt0 39584 Lemma for sn-inelr 39585. (Contributed by SN, 1-Jun-2024.)
(0 − 1) < 0
 
1-Jun-2024it1ei 39568 1 is a multiplicative identity for i (see sn-mulid2 39567 for commuted version). (Contributed by SN, 1-Jun-2024.)
(i · 1) = i
 
1-Jun-2024ringcmnd 39439 A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
(𝜑𝑅 ∈ Ring)       (𝜑𝑅 ∈ CMnd)
 
1-Jun-2024ringabld 39438 A ring is an Abelian group. EDITORIAL: This cannot be used to shorten ringgrpd 19299 because ringabl 19326 depends on ringgrp 19295. (Contributed by SN, 1-Jun-2024.)
(𝜑𝑅 ∈ Ring)       (𝜑𝑅 ∈ Abel)
 
1-Jun-2024ablcmnd 39437 An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
(𝜑𝐺 ∈ Abel)       (𝜑𝐺 ∈ CMnd)
 
1-Jun-2024grpmndd 39436 A group is a monoid. (Contributed by SN, 1-Jun-2024.)
(𝜑𝐺 ∈ Grp)       (𝜑𝐺 ∈ Mnd)
 
1-Jun-2024isufd 31071 The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝐴 = (AbsVal‘𝑅)    &   𝐼 = (PrmIdeal‘𝑅)    &   𝑃 = (RPrime‘𝑅)       (𝑅 ∈ UFD ↔ (𝑅 ∈ CRing ∧ (𝐴 ≠ ∅ ∧ ∀𝑖𝐼 (𝑖𝑃) ≠ ∅)))
 
1-Jun-2024idlsrgcmnd 31068 The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)       (𝑅 ∈ Ring → 𝑆 ∈ CMnd)
 
1-Jun-2024idlsrgmnd 31067 The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)       (𝑅 ∈ Ring → 𝑆 ∈ Mnd)
 
1-Jun-2024idlsrgmulrcl 31063 Ideals of a ring 𝑅 are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐵 = (LIdeal‘𝑅)    &    = (.r𝑆)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝐼𝐵)    &   (𝜑𝐽𝐵)       (𝜑 → (𝐼 𝐽) ∈ 𝐵)
 
1-Jun-2024idlsrgmulrval 31062 Value of the ring multiplication for the ideals of a ring 𝑅. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐵 = (LIdeal‘𝑅)    &    = (.r𝑆)    &   𝐺 = (mulGrp‘𝑅)    &    · = (LSSum‘𝐺)    &   (𝜑𝑅𝑉)    &   (𝜑𝐼𝐵)    &   (𝜑𝐽𝐵)       (𝜑 → (𝐼 𝐽) = ((RSpan‘𝑅)‘(𝐼 · 𝐽)))
 
1-Jun-2024idlsrgtset 31061 Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐼 = (LIdeal‘𝑅)    &   𝐽 = ran (𝑖𝐼 ↦ {𝑗𝐼 ∣ ¬ 𝑖𝑗})       (𝑅𝑉𝐽 = (TopSet‘𝑆))
 
1-Jun-2024idlsrgmulr 31060 Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐵 = (LIdeal‘𝑅)    &   𝐺 = (mulGrp‘𝑅)    &    = (LSSum‘𝐺)       (𝑅𝑉 → (𝑖𝐵, 𝑗𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 𝑗))) = (.r𝑆))
 
1-Jun-2024idlsrg0g 31059 The zero ideal is the additive identity of the semiring of ideals. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &    0 = (0g𝑅)       (𝑅 ∈ Ring → { 0 } = (0g𝑆))
 
1-Jun-2024idlsrgplusg 31058 Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &    = (LSSum‘𝑅)       (𝑅𝑉 = (+g𝑆))
 
1-Jun-2024idlsrgbas 31057 Baae of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑆 = (IDLsrg‘𝑅)    &   𝐼 = (LIdeal‘𝑅)       (𝑅𝑉𝐼 = (Base‘𝑆))
 
1-Jun-2024idlsrgval 31056 Lemma for idlsrgbas 31057 through idlsrgtset 31061. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝐼 = (LIdeal‘𝑅)    &    = (LSSum‘𝑅)    &   𝐺 = (mulGrp‘𝑅)    &    = (LSSum‘𝐺)       (𝑅𝑉 → (IDLsrg‘𝑅) = ({⟨(Base‘ndx), 𝐼⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), (𝑖𝐼, 𝑗𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 𝑗)))⟩} ∪ {⟨(TopSet‘ndx), ran (𝑖𝐼 ↦ {𝑗𝐼 ∣ ¬ 𝑖𝑗})⟩, ⟨(le‘ndx), {⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ 𝐼𝑖𝑗)}⟩}))
 
1-Jun-2024idlsrgstr 31055 A constructed semiring of ideals is a structure. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑊 = ({⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx), · ⟩} ∪ {⟨(TopSet‘ndx), 𝐽⟩, ⟨(le‘ndx), ⟩})       𝑊 Struct ⟨1, 10⟩
 
1-Jun-2024lsmssass 31009 Group sum is associative, subset version (see lsmass 18787). (Contributed by Thierry Arnoux, 1-Jun-2024.)
= (LSSum‘𝐺)    &   𝐵 = (Base‘𝐺)    &   (𝜑𝐺 ∈ Mnd)    &   (𝜑𝑅𝐵)    &   (𝜑𝑇𝐵)    &   (𝜑𝑈𝐵)       (𝜑 → ((𝑅 𝑇) 𝑈) = (𝑅 (𝑇 𝑈)))
 
1-Jun-2024rspidlid 30990 The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝐾 = (RSpan‘𝑅)    &   𝑈 = (LIdeal‘𝑅)       ((𝑅 ∈ Ring ∧ 𝐼𝑈) → (𝐾𝐼) = 𝐼)
 
1-Jun-2024elrsp 30989 Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024.)
𝑁 = (RSpan‘𝑅)    &   𝐵 = (Base‘𝑅)    &    0 = (0g𝑅)    &    · = (.r𝑅)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝐼𝐵)       (𝜑 → (𝑋 ∈ (𝑁𝐼) ↔ ∃𝑎 ∈ (𝐵m 𝐼)(𝑎 finSupp 0𝑋 = (𝑅 Σg (𝑖𝐼 ↦ ((𝑎𝑖) · 𝑖))))))
 
1-Jun-2024cmnmndd 18921 A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.)
(𝜑𝐺 ∈ CMnd)       (𝜑𝐺 ∈ Mnd)
 
1-Jun-2024fndmi 6426 The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.)
𝐹 Fn 𝐴       dom 𝐹 = 𝐴
 
31-May-2024frobrhm 30910 In a commutative ring with prime characteristic, the Frobenius function 𝐹 is a ring endomorphism, thus named the Frobenius endomorphism. (Contributed by Thierry Arnoux, 31-May-2024.)
𝐵 = (Base‘𝑅)    &   𝑃 = (chr‘𝑅)    &    = (.g‘(mulGrp‘𝑅))    &   𝐹 = (𝑥𝐵 ↦ (𝑃 𝑥))    &   (𝜑𝑅 ∈ CRing)    &   (𝜑𝑃 ∈ ℙ)       (𝜑𝐹 ∈ (𝑅 RingHom 𝑅))
 
29-May-2024dmmpoga 7753 Domain of an operation given by the maps-to notation, closed form of dmmpo 7751. (Contributed by Alexander van der Vekens, 10-Feb-2019.) (Proof shortened by Lammen, 29-May-2024.)
𝐹 = (𝑥𝐴, 𝑦𝐵𝐶)       (∀𝑥𝐴𝑦𝐵 𝐶𝑉 → dom 𝐹 = (𝐴 × 𝐵))
 
29-May-2024f1eqcocnv 7035 Condition for function equality in terms of vanishing of the composition with the inverse. (Contributed by Stefan O'Rear, 12-Feb-2015.) (Proof shortened by Wolf Lammen, 29-May-2024.)
((𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵) → (𝐹 = 𝐺 ↔ (𝐹𝐺) = ( I ↾ 𝐴)))
 
29-May-2024f1dm 6553 The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Wolf Lammen, 29-May-2024.)
(𝐹:𝐴1-1𝐵 → dom 𝐹 = 𝐴)
 
29-May-2024fdm 6495 The domain of a mapping. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 29-May-2024.)
(𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
 
28-May-2024metakunt25 39369 B is a permutation. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀𝐼)), (𝑥 + (1 − 𝐼)))))       (𝜑𝐵:(1...𝑀)–1-1-onto→(1...𝑀))
 
28-May-2024metakunt24 39368 Technical condition such that metakunt17 39361 holds (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)       (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀𝐼))) ∪ {𝑀})))
 
28-May-2024metakunt23 39367 B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀𝐼)), (𝑥 + (1 − 𝐼)))))    &   𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀𝐼)))    &   𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   (𝜑𝑋 ∈ (1...𝑀))       (𝜑 → (𝐵𝑋) = (((𝐶𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
 
28-May-2024metakunt22 39366 Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀𝐼)), (𝑥 + (1 − 𝐼)))))    &   𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀𝐼)))    &   𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   (𝜑𝑋 ∈ (1...𝑀))    &   (𝜑 → ¬ 𝑋 = 𝑀)    &   (𝜑 → ¬ 𝑋 < 𝐼)       (𝜑 → (𝐵𝑋) = (((𝐶𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
 
28-May-2024metakunt21 39365 Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀𝐼)), (𝑥 + (1 − 𝐼)))))    &   𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀𝐼)))    &   𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   (𝜑𝑋 ∈ (1...𝑀))    &   (𝜑 → ¬ 𝑋 = 𝑀)    &   (𝜑𝑋 < 𝐼)       (𝜑 → (𝐵𝑋) = (((𝐶𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
 
28-May-2024metakunt20 39364 Show that B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀𝐼)), (𝑥 + (1 − 𝐼)))))    &   𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀𝐼)))    &   𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))    &   (𝜑𝑋 ∈ (1...𝑀))    &   (𝜑𝑋 = 𝑀)       (𝜑 → (𝐵𝑋) = (((𝐶𝐷) ∪ {⟨𝑀, 𝑀⟩})‘𝑋))
 
28-May-2024metakunt19 39363 Domains on restrictions of functions. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀𝐼)), (𝑥 + (1 − 𝐼)))))    &   𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀𝐼)))    &   𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))       (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {⟨𝑀, 𝑀⟩} Fn {𝑀}))
 
28-May-2024metakunt18 39362 Disjoint domains and codomains. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)       (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀𝐼))) = ∅ ∧ ((((𝑀𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀𝐼)) ∩ {𝑀}) = ∅)))
 
28-May-2024metakunt17 39361 The union of three disjoint bijections is a bijection. (Contributed by metakunt, 28-May-2024.)
(𝜑𝐺:𝐴1-1-onto𝑋)    &   (𝜑𝐻:𝐵1-1-onto𝑌)    &   (𝜑𝐼:𝐶1-1-onto𝑍)    &   (𝜑 → (𝐴𝐵) = ∅)    &   (𝜑 → (𝐴𝐶) = ∅)    &   (𝜑 → (𝐵𝐶) = ∅)    &   (𝜑 → (𝑋𝑌) = ∅)    &   (𝜑 → (𝑋𝑍) = ∅)    &   (𝜑 → (𝑌𝑍) = ∅)    &   (𝜑𝐹 = ((𝐺𝐻) ∪ 𝐼))    &   (𝜑𝐷 = ((𝐴𝐵) ∪ 𝐶))    &   (𝜑𝑊 = ((𝑋𝑌) ∪ 𝑍))       (𝜑𝐹:𝐷1-1-onto𝑊)
 
28-May-2024fzsplitnr 39268 Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
(𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝐾 ∈ ℤ)    &   (𝜑𝑀𝐾)    &   (𝜑𝐾𝑁)       (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
 
28-May-2024fzsplitnd 39267 Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024.)
(𝜑𝐾 ∈ (𝑀...𝑁))       (𝜑 → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
 
28-May-2024eqfnfv2d2 39266 Equality of functions is determined by their values, a deduction version. (Contributed by metakunt, 28-May-2024.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑𝐴 = 𝐵)    &   ((𝜑𝑥𝐴) → (𝐹𝑥) = (𝐺𝑥))       (𝜑𝐹 = 𝐺)
 
28-May-2024find 7587 The Principle of Finite Induction (mathematical induction). Corollary 7.31 of [TakeutiZaring] p. 43. The simpler hypothesis shown here was suggested in an email from "Colin" on 1-Oct-2001. The hypothesis states that 𝐴 is a set of natural numbers, zero belongs to 𝐴, and given any member of 𝐴 the member's successor also belongs to 𝐴. The conclusion is that every natural number is in 𝐴. (Contributed by NM, 22-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Wolf Lammen, 28-May-2024.)
(𝐴 ⊆ ω ∧ ∅ ∈ 𝐴 ∧ ∀𝑥𝐴 suc 𝑥𝐴)       𝐴 = ω
 
28-May-2024fvun2d 6732 The value of a union when the argument is in the second domain, a deduction version. (Contributed by metakunt, 28-May-2024.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑 → (𝐴𝐵) = ∅)    &   (𝜑𝑋𝐵)       (𝜑 → ((𝐹𝐺)‘𝑋) = (𝐺𝑋))
 
28-May-2024fvun1d 6731 The value of a union when the argument is in the first domain, a deduction version. (Contributed by metakunt, 28-May-2024.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑 → (𝐴𝐵) = ∅)    &   (𝜑𝑋𝐴)       (𝜑 → ((𝐹𝐺)‘𝑋) = (𝐹𝑋))
 
28-May-2024fnund 6435 The union of two functions with disjoint domains, a deduction version. (Contributed by metakunt, 28-May-2024.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺 Fn 𝐵)    &   (𝜑 → (𝐴𝐵) = ∅)       (𝜑 → (𝐹𝐺) Fn (𝐴𝐵))
 
27-May-2024sn-mulid2 39567 mulid2 10629 without ax-mulcom 10590. (Contributed by SN, 27-May-2024.)
(𝐴 ∈ ℂ → (1 · 𝐴) = 𝐴)
 
27-May-2024sn-1ticom 39566 Lemma for sn-mulid2 39567 and it1ei 39568. (Contributed by SN, 27-May-2024.)
(1 · i) = (i · 1)
 
27-May-2024rei4 39555 i4 13563 without ax-mulcom 10590. (Contributed by SN, 27-May-2024.)
((i · i) · (i · i)) = 1
 
27-May-2024onnev 6279 The class of ordinal numbers is not equal to the universe. (Contributed by NM, 16-Jun-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2013.) (Proof shortened by Wolf Lammen, 27-May-2024.)
On ≠ V
 
27-May-2024ssel 3908 Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993.) Avoid ax-12 2175. (Revised by SN, 27-May-2024.)
(𝐴𝐵 → (𝐶𝐴𝐶𝐵))
 
26-May-202419.9dev 39391 19.9d 2201 in the case of an existential quantifier, avoiding the ax-10 2142 from nfex 2332 that would be used for the hypothesis of 19.9d 2201, at the cost of an additional DV condition on 𝑦, 𝜑. (Contributed by SN, 26-May-2024.)
(𝜑 → Ⅎ𝑥𝜓)       (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑦𝜓))
 
26-May-2024bj-iminvid 34607 Functorial property of the inverse image: the inverse image by the identity on a set is the identity on the powerset. (Contributed by BJ, 26-May-2024.)
(𝜑𝐴𝑈)       (𝜑 → ((𝐴𝒫*𝐴)‘( I ↾ 𝐴)) = ( I ↾ 𝒫 𝐴))
 
26-May-2024bj-imdiridlem 34597 Lemma for bj-imdirid 34598 and bj-iminvid 34607. (Contributed by BJ, 26-May-2024.)
((𝑥𝐴𝑦𝐴) → (𝜑𝑥 = 𝑦))       {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐴) ∧ 𝜑)} = ( I ↾ 𝒫 𝐴)
 
26-May-2024bj-substw 34166 Weak form of the LHS of bj-subst 34165 proved from the core axiom schemes. Compare ax12w 2134. (Contributed by BJ, 26-May-2024.) (Proof modification is discouraged.)
(𝑥 = 𝑡 → (𝜑𝜓))       (∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑))
 
26-May-2024elpwi2 5213 Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.)
𝐵𝑉    &   𝐴𝐵       𝐴 ∈ 𝒫 𝐵
 
26-May-2024opeq2 4765 Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 26-May-2024.)
(𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
 
26-May-2024opeq1 4763 Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 26-May-2024.)
(𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
 
26-May-2024nfcriOLD 2946 Obsolete version of nfcri 2943 as of 3-Jun-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2142, ax-11 2158. (Revised by Gino Giotto, 23-May-2024.) Avoid ax-12 2175. (Revised by SN, 26-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑥𝐴       𝑥 𝑦𝐴
 
25-May-2024metakunt16 39360 Construction of another permutation. (Contributed by metakunt, 25-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐹 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))       (𝜑𝐹:(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀𝐼)))
 
25-May-2024metakunt15 39359 Construction of another permutation. (Contributed by metakunt, 25-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐹 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀𝐼)))       (𝜑𝐹:(1...(𝐼 − 1))–1-1-onto→(((𝑀𝐼) + 1)...(𝑀 − 1)))
 
25-May-2024metakunt14 39358 A is a primitive permutation that moves the I-th element to the end and C is its inverse that moves the last element back to the I-th position. (Contributed by metakunt, 25-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))       (𝜑 → (𝐴:(1...𝑀)–1-1-onto→(1...𝑀) ∧ 𝐴 = 𝐶))
 
25-May-2024metakunt13 39357 C is the right inverse for A. (Contributed by metakunt, 25-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       (𝜑 → (𝐴‘(𝐶𝑋)) = 𝑋)
 
25-May-2024metakunt12 39356 C is the right inverse for A. (Contributed by metakunt, 25-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       ((𝜑 ∧ ¬ (𝑋 = 𝑀𝑋 < 𝐼)) → (𝐴‘(𝐶𝑋)) = 𝑋)
 
25-May-2024mhpvarcl 20798 A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.)
𝐻 = (𝐼 mHomP 𝑅)    &   𝑉 = (𝐼 mVar 𝑅)    &   (𝜑𝐼𝑊)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝑋𝐼)       (𝜑 → (𝑉𝑋) ∈ (𝐻‘1))
 
25-May-2024ismhp2 20794 Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024.)
𝐻 = (𝐼 mHomP 𝑅)    &   𝑃 = (𝐼 mPoly 𝑅)    &   𝐵 = (Base‘𝑃)    &    0 = (0g𝑅)    &   𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}    &   (𝜑𝐼𝑉)    &   (𝜑𝑅𝑊)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑𝑋𝐵)    &   (𝜑 → (𝑋 supp 0 ) ⊆ {𝑔𝐷 ∣ ((ℂflds0) Σg 𝑔) = 𝑁})       (𝜑𝑋 ∈ (𝐻𝑁))
 
25-May-2024mplneg 20681 The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.)
𝑃 = (𝐼 mPoly 𝑅)    &   𝐵 = (Base‘𝑃)    &   𝑁 = (invg𝑅)    &   𝑀 = (invg𝑃)    &   (𝜑𝐼𝑉)    &   (𝜑𝑅 ∈ Grp)    &   (𝜑𝑋𝐵)       (𝜑 → (𝑀𝑋) = (𝑁𝑋))
 
25-May-2024suppcoss 7854 The support of the composition of two functions is a subset of the support of the inner function if the outer function preserves zero. Compare suppssfv 7849, which has a sethood condition on 𝐴 instead of 𝐵. (Contributed by SN, 25-May-2024.)
(𝜑𝐹 Fn 𝐴)    &   (𝜑𝐺:𝐵𝐴)    &   (𝜑𝐵𝑊)    &   (𝜑𝑌𝑉)    &   (𝜑 → (𝐹𝑌) = 𝑍)       (𝜑 → ((𝐹𝐺) supp 𝑍) ⊆ (𝐺 supp 𝑌))
 
25-May-2024elpr2g 4549 A member of a pair of sets is one or the other of them, and conversely. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 14-Oct-2005.) Generalize from sethood hypothesis to sethood antecedent. (Revised by BJ, 25-May-2024.)
((𝐵𝑉𝐶𝑊) → (𝐴 ∈ {𝐵, 𝐶} ↔ (𝐴 = 𝐵𝐴 = 𝐶)))
 
24-May-2024metakunt11 39355 C is the right inverse for A. (Contributed by metakunt, 24-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       ((𝜑𝑋 < 𝐼) → (𝐴‘(𝐶𝑋)) = 𝑋)
 
24-May-2024metakunt10 39354 C is the right inverse for A. (Contributed by metakunt, 24-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       ((𝜑𝑋 = 𝑀) → (𝐴‘(𝐶𝑋)) = 𝑋)
 
24-May-2024metakunt9 39353 C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       (𝜑 → (𝐶‘(𝐴𝑋)) = 𝑋)
 
24-May-2024metakunt8 39352 C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       ((𝜑𝐼 < 𝑋) → (𝐶‘(𝐴𝑋)) = 𝑋)
 
24-May-2024metakunt7 39351 C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       ((𝜑𝐼 < 𝑋) → ((𝐴𝑋) = (𝑋 − 1) ∧ ¬ (𝐴𝑋) = 𝑀 ∧ ¬ (𝐴𝑋) < 𝐼))
 
24-May-2024metakunt6 39350 C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       ((𝜑𝑋 < 𝐼) → (𝐶‘(𝐴𝑋)) = 𝑋)
 
24-May-2024metakunt5 39349 C is the left inverse for A. (Contributed by metakunt, 24-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   𝐶 = (𝑦 ∈ (1...𝑀) ↦ if(𝑦 = 𝑀, 𝐼, if(𝑦 < 𝐼, 𝑦, (𝑦 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       ((𝜑𝑋 = 𝐼) → (𝐶‘(𝐴𝑋)) = 𝑋)
 
23-May-20242arymaptf1o 45064 The mapping of binary (endo)functions is a one-to-one function onto the set of binary operations (Contributed by AV, 23-May-2024.)
𝐻 = ( ∈ (2-aryF 𝑋) ↦ (𝑥𝑋, 𝑦𝑋 ↦ (‘{⟨0, 𝑥⟩, ⟨1, 𝑦⟩})))       (𝑋𝑉𝐻:(2-aryF 𝑋)–1-1-onto→(𝑋m (𝑋 × 𝑋)))
 
23-May-20242arymaptfo 45063 The mapping of binary (endo)functions is a function onto the set of binary operations. (Contributed by AV, 23-May-2024.)
𝐻 = ( ∈ (2-aryF 𝑋) ↦ (𝑥𝑋, 𝑦𝑋 ↦ (‘{⟨0, 𝑥⟩, ⟨1, 𝑦⟩})))       (𝑋𝑉𝐻:(2-aryF 𝑋)–onto→(𝑋m (𝑋 × 𝑋)))
 
23-May-2024metakunt4 39348 Value of A. (Contributed by metakunt, 23-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       (𝜑 → (𝐴𝑋) = if(𝑋 = 𝑀, 𝐼, if(𝑋 < 𝐼, 𝑋, (𝑋 + 1))))
 
23-May-2024metakunt3 39347 Value of A. (Contributed by metakunt, 23-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))    &   (𝜑𝑋 ∈ (1...𝑀))       (𝜑 → (𝐴𝑋) = if(𝑋 = 𝐼, 𝑀, if(𝑋 < 𝐼, 𝑋, (𝑋 − 1))))
 
23-May-2024metakunt2 39346 A is an endomapping. (Contributed by metakunt, 23-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝐼, if(𝑥 < 𝐼, 𝑥, (𝑥 + 1))))       (𝜑𝐴:(1...𝑀)⟶(1...𝑀))
 
23-May-2024metakunt1 39345 A is an endomapping. (Contributed by metakunt, 23-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝐼 ∈ ℕ)    &   (𝜑𝐼𝑀)    &   𝐴 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑀, if(𝑥 < 𝐼, 𝑥, (𝑥 − 1))))       (𝜑𝐴:(1...𝑀)⟶(1...𝑀))
 
23-May-2024fzne2d 39265 Elementhood in a finite set of sequential integers, except its upper bound. (Contributed by metakunt, 23-May-2024.)
(𝜑𝐾 ∈ (𝑀...𝑁))    &   (𝜑𝐾𝑁)       (𝜑𝐾 < 𝑁)
 
23-May-2024zltp1led 39264 Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.)
(𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
 
23-May-2024zltlem1d 39263 Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024.)
(𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝑀 < 𝑁𝑀 ≤ (𝑁 − 1)))
 
23-May-2024bj-iminvval2 34606 Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
(𝜑𝐴𝑈)    &   (𝜑𝐵𝑉)    &   (𝜑𝑅 ⊆ (𝐴 × 𝐵))       (𝜑 → ((𝐴𝒫*𝐵)‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑥 = (𝑅𝑦))})
 
23-May-2024bj-iminvval 34605 Value of the functionalized inverse image. (Contributed by BJ, 23-May-2024.)
(𝜑𝐴𝑈)    &   (𝜑𝐵𝑉)       (𝜑 → (𝐴𝒫*𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑥 = (𝑟𝑦))}))
 
23-May-2024bj-imdirco 34602 Functorial property of the direct image: the direct image by a composition is the composition of the direct images. (Contributed by BJ, 23-May-2024.)
(𝜑𝐴𝑈)    &   (𝜑𝐵𝑉)    &   (𝜑𝐶𝑊)    &   (𝜑𝑅 ⊆ (𝐴 × 𝐵))    &   (𝜑𝑆 ⊆ (𝐵 × 𝐶))       (𝜑 → ((𝐴𝒫*𝐶)‘(𝑆𝑅)) = (((𝐵𝒫*𝐶)‘𝑆) ∘ ((𝐴𝒫*𝐵)‘𝑅)))
 
23-May-2024bj-imdirval2lem 34594 Lemma for bj-imdirval2 34595 and bj-iminvval2 34606. (Contributed by BJ, 23-May-2024.)
(𝜑𝐴𝑈)    &   (𝜑𝐵𝑉)       (𝜑 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜓)} ∈ V)
 
23-May-2024bj-imdirvallem 34592 Lemma for bj-imdirval 34593 and bj-iminvval 34605. (Contributed by BJ, 23-May-2024.)
(𝜑𝐴𝑈)    &   (𝜑𝐵𝑉)    &   𝐶 = (𝑎 ∈ V, 𝑏 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑎 × 𝑏) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝑎𝑦𝑏) ∧ 𝜓)}))       (𝜑 → (𝐴𝐶𝐵) = (𝑟 ∈ 𝒫 (𝐴 × 𝐵) ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝜓)}))
 
23-May-2024cbvrmow 3390 Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 3395 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (Contributed by NM, 16-Jun-2017.) (Revised by Gino Giotto, 23-May-2024.)
𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       (∃*𝑥𝐴 𝜑 ↔ ∃*𝑦𝐴 𝜓)
 
23-May-2024cbvralfw 3382 Rule used to change bound variables, using implicit substitution. Version of cbvralf 3385 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (Contributed by NM, 7-Mar-2004.) (Revised by Gino Giotto, 23-May-2024.)
𝑥𝐴    &   𝑦𝐴    &   𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
 
23-May-2024nfcrii 2948 Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2142, ax-11 2158. (Revised by Gino Giotto, 23-May-2024.)
𝑥𝐴       (𝑦𝐴 → ∀𝑥 𝑦𝐴)
 
23-May-2024nfcriOLDOLD 2947 Obsolete version of nfcri 2943 as of 26-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) Avoid ax-10 2142, ax-11 2158. (Revised by Gino Giotto, 23-May-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
𝑥𝐴       𝑥 𝑦𝐴
 
23-May-2024cbvabw 2867 Rule used to change bound variables, using implicit substitution. Version of cbvab 2869 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 23-May-2024.)
𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       {𝑥𝜑} = {𝑦𝜓}
 
23-May-2024cbveuw 2666 Version of cbveu 2668 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (Contributed by NM, 25-Nov-1994.) (Revised by Gino Giotto, 23-May-2024.)
𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       (∃!𝑥𝜑 ↔ ∃!𝑦𝜓)
 
23-May-2024cbvmow 2663 Rule used to change bound variables, using implicit substitution. Version of cbvmo 2665 with a disjoint variable condition, which does not require ax-10 2142, ax-13 2379. (Contributed by NM, 9-Mar-1995.) (Revised by Gino Giotto, 23-May-2024.)
𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
 
23-May-2024hbsbw 2173 If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Version of hbsb 2544 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 12-Aug-1993.) (Revised by Gino Giotto, 23-May-2024.)
(𝜑 → ∀𝑧𝜑)       ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
 
22-May-20242arymaptf1 45062 The mapping of binary (endo)functions is a one-to-one function into the set of binary operations. (Contributed by AV, 22-May-2024.)
𝐻 = ( ∈ (2-aryF 𝑋) ↦ (𝑥𝑋, 𝑦𝑋 ↦ (‘{⟨0, 𝑥⟩, ⟨1, 𝑦⟩})))       (𝑋𝑉𝐻:(2-aryF 𝑋)–1-1→(𝑋m (𝑋 × 𝑋)))
 
22-May-2024reabssgn 40331 Alternate expression for the absolute value of a real number. (Contributed by RP, 22-May-2024.)
(𝐴 ∈ ℝ → (abs‘𝐴) = ((sgn‘𝐴) · 𝐴))
 
22-May-20243lexlogpow5ineq3 39340 Combined inequality chain for a specific power of the binary logarithm, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
(𝜑𝑋 ∈ ℝ)    &   (𝜑 → 3 ≤ 𝑋)       (𝜑 → 7 < ((2 logb 𝑋)↑5))
 
22-May-20243lexlogpow5ineq2 39339 Second inequality in inequality chain, proposed by Mario Carneiro. (Contributed by metakunt, 22-May-2024.)
(𝜑𝑋 ∈ ℝ)    &   (𝜑 → 3 ≤ 𝑋)       (𝜑 → ((3 / 2)↑5) ≤ ((2 logb 𝑋)↑5))
 
22-May-20243lexlogpow5ineq1 39338 First inequality in inequality chain, proposed by Mario Carneiro (Contributed by metakunt, 22-May-2024.)
7 < ((3 / 2)↑5)
 
22-May-2024logblebd 39259 The general logarithm is monotone/increasing, a deduction version. (Contributed by metakunt, 22-May-2024.)
(𝜑𝐵 ∈ ℤ)    &   (𝜑 → 2 ≤ 𝐵)    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑 → 0 < 𝑋)    &   (𝜑𝑌 ∈ ℝ)    &   (𝜑 → 0 < 𝑌)    &   (𝜑𝑋𝑌)       (𝜑 → (𝐵 logb 𝑋) ≤ (𝐵 logb 𝑌))
 
22-May-2024relogbzexpd 39258 Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power, a deduction version (Contributed by metakunt, 22-May-2024.)
(𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐵 ≠ 1)    &   (𝜑𝐶 ∈ ℝ+)    &   (𝜑𝑁 ∈ ℤ)       (𝜑 → (𝐵 logb (𝐶𝑁)) = (𝑁 · (𝐵 logb 𝐶)))
 
22-May-2024relogbexpd 39257 Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024.)
(𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐵 ≠ 1)    &   (𝜑𝑀 ∈ ℤ)       (𝜑 → (𝐵 logb (𝐵𝑀)) = 𝑀)
 
22-May-2024relogbcld 39256 Closure of the general logarithm with a positive real base on positive reals, a deduction version. (Contributed by metakunt, 22-May-2024.)
(𝜑𝐵 ∈ ℝ)    &   (𝜑 → 0 < 𝐵)    &   (𝜑𝑋 ∈ ℝ)    &   (𝜑 → 0 < 𝑋)    &   (𝜑𝐵 ≠ 1)       (𝜑 → (𝐵 logb 𝑋) ∈ ℝ)
 
22-May-2024leexp1ad 39255 Weak mantissa ordering relationship for exponentiation, a deduction version. (Contributed by metakunt, 22-May-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   (𝜑𝑁 ∈ ℕ0)    &   (𝜑 → 0 ≤ 𝐴)    &   (𝜑𝐴𝐵)       (𝜑 → (𝐴𝑁) ≤ (𝐵𝑁))
 
22-May-2024bj-xpcossxp 34601 The composition of two Cartesian products is included in the expected Cartesian product. There is equality if (𝐵𝐶) ≠ ∅, see xpcogend 14325. (Contributed by BJ, 22-May-2024.)
((𝐶 × 𝐷) ∘ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐷)
 
22-May-2024bj-opabco 34600 Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024.)
({⟨𝑦, 𝑧⟩ ∣ 𝜓} ∘ {⟨𝑥, 𝑦⟩ ∣ 𝜑}) = {⟨𝑥, 𝑧⟩ ∣ ∃𝑦(𝜑𝜓)}
 
22-May-2024bj-opelopabid 34599 Membership in an ordered-pair class abstraction. One can remove the DV condition on 𝑥, 𝑦 by using opabid 5378 in place of opabidw 5377. (Contributed by BJ, 22-May-2024.)
(𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}𝑦𝜑)
 
21-May-20242arymaptf 45061 The mapping of binary (endo)functions is a function into the set of binary operations. (Contributed by AV, 21-May-2024.)
𝐻 = ( ∈ (2-aryF 𝑋) ↦ (𝑥𝑋, 𝑦𝑋 ↦ (‘{⟨0, 𝑥⟩, ⟨1, 𝑦⟩})))       (𝑋𝑉𝐻:(2-aryF 𝑋)⟶(𝑋m (𝑋 × 𝑋)))
 
21-May-20242arymaptfv 45060 The value of the mapping of binary (endo)functions. (Contributed by AV, 21-May-2024.)
𝐻 = ( ∈ (2-aryF 𝑋) ↦ (𝑥𝑋, 𝑦𝑋 ↦ (‘{⟨0, 𝑥⟩, ⟨1, 𝑦⟩})))       (𝐹 ∈ (2-aryF 𝑋) → (𝐻𝐹) = (𝑥𝑋, 𝑦𝑋 ↦ (𝐹‘{⟨0, 𝑥⟩, ⟨1, 𝑦⟩})))
 
21-May-2024imsqrtvalex 40341 Example for imsqrtval 40339. (Contributed by RP, 21-May-2024.)
(ℑ‘(√‘(15 + (i · 8)))) = 1
 
21-May-2024resqrtvalex 40340 Example for resqrtval 40338. (Contributed by RP, 21-May-2024.)
(ℜ‘(√‘(15 + (i · 8)))) = 4
 
21-May-2024bj-subst 34165 Equivalent form of the axiom of substitution bj-ax12 34100. Although both sides need a DV condition on 𝑥, 𝑡 (or as in bj-ax12v3 34129 on 𝑡, 𝜑) to hold, their equivalence holds without DV conditions. The forward implication is proved in modal (K4) while the reverse implication is proved in modal (T5). The LHS has the advantage of not involving nested quantifiers on the same variable. Its metaweakening is proved from the core axiom schemes in bj-substw 34166. Note that in the LHS, the reverse implication holds by equs4 2427 (or equs4v 2006 if a DV condition is added on 𝑥, 𝑡 as in bj-ax12 34100).

The LHS can be read as saying that if there exists a setvar equal to a given term witnessing 𝜑, then all setvars equal to that term also witness 𝜑. An equivalent suggestive form for the LHS is ¬ (∃𝑥(𝑥 = 𝑡𝜑) ∧ ∃𝑥(𝑥 = 𝑡 ∧ ¬ 𝜑)), which expresses that there can be no two variables both equal to a given term, one witnessing 𝜑 and the other witnessing ¬ 𝜑. (Contributed by BJ, 21-May-2024.) (Proof modification is discouraged.)

((∃𝑥(𝑥 = 𝑡𝜑) → ∀𝑥(𝑥 = 𝑡𝜑)) ↔ ∀𝑥(𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡𝜑))))
 
20-May-20242arymptfv 45059 The value of a binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.)
𝐹 = (𝑥 ∈ (𝑋m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1)))       ((𝑋𝑉𝐴𝑋𝐵𝑋) → (𝐹‘{⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) = (𝐴𝑂𝐵))
 
20-May-20242arympt 45058 A binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024.)
𝐹 = (𝑥 ∈ (𝑋m {0, 1}) ↦ ((𝑥‘0)𝑂(𝑥‘1)))       ((𝑋𝑉𝑂:(𝑋 × 𝑋)⟶𝑋) → 𝐹 ∈ (2-aryF 𝑋))
 
20-May-2024fv2arycl 45057 Closure of a binary (endo)function. (Contributed by AV, 20-May-2024.)
((𝐺 ∈ (2-aryF 𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐺‘{⟨0, 𝐴⟩, ⟨1, 𝐵⟩}) ∈ 𝑋)
 
20-May-20242aryfvalel 45056 A binary (endo)function on a set 𝑋. (Contributed by AV, 20-May-2024.)
(𝑋𝑉 → (𝐹 ∈ (2-aryF 𝑋) ↔ 𝐹:(𝑋m {0, 1})⟶𝑋))
 
20-May-2024fprmappr 44742 A function with a domain of two elements as element of the mapping operator applied to a pair. (Contributed by AV, 20-May-2024.)
((𝑋𝑉 ∧ (𝐴𝑈𝐵𝑊𝐴𝐵) ∧ (𝐶𝑋𝐷𝑋)) → {⟨𝐴, 𝐶⟩, ⟨𝐵, 𝐷⟩} ∈ (𝑋m {𝐴, 𝐵}))
 
20-May-2024irrdifflemf 34736 Lemma for irrdiff 34737. The forward direction. (Contributed by Jim Kingdon, 20-May-2024.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑 → ¬ 𝐴 ∈ ℚ)    &   (𝜑𝑄 ∈ ℚ)    &   (𝜑𝑅 ∈ ℚ)    &   (𝜑𝑄𝑅)       (𝜑 → (abs‘(𝐴𝑄)) ≠ (abs‘(𝐴𝑅)))
 
20-May-2024fodomg 9933 An onto function implies dominance of domain over range. Lemma 10.20 of [Kunen] p. 30. This theorem uses the axiom of choice ac7g 9885. The axiom of choice is not needed for finite sets, see fodomfi 8781. See also fodomnum 9468. (Contributed by NM, 23-Jul-2004.) (Proof shortened by BJ, 20-May-2024.)
(𝐴𝑉 → (𝐹:𝐴onto𝐵𝐵𝐴))
 
20-May-2024inf0 9068 Existence of ω implies our axiom of infinity ax-inf 9085. The proof shows that the especially contrived class "ran (rec((𝑣 ∈ V ↦ suc 𝑣), 𝑥) ↾ ω) " exists, is a subset of its union, and contains a given set 𝑥 (and thus is nonempty). Thus, it provides an example demonstrating that a set 𝑦 exists with the necessary properties demanded by ax-inf 9085. (Contributed by NM, 15-Oct-1996.) Revised to closed form. (Revised by BJ, 20-May-2024.)
(ω ∈ 𝑉 → ∃𝑦(𝑥𝑦 ∧ ∀𝑧(𝑧𝑦 → ∃𝑤(𝑧𝑤𝑤𝑦))))
 
20-May-2024nsyl5 162 A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.)
(𝜑𝜓)    &   𝜑𝜒)       𝜓𝜒)
 
19-May-20242aryenef 45065 The set of binary (endo)functions and the set of binary operations are equinumerous. (Contributed by AV, 19-May-2024.)
(2-aryF 𝑋) ≈ (𝑋m (𝑋 × 𝑋))
 
19-May-20241aryenefmnd 45055 The set of unary (endo)functions and the base set of the monoid of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.)
(1-aryF 𝑋) ≈ (Base‘(EndoFMnd‘𝑋))
 
19-May-20241aryenef 45054 The set of unary (endo)functions and the set of endofunctions are equinumerous. (Contributed by AV, 19-May-2024.)
(1-aryF 𝑋) ≈ (𝑋m 𝑋)
 
19-May-20241arymaptf1o 45053 The mapping of unary (endo)functions is a one-to-one function onto the set of endofunctions (Contributed by AV, 19-May-2024.)
𝐻 = ( ∈ (1-aryF 𝑋) ↦ (𝑥𝑋 ↦ (‘{⟨0, 𝑥⟩})))       (𝑋𝑉𝐻:(1-aryF 𝑋)–1-1-onto→(𝑋m 𝑋))
 
19-May-20241arymaptf1 45051 The mapping of unary (endo)functions is a one-to-one function into the set of endofunctions. (Contributed by AV, 19-May-2024.)
𝐻 = ( ∈ (1-aryF 𝑋) ↦ (𝑥𝑋 ↦ (‘{⟨0, 𝑥⟩})))       (𝑋𝑉𝐻:(1-aryF 𝑋)–1-1→(𝑋m 𝑋))
 
19-May-20240aryfvalelfv 45044 The value of a nullary (endo)function on a set 𝑋. (Contributed by AV, 19-May-2024.)
(𝐹 ∈ (0-aryF 𝑋) → ∃𝑥𝑋 (𝐹‘∅) = 𝑥)
 
19-May-2024naryfvalixp 45038 The set of the n-ary (endo)functions on a class 𝑋 expressed with the notation of infinite Cartesian products. (Contributed by AV, 19-May-2024.)
𝐼 = (0..^𝑁)       (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋m X𝑥𝐼 𝑋))
 
19-May-2024irrdiff 34737 The irrationals are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 19-May-2024.)
(𝐴 ∈ ℝ → (¬ 𝐴 ∈ ℚ ↔ ∀𝑞 ∈ ℚ ∀𝑟 ∈ ℚ (𝑞𝑟 → (abs‘(𝐴𝑞)) ≠ (abs‘(𝐴𝑟)))))
 
18-May-20241arymaptfo 45052 The mapping of unary (endo)functions is a function onto the set of endofunctions. (Contributed by AV, 18-May-2024.)
𝐻 = ( ∈ (1-aryF 𝑋) ↦ (𝑥𝑋 ↦ (‘{⟨0, 𝑥⟩})))       (𝑋𝑉𝐻:(1-aryF 𝑋)–onto→(𝑋m 𝑋))
 
18-May-20241arymaptf 45050 The mapping of unary (endo)functions is a function into the set of endofunctions. (Contributed by AV, 18-May-2024.)
𝐻 = ( ∈ (1-aryF 𝑋) ↦ (𝑥𝑋 ↦ (‘{⟨0, 𝑥⟩})))       (𝑋𝑉𝐻:(1-aryF 𝑋)⟶(𝑋m 𝑋))
 
18-May-20241arymaptfv 45049 The value of the mapping of unary (endo)functions. (Contributed by AV, 18-May-2024.)
𝐻 = ( ∈ (1-aryF 𝑋) ↦ (𝑥𝑋 ↦ (‘{⟨0, 𝑥⟩})))       (𝐹 ∈ (1-aryF 𝑋) → (𝐻𝐹) = (𝑥𝑋 ↦ (𝐹‘{⟨0, 𝑥⟩})))
 
18-May-2024fv1arycl 45046 Closure of a unary (endo)function. (Contributed by AV, 18-May-2024.)
((𝐺 ∈ (1-aryF 𝑋) ∧ 𝐴𝑋) → (𝐺‘{⟨0, 𝐴⟩}) ∈ 𝑋)
 
18-May-2024imsqrtval 40339 Imaginary part of the complex square root. (Contributed by RP, 18-May-2024.)
(𝐴 ∈ ℂ → (ℑ‘(√‘𝐴)) = (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))
 
18-May-2024resqrtval 40338 Real part of the complex square root. (Contributed by RP, 18-May-2024.)
(𝐴 ∈ ℂ → (ℜ‘(√‘𝐴)) = (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)))
 
18-May-2024sqrtcval2 40337 Explicit formula for the complex square root in terms of the square root of non-negative reals. The right side is slightly more compact than sqrtcval 40336. (Contributed by RP, 18-May-2024.)
(𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (if((ℑ‘𝐴) < 0, -i, i) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)))))
 
18-May-2024sqrtcval 40336 Explicit formula for the complex square root in terms of the square root of non-negative reals. The right-hand side is decomposed into real and imaginary parts in the format expected by crrei 14543 and crimi 14544. This formula can be found in section 3.7.27 of Handbook of Mathematical Functions, ed. M. Abramowitz and I. A. Stegun (1965, Dover Press). (Contributed by RP, 18-May-2024.)
(𝐴 ∈ ℂ → (√‘𝐴) = ((√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) + (i · (if((ℑ‘𝐴) < 0, -1, 1) · (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2))))))
 
18-May-2024fsuppind 39451 Induction on functions 𝐹:𝐴𝐵 with finite support, or in other words the base set of the free module (see frlmelbas 20445 and frlmplusgval 20453). This theorem is structurally general for polynomial proof usage (see mplelbas 20668 and mpladd 20680). (Contributed by SN, 18-May-2024.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    + = (+g𝐺)    &   (𝜑𝐺 ∈ Grp)    &   (𝜑𝐼𝑉)    &   (𝜑 → (𝐼 × { 0 }) ∈ 𝐻)    &   ((𝜑 ∧ (𝑎𝐼𝑏𝐵)) → (𝑥𝐼 ↦ if(𝑥 = 𝑎, 𝑏, 0 )) ∈ 𝐻)    &   ((𝜑 ∧ (𝑥𝐻𝑦𝐻)) → (𝑥f + 𝑦) ∈ 𝐻)       ((𝜑 ∧ (𝑋:𝐼𝐵𝑋 finSupp 0 )) → 𝑋𝐻)
 
17-May-2024sqrtcvallem1 40326 Two ways of saying a complex number does not lie on the positive real axis. Lemma for sqrtcval 40336. (Contributed by RP, 17-May-2024.)
(𝜑𝐴 ∈ ℂ)       (𝜑 → (((ℑ‘𝐴) = 0 → (ℜ‘𝐴) ≤ 0) ↔ ¬ 𝐴 ∈ ℝ+))
 
16-May-20241arympt1fv 45048 The value of a unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
𝐹 = (𝑥 ∈ (𝑋m {0}) ↦ (𝐴‘(𝑥‘0)))       ((𝑋𝑉𝐵𝑋) → (𝐹‘{⟨0, 𝐵⟩}) = (𝐴𝐵))
 
16-May-20241arympt1 45047 A unary (endo)function in maps-to notation. (Contributed by AV, 16-May-2024.)
𝐹 = (𝑥 ∈ (𝑋m {0}) ↦ (𝐴‘(𝑥‘0)))       ((𝑋𝑉𝐴:𝑋𝑋) → 𝐹 ∈ (1-aryF 𝑋))
 
16-May-2024lvecgrpd 39445 A vector space is a group. (Contributed by SN, 16-May-2024.)
(𝜑𝑊 ∈ LVec)       (𝜑𝑊 ∈ Grp)
 
16-May-2024lveclmodd 39444 A vector space is a left module. (Contributed by SN, 16-May-2024.)
(𝜑𝑊 ∈ LVec)       (𝜑𝑊 ∈ LMod)
 
16-May-2024lmodgrpd 39442 A left module is a group. (Contributed by SN, 16-May-2024.)
(𝜑𝑊 ∈ LMod)       (𝜑𝑊 ∈ Grp)
 
16-May-2024drnggrpd 39441 A division ring is a group. (Contributed by SN, 16-May-2024.)
(𝜑𝑅 ∈ DivRing)       (𝜑𝑅 ∈ Grp)
 
16-May-2024drngringd 39440 A division ring is a ring. (Contributed by SN, 16-May-2024.)
(𝜑𝑅 ∈ DivRing)       (𝜑𝑅 ∈ Ring)
 
16-May-2024lcmineqlem 39337 The least common multiple inequality lemma, a central result for future use. Theorem 3.1 from https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 16-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 7 ≤ 𝑁)       (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))
 
16-May-2024crnggrpd 19304 A commutative ring is a group. (Contributed by SN, 16-May-2024.)
(𝜑𝑅 ∈ CRing)       (𝜑𝑅 ∈ Grp)
 
16-May-2024crngringd 19303 A commutative ring is a ring. (Contributed by SN, 16-May-2024.)
(𝜑𝑅 ∈ CRing)       (𝜑𝑅 ∈ Ring)
 
16-May-2024ringgrpd 19299 A ring is a group. (Contributed by SN, 16-May-2024.)
(𝜑𝑅 ∈ Ring)       (𝜑𝑅 ∈ Grp)
 
16-May-2024dfss2 3901 Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.) Avoid ax-10 2142, ax-11 2158, ax-12 2175. (Revised by SN, 16-May-2024.)
(𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 
16-May-2024elab2gw 3613 Membership in a class abstraction, using implicit substitution and an intermediate setvar 𝑦 to avoid ax-10 2142, ax-11 2158, ax-12 2175. It also avoids a disjoint variable condition on 𝑥 and 𝐴. (Contributed by SN, 16-May-2024.)
(𝑥 = 𝑦 → (𝜑𝜓))    &   (𝑦 = 𝐴 → (𝜓𝜒))    &   𝐵 = {𝑥𝜑}       (𝐴𝑉 → (𝐴𝐵𝜒))
 
15-May-20241aryfvalel 45045 A unary (endo)function on a set 𝑋. (Contributed by AV, 15-May-2024.)
(𝑋𝑉 → (𝐹 ∈ (1-aryF 𝑋) ↔ 𝐹:(𝑋m {0})⟶𝑋))
 
15-May-20240aryfvalel 45043 A nullary (endo)function on a set 𝑋 is a singleton of an ordered pair with the empty set as first component. A nullary function represents a constant: (𝐹‘∅) = 𝐶 with 𝐶𝑋, see also 0aryfvalelfv 45044. Instead of (𝐹‘∅), nullary functions are usually written as 𝐹() in literature. (Contributed by AV, 15-May-2024.)
(𝑋𝑉 → (𝐹 ∈ (0-aryF 𝑋) ↔ ∃𝑥𝑋 𝐹 = {⟨∅, 𝑥⟩}))
 
14-May-2024naryfvalelfv 45041 The value of an n-ary (endo)function on a set 𝑋 is an element of 𝑋. (Contributed by AV, 14-May-2024.)
𝐼 = (0..^𝑁)       ((𝐹 ∈ (𝑁-aryF 𝑋) ∧ 𝐴:𝐼𝑋) → (𝐹𝐴) ∈ 𝑋)
 
14-May-2024naryrcl 45040 Reverse closure for n-ary (endo)functions. (Contributed by AV, 14-May-2024.)
𝐼 = (0..^𝑁)       (𝐹 ∈ (𝑁-aryF 𝑋) → (𝑁 ∈ ℕ0𝑋 ∈ V))
 
14-May-2024naryfvalel 45039 An n-ary (endo)function on a set 𝑋. (Contributed by AV, 14-May-2024.)
𝐼 = (0..^𝑁)       ((𝑁 ∈ ℕ0𝑋𝑉) → (𝐹 ∈ (𝑁-aryF 𝑋) ↔ 𝐹:(𝑋m 𝐼)⟶𝑋))
 
14-May-2024mnringmulrcld 40931 Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝐹)    &   𝐴 = (Base‘𝑀)    &    · = (.r𝐹)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝑀𝑈)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)       (𝜑 → (𝑋 · 𝑌) ∈ 𝐵)
 
14-May-2024mnringmulrvald 40930 Value of multiplication in a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝐹)    &    = (.r𝑅)    &    𝟎 = (0g𝑅)    &   𝐴 = (Base‘𝑀)    &    + = (+g𝑀)    &    · = (.r𝐹)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)       (𝜑 → (𝑋 · 𝑌) = (𝐹 Σg (𝑎𝐴, 𝑏𝐴 ↦ (𝑖𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑋𝑎) (𝑌𝑏)), 𝟎 )))))
 
14-May-2024mnringlmodd 40929 Monoid rings are left modules. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝑀𝑈)       (𝜑𝐹 ∈ LMod)
 
14-May-2024mnringvscad 40928 The scalar product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐵)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → ( ·𝑠𝑉) = ( ·𝑠𝐹))
 
14-May-2024mnringscad 40927 The scalar ring of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑𝑅 = (Scalar‘𝐹))
 
14-May-2024mnringmulrd 40926 The ring product of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝐹)    &    · = (.r𝑅)    &    0 = (0g𝑅)    &   𝐴 = (Base‘𝑀)    &    + = (+g𝑀)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → (𝑥𝐵, 𝑦𝐵 ↦ (𝐹 Σg (𝑎𝐴, 𝑏𝐴 ↦ (𝑖𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥𝑎) · (𝑦𝑏)), 0 ))))) = (.r𝐹))
 
14-May-2024mnring0g2d 40925 The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &    0 = (0g𝑅)    &   𝐴 = (Base‘𝑀)    &   (𝜑𝑅 ∈ Ring)    &   (𝜑𝑀𝑊)       (𝜑 → (𝐴 × { 0 }) = (0g𝐹))
 
14-May-2024mnring0gd 40924 The additive identity of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → (0g𝑉) = (0g𝐹))
 
14-May-2024mnringaddgd 40923 The additive operation of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → (+g𝑉) = (+g𝐹))
 
14-May-2024mnringbasefsuppd 40922 Elements of a monoid ring are finitely supported. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝐹)    &    0 = (0g𝑅)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)    &   (𝜑𝑋𝐵)       (𝜑𝑋 finSupp 0 )
 
14-May-2024mnringbasefd 40921 Elements of a monoid ring are functions. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝐹)    &   𝐴 = (Base‘𝑀)    &   𝐶 = (Base‘𝑅)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)    &   (𝜑𝑋𝐵)       (𝜑𝑋:𝐴𝐶)
 
14-May-2024mnringelbased 40920 Membership in the base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝐹)    &   𝐴 = (Base‘𝑀)    &   𝐶 = (Base‘𝑅)    &    0 = (0g𝑅)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → (𝑋𝐵 ↔ (𝑋 ∈ (𝐶m 𝐴) ∧ 𝑋 finSupp 0 )))
 
14-May-2024mnringbaserd 40919 The base set of a monoid ring. Converse of mnringbased 40918. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐵 = (Base‘𝐹)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑𝐵 = (Base‘𝑉))
 
14-May-2024mnringbased 40918 The base set of a monoid ring. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   𝐵 = (Base‘𝑉)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑𝐵 = (Base‘𝐹))
 
14-May-2024mnringnmulrd 40917 Components of a monoid ring other than its ring product match its underlying free module. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &   𝐸 = Slot 𝑁    &   𝑁 ∈ ℕ    &   𝑁 ≠ (.r‘ndx)    &   𝐴 = (Base‘𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑 → (𝐸𝑉) = (𝐸𝐹))
 
14-May-2024mnringvald 40916 Value of the monoid ring function. (Contributed by Rohan Ridenour, 14-May-2024.)
𝐹 = (𝑅 MndRing 𝑀)    &    · = (.r𝑅)    &    0 = (0g𝑅)    &   𝐴 = (Base‘𝑀)    &    + = (+g𝑀)    &   𝑉 = (𝑅 freeLMod 𝐴)    &   𝐵 = (Base‘𝑉)    &   (𝜑𝑅𝑈)    &   (𝜑𝑀𝑊)       (𝜑𝐹 = (𝑉 sSet ⟨(.r‘ndx), (𝑥𝐵, 𝑦𝐵 ↦ (𝑉 Σg (𝑎𝐴, 𝑏𝐴 ↦ (𝑖𝐴 ↦ if(𝑖 = (𝑎 + 𝑏), ((𝑥𝑎) · (𝑦𝑏)), 0 )))))⟩))
 
14-May-2024fvmpopr2d 7290 Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.)
(𝜑𝐹 = (𝑎𝐴, 𝑏𝐵𝐶))    &   (𝜑𝑃 = ⟨𝑎, 𝑏⟩)    &   ((𝜑𝑎𝐴𝑏𝐵) → 𝐶𝑉)       ((𝜑𝑎𝐴𝑏𝐵) → (𝐹𝑃) = 𝐶)
 
13-May-2024naryfval 45037 The set of the n-ary (endo)functions on a class 𝑋. (Contributed by AV, 13-May-2024.)
𝐼 = (0..^𝑁)       (𝑁 ∈ ℕ0 → (𝑁-aryF 𝑋) = (𝑋m (𝑋m 𝐼)))
 
13-May-2024df-mnring 40915 Define the monoid ring function. This takes a monoid 𝑀 and a ring 𝑅 and produces a free left module over 𝑅 with a product extending the monoid function on 𝑀. (Contributed by Rohan Ridenour, 13-May-2024.)
MndRing = (𝑟 ∈ V, 𝑚 ∈ V ↦ (𝑟 freeLMod (Base‘𝑚)) / 𝑣(𝑣 sSet ⟨(.r‘ndx), (𝑥 ∈ (Base‘𝑣), 𝑦 ∈ (Base‘𝑣) ↦ (𝑣 Σg (𝑎 ∈ (Base‘𝑚), 𝑏 ∈ (Base‘𝑚) ↦ (𝑖 ∈ (Base‘𝑚) ↦ if(𝑖 = (𝑎(+g𝑚)𝑏), ((𝑥𝑎)(.r𝑟)(𝑦𝑏)), (0g𝑟))))))⟩))
 
13-May-2024finnzfsuppd 40910 If a function is zero outside of a finite set, it has finite support. (Contributed by Rohan Ridenour, 13-May-2024.)
(𝜑𝐹𝑉)    &   (𝜑𝐹 Fn 𝐷)    &   (𝜑𝑍𝑈)    &   (𝜑𝐴 ∈ Fin)    &   ((𝜑𝑥𝐷) → (𝑥𝐴 ∨ (𝐹𝑥) = 𝑍))       (𝜑𝐹 finSupp 𝑍)
 
13-May-2024fndmexd 7597 If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.)
(𝜑𝐹𝑉)    &   (𝜑𝐹 Fn 𝐷)       (𝜑𝐷 ∈ V)
 
12-May-2024lcmineqlem23 39336 Penultimate step to the lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 9 ≤ 𝑁)       (𝜑 → (2↑𝑁) ≤ (lcm‘(1...𝑁)))
 
12-May-2024lcmineqlem22 39335 The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 4 ≤ 𝑁)       (𝜑 → ((2↑((2 · 𝑁) + 1)) ≤ (lcm‘(1...((2 · 𝑁) + 1))) ∧ (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 2)))))
 
12-May-2024lcmineqlem21 39334 The lcm inequality lemma without base cases 7 and 8. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑 → 4 ≤ 𝑁)       (𝜑 → (2↑((2 · 𝑁) + 2)) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
 
12-May-2024lcmineqlem20 39333 Inequality for lcm lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → (𝑁 · (2↑(2 · 𝑁))) ≤ (lcm‘(1...((2 · 𝑁) + 1))))
 
12-May-2024lcmineqlem19 39332 Dividing implies inequality for lcm inequality lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → ((𝑁 · ((2 · 𝑁) + 1)) · ((2 · 𝑁)C𝑁)) ∥ (lcm‘(1...((2 · 𝑁) + 1))))
 
12-May-2024lcmineqlem18 39331 Technical lemma to shift factors in binomial coefficient. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → ((𝑁 + 1) · (((2 · 𝑁) + 1)C(𝑁 + 1))) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
 
12-May-2024lcmineqlem16 39329 Technical divisibility lemma. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → (𝑀 · (𝑁C𝑀)) ∥ (lcm‘(1...𝑁)))
 
12-May-2024lcmineqlem14 39327 Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐴 ∈ ℕ)    &   (𝜑𝐵 ∈ ℕ)    &   (𝜑𝐶 ∈ ℕ)    &   (𝜑𝐷 ∈ ℕ)    &   (𝜑𝐸 ∈ ℕ)    &   (𝜑 → (𝐴 · 𝐶) ∥ 𝐷)    &   (𝜑 → (𝐵 · 𝐶) ∥ 𝐸)    &   (𝜑𝐷𝐸)    &   (𝜑 → (𝐴 gcd 𝐵) = 1)       (𝜑 → ((𝐴 · 𝐵) · 𝐶) ∥ 𝐸)
 
12-May-2024lcmineqlem13 39326 Induction proof for lcm integral. (Contributed by metakunt, 12-May-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑𝐹 = (1 / (𝑀 · (𝑁C𝑀))))
 
12-May-2024lcmineqlem12 39325 Base case for induction. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → ∫(0[,]1)((𝑡↑(1 − 1)) · ((1 − 𝑡)↑(𝑁 − 1))) d𝑡 = (1 / (1 · (𝑁C1))))
 
12-May-2024lcmineqlem11 39324 Induction step, continuation for binomial coefficients. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 < 𝑁)       (𝜑 → (1 / ((𝑀 + 1) · (𝑁C(𝑀 + 1)))) = ((𝑀 / (𝑁𝑀)) · (1 / (𝑀 · (𝑁C𝑀)))))
 
12-May-2024lcmineqlem10 39323 Induction step of lcmineqlem13 39326 (deduction form). (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 < 𝑁)       (𝜑 → ∫(0[,]1)((𝑥↑((𝑀 + 1) − 1)) · ((1 − 𝑥)↑(𝑁 − (𝑀 + 1)))) d𝑥 = ((𝑀 / (𝑁𝑀)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥))
 
12-May-2024lcmineqlem9 39322 (1-x)^(N-M) is continuous. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁𝑀))) ∈ (ℂ–cn→ℂ))
 
12-May-2024lcmineqlem8 39321 Derivative of (1-x)^(N-M). (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 < 𝑁)       (𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ ((1 − 𝑥)↑(𝑁𝑀)))) = (𝑥 ∈ ℂ ↦ (-(𝑁𝑀) · ((1 − 𝑥)↑((𝑁𝑀) − 1)))))
 
12-May-2024lcmineqlem7 39320 Derivative of 1-x for chain rule application. (Contributed by metakunt, 12-May-2024.)
(ℂ D (𝑥 ∈ ℂ ↦ (1 − 𝑥))) = (𝑥 ∈ ℂ ↦ -1)
 
12-May-2024resdvopclptsd 39313 Restrict derivative on unit interval. (Contributed by metakunt, 12-May-2024.)
(𝜑 → (ℂ D (𝑥 ∈ ℂ ↦ 𝐴)) = (𝑥 ∈ ℂ ↦ 𝐵))    &   ((𝜑𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)    &   ((𝜑𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)       (𝜑 → (ℝ D (𝑥 ∈ (0[,]1) ↦ 𝐴)) = (𝑥 ∈ (0(,)1) ↦ 𝐵))
 
12-May-2024resclunitintvd 39312 Restrict continuous function on closed unit interval. (Contributed by metakunt, 12-May-2024.)
(𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ))       (𝜑 → (𝑥 ∈ (0[,]1) ↦ 𝐴) ∈ ((0[,]1)–cn→ℂ))
 
12-May-2024resopunitintvd 39311 Restrict continuous function on open unit interval. (Contributed by metakunt, 12-May-2024.)
(𝜑 → (𝑥 ∈ ℂ ↦ 𝐴) ∈ (ℂ–cn→ℂ))       (𝜑 → (𝑥 ∈ (0(,)1) ↦ 𝐴) ∈ ((0(,)1)–cn→ℂ))
 
12-May-2024coprmdvds2d 39287 If an integer is divisible by two coprime integers, then it is divisible by their product, a deduction version. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐾 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑 → (𝐾 gcd 𝑀) = 1)    &   (𝜑𝐾𝑁)    &   (𝜑𝑀𝑁)       (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)
 
12-May-2024nnproddivdvdsd 39286 A product of natural numbers divides a natural number if and only if a factor divides the quotient, a deduction version. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐾 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → ((𝐾 · 𝑀) ∥ 𝑁𝐾 ∥ (𝑁 / 𝑀)))
 
12-May-2024nndivdvdsd 39285 A positive integer divides a natural number if and only if the quotient is a positive integer, a deduction version of nndivdvds 15608. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑀 ∈ ℕ)    &   (𝜑𝑁 ∈ ℕ)       (𝜑 → (𝑀𝑁 ↔ (𝑁 / 𝑀) ∈ ℕ))
 
12-May-2024muldvds2d 39284 If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐾 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)       (𝜑𝑀𝑁)
 
12-May-2024muldvds1d 39283 If a product divides an integer, so does one of its factors, a deduction version. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐾 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑 → (𝐾 · 𝑀) ∥ 𝑁)       (𝜑𝐾𝑁)
 
12-May-2024dvdstrd 39282 The divides relation is transitive, a deduction version of dvdstr 15638. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐾 ∈ ℤ)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝐾𝑀)    &   (𝜑𝑀𝑁)       (𝜑𝐾𝑁)
 
12-May-2024recbothd 39277 Take reciprocal on both sides. (Contributed by metakunt, 12-May-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐴 ≠ 0)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐵 ≠ 0)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐶 ≠ 0)    &   (𝜑𝐷 ∈ ℂ)    &   (𝜑𝐷 ≠ 0)       (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐵 / 𝐴) = (𝐷 / 𝐶)))
 
12-May-2024bccl2d 39276 Closure of the binomial coefficient, a deduction version. (Contributed by metakunt, 12-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝐾 ∈ ℕ0)    &   (𝜑𝐾𝑁)       (𝜑 → (𝑁C𝐾) ∈ ℕ)
 
12-May-2024fzindd 39260 Induction on the integers from M to N inclusive, a deduction version. (Contributed by metakunt, 12-May-2024.)
(𝑥 = 𝑀 → (𝜓𝜒))    &   (𝑥 = 𝑦 → (𝜓𝜃))    &   (𝑥 = (𝑦 + 1) → (𝜓𝜏))    &   (𝑥 = 𝐴 → (𝜓𝜂))    &   (𝜑𝜒)    &   ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑀𝑦𝑦 < 𝑁) ∧ 𝜃) → 𝜏)    &   (𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝑀𝑁)       ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 𝑀𝐴𝐴𝑁)) → 𝜂)
 
11-May-2024sqrtcvallem5 40335 Equivalent to saying that the real component of the square root of a complex number is a real number. Lemma for resqrtval 40338 and imsqrtval 40339. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℂ → (√‘(((abs‘𝐴) + (ℜ‘𝐴)) / 2)) ∈ ℝ)
 
11-May-2024sqrtcvallem4 40334 Equivalent to saying that the square of the real component of the square root of a complex number is a non-negative real number. Lemma for sqrtcval 40336. See resqrtval 40338. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) + (ℜ‘𝐴)) / 2))
 
11-May-2024sqrtcvallem3 40333 Equivalent to saying that the absolute value of the imaginary component of the square root of a complex number is a real number. Lemma for sqrtcval 40336, sqrtcval2 40337, resqrtval 40338, and imsqrtval 40339. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℂ → (√‘(((abs‘𝐴) − (ℜ‘𝐴)) / 2)) ∈ ℝ)
 
11-May-2024sqrtcvallem2 40332 Equivalent to saying that the square of the imaginary component of the square root of a complex number is a non-negative real number. Lemma for sqrtcval 40336. See imsqrtval 40339. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℂ → 0 ≤ (((abs‘𝐴) − (ℜ‘𝐴)) / 2))
 
11-May-2024reabsifnneg 40330 Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℝ → (abs‘𝐴) = if(0 ≤ 𝐴, 𝐴, -𝐴))
 
11-May-2024reabsifpos 40329 Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℝ → (abs‘𝐴) = if(0 < 𝐴, 𝐴, -𝐴))
 
11-May-2024reabsifnpos 40328 Alternate expression for the absolute value of a real number. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℝ → (abs‘𝐴) = if(𝐴 ≤ 0, -𝐴, 𝐴))
 
11-May-2024reabsifneg 40327 Alternate expression for the absolute value of a real number. Lemma for sqrtcval 40336. (Contributed by RP, 11-May-2024.)
(𝐴 ∈ ℝ → (abs‘𝐴) = if(𝐴 < 0, -𝐴, 𝐴))
 
11-May-2024wl-2xor 34897 In the recursive scheme

"(n+1)-xor" ↔ if-(𝜑, ¬ "n-xor" , "n-xor" )

we set n = 1 to formally arrive at an expression for "2-xor". It is based on "1-xor", that is known to be equivalent to its only input (see wl-1xor 34896). (Contributed by Wolf Lammen, 11-May-2024.)

(if-(𝜑, ¬ 𝜓, 𝜓) ↔ (𝜑𝜓))
 
11-May-2024wl-1xor 34896 In the recursive scheme

"(n+1)-xor" ↔ if-(𝜑, ¬ "n-xor" , "n-xor" )

we set n = 0 to formally arrive at an expression for "1-xor". The base case "0-xor" is replaced with , as a sequence of 0 inputs never has an odd number being part of it. (Contributed by Wolf Lammen, 11-May-2024.)

(if-(𝜓, ¬ ⊥, ⊥) ↔ 𝜓)
 
10-May-2024lcmineqlem15 39328 F times the least common multiple of 1 to n is a natural number. (Contributed by metakunt, 10-May-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℕ)
 
10-May-2024lcmineqlem6 39319 Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 10-May-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑 → ((lcm‘(1...𝑁)) · 𝐹) ∈ ℤ)
 
10-May-2024lcmineqlem5 39318 Technical lemma for reciprocal multiplication in deduction form. (Contributed by metakunt, 10-May-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)    &   (𝜑𝐶 ≠ 0)       (𝜑 → (𝐴 · (𝐵 · (1 / 𝐶))) = (𝐵 · (𝐴 / 𝐶)))
 
10-May-2024lcmineqlem4 39317 Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. F is found in lcmineqlem6 39319. (Contributed by metakunt, 10-May-2024.)
(𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)    &   (𝜑𝐾 ∈ (0...(𝑁𝑀)))       (𝜑 → ((lcm‘(1...𝑁)) / (𝑀 + 𝐾)) ∈ ℤ)
 
10-May-2024fzadd2d 39262 Membership of a sum in a finite interval of integers, a deduction version. (Contributed by metakunt, 10-May-2024.)
(𝜑𝑀 ∈ ℤ)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝑂 ∈ ℤ)    &   (𝜑𝑃 ∈ ℤ)    &   (𝜑𝐽 ∈ (𝑀...𝑁))    &   (𝜑𝐾 ∈ (𝑂...𝑃))    &   (𝜑𝑄 = (𝑀 + 𝑂))    &   (𝜑𝑅 = (𝑁 + 𝑃))       (𝜑 → (𝐽 + 𝐾) ∈ (𝑄...𝑅))
 
10-May-2024wl-2mintru2 34905 Using the recursion formula

"(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" )

for "2-mintru-2" (meaning "2 out of 2 inputs are true") by plugging in n = 1, m = 1, and simplifying. See wl-1mintru1 34902 and wl-1mintru2 34903 to see that "1-mintru-1" / "1-mintru-2" evaluate to 𝜒 / respectively.

Negating a "n-mintru2" operation means 'at most one input is true', so all inputs exclude each other mutually. Such an exclusion is expressed by a NAND operation (𝜑𝜓), not by a XOR. Applying this idea here (n = 2) yields the expected NAND in case of a pair of inputs. (Contributed by Wolf Lammen, 10-May-2024.)

(if-(𝜓, 𝜒, ⊥) ↔ (𝜓𝜒))
 
10-May-2024wl-2mintru1 34904 Using the recursion formula

"(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" )

for "2-mintru-1" (meaning "at least 1 out of 2 inputs is true") by plugging in n = 1, m = 0, and simplifying. The expression "1-mintru-0" is a base case (meaning at least zero inputs out of 1 are true), evaluating to , and wl-1mintru1 34902 shows "1-mintru-1" is equivalent to the only input.

Negating an "n-mintru1" operation means: All n inputs 𝜑.. 𝜃 are false. This is also conveniently expressed as ¬ (𝜑.. 𝜃), in accordance with the result here. (Contributed by Wolf Lammen, 10-May-2024.)

(if-(𝜓, ⊤, 𝜒) ↔ (𝜓𝜒))
 
10-May-2024wl-1mintru2 34903 Using the recursion formula:

"(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" )

for "1-mintru-2" (meaning "at least 2 out of a single input are true") by plugging in n = 0, m = 1, and simplifying. The expressions "0-mintru-1" and "0-mintru-2" are base cases of the recursion, meaning "in a sequence of zero inputs at least 1 / 2 input is true", evaluate both to .

Since no sequence of inputs has a longer subsequence of whatever property, the resulting is to be expected.

Negating a "n-mintru2" operation has an interesting interpretation: at most one input is true, so all inputs exclude each other mutually. Such an exclusion is expressed by a NAND operation (𝜑𝜓), not by a XOR. Applying this idea here (n = 1) leads to the obvious "In a single input sequence 'at most one is true' always holds". (Contributed by Wolf Lammen, 10-May-2024.)

(if-(𝜒, ⊥, ⊥) ↔ ⊥)
 
10-May-2024wl-1mintru1 34902 Using the recursion formula:

"(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" )

for "1-mintru-1" (meaning "at least 1 out of 1 input is true") by plugging in n = 0, m = 0, and simplifying. The expressions "0-mintru-0" and "0-mintru-1" are base cases of the recursion, meaning "in a sequence of zero inputs, at least 0 / 1 input is true", respectively equvalent to / .

Negating an "n-mintru1" operation means: All n inputs 𝜑.. 𝜃 are false. This is also conveniently expressed as ¬ (𝜑.. 𝜃). Applying this idea here (n = 1) yields the obvious result that in an input sequence of size 1 only then all will be false, if its single input is. (Contributed by Wolf Lammen, 10-May-2024.)

(if-(𝜒, ⊤, ⊥) ↔ 𝜒)
 
9-May-2024ackval50 45107 The Ackermann function at (5,0). (Contributed by AV, 9-May-2024.)
((Ack‘5)‘0) = 65533
 
9-May-2024ackval42a 45106 The Ackermann function at (4,2), expressed with powers of 2. (Contributed by AV, 9-May-2024.)
((Ack‘4)‘2) = ((2↑(2↑(2↑(2↑2)))) − 3)
 
9-May-2024ackval42 45105 The Ackermann function at (4,2). (Contributed by AV, 9-May-2024.)
((Ack‘4)‘2) = ((2↑65536) − 3)
 
9-May-2024ackval41 45104 The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
((Ack‘4)‘1) = 65533
 
9-May-2024ackval41a 45103 The Ackermann function at (4,1). (Contributed by AV, 9-May-2024.)
((Ack‘4)‘1) = ((2↑16) − 3)
 
9-May-2024ackval40 45102 The Ackermann function at (4,0). (Contributed by AV, 9-May-2024.)
((Ack‘4)‘0) = 13
 
8-May-2024ackvalsucsucval 45097 The Ackermann function at the successors. This is the third equation of Péter's definition of the Ackermann function. (Contributed by AV, 8-May-2024.)
((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((Ack‘(𝑀 + 1))‘(𝑁 + 1)) = ((Ack‘𝑀)‘((Ack‘(𝑀 + 1))‘𝑁)))
 
8-May-2024ackfnnn0 45094 The Ackermann function at any nonnegative integer is a function on the nonnegative integers. (Contributed by AV, 4-May-2024.) (Proof shortened by AV, 8-May-2024.)
(𝑀 ∈ ℕ0 → (Ack‘𝑀) Fn ℕ0)
 
8-May-2024ackendofnn0 45093 The Ackermann function at any nonnegative integer is an endofunction on the nonnegative integers. (Contributed by AV, 8-May-2024.)
(𝑀 ∈ ℕ0 → (Ack‘𝑀):ℕ0⟶ℕ0)
 
7-May-2024ackval3012 45101 The Ackermann function at (3,0), (3,1), (3,2). (Contributed by AV, 7-May-2024.)
⟨((Ack‘3)‘0), ((Ack‘3)‘1), ((Ack‘3)‘2)⟩ = ⟨5, 13, 29⟩
 
7-May-2024ackval3 45092 The Ackermann function at 3. (Contributed by AV, 7-May-2024.)
(Ack‘3) = (𝑛 ∈ ℕ0 ↦ ((2↑(𝑛 + 3)) − 3))
 
7-May-2024itcovalt2 45086 The value of the function that returns the n-th iterate of the "times 2 plus a constant" function with regard to composition. (Contributed by AV, 7-May-2024.)
𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))       ((𝐼 ∈ ℕ0𝐶 ∈ ℕ0) → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝐼)) − 𝐶)))
 
7-May-2024itcovalt2lem2 45085 Lemma 2 for itcovalt2 45086: induction step. (Contributed by AV, 7-May-2024.)
𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))       ((𝑦 ∈ ℕ0𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑𝑦)) − 𝐶)) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑(𝑦 + 1))) − 𝐶))))
 
7-May-2024itcovalt2lem2lem2 45083 Lemma 2 for itcovalt2lem2 45085. (Contributed by AV, 7-May-2024.)
(((𝑌 ∈ ℕ0𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((2 · (((𝑁 + 𝐶) · (2↑𝑌)) − 𝐶)) + 𝐶) = (((𝑁 + 𝐶) · (2↑(𝑌 + 1))) − 𝐶))
 
7-May-2024itcovalendof 45078 The n-th iterate of an endofunction is an endofunction. (Contributed by AV, 7-May-2024.)
(𝜑𝐴𝑉)    &   (𝜑𝐹:𝐴𝐴)    &   (𝜑𝑁 ∈ ℕ0)       (𝜑 → ((IterComp‘𝐹)‘𝑁):𝐴𝐴)
 
7-May-2024cos0pilt1 25124 Cosine is between minus one and one on the open interval between zero and π. (Contributed by Jim Kingdon, 7-May-2024.)
(𝐴 ∈ (0(,)π) → (cos‘𝐴) ∈ (-1(,)1))
 
6-May-2024itcovalt2lem2lem1 45082 Lemma 1 for itcovalt2lem2 45085. (Contributed by AV, 6-May-2024.)
(((𝑌 ∈ ℕ ∧ 𝐶 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → (((𝑁 + 𝐶) · 𝑌) − 𝐶) ∈ ℕ0)
 
5-May-2024itcovalt2lem1 45084 Lemma 1 for itcovalt2 45086: induction basis. (Contributed by AV, 5-May-2024.)
𝐹 = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 𝐶))       (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 𝐶) · (2↑0)) − 𝐶)))
 
5-May-2024addinvcom 39563 A number commutes with its additive inverse. Compare remulinvcom 39564. (Contributed by SN, 5-May-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑 → (𝐴 + 𝐵) = 0)       (𝜑 → (𝐵 + 𝐴) = 0)
 
5-May-2024subresre 39562 Subtraction restricted to the reals. (Contributed by SN, 5-May-2024.)
= ( − ↾ (ℝ × ℝ))
 
5-May-2024resubeqsub 39561 Equivalence between real subtraction and subtraction. (Contributed by SN, 5-May-2024.)
((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 𝐵) = (𝐴𝐵))
 
5-May-2024sn-subf 39560 subf 10877 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.)
− :(ℂ × ℂ)⟶ℂ
 
5-May-2024sn-subcl 39559 subcl 10874 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐵) ∈ ℂ)
 
5-May-2024sn-subeu 39558 negeu 10865 without ax-mulcom 10590 and complex number version of resubeu 39510. (Contributed by SN, 5-May-2024.)
((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ∃!𝑥 ∈ ℂ (𝐴 + 𝑥) = 𝐵)
 
5-May-2024sn-mul01 39557 mul01 10808 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.)
(𝐴 ∈ ℂ → (𝐴 · 0) = 0)
 
5-May-2024sn-addid0 39556 A number that sums to itself is zero. Compare addid0 11048, readdid1addid2d 39460. (Contributed by SN, 5-May-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑 → (𝐴 + 𝐴) = 𝐴)       (𝜑𝐴 = 0)
 
5-May-2024reixi 39554 ixi 11258 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.)
(i · i) = (0 − 1)
 
5-May-2024sn-addcan2d 39553 addcan2d 10833 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 + 𝐶) = (𝐵 + 𝐶) ↔ 𝐴 = 𝐵))
 
5-May-2024sn-addid1 39552 addid1 10809 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.)
(𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
 
5-May-2024sn-addcand 39551 addcand 10832 without ax-mulcom 10590. Note how the proof is almost identical to addcan 10813. (Contributed by SN, 5-May-2024.)
(𝜑𝐴 ∈ ℂ)    &   (𝜑𝐵 ∈ ℂ)    &   (𝜑𝐶 ∈ ℂ)       (𝜑 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
 
5-May-2024sn-negex2 39550 Proof of cnegex2 10811 without ax-mulcom 10590. (Contributed by SN, 5-May-2024.)
(𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝑏 + 𝐴) = 0)
 
5-May-2024sn-negex12 39548 A combination of cnegex 10810 and cnegex2 10811, this proof takes cnre 10627 𝐴 = 𝑟 + i · 𝑠 and shows that i · -𝑠 + -𝑟 is both a left and right inverse. (Contributed by SN, 5-May-2024.)
(𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ ((𝐴 + 𝑏) = 0 ∧ (𝑏 + 𝐴) = 0))
 
5-May-2024sbcbi2 3778 Substituting into equivalent wff's gives equivalent results. (Contributed by Giovanni Mascellani, 9-Apr-2018.) (Proof shortened by Wolf Lammen, 4-May-2023.) Avoid ax-10, ax-12. (Revised by Steven Nguyen, 5-May-2024.)
(∀𝑥(𝜑𝜓) → ([𝐴 / 𝑥]𝜑[𝐴 / 𝑥]𝜓))
 
5-May-2024ifpn 1069 Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) (Proof shortened by Wolf Lammen, 5-May-2024.)
(if-(𝜑, 𝜓, 𝜒) ↔ if-(¬ 𝜑, 𝜒, 𝜓))
 
4-May-2024ackval2012 45100 The Ackermann function at (2,0), (2,1), (2,2). (Contributed by AV, 4-May-2024.)
⟨((Ack‘2)‘0), ((Ack‘2)‘1), ((Ack‘2)‘2)⟩ = ⟨3, 5, 7⟩
 
4-May-2024ackval1012 45099 The Ackermann function at (1,0), (1,1), (1,2). (Contributed by AV, 4-May-2024.)
⟨((Ack‘1)‘0), ((Ack‘1)‘1), ((Ack‘1)‘2)⟩ = ⟨2, 3, 4⟩
 
4-May-2024ackvalsuc0val 45096 The Ackermann function at a successor (of the first argument). This is the second equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.)
(𝑀 ∈ ℕ0 → ((Ack‘(𝑀 + 1))‘0) = ((Ack‘𝑀)‘1))
 
4-May-2024ackval0val 45095 The Ackermann function at 0 (for the first argument). This is the first equation of Péter's definition of the Ackermann function. (Contributed by AV, 4-May-2024.)
(𝑀 ∈ ℕ0 → ((Ack‘0)‘𝑀) = (𝑀 + 1))
 
4-May-2024ackval2 45091 The Ackermann function at 2. (Contributed by AV, 4-May-2024.)
(Ack‘2) = (𝑛 ∈ ℕ0 ↦ ((2 · 𝑛) + 3))
 
4-May-2024ackval1 45090 The Ackermann function at 1. (Contributed by AV, 4-May-2024.)
(Ack‘1) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 2))
 
4-May-2024ackvalsuc1 45088 The Ackermann function at a successor of the first argument and an arbitrary second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.)
((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((Ack‘(𝑀 + 1))‘𝑁) = (((IterComp‘(Ack‘𝑀))‘(𝑁 + 1))‘1))
 
4-May-2024ackvalsuc1mpt 45087 The Ackermann function at a successor of the first argument as a mapping of the second argument. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 4-May-2024.)
(𝑀 ∈ ℕ0 → (Ack‘(𝑀 + 1)) = (𝑛 ∈ ℕ0 ↦ (((IterComp‘(Ack‘𝑀))‘(𝑛 + 1))‘1)))
 
4-May-2024itcovalpc 45081 The value of the function that returns the n-th iterate of the "plus a constant" function with regard to composition. (Contributed by AV, 4-May-2024.)
𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))       ((𝐼 ∈ ℕ0𝐶 ∈ ℕ0) → ((IterComp‘𝐹)‘𝐼) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝐼))))
 
4-May-2024itcovalpclem2 45080 Lemma 2 for itcovalpc 45081: induction step. (Contributed by AV, 4-May-2024.)
𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))       ((𝑦 ∈ ℕ0𝐶 ∈ ℕ0) → (((IterComp‘𝐹)‘𝑦) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 𝑦))) → ((IterComp‘𝐹)‘(𝑦 + 1)) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · (𝑦 + 1))))))
 
4-May-2024itcovalpclem1 45079 Lemma 1 for itcovalpc 45081: induction basis. (Contributed by AV, 4-May-2024.)
𝐹 = (𝑛 ∈ ℕ0 ↦ (𝑛 + 𝐶))       (𝐶 ∈ ℕ0 → ((IterComp‘𝐹)‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + (𝐶 · 0))))
 
4-May-2024itcovalsucov 45077 The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.)
((𝐹𝑉𝑌 ∈ ℕ0 ∧ ((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐹𝐺))
 
4-May-2024itcovalsuc 45076 The value of the function that returns the n-th iterate of a function with regard to composition at a successor. (Contributed by AV, 4-May-2024.)
((𝐹𝑉𝑌 ∈ ℕ0 ∧ ((IterComp‘𝐹)‘𝑌) = 𝐺) → ((IterComp‘𝐹)‘(𝑌 + 1)) = (𝐺(𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹𝑔))𝐹))
 
4-May-2024itcoval0mpt 45075 A mapping iterated zero times (defined as identity function). (Contributed by AV, 4-May-2024.)
𝐹 = (𝑛𝐴𝐵)       ((𝐴𝑉 ∧ ∀𝑛𝐴 𝐵𝑊) → ((IterComp‘𝐹)‘0) = (𝑛𝐴𝑛))
 
4-May-2024ichim 43969 Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024.)
(([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) → [𝑎𝑏](𝜑𝜓))
 
4-May-2024ichan 43967 If two setvar variables are interchangeable in two wffs, then they are interchangeable in the conjunction of these two wffs. Notice that the reverse implication is not necessarily true. Corresponding theorems will hold for other commutative operations, too. (Contributed by AV, 31-Jul-2023.) Use df-ich 43958 instead of dfich2 43970 to reduce axioms. (Revised by SN, 4-May-2024.)
(([𝑎𝑏]𝜑 ∧ [𝑎𝑏]𝜓) → [𝑎𝑏](𝜑𝜓))
 
4-May-2024ichbidv 43965 Formula building rule for interchangeability (deduction). (Contributed by SN, 4-May-2024.)
(𝜑 → (𝜓𝜒))       (𝜑 → ([𝑥𝑦]𝜓 ↔ [𝑥𝑦]𝜒))
 
4-May-2024icht 43964 A theorem is interchangeable. (Contributed by SN, 4-May-2024.)
𝜑       [𝑥𝑦]𝜑
 
4-May-2024renegid2 39546 Commuted version of renegid 39506. (Contributed by SN, 4-May-2024.)
(𝐴 ∈ ℝ → ((0 − 𝐴) + 𝐴) = 0)
 
4-May-2024sbtd 39388 A true statement is true upon substitution (deduction). A similar proof is possible for icht 43964. (Contributed by SN, 4-May-2024.)
(𝜑𝜓)       (𝜑 → [𝑡 / 𝑥]𝜓)
 
3-May-2024seqp1d 13381 Value of the sequence builder function at a successor, deduction form. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by AV, 3-May-2024.)
𝑍 = (ℤ𝑀)    &   (𝜑𝑁𝑍)    &   𝐾 = (𝑁 + 1)    &   (𝜑 → (seq𝑀( + , 𝐹)‘𝑁) = 𝐴)    &   (𝜑 → (𝐹𝐾) = 𝐵)       (𝜑 → (seq𝑀( + , 𝐹)‘𝐾) = (𝐴 + 𝐵))
 
2-May-2024ackval0012 45098 The Ackermann function at (0,0), (0,1), (0,2). (Contributed by AV, 2-May-2024.)
⟨((Ack‘0)‘0), ((Ack‘0)‘1), ((Ack‘0)‘2)⟩ = ⟨1, 2, 3⟩
 
2-May-2024ackval0 45089 The Ackermann function at 0. (Contributed by AV, 2-May-2024.)
(Ack‘0) = (𝑛 ∈ ℕ0 ↦ (𝑛 + 1))
 
2-May-2024itcoval3 45074 A function iterated three times. (Contributed by AV, 2-May-2024.)
((Rel 𝐹𝐹𝑉) → ((IterComp‘𝐹)‘3) = (𝐹 ∘ (𝐹𝐹)))
 
2-May-2024itcoval2 45073 A function iterated twice. (Contributed by AV, 2-May-2024.)
((Rel 𝐹𝐹𝑉) → ((IterComp‘𝐹)‘2) = (𝐹𝐹))
 
2-May-2024itcoval1 45072 A function iterated once. (Contributed by AV, 2-May-2024.)
((Rel 𝐹𝐹𝑉) → ((IterComp‘𝐹)‘1) = 𝐹)
 
2-May-2024itcoval0 45071 A function iterated zero times (defined as identity function). (Contributed by AV, 2-May-2024.)
(𝐹𝑉 → ((IterComp‘𝐹)‘0) = ( I ↾ dom 𝐹))
 
2-May-2024itcoval 45070 The value of the function that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by AV, 2-May-2024.)
(𝐹𝑉 → (IterComp‘𝐹) = seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝐹𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝐹), 𝐹))))
 
2-May-2024df-ack 45069 Define the Ackermann function (recursively). (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.)
Ack = seq0((𝑓 ∈ V, 𝑗 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ (((IterComp‘𝑓)‘(𝑛 + 1))‘1))), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, (𝑛 ∈ ℕ0 ↦ (𝑛 + 1)), 𝑖)))
 
2-May-2024df-itco 45068 Define a function (recursively) that returns the n-th iterate of a class (usually a function) with regard to composition. (Contributed by Thierry Arnoux, 28-Apr-2024.) (Revised by AV, 2-May-2024.)
IterComp = (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))))
 
2-May-2024wl-df-3mintru2 34898 Alternative definition of wcad 1608. See df-cad 1609 to learn how it is currently introduced. The only use case so far is being a binary addition primitive for df-sad 15790. If inputs are viewed as binary digits (true is 1, false is 0), the result is whether ordinary binary full addition yields a carry bit. That is what the name df-cad 1609 is derived from: "carry of an addition". Here we stick with this abbreviated form of our notation above, but still use "adder carry" as a shorthand for "at least 2 out of 3" in text.

The core meaning is to check whether at least two of three inputs are true. So, if the first input is true, at least one of the two remaining must be true, else even both. This theorem is the in-between of "at least 1 out of 3", given by triple disjunction df-3or 1085, and "(at least) 3 out of 3", expressed by triple conjunction df-3an 1086.

The notion above can be generalized to other input numbers with other minimum values as follows. Let us introduce informally a logical operation "n-mintru-m" taking n inputs, and requiring at least m of them be true to let the operation itself be true. There now exists a recursive scheme to define it for increasing n, m. We start with the base case n = 0. Here "n-mintru-0" is equivalent to (any sequence of inputs contains at least zero true inputs), the other "0-mintru-m" is for any m > 0 equivalent to , because a sequence of zero inputs never has a positive number of them true. The general case adds a new input 𝜑 to a given sequence of n inputs, and reduces that case for all integers m to that of the smaller sequence by recursion, informally written as:

"(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" )

Our definition here matches "3-mintru-2" with inputs 𝜑, 𝜓 and 𝜒. Starting from the base cases we find after simplifications: "2-mintru-2" (𝜓, 𝜒) ↔ (𝜓𝜒) (wl-2mintru2 34905), and "2-mintru-1" (𝜓, 𝜒) ↔ (𝜓𝜒) (wl-2mintru1 34904). Plugging these expressions into the formula above for n = 3, m = 2 yields exactly our definition here. (Contributed by Wolf Lammen, 2-May-2024.)

(cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓𝜒), (𝜓𝜒)))
 
1-May-2024ichnfimlem 43975 Lemma for ichnfim 43976: A substitution of a non-free variable has no effect. (Contributed by Wolf Lammen, 6-Aug-2023.) Avoid ax-13 2379. (Revised by Gino Giotto, 1-May-2024.)
(∀𝑦𝑥𝜑 → ([𝑎 / 𝑥][𝑏 / 𝑦]𝜑 ↔ [𝑏 / 𝑦]𝜑))
 
1-May-2024wl-3xornot1 34894 Flipping the first input flips the triple xor. wl-3xorrot 34891 can rotate any input to the front, so flipping any one of them does the same. (Contributed by Wolf Lammen, 1-May-2024.)
(¬ hadd(𝜑, 𝜓, 𝜒) ↔ hadd(¬ 𝜑, 𝜓, 𝜒))
 
1-May-2024wl-df3xor3 34884 Alternative form of wl-df3xor2 34883. Copy of df-had 1595. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 1-May-2024.)
(hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ⊻ 𝜒))
 
1-May-2024wl-df3xor2 34883 Alternative definition of wl-df-3xor 34882, using triple exclusive disjunction, or XOR3. You can add more input by appending each one with a . Copy of hadass 1598. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 1-May-2024.)
(hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ (𝜓𝜒)))
 
30-Apr-2024sn-negex 39549 Proof of cnegex 10810 without ax-mulcom 10590. (Contributed by SN, 30-Apr-2024.)
(𝐴 ∈ ℂ → ∃𝑏 ∈ ℂ (𝐴 + 𝑏) = 0)
 
30-Apr-2024sn-it0e0 39547 Proof of it0e0 11847 without ax-mulcom 10590. Informally, a real number times 0 is 0, and 𝑟 ∈ ℝ𝑟 = i · 𝑠 by ax-cnre 10599 and renegid2 39546. (Contributed by SN, 30-Apr-2024.)
(i · 0) = 0
 
30-Apr-2024lcmineqlem3 39316 Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 30-Apr-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑𝐹 = Σ𝑘 ∈ (0...(𝑁𝑀))(((-1↑𝑘) · ((𝑁𝑀)C𝑘)) · (1 / (𝑀 + 𝑘))))
 
30-Apr-2024eliminable-abelab 34305 A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
({𝑥𝜑} ∈ {𝑦𝜓} ↔ ∃𝑧(∀𝑡(𝑡𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ [𝑧 / 𝑦]𝜓))
 
30-Apr-2024eliminable-abelv 34304 A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to variable. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
({𝑥𝜑} ∈ 𝑦 ↔ ∃𝑧(∀𝑡(𝑡𝑧 ↔ [𝑡 / 𝑥]𝜑) ∧ 𝑧𝑦))
 
30-Apr-2024eliminable-abeqab 34303 A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
({𝑥𝜑} = {𝑦𝜓} ↔ ∀𝑧([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓))
 
30-Apr-2024eliminable-abeqv 34302 A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction equals variable. (Contributed by BJ, 30-Apr-2024.) Beware not to use symmetry of class equality. (Proof modification is discouraged.) (New usage is discouraged.)
({𝑥𝜑} = 𝑦 ↔ ∀𝑧([𝑧 / 𝑥]𝜑𝑧𝑦))
 
30-Apr-2024eliminable-veqab 34301 A theorem used to prove the base case of the Eliminability Theorem (see section comment): variable equals abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝑥 = {𝑦𝜑} ↔ ∀𝑧(𝑧𝑥 ↔ [𝑧 / 𝑦]𝜑))
 
30-Apr-2024eliminable-velab 34300 A theorem used to prove the base case of the Eliminability Theorem (see section comment): variable belongs to abstraction. (Contributed by BJ, 30-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
(𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
 
30-Apr-2024ifpdfbi 1066 Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.)
((𝜑𝜓) ↔ if-(𝜑, 𝜓, ¬ 𝜓))
 
29-Apr-2024lcmineqlem17 39330 Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024.)
(𝜑𝑁 ∈ ℕ0)       (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
 
29-Apr-2024lcmineqlem2 39315 Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑𝐹 = Σ𝑘 ∈ (0...(𝑁𝑀))(((-1↑𝑘) · ((𝑁𝑀)C𝑘)) · ∫(0[,]1)((𝑥↑(𝑀 − 1)) · (𝑥𝑘)) d𝑥))
 
29-Apr-2024lcmineqlem1 39314 Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. (Contributed by metakunt, 29-Apr-2024.)
𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · ((1 − 𝑥)↑(𝑁𝑀))) d𝑥    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑀 ∈ ℕ)    &   (𝜑𝑀𝑁)       (𝜑𝐹 = ∫(0[,]1)((𝑥↑(𝑀 − 1)) · Σ𝑘 ∈ (0...(𝑁𝑀))(((-1↑𝑘) · ((𝑁𝑀)C𝑘)) · (𝑥𝑘))) d𝑥)
 
29-Apr-2024lcmfunnnd 39297 Useful equation to calculate the least common multiple of 1 to n. (Contributed by metakunt, 29-Apr-2024.)
(𝜑𝑁 ∈ ℕ)       (𝜑 → (lcm‘(1...𝑁)) = ((lcm‘(1...(𝑁 − 1))) lcm 𝑁))
 
29-Apr-2024wl-3xorfal 34886 If the first input is false, then triple xor is equivalent to the exclusive disjunction of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 29-Apr-2024.)
𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓𝜒)))
 
28-Apr-2024ifpbi23d 1077 Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.)
(𝜑 → (𝜒𝜂))    &   (𝜑 → (𝜃𝜁))       (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜓, 𝜂, 𝜁)))
 
26-Apr-20243factsumint 39310 Helpful equation for lcm inequality proof. (Contributed by metakunt, 26-Apr-2024.)
𝐴 = (𝐿[,]𝑈)    &   (𝜑𝐵 ∈ Fin)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   (𝜑 → (𝑥𝐴𝐹) ∈ (𝐴cn→ℂ))    &   ((𝜑𝑘𝐵) → 𝐺 ∈ ℂ)    &   ((𝜑𝑘𝐵) → (𝑥𝐴𝐻) ∈ (𝐴cn→ℂ))       (𝜑 → ∫𝐴(𝐹 · Σ𝑘𝐵 (𝐺 · 𝐻)) d𝑥 = Σ𝑘𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥))
 
26-Apr-20243factsumint4 39309 Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
(𝜑𝐵 ∈ Fin)    &   ((𝜑𝑥𝐴) → 𝐹 ∈ ℂ)    &   ((𝜑𝑘𝐵) → 𝐺 ∈ ℂ)    &   ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐻 ∈ ℂ)       (𝜑 → ∫𝐴Σ𝑘𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = ∫𝐴(𝐹 · Σ𝑘𝐵 (𝐺 · 𝐻)) d𝑥)
 
26-Apr-20243factsumint3 39308 Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
𝐴 = (𝐿[,]𝑈)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   ((𝜑𝑥𝐴) → 𝐹 ∈ ℂ)    &   (𝜑 → (𝑥𝐴𝐹) ∈ (𝐴cn→ℂ))    &   ((𝜑𝑘𝐵) → 𝐺 ∈ ℂ)    &   ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐻 ∈ ℂ)    &   ((𝜑𝑘𝐵) → (𝑥𝐴𝐻) ∈ (𝐴cn→ℂ))       (𝜑 → Σ𝑘𝐵𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥 = Σ𝑘𝐵 (𝐺 · ∫𝐴(𝐹 · 𝐻) d𝑥))
 
26-Apr-20243factsumint2 39307 Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
((𝜑𝑥𝐴) → 𝐹 ∈ ℂ)    &   ((𝜑𝑘𝐵) → 𝐺 ∈ ℂ)    &   ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐻 ∈ ℂ)       (𝜑 → Σ𝑘𝐵𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘𝐵𝐴(𝐺 · (𝐹 · 𝐻)) d𝑥)
 
26-Apr-20243factsumint1 39306 Move constants out of integrals or sums and/or commute sum and integral. (Contributed by metakunt, 26-Apr-2024.)
𝐴 = (𝐿[,]𝑈)    &   (𝜑𝐵 ∈ Fin)    &   (𝜑𝐿 ∈ ℝ)    &   (𝜑𝑈 ∈ ℝ)    &   ((𝜑𝑥𝐴) → 𝐹 ∈ ℂ)    &   (𝜑 → (𝑥𝐴𝐹) ∈ (𝐴cn→ℂ))    &   ((𝜑𝑘𝐵) → 𝐺 ∈ ℂ)    &   ((𝜑 ∧ (𝑥𝐴𝑘𝐵)) → 𝐻 ∈ ℂ)    &   ((𝜑𝑘𝐵) → (𝑥𝐴𝐻) ∈ (𝐴cn→ℂ))       (𝜑 → ∫𝐴Σ𝑘𝐵 (𝐹 · (𝐺 · 𝐻)) d𝑥 = Σ𝑘𝐵𝐴(𝐹 · (𝐺 · 𝐻)) d𝑥)
 
26-Apr-2024pwrssmgc 30706 Given a function 𝐹, exhibit a Galois connection between subsets of its domain and subsets of its range. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐺 = (𝑛 ∈ 𝒫 𝑌 ↦ (𝐹𝑛))    &   𝐻 = (𝑚 ∈ 𝒫 𝑋 ↦ {𝑦𝑌 ∣ (𝐹 “ {𝑦}) ⊆ 𝑚})    &   𝑉 = (toInc‘𝒫 𝑌)    &   𝑊 = (toInc‘𝒫 𝑋)    &   (𝜑𝑋𝐴)    &   (𝜑𝑌𝐵)    &   (𝜑𝐹:𝑋𝑌)       (𝜑𝐺(𝑉MGalConn𝑊)𝐻)
 
26-Apr-2024mcgcnv 30705 The inverse Galois connection is the Galois connection of the dual orders. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐻 = (𝑉MGalConn𝑊)    &   𝑀 = ((ODual‘𝑊)MGalConn(ODual‘𝑉))       ((𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → (𝐹𝐻𝐺𝐺𝑀𝐹))
 
26-Apr-2024dfmgc2 30704 Alternate definition of the monotone Galois connection. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )       (𝜑 → (𝐹𝐻𝐺 ↔ ((𝐹:𝐴𝐵𝐺:𝐵𝐴) ∧ ((∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)) ∧ ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣))) ∧ (∀𝑢𝐵 (𝐹‘(𝐺𝑢)) 𝑢 ∧ ∀𝑥𝐴 𝑥 (𝐺‘(𝐹𝑥)))))))
 
26-Apr-2024dfmgc2lem 30703 Lemma for dfmgc2, backwards direction. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )    &   (𝜑𝐹:𝐴𝐵)    &   (𝜑𝐺:𝐵𝐴)    &   (𝜑 → ∀𝑥𝐴𝑦𝐴 (𝑥 𝑦 → (𝐹𝑥) (𝐹𝑦)))    &   (𝜑 → ∀𝑢𝐵𝑣𝐵 (𝑢 𝑣 → (𝐺𝑢) (𝐺𝑣)))    &   ((𝜑𝑥𝐴) → 𝑥 (𝐺‘(𝐹𝑥)))    &   ((𝜑𝑢𝐵) → (𝐹‘(𝐺𝑢)) 𝑢)       (𝜑𝐹𝐻𝐺)
 
26-Apr-2024mgcmntco 30702 A Galois connection like statement, for two functions with same range. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )    &   (𝜑𝐹𝐻𝐺)    &   𝐶 = (Base‘𝑋)    &    < = (le‘𝑋)    &   (𝜑𝑋 ∈ Proset )    &   (𝜑𝐾 ∈ (𝑉Monot𝑋))    &   (𝜑𝐿 ∈ (𝑊Monot𝑋))       (𝜑 → (∀𝑥𝐴 (𝐾𝑥) < (𝐿‘(𝐹𝑥)) ↔ ∀𝑦𝐵 (𝐾‘(𝐺𝑦)) < (𝐿𝑦)))
 
26-Apr-2024mcgmnt2 30701 The upper adjoint 𝐺 of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )    &   (𝜑𝐹𝐻𝐺)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)    &   (𝜑𝑋 𝑌)       (𝜑 → (𝐺𝑋) (𝐺𝑌))
 
26-Apr-2024mcgmnt1 30700 The lower adjoint 𝐹 of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )    &   (𝜑𝐹𝐻𝐺)    &   (𝜑𝑋𝐴)    &   (𝜑𝑌𝐴)    &   (𝜑𝑋 𝑌)       (𝜑 → (𝐹𝑋) (𝐹𝑌))
 
26-Apr-2024mgccole2 30699 Inequality for the closure operator (𝐹𝐺) of the Galois connection 𝐻. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )    &   (𝜑𝐹𝐻𝐺)    &   (𝜑𝑌𝐵)       (𝜑 → (𝐹‘(𝐺𝑌)) 𝑌)
 
26-Apr-2024mgccole1 30698 An inequality for the kernel operator 𝐺𝐹. (Contributed by Thierry Arnoux, 26-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )    &   (𝜑𝐹𝐻𝐺)    &   (𝜑𝑋𝐴)       (𝜑𝑋 (𝐺‘(𝐹𝑋)))
 
26-Apr-2024isposd 17557 Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by AV, 26-Apr-2024.)
(𝜑𝐾𝑉)    &   (𝜑𝐵 = (Base‘𝐾))    &   (𝜑 = (le‘𝐾))    &   ((𝜑𝑥𝐵) → 𝑥 𝑥)    &   ((𝜑𝑥𝐵𝑦𝐵) → ((𝑥 𝑦𝑦 𝑥) → 𝑥 = 𝑦))    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵𝑧𝐵)) → ((𝑥 𝑦𝑦 𝑧) → 𝑥 𝑧))       (𝜑𝐾 ∈ Poset)
 
25-Apr-2024lcm8un 39305 Least common multiple of natural numbers up to 8 equals 840. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...8)) = 840
 
25-Apr-2024lcm7un 39304 Least common multiple of natural numbers up to 7 equals 420. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...7)) = 420
 
25-Apr-2024lcm6un 39303 Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...6)) = 60
 
25-Apr-2024lcm5un 39302 Least common multiple of natural numbers up to 5 equals 60. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...5)) = 60
 
25-Apr-2024lcm4un 39301 Least common multiple of natural numbers up to 4 equals 12. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...4)) = 12
 
25-Apr-2024lcm3un 39300 Least common multiple of natural numbers up to 3 equals 6. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...3)) = 6
 
25-Apr-2024lcm2un 39299 Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...2)) = 2
 
25-Apr-2024lcm1un 39298 Least common multiple of natural numbers up to 1 equals 1. (Contributed by metakunt, 25-Apr-2024.)
(lcm‘(1...1)) = 1
 
25-Apr-2024420lcm8e840 39296 The lcm of 420 and 8 is 840. (Contributed by metakunt, 25-Apr-2024.)
(420 lcm 8) = 840
 
25-Apr-202460lcm7e420 39295 The lcm of 60 and 7 is 420. (Contributed by metakunt, 25-Apr-2024.)
(60 lcm 7) = 420
 
25-Apr-202460lcm6e60 39294 The lcm of 60 and 6 is 60. (Contributed by metakunt, 25-Apr-2024.)
(60 lcm 6) = 60
 
25-Apr-202412lcm5e60 39293 The lcm of 12 and 5 is 60. (Contributed by metakunt, 25-Apr-2024.)
(12 lcm 5) = 60
 
25-Apr-2024lcmeprodgcdi 39292 Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝐺 ∈ ℕ    &   𝐻 ∈ ℕ    &   (𝑀 gcd 𝑁) = 𝐺    &   (𝐺 · 𝐻) = 𝐴    &   (𝑀 · 𝑁) = 𝐴       (𝑀 lcm 𝑁) = 𝐻
 
25-Apr-2024420gcd8e4 39291 The gcd of 420 and 8 is 4. (Contributed by metakunt, 25-Apr-2024.)
(420 gcd 8) = 4
 
25-Apr-202460gcd7e1 39290 The gcd of 60 and 7 is 1. (Contributed by metakunt, 25-Apr-2024.)
(60 gcd 7) = 1
 
25-Apr-202460gcd6e6 39289 The gcd of 60 and 6 is 6. (Contributed by metakunt, 25-Apr-2024.)
(60 gcd 6) = 6
 
25-Apr-202412gcd5e1 39288 The gcd of 12 and 5 is 1. (Contributed by metakunt, 25-Apr-2024.)
(12 gcd 5) = 1
 
25-Apr-2024gcdnncli 39281 Closure of the gcd operator. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ       (𝑀 gcd 𝑁) ∈ ℕ
 
25-Apr-2024gcdaddmzz2nncomi 39280 Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝐾 ∈ ℤ       (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))
 
25-Apr-2024gcdaddmzz2nni 39279 Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ    &   𝐾 ∈ ℤ       (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀)))
 
25-Apr-2024gcdmultiplei 39278 The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ       (𝑀 gcd (𝑀 · 𝑁)) = 𝑀
 
25-Apr-2024neggcdnni 39275 Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ       (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)
 
25-Apr-2024gcdnegnni 39274 Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ       (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)
 
25-Apr-2024gcdcomnni 39273 Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024.)
𝑀 ∈ ℕ    &   𝑁 ∈ ℕ       (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)
 
25-Apr-2024mulcomnni 39272 Commutative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
𝐴 ∈ ℕ    &   𝐵 ∈ ℕ       (𝐴 · 𝐵) = (𝐵 · 𝐴)
 
25-Apr-2024mulassnni 39271 Associative law for multiplication. (Contributed by metakunt, 25-Apr-2024.)
𝐴 ∈ ℕ    &   𝐵 ∈ ℕ    &   𝐶 ∈ ℕ       ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
 
25-Apr-2024addcomnni 39270 Commutative law for addition. (Contributed by metakunt, 25-Apr-2024.)
𝐴 ∈ ℕ    &   𝐵 ∈ ℕ       (𝐴 + 𝐵) = (𝐵 + 𝐴)
 
25-Apr-2024addassnni 39269 Associative law for addition. (Contributed by metakunt, 25-Apr-2024.)
𝐴 ∈ ℕ    &   𝐵 ∈ ℕ    &   𝐶 ∈ ℕ       ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
 
25-Apr-2024frgpnabllem2 18987 Lemma for frgpnabl 18988. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.)
𝐺 = (freeGrp‘𝐼)    &   𝑊 = ( I ‘Word (𝐼 × 2o))    &    = ( ~FG𝐼)    &    + = (+g𝐺)    &   𝑀 = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)    &   𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))    &   𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))    &   𝑈 = (varFGrp𝐼)    &   (𝜑𝐼𝑉)    &   (𝜑𝐴𝐼)    &   (𝜑𝐵𝐼)    &   (𝜑 → ((𝑈𝐴) + (𝑈𝐵)) = ((𝑈𝐵) + (𝑈𝐴)))       (𝜑𝐴 = 𝐵)
 
25-Apr-2024frgpnabllem1 18986 Lemma for frgpnabl 18988. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.)
𝐺 = (freeGrp‘𝐼)    &   𝑊 = ( I ‘Word (𝐼 × 2o))    &    = ( ~FG𝐼)    &    + = (+g𝐺)    &   𝑀 = (𝑦𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o𝑧)⟩)    &   𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))    &   𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))    &   𝑈 = (varFGrp𝐼)    &   (𝜑𝐼𝑉)    &   (𝜑𝐴𝐼)    &   (𝜑𝐵𝐼)       (𝜑 → ⟨“⟨𝐴, ∅⟩⟨𝐵, ∅⟩”⟩ ∈ (𝐷 ∩ ((𝑈𝐴) + (𝑈𝐵))))
 
25-Apr-2024lsmpropd 18795 If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-2015.) (Revised by AV, 25-Apr-2024.)
(𝜑𝐵 = (Base‘𝐾))    &   (𝜑𝐵 = (Base‘𝐿))    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐾)𝑦) = (𝑥(+g𝐿)𝑦))    &   (𝜑𝐾𝑉)    &   (𝜑𝐿𝑊)       (𝜑 → (LSSum‘𝐾) = (LSSum‘𝐿))
 
24-Apr-2024wl-3xorcomb 34893 Commutative law for triple xor. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024.)
(hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜑, 𝜒, 𝜓))
 
24-Apr-2024wl-3xorrot 34891 Rotation law for triple xor. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024.)
(hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜓, 𝜒, 𝜑))
 
24-Apr-2024wl-3xorbi123d 34889 Equivalence theorem for triple xor. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024.)
(𝜑 → (𝜓𝜒))    &   (𝜑 → (𝜃𝜏))    &   (𝜑 → (𝜂𝜁))       (𝜑 → (hadd(𝜓, 𝜃, 𝜂) ↔ hadd(𝜒, 𝜏, 𝜁)))
 
24-Apr-2024wl-3xorbi2 34888 Alternative form of wl-3xorbi 34887. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024.)
(hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑𝜓) ↔ 𝜒))
 
24-Apr-2024wl-3xorbi 34887 Triple xor can be replaced with a triple biconditional. Unlike , you cannot add more inputs by simply stacking up more biconditionals, and still express an "odd number of inputs". (Contributed by Wolf Lammen, 24-Apr-2024.)
(hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ↔ (𝜓𝜒)))
 
24-Apr-2024wl-3xortru 34885 If the first input is true, then triple xor is equivalent to the biconditionality of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) df-had redefined. (Revised by Wolf Lammen, 24-Apr-2024.)
(𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ ¬ (𝜓𝜒)))
 
24-Apr-2024wl-df-3xor 34882 Alternative definition of whad 1594 based on hadifp 1607. See df-had 1595 to learn how it is currently introduced. The only use case so far is being a binary addition primitive for df-sad 15790. If inputs are viewed as binary digits (true is 1, false is 0), the result is what a binary single-bit addition with carry-in yields in the low bit of their sum.

The core meaning is to check whether an odd number of three inputs are true. The operation tests this for two inputs. So, if the first input is true, the two remaining inputs need to amount to an even (or: not an odd) number, else to an odd number.

The idea of an odd number of inputs being true carries over to other than 3 inputs by recursion: In an informal notation we depend the case with n+1 inputs, 𝜑 being the additional one, recursively on that of n inputs: "(n+1)-xor" ↔ if-(𝜑, ¬ "n-xor" , "n-xor" ). The base case is "0-xor" being , because zero inputs never contain an odd number among them. Then we find, after simplifying, in our informal notation:

"2-xor" (𝜑, 𝜓) ↔ (𝜑𝜓) (see wl-2xor 34897).

Our definition here follows exactly the above pattern.

In microprocessor technology an addition limited to a range (a one-bit range in our case) is called a "wrap-around operation". The name "had", as in df-had 1595, by contrast, is somehow suggestive of a "half adder" instead. Such a circuit, for one, takes two inputs only, no carry-in, and then yields two outputs - both sum and carry. That's why we use "3xor" instead of "had" here. (Contributed by Wolf Lammen, 24-Apr-2024.)

(hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ (𝜓𝜒), (𝜓𝜒)))
 
24-Apr-2024bj-elabtru 34309 This is as close as we can get to proving extensionality for "the" "universal" class without ax-ext 2770. (Contributed by BJ, 24-Apr-2024.)
(𝐴 ∈ {𝑥 ∣ ⊤} ↔ 𝐴 ∈ {𝑦 ∣ ⊤})
 
24-Apr-2024bj-issettru 34308 Weak version of isset 3453 without ax-ext 2770. (Contributed by BJ, 24-Apr-2024.)
(∃𝑥 𝑥 = 𝐴𝐴 ∈ {𝑦 ∣ ⊤})
 
24-Apr-2024bj-denoteslem 34306 Lemma for bj-denotes 34307. (Contributed by BJ, 24-Apr-2024.)
(∃𝑥 𝑥 = 𝐴𝐴 ∈ {𝑦 ∣ ⊤})
 
24-Apr-2024mgcf2 30697 The upper adjoint 𝐺 of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘𝑊)    &   𝐻 = (𝑉MGalConn𝑊)    &   (𝜑𝑉 ∈ Proset )    &   (𝜑𝑊 ∈ Proset )    &   (𝜑𝐹𝐻𝐺)       (𝜑𝐺:𝐵𝐴)
 
24-Apr-2024mgcf1 30696 The lower adjoint 𝐹 of a Galois connection is a function. (Contributed by Thierry Arnoux, 24-Apr-2024.)
𝐴 = (Base‘𝑉)    &   𝐵 = (Base‘𝑊)    &    = (le‘𝑉)    &    = (le‘