P. 367 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36601-36700   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-zrng 36601	Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ ZRing = (𝑟 ∈ V ↦ (𝑟 IntgRing ran (ℤRHom‘𝑟)))
Definition	df-gf 36602*	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 36603*	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 36604*	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 36605*	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 36606*	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 36607	Define the 𝑝-adic integers, as a subset of the 𝑝-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Zp = (ZRing ∘ Qp)
Definition	df-qpa 36608*	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 36609	Define the metric completion of the algebraic completion of the 𝑝 -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ Cp = ( cplMetSp ∘ _Qp)
21.8  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 36610	Practice problem 1. Clues: 5p4e9 12530 3p2e5 12523 eqtri 2786 oveq1i 7456. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ ((3 + 2) + 4) = 9
Theorem	problem2 36611	Practice problem 2. Clues: oveq12i 7458 adddiri 11352 add4i 11565 mulcli 11346 recni 11353 2re 12447 3eqtri 2790 10re 12867 5re 12460 1re 11338 4re 12457 eqcomi 2772 5p4e9 12530 oveq1i 7456 df-3 12436. (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 36612	Practice problem 3. Clues: eqcomi 2772 eqtri 2786 subaddrii 11677 recni 11353 4re 12457 3re 12453 1re 11338 df-4 12437 addcomi 11531. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ (𝐴 + 3) = 4    ⇒   ⊢ 𝐴 = 1
Theorem	problem4 36613	Practice problem 4. Clues: pm3.2i 476 eqcomi 2772 eqtri 2786 subaddrii 11677 recni 11353 7re 12466 6re 12463 ax-1cn 11288 df-7 12440 ax-mp 5 oveq1i 7456 3cn 12454 2cn 12448 df-3 12436 mullidi 11344 subdiri 11796 mp3an 1491 mulcli 11346 subadd23 11599 oveq2i 7457 oveq12i 7458 3t2e6 12538 mulcomi 11347 subcli 11664 biimpri 231 subadd2i 11676. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ (𝐴 + 𝐵) = 3    &   ⊢ ((3 · 𝐴) + (2 · 𝐵)) = 7    ⇒   ⊢ (𝐴 = 1 ∧ 𝐵 = 2)
Theorem	problem5 36614	Practice problem 5. Clues: 3brtr3i 5138 mpbi 233 breqtri 5134 ltaddsubi 11907 remulcli 11355 2re 12447 3re 12453 9re 12472 eqcomi 2772 mvlladdi 11606 3cn 6cn 12464 eqtr3i 2788 6p3e9 12532 addcomi 11531 ltdiv1ii 12276 6re 12463 nngt0i 12407 2nn 12446 divcan3i 12093 recni 11353 2cn 12448 2ne0 12479 mpbir 234 eqtri 2786 mulcomi 11347 3t2e6 12538 divmuli 12101. (Contributed by Filip Cernatescu, 16-Mar-2019.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ ℝ    &   ⊢ ((2 · 𝐴) + 3) < 9    ⇒   ⊢ 𝐴 < 3
Theorem	quad3 36615	Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.)
⊢ 𝑋 ∈ ℂ    &   ⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 ≠ 0    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0    ⇒   ⊢ (𝑋 = (( -𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = (( -𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)))
21.9  Mathbox for Paul Chapman
21.9.1  Real and complex numbers (cont.)
Theorem	climuzcnv 36616*	Utility lemma to convert between 𝑚 ≤ 𝑘 and 𝑘 ∈ (ℤ≥‘𝑚) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012.)
⊢ (𝑚 ∈ ℕ → ((𝑘 ∈ (ℤ≥‘𝑚) → 𝜑) ↔ (𝑘 ∈ ℕ → (𝑚 ≤ 𝑘 → 𝜑))))
Theorem	sinccvglem 36617*	((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 36618*	((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 36619*	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.9.2  Miscellaneous theorems
Theorem	elfzm12 36620	Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑁 ∈ ℕ → (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (1...𝑁)))
Theorem	nn0seqcvg 36621*	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 36622	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 36623	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 36624	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 36625	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 36626	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 36627	Difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((abs‘𝐴) − (abs‘𝐵)) ≤ (abs‘(𝐴 − 𝐵))
Theorem	abs2difabsi 36628	Absolute value of difference of absolute values. (Contributed by Paul Chapman, 7-Sep-2007.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (abs‘((abs‘𝐴) − (abs‘𝐵))) ≤ (abs‘(𝐴 − 𝐵))
21.10  Mathbox for Hongxiu Chen
Theorem	2thALT 36629	Alternate proof of 2th 267. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	orbi2iALT 36630	Alternate proof of orbi2i 926. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	pm3.48ALT 36631	Alternate proof of pm3.48 978. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	3jcadALT 36632	Alternate proof of 3jcad 1147. (Contributed by Hongxiu Chen, 29-Jun-2025.) (Proof modification is discouraged.) Use 3jcad instead. (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏)))
21.11  Mathbox for Adrian Ducourtial
21.11.1  Propositional calculus
Theorem	currybi 36633	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 37620 in BJ's mathbox for the classical version. (Contributed by Adrian Ducourtial, 18-Mar-2025.)
⊢ ((𝜑 ↔ (𝜑 ↔ 𝜓)) → 𝜓)
Theorem	antnest 36634	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 36635	Lemma for antnestlaw3 36638. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ (¬ (((𝜑 → 𝜓) → 𝜒) → 𝜒) → ¬ (((𝜑 → 𝜒) → 𝜓) → 𝜓))
Theorem	antnestlaw1 36636	A law of nested antecedents. The converse direction is a subschema of pm2.27 43. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜓) ↔ (𝜑 → 𝜓))
Theorem	antnestlaw2 36637	A law of nested antecedents. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜒) ↔ (((𝜑 → 𝜒) → 𝜓) → 𝜒))
Theorem	antnestlaw3 36638	A law of nested antecedents. Compare with looinv 206. (Contributed by Adrian Ducourtial, 5-Dec-2025.)
⊢ ((((𝜑 → 𝜓) → 𝜒) → 𝜒) ↔ (((𝜑 → 𝜒) → 𝜓) → 𝜓))
Theorem	antnestALT 36639	Alternative proof of antnest 36634 from the valid schema ((((⊤ → 𝜑) → 𝜑) → 𝜓) → 𝜓) using laws of nested antecedents. Our proof uses only the laws antnestlaw1 36636 and antnestlaw3 36638. (Contributed by Adrian Ducourtial, 5-Dec-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((((⊤ → 𝜑) → 𝜓) → 𝜓) → 𝜑) → 𝜓) → 𝜓)
21.11.2  Set theory
Theorem	mirimanoffr 36640*	Relative version of mirimanoff 36641 (which corresponds to the case 𝑉 = V). Note that the definition of 𝑀 presupposes that ω is available as a set (omex 9674), which is equivalent to assuming ax-inf2 9672. (Contributed by Adrian Ducourtial, 13-Oct-2026.)
⊢ 𝑀 = {𝑥 ∈ 𝑉 ∣ ¬ ∃𝑓(𝑓 Fn ω ∧ (𝑓‘∅) = 𝑥 ∧ ∀𝑛 ∈ ω (𝑓‘suc 𝑛) ∈ (𝑓‘𝑛))}    ⇒   ⊢ 𝑀 ∉ 𝑉
Theorem	mirimanoff 36641*	Mirimanoff's paradox: The class of grounded sets is not a set. Here, a set 𝑥 is grounded if there is no infinite membership-descending sequence of sets beginning with 𝑥. See Paragraph 1 of [Quine] p. 37 . (Contributed by Adrian Ducourtial, 11-Oct-2026.)
⊢ 𝑀 = {𝑥 ∣ ¬ ∃𝑓(𝑓 Fn ω ∧ (𝑓‘∅) = 𝑥 ∧ ∀𝑛 ∈ ω (𝑓‘suc 𝑛) ∈ (𝑓‘𝑛))}    ⇒   ⊢ 𝑀 ∉ V
Theorem	mirimanofffr 36642*	Relative version of mirimanofff 36643 (which corresponds to the case 𝑉 = V). (Contributed by Adrian Ducourtial, 28-Oct-2026.)
⊢ 𝑀 = {𝑥 ∈ 𝑉 ∣ ∀𝑦(𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)}    ⇒   ⊢ 𝑀 ∉ 𝑉
Theorem	mirimanofff 36643*	Mirimanoff's paradox mirimanoff 36641 for founded sets. A set 𝑥 is founded if every set containing 𝑥 has a minimal element under membership. Compare with zfreg 9620 the defining condition of 𝑀 in the hypothesis. (Contributed by Adrian Ducourtial, 28-Oct-2026.)
⊢ 𝑀 = {𝑥 ∣ ∀𝑦(𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)}    ⇒   ⊢ 𝑀 ∉ V
Theorem	onprcr 36644*	Relative version of onprc 7819. (Contributed by Adrian Ducourtial, 15-Oct-2026.)
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ Ord 𝑥}    &   ⊢ Tr 𝐴    ⇒   ⊢ ¬ 𝐴 ∈ 𝑉
Theorem	onprcALT 36645	Alternate proof of onprc 7819 from onprcr 36644. (Contributed by Adrian Ducourtial, 15-Oct-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ On ∈ V
Theorem	cardprcr 36646*	Relative version of cardprc 10091. (Contributed by Adrian Ducourtial, 15-Oct-2026.)
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (card‘𝑥) = 𝑥}    &   ⊢ (𝐴 ∈ 𝑉 → (har‘∪ 𝐴) ∈ 𝑉)    ⇒   ⊢ ¬ 𝐴 ∈ 𝑉
Theorem	cardprcALT 36647	Alternate proof of cardprc 10091 from cardprcr 36646. (Contributed by Adrian Ducourtial, 15-Oct-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} ∉ V
Theorem	elpssex 36648*	A class has an element just in case it has a proper subset. (Contributed by Adrian Ducourtial, 26-Oct-2026.)
⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ⊊ 𝐴)
Theorem	elpssmo 36649*	Uniqueness of elements is equivalent to uniqueness of proper subsets. (Contributed by Adrian Ducourtial, 26-Oct-2026.)
⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑦 𝑦 ⊊ 𝐴)
Theorem	elpsseu 36650*	A class has a unique element just in case it has a unique proper subset. (Contributed by Adrian Ducourtial, 26-Oct-2026.)
⊢ (∃!𝑥 𝑥 ∈ 𝐴 ↔ ∃!𝑦 𝑦 ⊊ 𝐴)
21.11.3  Clone theory
Syntax	ccloneop 36651	Syntax for the function of the class of operations on a set.
class CloneOp
Definition	df-cloneop 36652*	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 36653	Syntax for the function of projections on sets.
class prj
Definition	df-prj 36654*	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 36655	Syntax for the function of superpositions.
class suppos
Definition	df-suppos 36656*	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.12  Mathbox for Scott Fenton
21.12.1  ZFC Axioms in primitive form
Theorem	axextprim 36657	ax-ext 2735 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ((𝑥 ∈ 𝑦 → 𝑥 ∈ 𝑧) → ((𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦) → 𝑦 = 𝑧))
Theorem	axrepprim 36658	ax-rep 5236 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (¬ ∀𝑦 ¬ ∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧 ¬ ((∀𝑦 𝑧 ∈ 𝑥 → ¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑)) → ¬ (¬ ∀𝑥(∀𝑧 𝑥 ∈ 𝑦 → ¬ ∀𝑦𝜑) → ∀𝑦 𝑧 ∈ 𝑥)))
Theorem	axunprim 36659	ax-un 7778 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦(¬ ∀𝑥(𝑦 ∈ 𝑥 → ¬ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Theorem	axpowprim 36660	ax-pow 5332 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (∀𝑥 ¬ ∀𝑦(∀𝑥(¬ ∀𝑧 ¬ 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) → 𝑥 = 𝑦)
Theorem	axregprim 36661	ax-reg 9616 without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ (𝑥 ∈ 𝑦 → ¬ ∀𝑥(𝑥 ∈ 𝑦 → ¬ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Theorem	axinfprim 36662	ax-inf 9669 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ (𝑦 ∈ 𝑥 → ¬ ∀𝑦(𝑦 ∈ 𝑥 → ¬ ∀𝑧(𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑥))))
Theorem	axacprim 36663	ax-ac 10567 without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 26-Oct-2010.)
⊢ ¬ ∀𝑥 ¬ ∀𝑦∀𝑧(∀𝑥 ¬ (𝑦 ∈ 𝑧 → ¬ 𝑧 ∈ 𝑤) → ¬ ∀𝑤 ¬ ∀𝑦 ¬ ((¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))) → 𝑦 = 𝑤) → ¬ (𝑦 = 𝑤 → ¬ ∀𝑤(𝑦 ∈ 𝑧 → (𝑧 ∈ 𝑤 → (𝑦 ∈ 𝑤 → ¬ 𝑤 ∈ 𝑥))))))
21.12.2  Untangled classes
Theorem	untelirr 36664*	We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 36745). 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 36665*	The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011.)
⊢ (∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝑦 ¬ 𝑥 ∈ 𝑥)
Theorem	untsucf 36666*	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 36667	The empty set is untangled. (Contributed by Scott Fenton, 10-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
⊢ ∀𝑥 ∈ ∅ ¬ 𝑥 ∈ 𝑥
Theorem	untint 36668*	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 36669*	If 𝐴 is well-founded by E, then it is untangled. (Contributed by Scott Fenton, 1-Mar-2011.)
⊢ ( E Fr 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥)
Theorem	untangtr 36670*	A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011.)
⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 ¬ 𝑦 ∈ 𝑦))
21.12.3  Extra propositional calculus theorems
Theorem	3jaodd 36671	Double deduction form of 3jaoi 1455. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))    &   ⊢ (𝜑 → (𝜓 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃 ∨ 𝜏) → 𝜂)))
Theorem	3orit 36672	Closed form of 3ori 1452. (Contributed by Scott Fenton, 20-Apr-2011.)
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒))
Theorem	biimpexp 36673	A biconditional in the antecedent is the same as two implications. (Contributed by Scott Fenton, 12-Dec-2010.)
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → 𝜒)))
21.12.4  Misc. Useful Theorems
Theorem	nepss 36674	Two classes are unequal iff their intersection is a proper subset of one of them. (Contributed by Scott Fenton, 23-Feb-2011.)
⊢ (𝐴 ≠ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) ⊊ 𝐵))
Theorem	3ccased 36675	Triple disjunction form of ccased 1054. (Contributed by Scott Fenton, 27-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝜑 → ((𝜒 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜒 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜃 ∧ 𝜎) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜂) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜁) → 𝜓))    &   ⊢ (𝜑 → ((𝜏 ∧ 𝜎) → 𝜓))    ⇒   ⊢ (𝜑 → (((𝜒 ∨ 𝜃 ∨ 𝜏) ∧ (𝜂 ∨ 𝜁 ∨ 𝜎)) → 𝜓))
Theorem	dfso3 36676*	Expansion of the definition of a strict order. (Contributed by Scott Fenton, 6-Jun-2016.)
⊢ (𝑅 Or 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ∧ (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
Theorem	brtpid1 36677	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{⟨𝐴, 𝐵⟩, 𝐶, 𝐷}𝐵
Theorem	brtpid2 36678	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, ⟨𝐴, 𝐵⟩, 𝐷}𝐵
Theorem	brtpid3 36679	A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016.)
⊢ 𝐴{𝐶, 𝐷, ⟨𝐴, 𝐵⟩}𝐵
Theorem	iota5f 36680*	A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (𝜓 ↔ 𝑥 = 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑉) → (℩𝑥𝜓) = 𝐴)
Theorem	jath 36681	Closed form of ja 188. Proved using the completeness script. (Proof modification is discouraged.) (Contributed by Scott Fenton, 13-Dec-2021.)
⊢ ((¬ 𝜑 → 𝜒) → ((𝜓 → 𝜒) → ((𝜑 → 𝜓) → 𝜒)))
Theorem	xpab 36682*	Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024.)
⊢ ({𝑥 ∣ 𝜑} × {𝑦 ∣ 𝜓}) = {⟨𝑥, 𝑦⟩ ∣ (𝜑 ∧ 𝜓)}
Theorem	nnuni 36683	The union of a finite ordinal is a finite ordinal. (Contributed by Scott Fenton, 17-Oct-2024.)
⊢ (𝐴 ∈ ω → ∪ 𝐴 ∈ ω)
21.12.5  Properties of real and complex numbers
Theorem	sqdivzi 36684	Distribution of square over division. (Contributed by Scott Fenton, 7-Jun-2013.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 ≠ 0 → ((𝐴 / 𝐵)↑2) = ((𝐴↑2) / (𝐵↑2)))
Theorem	supfz 36685	The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → sup((𝑀...𝑁), ℤ, < ) = 𝑁)
Theorem	inffz 36686	The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by AV, 10-Oct-2021.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → inf((𝑀...𝑁), ℤ, < ) = 𝑀)
Theorem	fz0n 36687	The sequence (0...(𝑁 − 1)) is empty iff 𝑁 is zero. (Contributed by Scott Fenton, 16-May-2014.)
⊢ (𝑁 ∈ ℕ0 → ((0...(𝑁 − 1)) = ∅ ↔ 𝑁 = 0))
Theorem	shftvalg 36688	Value of a sequence shifted by 𝐴. (Contributed by Scott Fenton, 16-Dec-2017.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 shift 𝐴)‘𝐵) = (𝐹‘(𝐵 − 𝐴)))
Theorem	divcnvlin 36689*	Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((𝑘 + 𝐴) / (𝑘 + 𝐵)))    ⇒   ⊢ (𝜑 → 𝐹 ⇝ 1)
Theorem	climlec3 36690*	Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐹 ⇝ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ≤ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	iexpire 36691	i raised to itself is real. (Contributed by Scott Fenton, 13-Apr-2020.)
⊢ (i↑𝑐i) ∈ ℝ
Theorem	bcneg1 36692	The binomial coefficient over negative one is zero. (Contributed by Scott Fenton, 29-May-2020.)
⊢ (𝑁 ∈ ℕ0 → (𝑁C -1) = 0)
Theorem	bcm1nt 36693	The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...(𝑁 − 1))) → (𝑁C𝐾) = (((𝑁 − 1)C𝐾) · (𝑁 / (𝑁 − 𝐾))))
Theorem	bcprod 36694*	A product identity for binomial coefficients. (Contributed by Scott Fenton, 23-Jun-2020.)
⊢ (𝑁 ∈ ℕ → ∏𝑘 ∈ (1...(𝑁 − 1))((𝑁 − 1)C𝑘) = ∏𝑘 ∈ (1...(𝑁 − 1))(𝑘↑((2 · 𝑘) − 𝑁)))
Theorem	bccolsum 36695*	A column-sum rule for binomial coefficients. (Contributed by Scott Fenton, 24-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) → Σ𝑘 ∈ (0...𝑁)(𝑘C𝐶) = ((𝑁 + 1)C(𝐶 + 1)))
21.12.6  Infinite products
Theorem	iprodefisumlem 36696	Lemma for iprodefisum 36697. (Contributed by Scott Fenton, 11-Feb-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶ℂ)    ⇒   ⊢ (𝜑 → seq𝑀( · , (exp ∘ 𝐹)) = (exp ∘ seq𝑀( + , 𝐹)))
Theorem	iprodefisum 36697*	Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝑍 (exp‘𝐵) = (exp‘Σ𝑘 ∈ 𝑍 𝐵))
Theorem	iprodgam 36698*	An infinite product version of Euler's gamma function. (Contributed by Scott Fenton, 12-Feb-2018.)
⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))    ⇒   ⊢ (𝜑 → (Γ‘𝐴) = (∏𝑘 ∈ ℕ (((1 + (1 / 𝑘))↑𝑐𝐴) / (1 + (𝐴 / 𝑘))) / 𝐴))
21.12.7  Factorial limits
Theorem	faclimlem1 36699*	Lemma for faclim 36702. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))))
Theorem	faclimlem2 36700*	Lemma for faclim 36702. Show a limit for the inductive step. (Contributed by Scott Fenton, 15-Dec-2017.)
⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) ⇝ (𝑀 + 1))