P. 345 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34401-34500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	f1resfz0f1d 34401	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 34402	A finite set is equal to its subset if they are the same size. (Contributed by BTernaryTau, 3-Oct-2023.)
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ (♯‘𝐴) = (♯‘𝐵)) → 𝐴 = 𝐵)
Theorem	hashf1dmcdm 34403	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 34404	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 34405	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 34406*	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 34407*	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 34408*	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 34409*	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 34410	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 34411	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 34412	A prefix of a walk is a walk. (Contributed by BTernaryTau, 2-Dec-2023.)
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ 𝐿 ∈ (0...(♯‘𝐹))) → (𝐹 prefix 𝐿)(Walks‘𝐺)(𝑃 prefix (𝐿 + 1)))
Theorem	revwlk 34413	The reverse of a walk is a walk. (Contributed by BTernaryTau, 30-Nov-2023.)
⊢ (𝐹(Walks‘𝐺)𝑃 → (reverse‘𝐹)(Walks‘𝐺)(reverse‘𝑃))
Theorem	revwlkb 34414	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 34415	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 34416	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 34417	A path is either a simple path or a cycle (or both). (Contributed by BTernaryTau, 20-Oct-2023.)
⊢ (𝐹(Paths‘𝐺)𝑃 → (𝐹(SPaths‘𝐺)𝑃 ∨ 𝐹(Cycles‘𝐺)𝑃))
Theorem	spthcycl 34418	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 34419	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 34420	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 34421	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 34422	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 34423	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 34424	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 34425*	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 34426*	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 34427	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))    &   ⊢ (𝜑 → (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐴 = 𝐶)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	2cycl2d 34428	Construction of a 2-cycle from two given edges in a graph. (Contributed by BTernaryTau, 16-Oct-2023.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐴”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ (𝜑 → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉))    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐴, 𝐵} ⊆ (𝐼‘𝐾)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    ⇒   ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃)
Theorem	umgr2cycllem 34429*	Lemma for umgr2cycl 34430. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ 𝐹 = ⟨“𝐽𝐾”⟩    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UMGraph)    &   ⊢ (𝜑 → 𝐽 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → (𝐼‘𝐽) = (𝐼‘𝐾))    ⇒   ⊢ (𝜑 → ∃𝑝 𝐹(Cycles‘𝐺)𝑝)
Theorem	umgr2cycl 34430*	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 34431	Extend class notation with acyclic graphs.
class AcyclicGraph
Definition	df-acycgr 34432*	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 34433*	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 34434*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅)))
Theorem	isacycgr1 34435*	The property of being an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ AcyclicGraph ↔ ∀𝑓∀𝑝(𝑓(Cycles‘𝐺)𝑝 → 𝑓 = ∅)))
Theorem	acycgrcycl 34436	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 34437	A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑉 = ∅) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr1v 34438	A multigraph with one vertex is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UMGraph ∧ (♯‘𝑉) = 1) → 𝐺 ∈ AcyclicGraph)
Theorem	acycgr2v 34439	A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝑉) = 2) → 𝐺 ∈ AcyclicGraph)
Theorem	prclisacycgr 34440*	A proper class (representing a null graph, see vtxvalprc 28572) has the property of an acyclic graph (see also acycgr0v 34437). (Contributed by BTernaryTau, 11-Oct-2023.) (New usage is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (¬ 𝐺 ∈ V → ¬ ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ 𝑓 ≠ ∅))
Theorem	acycgrislfgr 34441*	An acyclic hypergraph is a loop-free hypergraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐺 ∈ UHGraph) → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})
Theorem	upgracycumgr 34442	An acyclic pseudograph is a multigraph. (Contributed by BTernaryTau, 15-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ UMGraph)
Theorem	umgracycusgr 34443	An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UMGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	upgracycusgr 34444	An acyclic pseudograph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐺 ∈ AcyclicGraph) → 𝐺 ∈ USGraph)
Theorem	cusgracyclt3v 34445	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 34446	A path in an acyclic graph is a simple path. (Contributed by BTernaryTau, 21-Oct-2023.)
⊢ ((𝐺 ∈ AcyclicGraph ∧ 𝐹(Paths‘𝐺)𝑃) → 𝐹(SPaths‘𝐺)𝑃)
Theorem	acycgrsubgr 34447	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 34448*	Distinct variable version of ax-11 2152. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Axiom	ax-8d 34449*	Distinct variable version of ax-7 2009. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
Axiom	ax-9d1 34450	Distinct variable version of ax-6 1969, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑥
Axiom	ax-9d2 34451*	Distinct variable version of ax-6 1969, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Axiom	ax-10d 34452*	Distinct variable version of axc11n 2423. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Axiom	ax-11d 34453*	Distinct variable version of ax-12 2169. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
21.6.2  Miscellaneous stuff
Theorem	quartfull 34454	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 34455*	Lemma for derangements. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ (𝐴 ∈ Fin → {𝑓 ∣ (𝑓:𝐴–1-1-onto→𝐴 ∧ 𝜑)} ∈ Fin)
Theorem	derangval 34456*	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 34457*	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 34458*	The derangement number of the empty set. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐷‘∅) = 1
Theorem	derangsn 34459*	The derangement number of a singleton. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐷‘{𝐴}) = 0)
Theorem	derangenlem 34460*	One half of derangen 34461. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    ⇒   ⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ Fin) → (𝐷‘𝐴) ≤ (𝐷‘𝐵))
Theorem	derangen 34461*	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 34462*	The subfactorial is defined as the number of derangements (see derangval 34456) of the set (1...𝑁). (Contributed by Mario Carneiro, 21-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) = (𝐷‘(1...𝑁)))
Theorem	derangen2 34463*	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 34464*	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 34465*	The subfactorial is less than the factorial. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ0 → (𝑆‘𝑁) ≤ (!‘𝑁))
Theorem	subfac0 34466*	The subfactorial at zero. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘0) = 1
Theorem	subfac1 34467*	The subfactorial at one. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑆‘1) = 0
Theorem	subfacp1lem1 34468*	Lemma for subfacp1 34475. 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 34469*	Lemma for subfacp1 34475. 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 34470*	Lemma for subfacp1 34475. 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 34471*	Lemma for subfacp1 34475. In subfacp1lem6 34474 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 34472*	Lemma for subfacp1 34475. 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 34473*	Lemma for subfacp1 34475. In subfacp1lem6 34474 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 34474*	Lemma for subfacp1 34475. 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 34471), while the subset with (𝑓‘𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 34473). 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 34475*	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 34466, subfac1 34467. (Contributed by Mario Carneiro, 23-Jan-2015.)
⊢ 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥–1-1-onto→𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) ≠ 𝑦)}))    &   ⊢ 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆‘𝑁) + (𝑆‘(𝑁 − 1)))))
Theorem	subfacval2 34476*	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 34477*	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 34478*	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 34479*	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 34480*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑋) Isom < , 𝑂 (𝑋, (𝐹 “ 𝑋)) ∧ 𝐴 ∈ 𝑋))
Theorem	erdszelem2 34481*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝑆 = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}    ⇒   ⊢ ((♯ “ 𝑆) ∈ Fin ∧ (♯ “ 𝑆) ⊆ ℕ)
Theorem	erdszelem3 34482*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    ⇒   ⊢ (𝐴 ∈ (1...𝑁) → (𝐾‘𝐴) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}), ℝ, < ))
Theorem	erdszelem4 34483*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → {𝐴} ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})
Theorem	erdszelem5 34484*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
Theorem	erdszelem6 34485*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    ⇒   ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
Theorem	erdszelem7 34486*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → ¬ (𝐾‘𝐴) ∈ (1...(𝑅 − 1)))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 (1...𝑁)(𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , 𝑂 (𝑠, (𝐹 “ 𝑠))))
Theorem	erdszelem8 34487*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑂 Or ℝ    &   ⊢ (𝜑 → 𝐴 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))
Theorem	erdszelem9 34488*	Lemma for erdsze 34491. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)    &   ⊢ 𝐼 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝐽 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , ◡ < (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))    &   ⊢ 𝑇 = (𝑛 ∈ (1...𝑁) ↦ ⟨(𝐼‘𝑛), (𝐽‘𝑛)⟩)    ⇒   ⊢ (𝜑 → 𝑇:(1...𝑁)–1-1→(ℕ × ℕ))
Theorem	erdszelem10 34489*	Lemma for erdsze 34491. (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 34490*	Lemma for erdsze 34491. (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 34491*	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 34492*	Lemma for erdsze2 34494. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓:(1...(𝑁 + 1))–1-1→𝐴 ∧ 𝑓 Isom < , < ((1...(𝑁 + 1)), ran 𝑓)))
Theorem	erdsze2lem2 34493*	Lemma for erdsze2 34494. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1→ℝ)    &   ⊢ (𝜑 → 𝐴 ⊆ ℝ)    &   ⊢ 𝑁 = ((𝑅 − 1) · (𝑆 − 1))    &   ⊢ (𝜑 → 𝑁 < (♯‘𝐴))    &   ⊢ (𝜑 → 𝐺:(1...(𝑁 + 1))–1-1→𝐴)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(𝑁 + 1)), ran 𝐺))    ⇒   ⊢ (𝜑 → ∃𝑠 ∈ 𝒫 𝐴((𝑅 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , < (𝑠, (𝐹 “ 𝑠))) ∨ (𝑆 ≤ (♯‘𝑠) ∧ (𝐹 ↾ 𝑠) Isom < , ◡ < (𝑠, (𝐹 “ 𝑠)))))
Theorem	erdsze2 34494*	Generalize the statement of the Erdős-Szekeres theorem erdsze 34491 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 34495	Lemma for kur14 34505. (Contributed by Mario Carneiro, 17-Feb-2015.)
⊢ 𝐴 ⊆ 𝑋    &   ⊢ (𝑋 ∖ 𝐴) ∈ 𝑇    &   ⊢ (𝐾‘𝐴) ∈ 𝑇    ⇒   ⊢ (𝑁 = 𝐴 → (𝑁 ⊆ 𝑋 ∧ {(𝑋 ∖ 𝑁), (𝐾‘𝑁)} ⊆ 𝑇))
Theorem	kur14lem2 34496	Lemma for kur14 34505. 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 34497	Lemma for kur14 34505. A closure is a subset of the base set. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝐾‘𝐴) ⊆ 𝑋
Theorem	kur14lem4 34498	Lemma for kur14 34505. Complementation is an involution on the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝑋 ∖ (𝑋 ∖ 𝐴)) = 𝐴
Theorem	kur14lem5 34499	Lemma for kur14 34505. Closure is an idempotent operation in the set of subsets of a topology. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    ⇒   ⊢ (𝐾‘(𝐾‘𝐴)) = (𝐾‘𝐴)
Theorem	kur14lem6 34500	Lemma for kur14 34505. If 𝑘 is the complementation operator and 𝑘 is the closure operator, this expresses the identity 𝑘𝑐𝑘𝐴 = 𝑘𝑐𝑘𝑐𝑘𝑐𝑘𝐴 for any subset 𝐴 of the topological space. This is the key result that lets us cut down long enough sequences of 𝑐𝑘𝑐𝑘... that arise when applying closure and complement repeatedly to 𝐴, and explains why we end up with a number as large as 14, yet no larger. (Contributed by Mario Carneiro, 11-Feb-2015.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (cls‘𝐽)    &   ⊢ 𝐼 = (int‘𝐽)    &   ⊢ 𝐴 ⊆ 𝑋    &   ⊢ 𝐵 = (𝑋 ∖ (𝐾‘𝐴))    ⇒   ⊢ (𝐾‘(𝐼‘(𝐾‘𝐵))) = (𝐾‘𝐵)