P. 342 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34101-34200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nn0ltp1ne 34101	Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 + 1) < 𝐵 ↔ (𝐴 < 𝐵 ∧ 𝐵 ≠ (𝐴 + 1))))
Theorem	0nn0m1nnn0 34102	A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023.)
⊢ (𝑁 = 0 ↔ (𝑁 ∈ ℕ0 ∧ ¬ (𝑁 − 1) ∈ ℕ0))
Theorem	f1resfz0f1d 34103	If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐹:(0...𝐾)⟶𝑉)    &   ⊢ (𝜑 → (𝐹 ↾ (1...𝐾)):(1...𝐾)–1-1→𝑉)    &   ⊢ (𝜑 → ((𝐹 “ {0}) ∩ (𝐹 “ (1...𝐾))) = ∅)    ⇒   ⊢ (𝜑 → 𝐹:(0...𝐾)–1-1→𝑉)
Theorem	fisshasheq 34104	A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵)
Theorem	hashf1dmcdm 34105	The size of the domain of a one-to-one set function is less than or equal to the size of its codomain, if it exists. (Contributed by BTernaryTau, 1-Oct-2023.)
⊢ ((𝐹 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐹:𝐴–1-1→𝐵) → (♯‘𝐴) ≤ (♯‘𝐵))
Theorem	revpfxsfxrev 34106	The reverse of a prefix of a word is equal to the same-length suffix of the reverse of that word. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (reverse‘(𝑊 prefix 𝐿)) = ((reverse‘𝑊) substr ⟨((♯‘𝑊) − 𝐿), (♯‘𝑊)⟩))
Theorem	swrdrevpfx 34107	A subword expressed in terms of reverses and prefixes. (Contributed by BTernaryTau, 3-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝐹, 𝐿⟩) = (reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹))))
21.5.3  Graph theory
Theorem	lfuhgr 34108*	A hypergraph is loop-free if and only if every edge connects at least two vertices. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)2 ≤ (♯‘𝑥)))
Theorem	lfuhgr2 34109*	A hypergraph is loop-free if and only if every edge is not a loop. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ∀𝑥 ∈ (Edg‘𝐺)(♯‘𝑥) ≠ 1))
Theorem	lfuhgr3 34110*	A hypergraph is loop-free if and only if none of its edges connect to only one vertex. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} ↔ ¬ ∃𝑎{𝑎} ∈ (Edg‘𝐺)))
Theorem	cplgredgex 34111*	Any two (distinct) vertices in a complete graph are connected to each other by at least one edge. (Contributed by BTernaryTau, 2-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒))
Theorem	cusgredgex 34112	Any two (distinct) vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	cusgredgex2 34113	Any two distinct vertices in a complete simple graph are connected to each other by an edge. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ∈ 𝐸))
Theorem	pfxwlk 34114	A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝐿)(Walks‘𝐺)(𝑃 prefix (𝐿 + 1)))
Theorem	revwlk 34115	The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃))
Theorem	revwlkb 34116	Two words represent a walk if and only if their reverses also represent a walk. (Contributed by BTernaryTau, 4-Dec-2023.)
⊢ ((𝐹 ∈ Word 𝑊 ∧ 𝑃 ∈ Word 𝑈) → (𝐹(Walks‘𝐺)𝑃 ↔ (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃)))
Theorem	swrdwlk 34117	Two matching subwords of a walk also represent a walk. (Contributed by BTernaryTau, 7-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐵 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 substr ⟨𝐵, 𝐿⟩)(Walks‘𝐺)(𝑃 substr ⟨𝐵, (𝐿 + 1)⟩))
Theorem	pthhashvtx 34118	A graph containing a path has at least as many vertices as there are edges in the path. (Contributed by BTernaryTau, 5-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ≤ (♯‘𝑉))
Theorem	pthisspthorcycl 34119	A path is either a simple path or a cycle (or both). (Contributed by BTernaryTau, 20-Oct-2023.)
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝐹(SPaths‘𝐺)𝑃 ∨ 𝐹(Cycles‘𝐺)𝑃))
Theorem	spthcycl 34120	A walk is a trivial path if and only if it is both a simple path and a cycle. (Contributed by BTernaryTau, 8-Oct-2023.)
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 𝐹 = ∅) ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ 𝐹(Cycles‘𝐺)𝑃))
Theorem	usgrgt2cycl 34121	A non-trivial cycle in a simple graph has a length greater than 2. (Contributed by BTernaryTau, 24-Sep-2023.)
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝐹))
Theorem	usgrcyclgt2v 34122	A simple graph with a non-trivial cycle must have at least 3 vertices. (Contributed by BTernaryTau, 5-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 < (♯‘𝑉))
Theorem	subgrwlk 34123	If a walk exists in a subgraph of a graph 𝐺, then that walk also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Walks‘𝑆)𝑃 → 𝐹(Walks‘𝐺)𝑃))
Theorem	subgrtrl 34124	If a trail exists in a subgraph of a graph 𝐺, then that trail also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Trails‘𝑆)𝑃 → 𝐹(Trails‘𝐺)𝑃))
Theorem	subgrpth 34125	If a path exists in a subgraph of a graph 𝐺, then that path also exists in 𝐺. (Contributed by BTernaryTau, 22-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Paths‘𝑆)𝑃 → 𝐹(Paths‘𝐺)𝑃))
Theorem	subgrcycl 34126	If a cycle exists in a subgraph of a graph 𝐺, then that cycle also exists in 𝐺. (Contributed by BTernaryTau, 23-Oct-2023.)
⊢ (𝑆 SubGraph 𝐺 → (𝐹(Cycles‘𝑆)𝑃 → 𝐹(Cycles‘𝐺)𝑃))
Theorem	cusgr3cyclex 34127*	Every complete simple graph with more than two vertices has a 3-cycle. (Contributed by BTernaryTau, 4-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 2 < (♯‘𝑉)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3))
Theorem	loop1cycl 34128*	A hypergraph has a cycle of length one if and only if it has a loop. (Contributed by BTernaryTau, 13-Oct-2023.)
⊢ (𝐺 ∈ UHGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 1 ∧ (𝑝‘0) = 𝐴) ↔ {𝐴} ∈ (Edg‘𝐺)))
Theorem	2cycld 34129	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	2cycl2d 34130	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐴”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐴, 𝐵} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	umgr2cycllem 34131*	Lemma for umgr2cycl 34132. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐽 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → (𝐼‘𝐽) = (𝐼‘𝐾))    ⇒   ⊢ (𝜑 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)
Theorem	umgr2cycl 34132*	A multigraph with two distinct edges that connect the same vertices has a 2-cycle. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ ∃𝑗 ∈ dom 𝐼∃𝑘 ∈ dom 𝐼((𝐼‘𝑗) = (𝐼‘𝑘) ∧ 𝑗 ≠ 𝑘)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 2))
21.5.3.1  Acyclic graphs
Syntax	cacycgr 34133	Extend class notation with acyclic graphs.
class AcyclicGraph
Definition	df-acycgr 34134*	Define the class of all acyclic graphs. A graph is called acyclic if it has no (non-trivial) cycles. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝑔)𝑝 ∧ 𝑓 ≠ ∅)}
Theorem	dfacycgr1 34135*	An alternate definition of the class of all acyclic graphs that requires all cycles to be trivial. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ AcyclicGraph = {𝑔 ∣ ∀𝑓∀𝑝(𝑓(Cycles‘𝑔)𝑝 → 𝑓 = ∅)}
Theorem	isacycgr 34136*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅)))
Theorem	isacycgr1 34137*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝐺)𝑝 → 𝑓 = ∅)))
Theorem	acycgrcycl 34138	Any cycle in an acyclic graph is trivial (i.e. has one vertex and no edges). (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → 𝐹 = ∅)
Theorem	acycgr0v 34139	A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr1v 34140	A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ (♯‘𝑉) = 1) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr2v 34141	A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 2) → 𝐺 ∈ AcyclicGraph)
Theorem	prclisacycgr 34142*	A proper class (representing a null graph, see vtxvalprc 28305) has the property of an acyclic graph (see also acycgr0v 34139). (Contributed by BTernaryTau, 11-Oct-2023.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ 𝐺 ∈ V → ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅))
Theorem	acycgrislfgr 34143*	An acyclic hypergraph is a loop-free hypergraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph) → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})
Theorem	upgracycumgr 34144	An acyclic pseudograph is a multigraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ UMGraph)
Theorem	umgracycusgr 34145	An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	upgracycusgr 34146	An acyclic pseudograph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	cusgracyclt3v 34147	A complete simple graph is acyclic if and only if it has fewer than three vertices. (Contributed by BTernaryTau, 20-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ ComplUSGraph → (𝐺 ∈ AcyclicGraph ↔ (♯‘𝑉) < 3))
Theorem	pthacycspth 34148	A path in an acyclic graph is a simple path. (Contributed by BTernaryTau, 21-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Paths‘𝐺)𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	acycgrsubgr 34149	The subgraph of an acyclic graph is also acyclic. (Contributed by BTernaryTau, 23-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ AcyclicGraph)
21.6  Mathbox for Mario Carneiro
21.6.1  Predicate calculus with all distinct variables
Axiom	ax-7d 34150*	Distinct variable version of ax-11 2155. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Axiom	ax-8d 34151*	Distinct variable version of ax-7 2012. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Axiom	ax-9d1 34152	Distinct variable version of ax-6 1972, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑥
Axiom	ax-9d2 34153*	Distinct variable version of ax-6 1972, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Axiom	ax-10d 34154*	Distinct variable version of axc11n 2426. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-11d 34155*	Distinct variable version of ax-12 2172. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
21.6.2  Miscellaneous stuff
Theorem	quartfull 34156	The quartic equation, written out in full. This actually makes a fairly good Metamath stress test. Note that the length of this formula could be shortened significantly if the intermediate expressions were expanded and simplified, but it's not like this theorem will be used anyway. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)) ≠ 0)    &   ⊢ (𝜑 → -((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3) ≠ 0)    ⇒   ⊢ (𝜑 → ((((𝑋↑4) + (𝐴 · (𝑋↑3))) + ((𝐵 · (𝑋↑2)) + ((𝐶 · 𝑋) + 𝐷))) = 0 ↔ ((𝑋 = ((-(𝐴 / 4) − ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) + (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) + ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2))))) ∨ 𝑋 = ((-(𝐴 / 4) − ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) − (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) + ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)))))) ∨ (𝑋 = ((-(𝐴 / 4) + ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) + (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) − ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2))))) ∨ 𝑋 = ((-(𝐴 / 4) + ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)) − (√‘((-(((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)↑2) − ((𝐵 − ((3 / 8) · (𝐴↑2))) / 2)) − ((((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8)) / 4) / ((√‘-((((2 · (𝐵 − ((3 / 8) · (𝐴↑2)))) + (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3))) + ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))) / (((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))) + (√‘((((-(2 · ((𝐵 − ((3 / 8) · (𝐴↑2)))↑3)) − (;27 · (((𝐶 − ((𝐴 · 𝐵) / 2)) + ((𝐴↑3) / 8))↑2))) + (;72 · ((𝐵 − ((3 / 8) · (𝐴↑2))) · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4)))))))↑2) − (4 · ((((𝐵 − ((3 / 8) · (𝐴↑2)))↑2) + (;12 · ((𝐷 − ((𝐶 · 𝐴) / 4)) + ((((𝐴↑2) · 𝐵) / ;16) − ((3 / ;;256) · (𝐴↑4))))))↑3))))) / 2)↑𝑐(1 / 3)))) / 3)) / 2)))))))))
21.6.3  Derangements and the Subfactorial
Theorem	deranglem 34157*	Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ 𝜑)} ∈ Fin)
Theorem	derangval 34158*	Define the derangement function, which counts the number of bijections from a set to itself such that no element is mapped to itself. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ≠ 𝑦)}))
Theorem	derangf 34159*	The derangement number is a function from finite sets to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ 𝐷:Fin⟶ℕ0
Theorem	derang0 34160*	The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐷‘∅) = 1
Theorem	derangsn 34161*	The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐷‘{𝐴}) = 0)
Theorem	derangenlem 34162*	One half of derangen 34163. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))
Theorem	derangen 34163*	The derangement number is a cardinal invariant, i.e. it only depends on the size of a set and not on its contents. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) = (𝐷‘𝐵))
Theorem	subfacval 34164*	The subfactorial is defined as the number of derangements (see derangval 34158) of the set (1...𝑁). (Contributed by Mario Carneiro, 21-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) = (𝐷‘(1...𝑁)))
Theorem	derangen2 34165*	Write the derangement number in terms of the subfactorial. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝐴 ∈ Fin → (𝐷‘𝐴) = (𝑆‘(♯‘𝐴)))
Theorem	subfacf 34166*	The subfactorial is a function from nonnegative integers to nonnegative integers. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ 𝑆:ℕ0⟶ℕ0
Theorem	subfaclefac 34167*	The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) ≤ (!‘𝑁))
Theorem	subfac0 34168*	The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘0) = 1
Theorem	subfac1 34169*	The subfactorial at one. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘1) = 0
Theorem	subfacp1lem1 34170*	Lemma for subfacp1 34177. The set 𝐾 together with {1, 𝑀} partitions the set 1...(𝑁 + 1). (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    ⇒   ⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (♯‘𝐾) = (𝑁 − 1)))
Theorem	subfacp1lem2a 34171*	Lemma for subfacp1 34177. Properties of a bijection on 𝐾 augmented with the two-element flip to get a bijection on 𝐾 ∪ {1, 𝑀}. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐹 = (𝐺 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    &   ⊢ (𝜑 → 𝐺:𝐾–1-1-onto→𝐾)    ⇒   ⊢ (𝜑 → (𝐹:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ (𝐹‘1) = 𝑀 ∧ (𝐹‘𝑀) = 1))
Theorem	subfacp1lem2b 34172*	Lemma for subfacp1 34177. Properties of a bijection on 𝐾 augmented with the two-element flip to get a bijection on 𝐾 ∪ {1, 𝑀}. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐹 = (𝐺 ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    &   ⊢ (𝜑 → 𝐺:𝐾–1-1-onto→𝐾)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐾) → (𝐹‘𝑋) = (𝐺‘𝑋))
Theorem	subfacp1lem3 34173*	Lemma for subfacp1 34177. In subfacp1lem6 34176 we cut up the set of all derangements on 1...(𝑁 + 1) first according to the value at 1, and then by whether or not (𝑓‘(𝑓‘1)) = 1. In this lemma, we show that the subset of all 𝑁 + 1 derangements that satisfy this for fixed 𝑀 = (𝑓‘1) is in bijection with 𝑁 − 1 derangements, by simply dropping the 𝑥 = 1 and 𝑥 = 𝑀 points from the function to get a derangement on 𝐾 = (1...(𝑁 − 1)) ∖ {1, 𝑀}. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) = 1)}    &   ⊢ 𝐶 = {𝑓 ∣ (𝑓:𝐾–1-1-onto→𝐾 ∧ ∀𝑦 ∈ 𝐾 (𝑓‘𝑦) ≠ 𝑦)}    ⇒   ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘(𝑁 − 1)))
Theorem	subfacp1lem4 34174*	Lemma for subfacp1 34177. The function 𝐹, which swaps 1 with 𝑀 and leaves all other elements alone, is a bijection of order 2, i.e. it is its own inverse. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}    &   ⊢ 𝐹 = (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    ⇒   ⊢ (𝜑 → ◡𝐹 = 𝐹)
Theorem	subfacp1lem5 34175*	Lemma for subfacp1 34177. In subfacp1lem6 34176 we cut up the set of all derangements on 1...(𝑁 + 1) first according to the value at 1, and then by whether or not (𝑓‘(𝑓‘1)) = 1. In this lemma, we show that the subset of all 𝑁 + 1 derangements with (𝑓‘(𝑓‘1)) ≠ 1 for fixed 𝑀 = (𝑓‘1) is in bijection with derangements of 2...(𝑁 + 1), because pre-composing with the function 𝐹 swaps 1 and 𝑀 and turns the function into a bijection with (𝑓‘1) = 1 and (𝑓‘𝑥) ≠ 𝑥 for all other 𝑥, so dropping the point at 1 yields a derangement on the 𝑁 remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1)))    &   ⊢ 𝑀 ∈ V    &   ⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀})    &   ⊢ 𝐵 = {𝑔 ∈ 𝐴 ∣ ((𝑔‘1) = 𝑀 ∧ (𝑔‘𝑀) ≠ 1)}    &   ⊢ 𝐹 = (( I ↾ 𝐾) ∪ {⟨1, 𝑀⟩, ⟨𝑀, 1⟩})    &   ⊢ 𝐶 = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    ⇒   ⊢ (𝜑 → (♯‘𝐵) = (𝑆‘𝑁))
Theorem	subfacp1lem6 34176*	Lemma for subfacp1 34177. By induction, we cut up the set of all derangements on 𝑁 + 1 according to the 𝑁 possible values of (𝑓‘1) (since (𝑓‘1) ≠ 1), and for each set for fixed 𝑀 = (𝑓‘1), the subset of derangements with (𝑓‘𝑀) = 1 has size 𝑆(𝑁 − 1) (by subfacp1lem3 34173), while the subset with (𝑓‘𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 34175). Adding it all up yields the desired equation 𝑁(𝑆(𝑁) + 𝑆(𝑁 − 1)) for the number of derangements on 𝑁 + 1. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    &   ⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓‘𝑦) ≠ 𝑦)}    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆‘𝑁) + (𝑆‘(𝑁 − 1)))))
Theorem	subfacp1 34177*	A two-term recurrence for the subfactorial. This theorem allows to forget the combinatorial definition of the derangement number in favor of the recursive definition provided by this theorem and subfac0 34168, subfac1 34169. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆‘𝑁) + (𝑆‘(𝑁 − 1)))))
Theorem	subfacval2 34178*	A closed-form expression for the subfactorial. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) = ((!‘𝑁) · Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) / (!‘𝑘))))
Theorem	subfaclim 34179*	The subfactorial converges rapidly to 𝑁! / e. This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (abs‘(((!‘𝑁) / e) − (𝑆‘𝑁))) < (1 / 𝑁))
Theorem	subfacval3 34180*	Another closed form expression for the subfactorial. The expression ⌊‘(𝑥 + 1 / 2) is a way of saying "rounded to the nearest integer". (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘𝑁) = (⌊‘(((!‘𝑁) / e) + (1 / 2))))
Theorem	derangfmla 34181*	The derangements formula, which expresses the number of derangements of a finite nonempty set in terms of the factorial. The expression ⌊‘(𝑥 + 1 / 2) is a way of saying "rounded to the nearest integer". This is part of Metamath 100 proof #88. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (𝐷‘𝐴) = (⌊‘(((!‘(♯‘𝐴)) / e) + (1 / 2))))
21.6.4  The Erdős-Szekeres theorem
Theorem	erdszelem1 34182*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))
Theorem	erdszelem2 34183*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ ((♯ “ 𝑆) ∈ Fin ∧ (♯ “ 𝑆) ⊆ ℕ)
Theorem	erdszelem3 34184*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    ⇒   ⊢ (𝐴 ∈ (1...𝑁) → (𝐾‘𝐴) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}), ℝ, < ))
Theorem	erdszelem4 34185*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})
Theorem	erdszelem5 34186*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
Theorem	erdszelem6 34187*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
Theorem	erdszelem7 34188*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝐾‘𝐴) ∈ (1...(𝑅 − 1)))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠))))
Theorem	erdszelem8 34189*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))
Theorem	erdszelem9 34190*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    ⇒   ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1→(ℕ × ℕ))
Theorem	erdszelem10 34191*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ (1...𝑁)(¬ (𝐼‘𝑚) ∈ (1...(𝑅 − 1)) ∨ ¬ (𝐽‘𝑚) ∈ (1...(𝑆 − 1))))
Theorem	erdszelem11 34192*	Lemma for erdsze 34193. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze 34193*	The Erdős-Szekeres theorem. For any injective sequence 𝐹 on the reals of length at least (𝑅 − 1) · (𝑆 − 1) + 1, there is either a subsequence of length at least 𝑅 on which 𝐹 is increasing (i.e. a < , < order isomorphism) or a subsequence of length at least 𝑆 on which 𝐹 is decreasing (i.e. a < , ◡ < order isomorphism, recalling that ◡ < is the "greater than" relation). This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < 𝑁)    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze2lem1 34194*	Lemma for erdsze2 34196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
Theorem	erdsze2lem2 34195*	Lemma for erdsze2 34196. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    &   ⊢ (𝜑 → 𝐺:(1...(𝑁 + 1))–1-1→𝐴)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(𝑁 + 1)), ran 𝐺))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze2 34196*	Generalize the statement of the Erdős-Szekeres theorem erdsze 34193 to "sequences" indexed by an arbitrary subset of ℝ, which can be infinite. This is part of Metamath 100 proof #73. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ (𝜑 → ((𝑅 − 1) · (𝑆 − 1)) < (♯‘𝐴))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
21.6.5  The Kuratowski closure-complement theorem
Theorem	kur14lem1 34197	Lemma for kur14 34207. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐴 ⊆ 𝑋    &   ⊢ (𝑋 ∖ 𝐴) ∈ 𝑇    &   ⊢ (𝐾‘𝐴) ∈ 𝑇    ⇒   ⊢ (𝑁 = 𝐴 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇))
Theorem	kur14lem2 34198	Lemma for kur14 34207. Write interior in terms of closure and complement: 𝑖𝐴 = 𝑐𝑘𝑐𝐴 where 𝑐 is complement and 𝑘 is closure. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝐼‘𝐴) = (𝑋 ∖ (𝐾‘(𝑋 ∖ 𝐴)))
Theorem	kur14lem3 34199	Lemma for kur14 34207. A closure is a subset of the base set. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝐾‘𝐴) ⊆ 𝑋
Theorem	kur14lem4 34200	Lemma for kur14 34207. Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴