P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	filnetlem4 35801*	Lemma for filnet 35802. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
⊢ 𝐻 = ∪ 𝑛 ∈ 𝐹 ({𝑛} × 𝑛)    &   ⊢ 𝐷 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻) ∧ (1st ‘𝑦) ⊆ (1st ‘𝑥))}    ⇒   ⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
Theorem	filnet 35802*	A filter has the same convergence and clustering properties as some net. (Contributed by Jeff Hankins, 12-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑑 ∈ DirRel ∃𝑓(𝑓:dom 𝑑⟶𝑋 ∧ 𝐹 = ((𝑋 FilMap 𝑓)‘ran (tail‘𝑑))))
21.13  Mathbox for Anthony Hart
21.13.1  Propositional Calculus
Theorem	tb-ax1 35803	The first of three axioms in the Tarski-Bernays axiom system. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	tb-ax2 35804	The second of three axioms in the Tarski-Bernays axiom system. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	tb-ax3 35805	The third of three axioms in the Tarski-Bernays axiom system. This axiom, along with ax-mp 5, tb-ax1 35803, and tb-ax2 35804, can be used to derive any theorem or rule that uses only →. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	tbsyl 35806	The weak syllogism from Tarski-Bernays'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	re1ax2lem 35807	Lemma for re1ax2 35808. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	re1ax2 35808	ax-2 7 rederived from the Tarski-Bernays axiom system. Often tb-ax1 35803 is replaced with this theorem to make a "standard" system. This is because this theorem is easier to work with, despite it being longer. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	naim1 35809	Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.)
⊢ ((𝜑 → 𝜓) → ((𝜓 ⊼ 𝜒) → (𝜑 ⊼ 𝜒)))
Theorem	naim2 35810	Constructor theorem for ⊼. (Contributed by Anthony Hart, 1-Sep-2011.)
⊢ ((𝜑 → 𝜓) → ((𝜒 ⊼ 𝜓) → (𝜒 ⊼ 𝜑)))
Theorem	naim1i 35811	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 ⊼ 𝜒)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	naim2i 35812	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 ⊼ 𝜓)    ⇒   ⊢ (𝜒 ⊼ 𝜑)
Theorem	naim12i 35813	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    &   ⊢ (𝜓 ⊼ 𝜃)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	nabi1i 35814	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ⊼ 𝜒)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Theorem	nabi2i 35815	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ⊼ 𝜓)    ⇒   ⊢ (𝜒 ⊼ 𝜑)
Theorem	nabi12i 35816	Constructor rule for ⊼. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜓 ⊼ 𝜃)    ⇒   ⊢ (𝜑 ⊼ 𝜒)
Syntax	w3nand 35817	The double nand.
wff (𝜑 ⊼ 𝜓 ⊼ 𝜒)
Definition	df-3nand 35818	The double nand. This definition allows to express the input of three variables only being false if all three are true. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 → (𝜓 → ¬ 𝜒)))
Theorem	df3nandALT1 35819	The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 ⊼ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒))))
Theorem	df3nandALT2 35820	The double nand expressed in terms of negation and and not. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ ¬ (𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	andnand1 35821	Double and in terms of double nand. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ⊼ (𝜑 ⊼ 𝜓 ⊼ 𝜒)))
Theorem	imnand2 35822	An → nand relation. (Contributed by Anthony Hart, 2-Sep-2011.)
⊢ ((¬ 𝜑 → 𝜓) ↔ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓)))
21.13.2  Predicate Calculus
Theorem	nalfal 35823	Not all sets hold ⊥ as true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∀𝑥⊥
Theorem	nexntru 35824	There does not exist a set such that ⊤ is not true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃𝑥 ¬ ⊤
Theorem	nexfal 35825	There does not exist a set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃𝑥⊥
Theorem	neufal 35826	There does not exist exactly one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃!𝑥⊥
Theorem	neutru 35827	There does not exist exactly one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃!𝑥⊤
Theorem	nmotru 35828	There does not exist at most one set such that ⊤ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ¬ ∃*𝑥⊤
Theorem	mofal 35829	There exist at most one set such that ⊥ is true. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ ∃*𝑥⊥
Theorem	nrmo 35830	"At most one" restricted existential quantifier for a statement which is never true. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ (𝑥 ∈ 𝐴 → ¬ 𝜑)    ⇒   ⊢ ∃*𝑥 ∈ 𝐴 𝜑
21.13.3  Miscellaneous single axioms
Theorem	meran1 35831	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜃 ∨ 𝜑) ∨ (𝜒 ∨ (𝜏 ∨ 𝜑))))
Theorem	meran2 35832	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜏 ∨ 𝜃) ∨ (𝜒 ∨ (𝜑 ∨ 𝜃))))
Theorem	meran3 35833	A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ (¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜒 ∨ (𝜃 ∨ 𝜏))) ∨ (¬ (¬ 𝜒 ∨ 𝜑) ∨ (𝜏 ∨ (𝜃 ∨ 𝜑))))
Theorem	waj-ax 35834	A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ (((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜑 ⊼ 𝜓))))
Theorem	lukshef-ax2 35835	A single axiom for propositional calculus discovered by Jan Lukasiewicz. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom L2 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
Theorem	arg-ax 35836	A single axiom for propositional calculus discovered by Ken Harris and Branden Fitelson. See: Fitelson, Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom HF1 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011.)
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜒 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
21.13.4  Connective Symmetry
Theorem	negsym1 35837	In the paper "On Variable Functors of Propositional Arguments", Lukasiewicz introduced a system that can handle variable connectives. This was done by introducing a variable, marked with a lowercase delta, which takes a wff as input. In the system, "delta 𝜑 " means that "something is true of 𝜑". The expression "delta 𝜑 " can be substituted with ¬ 𝜑, 𝜓 ∧ 𝜑, ∀𝑥𝜑, etc. Later on, Meredith discovered a single axiom, in the form of ( delta delta ⊥ → delta 𝜑 ). This represents the shortest theorem in the extended propositional calculus that cannot be derived as an instance of a theorem in propositional calculus. A symmetry with ¬. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ (¬ ¬ ⊥ → ¬ 𝜑)
Theorem	imsym1 35838	A symmetry with →. See negsym1 35837 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 → (𝜓 → ⊥)) → (𝜓 → 𝜑))
Theorem	bisym1 35839	A symmetry with ↔. See negsym1 35837 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ↔ (𝜓 ↔ ⊥)) → (𝜓 ↔ 𝜑))
Theorem	consym1 35840	A symmetry with ∧. See negsym1 35837 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∧ (𝜓 ∧ ⊥)) → (𝜓 ∧ 𝜑))
Theorem	dissym1 35841	A symmetry with ∨. See negsym1 35837 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ∨ (𝜓 ∨ ⊥)) → (𝜓 ∨ 𝜑))
Theorem	nandsym1 35842	A symmetry with ⊼. See negsym1 35837 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ ((𝜓 ⊼ (𝜓 ⊼ ⊥)) → (𝜓 ⊼ 𝜑))
Theorem	unisym1 35843	A symmetry with ∀. See negsym1 35837 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
⊢ (∀𝑥∀𝑥⊥ → ∀𝑥𝜑)
Theorem	exisym1 35844	A symmetry with ∃. See negsym1 35837 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
⊢ (∃𝑥∃𝑥⊥ → ∃𝑥𝜑)
Theorem	unqsym1 35845	A symmetry with ∃!. See negsym1 35837 for more information. (Contributed by Anthony Hart, 6-Sep-2011.)
⊢ (∃!𝑥∃!𝑥⊥ → ∃!𝑥𝜑)
Theorem	amosym1 35846	A symmetry with ∃*. See negsym1 35837 for more information. (Contributed by Anthony Hart, 13-Sep-2011.)
⊢ (∃*𝑥∃*𝑥⊥ → ∃*𝑥𝜑)
Theorem	subsym1 35847	A symmetry with [𝑥 / 𝑦]. See negsym1 35837 for more information. (Contributed by Anthony Hart, 11-Sep-2011.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]⊥ → [𝑦 / 𝑥]𝜑)
21.14  Mathbox for Chen-Pang He
21.14.1  Ordinal topology
Theorem	ontopbas 35848	An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.)
⊢ (𝐵 ∈ On → 𝐵 ∈ TopBases)
Theorem	onsstopbas 35849	The class of ordinal numbers is a subclass of the class of topological bases. (Contributed by Chen-Pang He, 8-Oct-2015.)
⊢ On ⊆ TopBases
Theorem	onpsstopbas 35850	The class of ordinal numbers is a proper subclass of the class of topological bases. (Contributed by Chen-Pang He, 9-Oct-2015.)
⊢ On ⊊ TopBases
Theorem	ontgval 35851	The topology generated from an ordinal number 𝐵 is suc ∪ 𝐵. (Contributed by Chen-Pang He, 10-Oct-2015.)
⊢ (𝐵 ∈ On → (topGen‘𝐵) = suc ∪ 𝐵)
Theorem	ontgsucval 35852	The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → (topGen‘suc 𝐴) = suc 𝐴)
Theorem	onsuctop 35853	A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Top)
Theorem	onsuctopon 35854	One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ (TopOn‘𝐴))
Theorem	ordtoplem 35855	Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ 𝑆)    ⇒   ⊢ (Ord 𝐴 → (𝐴 ≠ ∪ 𝐴 → 𝐴 ∈ 𝑆))
Theorem	ordtop 35856	An ordinal is a topology iff it is not its supremum (union), proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ≠ ∪ 𝐽))
Theorem	onsucconni 35857	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc 𝐴 ∈ Conn
Theorem	onsucconn 35858	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Conn)
Theorem	ordtopconn 35859	An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Conn))
Theorem	onintopssconn 35860	An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.)
⊢ (On ∩ Top) ⊆ Conn
Theorem	onsuct0 35861	A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (𝐴 ∈ On → suc 𝐴 ∈ Kol2)
Theorem	ordtopt0 35862	An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.)
⊢ (Ord 𝐽 → (𝐽 ∈ Top ↔ 𝐽 ∈ Kol2))
Theorem	onsucsuccmpi 35863	The successor of a successor ordinal number is a compact topology, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 18-Oct-2015.)
⊢ 𝐴 ∈ On    ⇒   ⊢ suc suc 𝐴 ∈ Comp
Theorem	onsucsuccmp 35864	The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015.)
⊢ (𝐴 ∈ On → suc suc 𝐴 ∈ Comp)
Theorem	limsucncmpi 35865	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ Lim 𝐴    ⇒   ⊢ ¬ suc 𝐴 ∈ Comp
Theorem	limsucncmp 35866	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
⊢ (Lim 𝐴 → ¬ suc 𝐴 ∈ Comp)
Theorem	ordcmp 35867	An ordinal topology is compact iff the underlying set is its supremum (union) only when the ordinal is 1o. (Contributed by Chen-Pang He, 1-Nov-2015.)
⊢ (Ord 𝐴 → (𝐴 ∈ Comp ↔ (∪ 𝐴 = ∪ ∪ 𝐴 → 𝐴 = 1o)))
Theorem	ssoninhaus 35868	The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ {1o, 2o} ⊆ (On ∩ Haus)
Theorem	onint1 35869	The ordinal T1 spaces are 1o and 2o, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 9-Nov-2015.)
⊢ (On ∩ Fre) = {1o, 2o}
Theorem	oninhaus 35870	The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.)
⊢ (On ∩ Haus) = {1o, 2o}
21.15  Mathbox for Jeff Hoffman
21.15.1  Inferences for finite induction on generic function values
Theorem	fveleq 35871	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝐴 = 𝐵 → ((𝜑 → (𝐹‘𝐴) ∈ 𝑃) ↔ (𝜑 → (𝐹‘𝐵) ∈ 𝑃)))
Theorem	findfvcl 35872*	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
⊢ (𝜑 → (𝐹‘∅) ∈ 𝑃)    &   ⊢ (𝑦 ∈ ω → (𝜑 → ((𝐹‘𝑦) ∈ 𝑃 → (𝐹‘suc 𝑦) ∈ 𝑃)))    ⇒   ⊢ (𝐴 ∈ ω → (𝜑 → (𝐹‘𝐴) ∈ 𝑃))
Theorem	findreccl 35873*	Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃))
Theorem	findabrcl 35874*	Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.)
⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃)    ⇒   ⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃) → ((𝑥 ∈ V ↦ (rec(𝐺, 𝐴)‘𝑥))‘𝐶) ∈ 𝑃)
21.15.2  gdc.mm
Theorem	nnssi2 35875	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐵 ∈ ℕ → 𝜑)    &   ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → 𝜓)
Theorem	nnssi3 35876	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ℕ ⊆ 𝐷    &   ⊢ (𝐶 ∈ ℕ → 𝜑)    &   ⊢ (((𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷) ∧ 𝜑) → 𝜓)    ⇒   ⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → 𝜓)
Theorem	nndivsub 35877	Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴 / 𝐶) ∈ ℕ ∧ 𝐴 < 𝐵)) → ((𝐵 / 𝐶) ∈ ℕ ↔ ((𝐵 − 𝐴) / 𝐶) ∈ ℕ))
Theorem	nndivlub 35878	A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / 𝐵) ∈ ℕ → 𝐵 ≤ 𝐴))
Syntax	cgcdOLD 35879	Extend class notation to include the gdc function. (New usage is discouraged.)
class gcdOLD (𝐴, 𝐵)
Definition	df-gcdOLD 35880*	gcdOLD (𝐴, 𝐵) is the largest positive integer that evenly divides both 𝐴 and 𝐵. (Contributed by Jeff Hoffman, 17-Jun-2008.) (New usage is discouraged.)
⊢ gcdOLD (𝐴, 𝐵) = sup({𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}, ℕ, < )
Theorem	ee7.2aOLD 35881	Lemma for Euclid's Elements, Book 7, proposition 2. The original mentions the smaller measure being 'continually subtracted' from the larger. Many authors interpret this phrase as 𝐴 mod 𝐵. Here, just one subtraction step is proved to preserve the gcdOLD. The rec function will be used in other proofs for iterated subtraction. (Contributed by Jeff Hoffman, 17-Jun-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 → gcdOLD (𝐴, 𝐵) = gcdOLD (𝐴, (𝐵 − 𝐴))))
21.16  Mathbox for Asger C. Ipsen
21.16.1  Continuous nowhere differentiable functions
Theorem	dnival 35882*	Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑇‘𝐴) = (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))
Theorem	dnicld1 35883	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)) ∈ ℝ)
Theorem	dnicld2 35884*	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) ∈ ℝ)
Theorem	dnif 35885	The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    ⇒   ⊢ 𝑇:ℝ⟶ℝ
Theorem	dnizeq0 35886*	The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑇‘𝐴) = 0)
Theorem	dnizphlfeqhlf 35887*	The distance to nearest integer is a half for half-integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑇‘(𝐴 + (1 / 2))) = (1 / 2))
Theorem	rddif2 35888	Variant of rddif 15311. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 ≤ ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))))
Theorem	dnibndlem1 35889*	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ 𝑆 ↔ (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ 𝑆))
Theorem	dnibndlem2 35890*	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = (⌊‘(𝐴 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem3 35891	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1))    ⇒   ⊢ (𝜑 → (abs‘(𝐵 − 𝐴)) = (abs‘((𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))) + (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))))
Theorem	dnibndlem4 35892	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐵 ∈ ℝ → 0 ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem5 35893	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝐴 ∈ ℝ → 0 < (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem6 35894	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) + ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))))
Theorem	dnibndlem7 35895	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵))) ≤ (𝐵 − ((⌊‘(𝐵 + (1 / 2))) − (1 / 2))))
Theorem	dnibndlem8 35896	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((1 / 2) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴))) ≤ (((⌊‘(𝐴 + (1 / 2))) + (1 / 2)) − 𝐴))
Theorem	dnibndlem9 35897*	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (⌊‘(𝐵 + (1 / 2))) = ((⌊‘(𝐴 + (1 / 2))) + 1))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))
Theorem	dnibndlem10 35898	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → 1 ≤ (𝐵 − 𝐴))
Theorem	dnibndlem11 35899	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → (abs‘((abs‘((⌊‘(𝐵 + (1 / 2))) − 𝐵)) − (abs‘((⌊‘(𝐴 + (1 / 2))) − 𝐴)))) ≤ (1 / 2))
Theorem	dnibndlem12 35900*	Lemma for dnibnd 35902. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
⊢ 𝑇 = (𝑥 ∈ ℝ ↦ (abs‘((⌊‘(𝑥 + (1 / 2))) − 𝑥)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → ((⌊‘(𝐴 + (1 / 2))) + 2) ≤ (⌊‘(𝐵 + (1 / 2))))    ⇒   ⊢ (𝜑 → (abs‘((𝑇‘𝐵) − (𝑇‘𝐴))) ≤ (abs‘(𝐵 − 𝐴)))