P. 325 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32401-32500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	alnof 32401	For all sets, F. is not true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- A. x -. F.
Theorem	nalf 32402	Not all sets hold F. as true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- -. A. x F.
Theorem	extt 32403	There exists a set that holds T. as true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- E. x T.
Theorem	nextnt 32404	There does not exist a set, such that T. is not true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- -. E. x -. T.
Theorem	nextf 32405	There does not exist a set, such that F. is true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- -. E. x F.
Theorem	unnf 32406	There does not exist exactly one set, such that F. is true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- -. E! x F.
Theorem	unnt 32407	There does not exist exactly one set, such that T. is true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- -. E! x T.
Theorem	mont 32408	There does not exist at most one set, such that T. is true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- -. E* x T.
Theorem	mof 32409	There exist at most one set, such that F. is true. (Contributed by Anthony Hart, 13-Sep-2011.)
|- E* x F.
20.10.3  Misc. Single Axiom Systems
Theorem	meran1 32410	A single axiom for propositional calculus offered by Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
|- ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. th \/ ph ) \/ ( ch \/ ( ta \/ ph ) ) ) )
Theorem	meran2 32411	A single axiom for propositional calculus offered by Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
|- ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. ta \/ th ) \/ ( ch \/ ( ph \/ th ) ) ) )
Theorem	meran3 32412	A single axiom for propositional calculus offered by Meredith. (Contributed by Anthony Hart, 13-Aug-2011.)
|- ( -. ( -. ( -. ph \/ ps ) \/ ( ch \/ ( th \/ ta ) ) ) \/ ( -. ( -. ch \/ ph ) \/ ( ta \/ ( th \/ ph ) ) ) )
Theorem	waj-ax 32413	A single axiom for propositional calculus offered by Wajsberg. (Contributed by Anthony Hart, 13-Aug-2011.)
|- ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) -/\ ( ph -/\ ( ph -/\ ps ) ) ) )
Theorem	lukshef-ax2 32414	A single axiom for propositional calculus offered by Lukasiewicz. (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ch -/\ ph ) ) -/\ ( ( th -/\ ps ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
Theorem	arg-ax 32415	? (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( ph -/\ ( ps -/\ ch ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ch -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
20.10.4  Connective Symmetry
Theorem	negsym1 32416	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 ph " means that "something is true of ph." "delta ph " can be substituted with -. ph, ps /\ ph, A. x ph, etc. Later on, Meredith discovered a single axiom, in the form of ( delta delta F. -> delta ph ). 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.)
|- ( -. -. F. -> -. ph )
Theorem	imsym1 32417	A symmetry with ->. See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
|- ( ( ps -> ( ps -> F. ) ) -> ( ps -> ph ) )
Theorem	bisym1 32418	A symmetry with <->. See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
|- ( ( ps <-> ( ps <-> F. ) ) -> ( ps <-> ph ) )
Theorem	consym1 32419	A symmetry with /\. See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
|- ( ( ps /\ ( ps /\ F. ) ) -> ( ps /\ ph ) )
Theorem	dissym1 32420	A symmetry with \/. See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
|- ( ( ps \/ ( ps \/ F. ) ) -> ( ps \/ ph ) )
Theorem	nandsym1 32421	A symmetry with -/\. See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
|- ( ( ps -/\ ( ps -/\ F. ) ) -> ( ps -/\ ph ) )
Theorem	unisym1 32422	A symmetry with A.. See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)
|- ( A. x A. x F. -> A. x ph )
Theorem	exisym1 32423	A symmetry with E.. See negsym1 32416 for more information. (Contributed by Anthony Hart, 4-Sep-2011.)
|- ( E. x E. x F. -> E. x ph )
Theorem	unqsym1 32424	A symmetry with E!. See negsym1 32416 for more information. (Contributed by Anthony Hart, 6-Sep-2011.)
|- ( E! x E! x F. -> E! x ph )
Theorem	amosym1 32425	A symmetry with E*. See negsym1 32416 for more information. (Contributed by Anthony Hart, 13-Sep-2011.)
|- ( E* x E* x F. -> E* x ph )
Theorem	subsym1 32426	A symmetry with [ x / y ]. See negsym1 32416 for more information. (Contributed by Anthony Hart, 11-Sep-2011.)
|- ( [ x / y ] [ x / y ] F. -> [ x / y ] ph )
20.11  Mathbox for Chen-Pang He
20.11.1  Ordinal topology
Theorem	ontopbas 32427	An ordinal number is a topological basis. (Contributed by Chen-Pang He, 8-Oct-2015.)
|- ( B e. On -> B e. TopBases )
Theorem	onsstopbas 32428	The class of ordinal numbers is a subclass of the class of topological bases. (Contributed by Chen-Pang He, 8-Oct-2015.)
|- On C_ TopBases
Theorem	onpsstopbas 32429	The class of ordinal numbers is a proper subclass of the class of topological bases. (Contributed by Chen-Pang He, 9-Oct-2015.)
|- On C. TopBases
Theorem	ontgval 32430	The topology generated from an ordinal number B is suc U. B. (Contributed by Chen-Pang He, 10-Oct-2015.)
|- ( B e. On -> ( topGen ` B ) = suc U. B )
Theorem	ontgsucval 32431	The topology generated from a successor ordinal number is itself. (Contributed by Chen-Pang He, 11-Oct-2015.)
|- ( A e. On -> ( topGen ` suc A ) = suc A )
Theorem	onsuctop 32432	A successor ordinal number is a topology. (Contributed by Chen-Pang He, 11-Oct-2015.)
|- ( A e. On -> suc A e. Top )
Theorem	onsuctopon 32433	One of the topologies on an ordinal number is its successor. (Contributed by Chen-Pang He, 7-Nov-2015.)
|- ( A e. On -> suc A e. (TopOn ` A ) )
Theorem	ordtoplem 32434	Membership of the class of successor ordinals. (Contributed by Chen-Pang He, 1-Nov-2015.)
|- ( U. A e. On -> suc U. A e. S )   =>    |- ( Ord A -> ( A =/= U. A -> A e. S ) )
Theorem	ordtop 32435	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 J -> ( J e. Top <-> J =/= U. J ) )
Theorem	onsucconni 32436	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
|- A e. On   =>    |- suc A e. Conn
Theorem	onsucconn 32437	A successor ordinal number is a connected topology. (Contributed by Chen-Pang He, 16-Oct-2015.)
|- ( A e. On -> suc A e. Conn )
Theorem	ordtopconn 32438	An ordinal topology is connected. (Contributed by Chen-Pang He, 1-Nov-2015.)
|- ( Ord J -> ( J e. Top <-> J e. Conn ) )
Theorem	onintopssconn 32439	An ordinal topology is connected, expressed in constants. (Contributed by Chen-Pang He, 16-Oct-2015.)
|- ( On i^i Top ) C_ Conn
Theorem	onsuct0 32440	A successor ordinal number is a T0 space. (Contributed by Chen-Pang He, 8-Nov-2015.)
|- ( A e. On -> suc A e. Kol2 )
Theorem	ordtopt0 32441	An ordinal topology is T0. (Contributed by Chen-Pang He, 8-Nov-2015.)
|- ( Ord J -> ( J e. Top <-> J e. Kol2 ) )
Theorem	onsucsuccmpi 32442	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.)
|- A e. On   =>    |- suc suc A e. Comp
Theorem	onsucsuccmp 32443	The successor of a successor ordinal number is a compact topology. (Contributed by Chen-Pang He, 18-Oct-2015.)
|- ( A e. On -> suc suc A e. Comp )
Theorem	limsucncmpi 32444	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
|- Lim A   =>    |- -. suc A e. Comp
Theorem	limsucncmp 32445	The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015.)
|- ( Lim A -> -. suc A e. Comp )
Theorem	ordcmp 32446	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 A -> ( A e. Comp <-> ( U. A = U. U. A -> A = 1o ) ) )
Theorem	ssoninhaus 32447	The ordinal topologies 1o and 2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.)
|- { 1o , 2o } C_ ( On i^i Haus )
Theorem	onint1 32448	The ordinal T1 spaces are 1o and 2o, proven without the Axiom of Regularity. (Contributed by Chen-Pang He, 9-Nov-2015.)
|- ( On i^i Fre ) = { 1o , 2o }
Theorem	oninhaus 32449	The ordinal Hausdorff spaces are 1o and 2o. (Contributed by Chen-Pang He, 10-Nov-2015.)
|- ( On i^i Haus ) = { 1o , 2o }
20.12  Mathbox for Jeff Hoffman
20.12.1  Inferences for finite induction on generic function values
Theorem	fveleq 32450	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
|- ( A = B -> ( ( ph -> ( F ` A ) e. P ) <-> ( ph -> ( F ` B ) e. P ) ) )
Theorem	findfvcl 32451*	Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008.)
|- ( ph -> ( F ` (/) ) e. P )   &    |- ( y e. om -> ( ph -> ( ( F ` y ) e. P -> ( F ` suc y ) e. P ) ) )   =>    |- ( A e. om -> ( ph -> ( F ` A ) e. P ) )
Theorem	findreccl 32452*	Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.)
|- ( z e. P -> ( G ` z ) e. P )   =>    |- ( C e. om -> ( A e. P -> ( rec ( G , A ) ` C ) e. P ) )
Theorem	findabrcl 32453*	Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008.) (Revised by Mario Carneiro, 11-Sep-2015.)
|- ( z e. P -> ( G ` z ) e. P )   =>    |- ( ( C e. om /\ A e. P ) -> ( ( x e. _V |-> ( rec ( G , A ) ` x ) ) ` C ) e. P )
20.12.2  gdc.mm
Theorem	nnssi2 32454	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- NN C_ D   &    |- ( B e. NN -> ph )   &    |- ( ( A e. D /\ B e. D /\ ph ) -> ps )   =>    |- ( ( A e. NN /\ B e. NN ) -> ps )
Theorem	nnssi3 32455	Convert a theorem for real/complex numbers into one for positive integers. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- NN C_ D   &    |- ( C e. NN -> ph )   &    |- ( ( ( A e. D /\ B e. D /\ C e. D ) /\ ph ) -> ps )   =>    |- ( ( A e. NN /\ B e. NN /\ C e. NN ) -> ps )
Theorem	nndivsub 32456	Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- ( ( ( A e. NN /\ B e. NN /\ C e. NN ) /\ ( ( A / C ) e. NN /\ A < B ) ) -> ( ( B / C ) e. NN <-> ( ( B - A ) / C ) e. NN ) )
Theorem	nndivlub 32457	A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008.)
|- ( ( A e. NN /\ B e. NN ) -> ( ( A / B ) e. NN -> B <_ A ) )
Syntax	cgcdOLD 32458	Extend class notation to include the gdc function. (New usage is discouraged.)
class gcdOLD ( A , B )
Definition	df-gcdOLD 32459*	gcdOLD ( A , B ) is the largest positive integer that evenly divides both A and B. (Contributed by Jeff Hoffman, 17-Jun-2008.) (New usage is discouraged.)
|- gcdOLD ( A , B ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )
Theorem	ee7.2aOLD 32460	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 A mod B. 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.)
|- ( ( A e. NN /\ B e. NN ) -> ( A < B -> gcdOLD ( A , B ) = gcdOLD ( A , ( B - A ) ) ) )
20.13  Mathbox for Asger C. Ipsen
20.13.1  Continuous nowhere differentiable functions
Theorem	dnival 32461*	Value of the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   =>    |- ( A e. RR -> ( T ` A ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
Theorem	dnicld1 32462	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
Theorem	dnicld2 32463*	Closure theorem for the "distance to nearest integer" function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   =>    |- ( ph -> ( T ` A ) e. RR )
Theorem	dnif 32464	The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   =>    |- T : RR --> RR
Theorem	dnizeq0 32465*	The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. ZZ )   =>    |- ( ph -> ( T ` A ) = 0 )
Theorem	dnizphlfeqhlf 32466*	The distance to nearest integer is a half for half-integers. (Contributed by Asger C. Ipsen, 15-Jun-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. ZZ )   =>    |- ( ph -> ( T ` ( A + ( 1 / 2 ) ) ) = ( 1 / 2 ) )
Theorem	rddif2 32467	Variant of rddif 14080. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( A e. RR -> 0 <_ ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
Theorem	dnibndlem1 32468*	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ S <-> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ S ) )
Theorem	dnibndlem2 32469*	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( |_ ` ( A + ( 1 / 2 ) ) ) )   =>    |- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
Theorem	dnibndlem3 32470	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )   =>    |- ( ph -> ( abs ` ( B - A ) ) = ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) )
Theorem	dnibndlem4 32471	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( B e. RR -> 0 <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )
Theorem	dnibndlem5 32472	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( A e. RR -> 0 < ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )
Theorem	dnibndlem6 32473	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) )
Theorem	dnibndlem7 32474	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( ph -> B e. RR )   =>    |- ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )
Theorem	dnibndlem8 32475	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )
Theorem	dnibndlem9 32476*	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )   =>    |- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
Theorem	dnibndlem10 32477	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )   =>    |- ( ph -> 1 <_ ( B - A ) )
Theorem	dnibndlem11 32478	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( 1 / 2 ) )
Theorem	dnibndlem12 32479*	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )   =>    |- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
Theorem	dnibndlem13 32480*	Lemma for dnibnd 32481. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )   =>    |- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
Theorem	dnibnd 32481*	The "distance to nearest integer" function is Lipshitz continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
Theorem	dnicn 32482	The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   =>    |- T e. ( RR -cn-> RR )
Theorem	knoppcnlem1 32483*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.)
|- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( ( F ` A ) ` M ) = ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) )
Theorem	knoppcnlem2 32484*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( ( C ^ M ) x. ( T ` ( ( ( 2 x. N ) ^ M ) x. A ) ) ) e. RR )
Theorem	knoppcnlem3 32485*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( ( F ` A ) ` M ) e. RR )
Theorem	knoppcnlem4 32486*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A e. RR )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( abs ` ( ( F ` A ) ` M ) ) <_ ( ( m e. NN0 |-> ( ( abs ` C ) ^ m ) ) ` M ) )
Theorem	knoppcnlem5 32487*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) : NN0 --> ( CC ^m RR ) )
Theorem	knoppcnlem6 32488*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( abs ` C ) < 1 )   =>    |- ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) e. dom ( ~~> u ` RR ) )
Theorem	knoppcnlem7 32489*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ` M ) = ( w e. RR |-> ( seq 0 ( + , ( F ` w ) ) ` M ) ) )
Theorem	knoppcnlem8 32490*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( CC ^m RR ) )
Theorem	knoppcnlem9 32491*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( abs ` C ) < 1 )   =>    |- ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) ( ~~> u ` RR ) W )
Theorem	knoppcnlem10 32492*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> M e. NN0 )   =>    |- ( ph -> ( z e. RR |-> ( ( F ` z ) ` M ) ) e. ( ( topGen ` ran (,) ) Cn ( TopOpen ` ℂfld ) ) )
Theorem	knoppcnlem11 32493*	Lemma for knoppcn 32494. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> seq 0 ( oF + , ( m e. NN0 |-> ( z e. RR |-> ( ( F ` z ) ` m ) ) ) ) : NN0 --> ( RR -cn-> CC ) )
Theorem	knoppcn 32494*	The continuous nowhere differentiable function W ( Knopp, K. (1918). Math. Z. 2, 1-26 ) is, in fact, continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021.) (Revised by Asger C. Ipsen, 5-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( abs ` C ) < 1 )   =>    |- ( ph -> W e. ( RR -cn-> CC ) )
Theorem	knoppcld 32495*	Closure theorem for Knopp's function. (Contributed by Asger C. Ipsen, 26-Jul-2021.)
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )   &    |- F = ( y e. RR |-> ( n e. NN0 |-> ( ( C ^ n ) x. ( T ` ( ( ( 2 x. N ) ^ n ) x. y ) ) ) ) )   &    |- W = ( w e. RR |-> sum_ i e. NN0 ( ( F ` w ) ` i ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> N e. NN )   &    |- ( ph -> C e. RR )   &    |- ( ph -> ( abs ` C ) < 1 )   =>    |- ( ph -> ( W ` A ) e. CC )
Theorem	addgtge0d 32496	Addition of positive and nonnegative numbers is positive. (Contributed by Asger C. Ipsen, 12-May-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 <_ B )   =>    |- ( ph -> 0 < ( A + B ) )
Theorem	unblimceq0lem 32497*	Lemma for unblimceq0 32498. (Contributed by Asger C. Ipsen, 12-May-2021.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : S --> CC )   &    |- ( ph -> A e. CC )   &    |- ( ph -> A. b e. RR+ A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) )   =>    |- ( ph -> A. c e. RR+ A. d e. RR+ E. y e. S ( y =/= A /\ ( abs ` ( y - A ) ) < d /\ c <_ ( abs ` ( F ` y ) ) ) )
Theorem	unblimceq0 32498*	If F is unbounded near A it has no limit at A. (Contributed by Asger C. Ipsen, 12-May-2021.)
|- ( ph -> S C_ CC )   &    |- ( ph -> F : S --> CC )   &    |- ( ph -> A e. CC )   &    |- ( ph -> A. b e. RR+ A. d e. RR+ E. x e. S ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( F ` x ) ) ) )   =>    |- ( ph -> ( F lim CC A ) = (/) )
Theorem	unbdqndv1 32499*	If the difference quotient ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) is unbounded near A then F is not differentiable at A. (Contributed by Asger C. Ipsen, 12-May-2021.)
|- G = ( z e. ( X \ { A } ) |-> ( ( ( F ` z ) - ( F ` A ) ) / ( z - A ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> F : X --> CC )   &    |- ( ph -> A. b e. RR+ A. d e. RR+ E. x e. ( X \ { A } ) ( ( abs ` ( x - A ) ) < d /\ b <_ ( abs ` ( G ` x ) ) ) )   =>    |- ( ph -> -. A e. dom ( S _D F ) )
Theorem	unbdqndv2lem1 32500	Lemma for unbdqndv2 32502. (Contributed by Asger C. Ipsen, 12-May-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> D =/= 0 )   &    |- ( ph -> ( 2 x. E ) <_ ( abs ` ( ( A - B ) / D ) ) )   =>    |- ( ph -> ( ( E x. ( abs ` D ) ) <_ ( abs ` ( A - C ) ) \/ ( E x. ( abs ` D ) ) <_ ( abs ` ( B - C ) ) ) )