P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rexxfr3d 36001*	Transfer existential quantification from a variable 𝑥 to another variable 𝑦 contained in expression 𝐴. (Contributed by SN, 20-Jun-2025.)
⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rexxfr3dALT 36002*	Longer proof of rexxfr3d 36001 using ax-11 2194 instead of ax-12 2215, without the disjoint variable condition 𝐴𝑥𝑦. (Contributed by SN, 19-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑋 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ ∃𝑦 ∈ 𝐵 𝑥 = 𝑋))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
Theorem	rspssbasd 36003	The span of a set of ring elements is a set of ring elements. (Contributed by SN, 19-Jun-2025.)
⊢ 𝐾 = (RSpan‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐵)    ⇒   ⊢ (𝜑 → (𝐾‘𝐺) ⊆ 𝐵)
Theorem	ellcsrspsn 36004*	Membership in a left coset in a quotient of a ring by the span of a singleton (that is, by the ideal generated by an element). This characterization comes from eqglact 19238 and elrspsn 21338. (Contributed by SN, 19-Jun-2025.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ + = (+g‘𝑅)    &   ⊢ · = (.r‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑈 = (𝑅 /s ∼ )    &   ⊢ 𝐼 = ((RSpan‘𝑅)‘{𝑀})    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝑀 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑈))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 (𝑋 = [𝑥] ∼ ∧ 𝑋 = {𝑧 ∣ ∃𝑦 ∈ 𝐵 𝑧 = (𝑥 + (𝑦 · 𝑀))}))
Theorem	ply1divalg3 36005*	Uniqueness of polynomial remainder: convert the subtraction in ply1divalg2 26257 to addition. (Contributed by SN, 20-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑃)    &   ⊢ + = (+g‘𝑃)    &   ⊢ ∙ = (.r‘𝑃)    &   ⊢ 𝐶 = (Unic1p‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Ring)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝐵 (𝐷‘(𝐹 + (𝑞 ∙ 𝐺))) < (𝐷‘𝐺))
Theorem	r1peuqusdeg1 36006*	Uniqueness of polynomial remainder in terms of a quotient structure in the sense of the right hand side of r1pid2 26280. (Contributed by SN, 21-Jun-2025.)
⊢ 𝑃 = (Poly1‘𝑅)    &   ⊢ 𝐼 = ((RSpan‘𝑃)‘{𝐹})    &   ⊢ 𝑇 = (𝑃 /s (𝑃 ~QG 𝐼))    &   ⊢ 𝑄 = (Base‘𝑇)    &   ⊢ 𝑁 = (Unic1p‘𝑅)    &   ⊢ 𝐷 = (deg1‘𝑅)    &   ⊢ (𝜑 → 𝑅 ∈ Domn)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑁)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑄)    ⇒   ⊢ (𝜑 → ∃!𝑞 ∈ 𝑍 (𝐷‘𝑞) < (𝐷‘𝐹))
Definition	df-sfl1 36007*	Temporary construction for the splitting field of a polynomial. The inputs are a field 𝑟 and a polynomial 𝑝 that we want to split, along with a tuple 𝑗 in the same format as the output. The output is a tuple ⟨𝑆, 𝐹⟩ where 𝑆 is the splitting field and 𝐹 is an injective homomorphism from the original field 𝑟. The function works by repeatedly finding the smallest monic irreducible factor, and extending the field by that factor using the polyFld construction. We keep track of a total order in each of the splitting fields so that we can pick an element definably without needing global choice. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ splitFld1 = (𝑟 ∈ V, 𝑗 ∈ V ↦ (𝑝 ∈ (Poly1‘𝑟) ↦ (rec((𝑠 ∈ V, 𝑓 ∈ V ↦ ⦋(Poly1‘𝑠) / 𝑚⦌⦋{𝑔 ∈ ((Monic1p‘𝑠) ∩ (Irred‘𝑚)) ∣ (𝑔(∥r‘𝑚)(𝑝 ∘ 𝑓) ∧ 1 < (𝑠deg1𝑔))} / 𝑏⦌if(((𝑝 ∘ 𝑓) = (0g‘𝑚) ∨ 𝑏 = ∅), ⟨𝑠, 𝑓⟩, ⦋(glb‘𝑏) / ℎ⦌⦋(𝑠 polyFld ℎ) / 𝑡⦌⟨(1st ‘𝑡), (𝑓 ∘ (2nd ‘𝑡))⟩)), 𝑗)‘(card‘(1...(𝑟deg1𝑝))))))
Definition	df-sfl 36008*	Define the splitting field of a finite collection of polynomials, given a total ordered base field. The output is a tuple ⟨𝑆, 𝐹⟩ where 𝑆 is the totally ordered splitting field and 𝐹 is an injective homomorphism from the original field 𝑟. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ splitFld = (𝑟 ∈ V, 𝑝 ∈ V ↦ (℩𝑥∃𝑓(𝑓 Isom < , (lt‘𝑟)((1...(♯‘𝑝)), 𝑝) ∧ 𝑥 = (seq0((𝑒 ∈ V, 𝑔 ∈ V ↦ ((𝑟 splitFld1 𝑒)‘𝑔)), (𝑓 ∪ {⟨0, ⟨𝑟, ( I ↾ (Base‘𝑟))⟩⟩}))‘(♯‘𝑝)))))
Definition	df-psl 36009*	Define the direct limit of an increasing sequence of fields produced by pasting together the splitting fields for each sequence of polynomials. That is, given a ring 𝑟, a strict order on 𝑟, and a sequence 𝑝:ℕ⟶(𝒫 𝑟 ∩ Fin) of finite sets of polynomials to split, we construct the direct limit system of field extensions by splitting one set at a time and passing the resulting construction to HomLim. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ polySplitLim = (𝑟 ∈ V, 𝑝 ∈ ((𝒫 (Base‘𝑟) ∩ Fin) ↑m ℕ) ↦ ⦋(1st ∘ seq0((𝑔 ∈ V, 𝑞 ∈ V ↦ ⦋(1st ‘𝑔) / 𝑒⦌⦋(1st ‘𝑒) / 𝑠⦌⦋(𝑠 splitFld ran (𝑥 ∈ 𝑞 ↦ (𝑥 ∘ (2nd ‘𝑔)))) / 𝑓⦌⟨𝑓, ((2nd ‘𝑔) ∘ (2nd ‘𝑓))⟩), (𝑝 ∪ {⟨0, ⟨⟨𝑟, ∅⟩, ( I ↾ (Base‘𝑟))⟩⟩}))) / 𝑓⦌((1st ∘ (𝑓 shift 1)) HomLim (2nd ∘ 𝑓)))
21.6.17  p-adic number fields
Syntax	czr 36010	Integral elements of a ring.
class ZRing
Syntax	cgf 36011	Galois finite field.
class GF
Syntax	cgfo 36012	Galois limit field.
class GF∞
Syntax	ceqp 36013	Equivalence relation for df-qp 36024.
class ~Qp
Syntax	crqp 36014	Equivalence relation representatives for df-qp 36024.
class /Qp
Syntax	cqp 36015	The set of 𝑝-adic rational numbers.
class Qp
Syntax	czp 36016	The set of 𝑝-adic integers. (Not to be confused with czn 21612.)
class Zp
Syntax	cqpa 36017	Algebraic completion of the 𝑝-adic rational numbers.
class _Qp
Syntax	ccp 36018	Metric completion of _Qp.
class Cp
Definition	df-zrng 36019	Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟)))
Definition	df-gf 36020*	Define the Galois finite field of order 𝑝↑𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ GF = (𝑝 ∈ ℙ, 𝑛 ∈ ℕ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(1st ‘(𝑟 splitFld {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
Definition	df-gfoo 36021*	Define the Galois field of order 𝑝↑+∞, as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ GF∞ = (𝑝 ∈ ℙ ↦ ⦋(ℤ/nℤ‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {⦋(Poly1‘𝑟) / 𝑠⦌⦋(var1‘𝑟) / 𝑥⦌(((𝑝↑𝑛)(.g‘(mulGrp‘𝑠))𝑥)(-g‘𝑠)𝑥)})))
Definition	df-eqp 36022*	Define an equivalence relation on ℤ-indexed sequences of integers such that two sequences are equivalent iff the difference is equivalent to zero, and a sequence is equivalent to zero iff the sum Σ𝑘 ≤ 𝑛𝑓(𝑘)(𝑝↑𝑘) is a multiple of 𝑝↑(𝑛 + 1) for every 𝑛. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ~Qp = (𝑝 ∈ ℙ ↦ {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m ℤ) ∧ ∀𝑛 ∈ ℤ Σ𝑘 ∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)})
Definition	df-rqp 36023*	There is a unique element of (ℤ ↑m (0...(𝑝 − 1))) ~Qp -equivalent to any element of (ℤ ↑m ℤ), if the sequences are zero for sufficiently large negative values; this function selects that element. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ /Qp = (𝑝 ∈ ℙ ↦ (~Qp ∩ ⦋{𝑓 ∈ (ℤ ↑m ℤ) ∣ ∃𝑥 ∈ ran ℤ≥(◡𝑓 “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑦⦌(𝑦 × (𝑦 ∩ (ℤ ↑m (0...(𝑝 − 1)))))))
Definition	df-qp 36024*	Define the 𝑝-adic completion of the rational numbers, as a normed field structure with a total order (that is not compatible with the operations). (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 10-Oct-2021.)
⊢ Qp = (𝑝 ∈ ℙ ↦ ⦋{ℎ ∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} / 𝑏⦌(({⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))⟩} ∪ {⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}⟩}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ, < ))))))
Definition	df-zp 36025	Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Zp = (ZRing ∘ Qp)
Definition	df-qpa 36026*	Define the completion of the 𝑝-adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the 𝑛-th set the collection of polynomials with degree less than 𝑛 and with coefficients < (𝑝↑𝑛)). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial 𝑥↑(𝑝↑𝑛) − 𝑥, which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ _Qp = (𝑝 ∈ ℙ ↦ ⦋(Qp‘𝑝) / 𝑟⦌(𝑟 polySplitLim (𝑛 ∈ ℕ ↦ {𝑓 ∈ (Poly1‘𝑟) ∣ ((𝑟deg1𝑓) ≤ 𝑛 ∧ ∀𝑑 ∈ ran (coe1‘𝑓)(◡𝑑 “ (ℤ ∖ {0})) ⊆ (0...𝑛))})))
Definition	df-cp 36027	Define the metric completion of the algebraic completion of the 𝑝 -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Cp = ( cplMetSp ∘ _Qp)
21.7  Mathbox for Filip Cernatescu I hope someone will enjoy solving (proving) the simple equations, inequalities, and calculations from this mathbox. I have proved these problems (theorems) using the Milpgame proof assistant. (It can be downloaded from https://us.metamath.org/other/milpgame/milpgame.html.)
Theorem	problem1 36028	Practice problem 1. Clues: 5p4e9 12389 3p2e5 12382 eqtri 2788 oveq1i 7410. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ ((3 + 2) + 4) = 9
Theorem	problem2 36029	Practice problem 2. Clues: oveq12i 7412 adddiri 11210 add4i 11423 mulcli 11204 recni 11211 2re 12306 3eqtri 2792 10re 12725 5re 12319 1re 11196 4re 12316 eqcomi 2774 5p4e9 12389 oveq1i 7410 df-3 12295. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Revised by AV, 9-Sep-2021.) (Proof modification is discouraged.)
⊢ (((2 · ;10) + 5) + ((1 · ;10) + 4)) = ((3 · ;10) + 9)
Theorem	problem3 36030	Practice problem 3. Clues: eqcomi 2774 eqtri 2788 subaddrii 11535 recni 11211 4re 12316 3re 12312 1re 11196 df-4 12296 addcomi 11389. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ (𝐴 + 3) = 4    ⇒   ⊢ 𝐴 = 1
Theorem	problem4 36031	Practice problem 4. Clues: pm3.2i 475 eqcomi 2774 eqtri 2788 subaddrii 11535 recni 11211 7re 12325 6re 12322 ax-1cn 11146 df-7 12299 ax-mp 5 oveq1i 7410 3cn 12313 2cn 12307 df-3 12295 mullidi 11202 subdiri 11652 mp3an 1485 mulcli 11204 subadd23 11457 oveq2i 7411 oveq12i 7412 3t2e6 12397 mulcomi 11205 subcli 11522 biimpri 231 subadd2i 11534. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 3    &   ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7    ⇒   ⊢ (𝐴 = 1 ∧ 𝐵 = 2)
Theorem	problem5 36032	Practice problem 5. Clues: 3brtr3i 5134 mpbi 233 breqtri 5130 ltaddsubi 11763 remulcli 11213 2re 12306 3re 12312 9re 12331 eqcomi 2774 mvlladdi 11464 3cn 6cn 12323 eqtr3i 2790 6p3e9 12391 addcomi 11389 ltdiv1ii 12135 6re 12322 nngt0i 12266 2nn 12305 divcan3i 11952 recni 11211 2cn 12307 2ne0 12338 mpbir 234 eqtri 2788 mulcomi 11205 3t2e6 12397 divmuli 11960. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℝ    &   ⊢ ((2 · 𝐴) + 3) < 9    ⇒   ⊢ 𝐴 < 3
Theorem	quad3 36033	Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.)
⊢ 𝑋 ∈ ℂ    &   ⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0    ⇒   ⊢ (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
21.8  Mathbox for Paul Chapman
21.8.1  Real and complex numbers (cont.)
Theorem	climuzcnv 36034*	Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑))))
Theorem	sinccvglem 36035*	((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Revised by Mario Carneiro, 21-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶(ℝ ∖ {0}))    &   ⊢ (𝜑 → 𝐹 ⇝ 0)    &   ⊢ 𝐺 = (𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥))    &   ⊢ 𝐻 = (𝑥 ∈ ℂ ↦ (1 − ((𝑥↑2) / 3)))    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (abs‘(𝐹‘𝑘)) < 1)    ⇒   ⊢ (𝜑 → (𝐺 ∘ 𝐹) ⇝ 1)
Theorem	sinccvg 36036*	((sin‘𝑥) / 𝑥) ⇝ 1 as (real) 𝑥 ⇝ 0. (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
⊢ ((𝐹:ℕ⟶(ℝ ∖ {0}) ∧ 𝐹 ⇝ 0) → ((𝑥 ∈ (ℝ ∖ {0}) ↦ ((sin‘𝑥) / 𝑥)) ∘ 𝐹) ⇝ 1)
Theorem	circum 36037*	The circumference of a circle of radius 𝑅, defined as the limit as 𝑛 ⇝ +∞ of the perimeter of an inscribed n-sided isogons, is ((2 · π) · 𝑅). (Contributed by Paul Chapman, 10-Nov-2012.) (Proof shortened by Mario Carneiro, 21-May-2014.)
⊢ 𝐴 = ((2 · π) / 𝑛)    &   ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ ((2 · 𝑛) · (𝑅 · (sin‘(𝐴 / 2)))))    &   ⊢ 𝑅 ∈ ℝ    ⇒   ⊢ 𝑃 ⇝ ((2 · π) · 𝑅)
21.8.2  Miscellaneous theorems
Theorem	elfzm12 36038	Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁)))
Theorem	nn0seqcvg 36039*	A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ 𝐹:ℕ0⟶ℕ0    &   ⊢ 𝑁 = (𝐹‘0)    &   ⊢ (𝑘 ∈ ℕ0 → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘)))    ⇒   ⊢ (𝐹‘𝑁) = 0
Theorem	lediv2aALT 36040	Division of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (((𝐴 ∈ ℝ ∧ 0 < 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵) ∧ (𝐶 ∈ ℝ ∧ 0 ≤ 𝐶)) → (𝐴 ≤ 𝐵 → (𝐶 / 𝐵) ≤ (𝐶 / 𝐴)))
Theorem	abs2sqlei 36041	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2))
Theorem	abs2sqlti 36042	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2))
Theorem	abs2sqle 36043	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) ≤ (abs‘𝐵) ↔ ((abs‘𝐴)↑2) ≤ ((abs‘𝐵)↑2)))
Theorem	abs2sqlt 36044	The absolute values of two numbers compare as their squares. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((abs‘𝐴) < (abs‘𝐵) ↔ ((abs‘𝐴)↑2) < ((abs‘𝐵)↑2)))
Theorem	abs2difi 36045	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))
Theorem	abs2difabsi 36046	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))
21.9  Mathbox for Hongxiu Chen
Theorem	2thALT 36047	Alternate proof of 2th 267. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	orbi2iALT 36048	Alternate proof of orbi2i 925. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	pm3.48ALT 36049	Alternate proof of pm3.48 978. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	3jcadALT 36050	Alternate proof of 3jcad 1145. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) Use 3jcad instead. (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))
21.10  Mathbox for Adrian Ducourtial
21.10.1  Propositional calculus
Theorem	currybi 36051	Biconditional version of Curry's paradox. If some proposition 𝜑 amounts to the self-referential statement "This very statement is equivalent to 𝜓", then 𝜓 is true. See bj-currypara 37014 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.)
⊢ ((𝜑 ↔ (𝜑 ↔ 𝜓)) → 𝜓)
Theorem	antnest 36052	Suppose 𝜑, 𝜓 are distinct atomic propositional formulas, and let Γ be the smallest class of formulas for which ⊤ ∈ Γ and (𝜒 → 𝜑), (𝜒 → 𝜓) ∈ Γ for 𝜒 ∈ Γ. The present theorem is then an element of Γ, and the implications occurring in the theorem are in one-to-one correspondence with the formulas in Γ up to logical equivalence. In particular, the theorem itself is equivalent to ⊤ ∈ Γ. (Contributed by Adrian Ducourtial, 2-Oct-2025.)
⊢ ((((((⊤ → 𝜑) → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)
Theorem	antnestlaw3lem 36053	Lemma for antnestlaw3 36056. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ (((𝜑 → 𝜒) → 𝜓) → 𝜓))
Theorem	antnestlaw1 36054	A law of nested antecedents. The converse direction is a subschema of pm2.27 43. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜓) ↔ (𝜑 → 𝜓))
Theorem	antnestlaw2 36055	A law of nested antecedents. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜒) ↔ (((𝜑 → 𝜒) → 𝜓) → 𝜒))
Theorem	antnestlaw3 36056	A law of nested antecedents. Compare with looinv 206. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜒) → 𝜒) ↔ (((𝜑 → 𝜒) → 𝜓) → 𝜓))
Theorem	antnestALT 36057	Alternative proof of antnest 36052 from the valid schema ((((⊤ → 𝜑) → 𝜑) → 𝜓) → 𝜓) using laws of nested antecedents. Our proof uses only the laws antnestlaw1 36054 and antnestlaw3 36056. (Contributed by Adrian Ducourtial, 5-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((((⊤ → 𝜑) → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)
21.10.2  Clone theory
Syntax	ccloneop 36058	Syntax for the function of the class of operations on a set.
class CloneOp
Definition	df-cloneop 36059*	Define the function that sends a set to the class of clone-theoretic operations on the set. For convenience, we take an operation on 𝑎 to be a function on finite sequences of elements of 𝑎 (rather than tuples) with values in 𝑎. Following line 6 of [Szendrei] p. 11, the arity 𝑛 of an operation (here, the length of the sequences at which the operation is defined) is always finite and nonzero, whence 𝑛 is taken to be a nonzero finite ordinal. (Contributed by Adrian Ducourtial, 3-Apr-2025.)
⊢ CloneOp = (𝑎 ∈ V ↦ {𝑥 ∣ ∃𝑛 ∈ (ω ∖ 1o)𝑥 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛))})
Syntax	cprj 36060	Syntax for the function of projections on sets.
class prj
Definition	df-prj 36061*	Define the function that, for a set 𝑎, arity 𝑛, and index 𝑖, returns the 𝑖-th 𝑛-ary projection on 𝑎. This is the 𝑛-ary operation on 𝑎 that, for any sequence of 𝑛 elements of 𝑎, returns the element having index 𝑖. (Contributed by Adrian Ducourtial, 3-Apr-2025.)
⊢ prj = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑖 ∈ 𝑛 ↦ (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖))))
Syntax	csuppos 36062	Syntax for the function of superpositions.
class suppos
Definition	df-suppos 36063*	Define the function that, when given an 𝑛-ary operation 𝑓 and 𝑛 many 𝑚-ary operations (𝑔‘∅), ..., (𝑔‘∪ 𝑛), returns the superposition of 𝑓 with the (𝑔‘𝑖), itself another 𝑚-ary operation on 𝑎. Given 𝑥 (a sequence of 𝑚 arguments in 𝑎), the superposition effectively applies each of the (𝑔‘𝑖) to 𝑥, then applies 𝑓 to the resulting sequence of 𝑛 function values. This can be seen as a generalized version of function composition; see paragraph 3 of [Szendrei] p. 11. (Contributed by Adrian Ducourtial, 3-Apr-2025.)
⊢ suppos = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥)))))))
21.11  Mathbox for Scott Fenton
21.11.1  ZFC Axioms in primitive form
Theorem	axextprim 36064	ax-ext 2737 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧))
Theorem	axrepprim 36065	ax-rep 5232 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥)))
Theorem	axunprim 36066	ax-un 7722 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpowprim 36067	ax-pow 5327 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦)
Theorem	axregprim 36068	ax-reg 9542 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	axinfprim 36069	ax-inf 9595 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))
Theorem	axacprim 36070	ax-ac 10431 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))))))
21.11.2  Untangled classes
Theorem	untelirr 36071*	We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 36153). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ¬ 𝐴 ∈ 𝐴)
Theorem	untuni 36072*	The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥)
Theorem	untsucf 36073*	If a class is untangled, then so is its successor. (Contributed by Scott Fenton, 28-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.)
⊢ Ⅎ𝑦𝐴    ⇒   ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 → ∀𝑦 ∈ suc 𝐴 ¬ 𝑦 ∈ 𝑦)
Theorem	unt0 36074	The null set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥
Theorem	untint 36075*	If there is an untangled element of a class, then the intersection of the class is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦 → ∀𝑦 ∈ ∩ 𝐴 ¬ 𝑦 ∈ 𝑦)
Theorem	efrunt 36076*	If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥)
Theorem	untangtr 36077*	A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.)
⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦))
21.11.3  Extra propositional calculus theorems
Theorem	3jaodd 36078	Double deduction form of 3jaoi 1450. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂)))
Theorem	3orit 36079	Closed form of 3ori 1447. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒))
Theorem	biimpexp 36080	A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒)))
21.11.4  Misc. Useful Theorems
Theorem	nepss 36081	Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.)
⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵))
Theorem	3ccased 36082	Triple disjunction form of ccased 1052. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓))    ⇒   ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓))
Theorem	dfso3 36083*	Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.)
⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	brtpid1 36084	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵
Theorem	brtpid2 36085	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵
Theorem	brtpid3 36086	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵
Theorem	iota5f 36087*	A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	jath 36088	Closed form of ja 188. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))
Theorem	xpab 36089*	Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)}
Theorem	nnuni 36090	The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝐴 ∈ ω → ∪ 𝐴 ∈ ω)
21.11.5  Properties of real and complex numbers
Theorem	sqdivzi 36091	Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
Theorem	supfz 36092	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁)
Theorem	inffz 36093	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)
Theorem	fz0n 36094	The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0))
Theorem	shftvalg 36095	Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	divcnvlin 36096*	Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵)))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	climlec3 36097*	Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	iexpire 36098	i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.)
⊢ (i↑𝑐i) ∈ ℝ
Theorem	bcneg1 36099	The binomial coefficient over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C-1) = 0)
Theorem	bcm1nt 36100	The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾))))