Most Recent Proofs - Intuitionistic Logic Explorer

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

Last updated on 26-Apr-2024 at 6:14 AM ET.

Recent Additions to the Intuitionistic Logic Explorer

Date	Label	Description
Theorem
13-Apr-2024	prodmodclem2 11346	Lemma for prodmodc 11347. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( f ` j ) / k ]_ B , 1 ) )   =>    |- ( ( ph /\ E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , F ) ~~> y ) /\ seq m ( x. , F ) ~~> x ) ) ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ z = ( seq 1 ( x. , G ) ` m ) ) -> x = z ) )
11-Apr-2024	prodmodclem2a 11345	Lemma for prodmodc 11347. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( f ` j ) / k ]_ B , 1 ) )   &    |- H = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( K ` j ) / k ]_ B , 1 ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> N e. NN )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ph -> f : ( 1 ... N ) -1-1-onto-> A )   &    |- ( ph -> K Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )   =>    |- ( ph -> seq M ( x. , F ) ~~> ( seq 1 ( x. , G ) ` N ) )
11-Apr-2024	prodmodclem3 11344	Lemma for prodmodc 11347. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- G = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( f ` j ) / k ]_ B , 1 ) )   &    |- H = ( j e. NN |-> if ( j <_ (♯ ` A ) , [_ ( K ` j ) / k ]_ B , 1 ) )   &    |- ( ph -> ( M e. NN /\ N e. NN ) )   &    |- ( ph -> f : ( 1 ... M ) -1-1-onto-> A )   &    |- ( ph -> K : ( 1 ... N ) -1-1-onto-> A )   =>    |- ( ph -> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , H ) ` N ) )
10-Apr-2024	jcnd 641	Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.)
|- ( ph -> ps )   &    |- ( ph -> -. ch )   =>    |- ( ph -> -. ( ps -> ch ) )
4-Apr-2024	prodrbdclem 11340	Lemma for prodrbdc 11343. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.)
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )   &    |- ( ( ph /\ k e. A ) -> B e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> DECID k e. A )   &    |- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) = seq N ( x. , F ) )
24-Mar-2024	prodfdivap 11316	The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) # 0 )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) / ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) / ( seq M ( x. , G ) ` N ) ) )
24-Mar-2024	prodfrecap 11315	The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) # 0 )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) = ( 1 / ( F ` k ) ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   =>    |- ( ph -> ( seq M ( x. , G ) ` N ) = ( 1 / ( seq M ( x. , F ) ` N ) ) )
23-Mar-2024	prodfap0 11314	The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) # 0 )   =>    |- ( ph -> ( seq M ( x. , F ) ` N ) # 0 )
22-Mar-2024	prod3fmul 11310	The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( G ` k ) e. CC )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( H ` k ) = ( ( F ` k ) x. ( G ` k ) ) )   =>    |- ( ph -> ( seq M ( x. , H ) ` N ) = ( ( seq M ( x. , F ) ` N ) x. ( seq M ( x. , G ) ` N ) ) )
21-Mar-2024	df-proddc 11320	Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sumdc 11123 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 21-Mar-2024.)
|- prod_ k e. A B = ( iota x ( E. m e. ZZ ( ( A C_ ( ZZ>= ` m ) /\ A. j e. ( ZZ>= ` m )DECID j e. A ) /\ ( E. n e. ( ZZ>= ` m ) E. y ( y # 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> if ( n <_ m , [_ ( f ` n ) / k ]_ B , 1 ) ) ) ` m ) ) ) )
19-Mar-2024	cos02pilt1 12932	Cosine is less than one between zero and 2 x. pi. (Contributed by Jim Kingdon, 19-Mar-2024.)
|- ( A e. ( 0 (,) ( 2 x. pi ) ) -> ( cos ` A ) < 1 )
19-Mar-2024	cosq34lt1 12931	Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.)
|- ( A e. ( pi [,) ( 2 x. pi ) ) -> ( cos ` A ) < 1 )
14-Mar-2024	coseq0q4123 12915	Location of the zeroes of cosine in ( -u ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ). (Contributed by Jim Kingdon, 14-Mar-2024.)
|- ( A e. ( -u ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ) -> ( ( cos ` A ) = 0 <-> A = ( pi / 2 ) ) )
14-Mar-2024	cosq23lt0 12914	The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.)
|- ( A e. ( ( pi / 2 ) (,) ( 3 x. ( pi / 2 ) ) ) -> ( cos ` A ) < 0 )
9-Mar-2024	pilem3 12864	Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.)
|- ( pi e. ( 2 (,) 4 ) /\ ( sin ` pi ) = 0 )
9-Mar-2024	exmidonfin 7050	If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6766 and nnon 4523. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
|- ( om = ( On i^i Fin ) -> EXMID )
9-Mar-2024	exmidonfinlem 7049	Lemma for exmidonfin 7050. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.)
|- A = { { x e. { (/) } | ph } , { x e. { (/) } | -. ph } }   =>    |- ( om = ( On i^i Fin ) -> DECID ph )
8-Mar-2024	sin0pilem2 12863	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
|- E. q e. ( 2 (,) 4 ) ( ( sin ` q ) = 0 /\ A. x e. ( 0 (,) q ) 0 < ( sin ` x ) )
8-Mar-2024	sin0pilem1 12862	Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.)
|- E. p e. ( 1 (,) 2 ) ( ( cos ` p ) = 0 /\ A. x e. ( p (,) ( 2 x. p ) ) 0 < ( sin ` x ) )
7-Mar-2024	cosz12 12861	Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.)
|- E. p e. ( 1 (,) 2 ) ( cos ` p ) = 0
6-Mar-2024	cos12dec 11474	Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.)
|- ( ( A e. ( 1 [,] 2 ) /\ B e. ( 1 [,] 2 ) /\ A < B ) -> ( cos ` B ) < ( cos ` A ) )
25-Feb-2024	mul2lt0pn 9551	The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < 0 )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> ( B x. A ) < 0 )
25-Feb-2024	mul2lt0np 9550	The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < 0 )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> ( A x. B ) < 0 )
25-Feb-2024	lt0ap0 8410	A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ( A e. RR /\ A < 0 ) -> A # 0 )
25-Feb-2024	negap0d 8393	The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> -u A # 0 )
24-Feb-2024	lt0ap0d 8411	A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> A # 0 )
20-Feb-2024	ivthdec 12791	The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` B ) < U /\ U < ( F ` A ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` y ) < ( F ` x ) )   =>    |- ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )
20-Feb-2024	ivthinclemex 12789	Lemma for ivthinc 12790. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> E! z e. ( A (,) B ) ( A. q e. L q < z /\ A. r e. R z < r ) )
19-Feb-2024	ivthinclemuopn 12785	Lemma for ivthinc 12790. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   &    |- ( ph -> S e. R )   =>    |- ( ph -> E. q e. R q < S )
19-Feb-2024	dedekindicc 12780	A Dedekind cut identifies a unique real number. Similar to df-inp 7274 except that the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 19-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E! x e. ( A (,) B ) ( A. q e. L q < x /\ A. r e. U x < r ) )
18-Feb-2024	ivthinclemloc 12788	Lemma for ivthinc 12790. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. R ) ) )
18-Feb-2024	ivthinclemdisj 12787	Lemma for ivthinc 12790. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> ( L i^i R ) = (/) )
18-Feb-2024	ivthinclemur 12786	Lemma for ivthinc 12790. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> A. r e. ( A [,] B ) ( r e. R <-> E. q e. R q < r ) )
18-Feb-2024	ivthinclemlr 12784	Lemma for ivthinc 12790. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )
18-Feb-2024	ivthinclemum 12782	Lemma for ivthinc 12790. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> E. r e. ( A [,] B ) r e. R )
18-Feb-2024	ivthinclemlm 12781	Lemma for ivthinc 12790. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   =>    |- ( ph -> E. q e. ( A [,] B ) q e. L )
15-Feb-2024	dedekindicclemeu 12778	Lemma for dedekindicc 12780. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   &    |- ( ph -> C e. ( A [,] B ) )   &    |- ( ph -> ( A. q e. L q < C /\ A. r e. U C < r ) )   &    |- ( ph -> D e. ( A [,] B ) )   &    |- ( ph -> ( A. q e. L q < D /\ A. r e. U D < r ) )   &    |- ( ph -> C < D )   =>    |- ( ph -> F. )
15-Feb-2024	dedekindicclemlu 12777	Lemma for dedekindicc 12780. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E. x e. ( A [,] B ) ( A. q e. L q < x /\ A. r e. U x < r ) )
15-Feb-2024	dedekindicclemlub 12776	Lemma for dedekindicc 12780. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E. x e. ( A [,] B ) ( A. y e. L -. x < y /\ A. y e. ( A [,] B ) ( y < x -> E. z e. L y < z ) ) )
15-Feb-2024	dedekindicclemloc 12775	Lemma for dedekindicc 12780. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( E. z e. L x < z \/ A. z e. L z < y ) ) )
15-Feb-2024	dedekindicclemub 12774	Lemma for dedekindicc 12780. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. ( A [,] B ) A. y e. L y < x )
15-Feb-2024	dedekindicclemuub 12773	Lemma for dedekindicc 12780. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> C e. U )   =>    |- ( ph -> A. z e. L z < C )
14-Feb-2024	suplociccex 12772	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7837 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B < C )   &    |- ( ph -> A C_ ( B [,] C ) )   &    |- ( ph -> E. x x e. A )   &    |- ( ph -> A. x e. ( B [,] C ) A. y e. ( B [,] C ) ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) )   =>    |- ( ph -> E. x e. ( B [,] C ) ( A. y e. A -. x < y /\ A. y e. ( B [,] C ) ( y < x -> E. z e. A y < z ) ) )
14-Feb-2024	suplociccreex 12771	An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7837 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
|- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B < C )   &    |- ( ph -> A C_ ( B [,] C ) )   &    |- ( ph -> E. x x e. A )   &    |- ( ph -> A. x e. ( B [,] C ) A. y e. ( B [,] C ) ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) )   =>    |- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
6-Feb-2024	ivthinclemlopn 12783	Lemma for ivthinc 12790. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   &    |- L = { w e. ( A [,] B ) | ( F ` w ) < U }   &    |- R = { w e. ( A [,] B ) | U < ( F ` w ) }   &    |- ( ph -> Q e. L )   =>    |- ( ph -> E. r e. L Q < r )
5-Feb-2024	ivthinc 12790	The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> U e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> ( A [,] B ) C_ D )   &    |- ( ph -> F e. ( D -cn-> CC ) )   &    |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. RR )   &    |- ( ph -> ( ( F ` A ) < U /\ U < ( F ` B ) ) )   &    |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ ( y e. ( A [,] B ) /\ x < y ) ) -> ( F ` x ) < ( F ` y ) )   =>    |- ( ph -> E. c e. ( A (,) B ) ( F ` c ) = U )
2-Feb-2024	dedekindeulemuub 12764	Lemma for dedekindeu 12770. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A e. U )   =>    |- ( ph -> A. z e. L z < A )
31-Jan-2024	dedekindeulemeu 12769	Lemma for dedekindeu 12770. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> ( A. q e. L q < A /\ A. r e. U A < r ) )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A. q e. L q < B /\ A. r e. U B < r ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> F. )
31-Jan-2024	dedekindeulemlu 12768	Lemma for dedekindeu 12770. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. RR ( A. q e. L q < x /\ A. r e. U x < r ) )
31-Jan-2024	dedekindeulemlub 12767	Lemma for dedekindeu 12770. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. RR ( A. y e. L -. x < y /\ A. y e. RR ( y < x -> E. z e. L y < z ) ) )
31-Jan-2024	dedekindeulemloc 12766	Lemma for dedekindeu 12770. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> A. x e. RR A. y e. RR ( x < y -> ( E. z e. L x < z \/ A. z e. L z < y ) ) )
31-Jan-2024	dedekindeulemub 12765	Lemma for dedekindeu 12770. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E. x e. RR A. y e. L y < x )
30-Jan-2024	axsuploc 7837	An inhabited, bounded-above, located set of reals has a supremum. Axiom for real and complex numbers, derived from ZF set theory. (This restates ax-pre-suploc 7741 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y < x /\ A. x e. RR A. y e. RR ( x < y -> ( E. z e. A x < z \/ A. z e. A z < y ) ) ) ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )
24-Jan-2024	axpre-suploclemres 7709	Lemma for axpre-suploc 7710. The result. The proof just needs to define B as basically the same set as A (but expressed as a subset of R. rather than a subset of RR), and apply suplocsr 7617. (Contributed by Jim Kingdon, 24-Jan-2024.)
|- ( ph -> A C_ RR )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. RR A. y e. A y <RR x )   &    |- ( ph -> A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) )   &    |- B = { w e. R. | <. w , 0R >. e. A }   =>    |- ( ph -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
23-Jan-2024	ax-pre-suploc 7741	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given x < y, either there is an element of the set greater than x, or y is an upper bound. Although this and ax-caucvg 7740 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7740. (Contributed by Jim Kingdon, 23-Jan-2024.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
23-Jan-2024	axpre-suploc 7710	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given x < y, either there is an element of the set greater than x, or y is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7741. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
22-Jan-2024	suplocsr 7617	An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
21-Jan-2024	bj-el2oss1o 12981	Shorter proof of el2oss1o 13188 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. 2o -> A C_ 1o )
21-Jan-2024	ltm1sr 7585	Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.)
|- ( A e. R. -> ( A +R -1R ) <R A )
19-Jan-2024	suplocsrlempr 7615	Lemma for suplocsr 7617. The set B has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. v e. P. ( A. w e. B -. v <P w /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) )
18-Jan-2024	suplocsrlemb 7614	Lemma for suplocsr 7617. The set B is located. (Contributed by Jim Kingdon, 18-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> A. u e. P. A. v e. P. ( u <P v -> ( E. q e. B u <P q \/ A. q e. B q <P v ) ) )
16-Jan-2024	suplocsrlem 7616	Lemma for suplocsr 7617. The set A has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
14-Jan-2024	suplocexprlemlub 7532	Lemma for suplocexpr 7533. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> ( y <P B -> E. z e. A y <P z ) )
14-Jan-2024	suplocexprlemub 7531	Lemma for suplocexpr 7533. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. y e. A -. B <P y )
10-Jan-2024	cbvcsbw 3007	Version of cbvcsb 3008 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
|- F/_ y C   &    |- F/_ x D   &    |- ( x = y -> C = D )   =>    |- [_ A / x ]_ C = [_ A / y ]_ D
10-Jan-2024	cbvsbcw 2936	Version of cbvsbc 2937 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( [. A / x ]. ph <-> [. A / y ]. ps )
10-Jan-2024	cbvreuvw 2660	Version of cbvreuv 2656 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x e. A ph <-> E! y e. A ps )
10-Jan-2024	cbvrexvw 2659	Version of cbvrexv 2655 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x e. A ph <-> E. y e. A ps )
10-Jan-2024	cbvralvw 2658	Version of cbvralv 2654 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x e. A ph <-> A. y e. A ps )
10-Jan-2024	cbvabw 2262	Version of cbvab 2263 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- { x | ph } = { y | ps }
9-Jan-2024	suplocexprlemloc 7529	Lemma for suplocexpr 7533. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. U. ( 1st " A ) \/ r e. ( 2nd ` B ) ) ) )
9-Jan-2024	suplocexprlemdisj 7528	Lemma for suplocexpr 7533. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. q e. Q. -. ( q e. U. ( 1st " A ) /\ q e. ( 2nd ` B ) ) )
9-Jan-2024	suplocexprlemru 7527	Lemma for suplocexpr 7533. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> A. r e. Q. ( r e. ( 2nd ` B ) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B ) ) ) )
9-Jan-2024	suplocexprlemrl 7525	Lemma for suplocexpr 7533. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> A. q e. Q. ( q e. U. ( 1st " A ) <-> E. r e. Q. ( q <Q r /\ r e. U. ( 1st " A ) ) ) )
9-Jan-2024	suplocexprlem2b 7522	Lemma for suplocexpr 7533. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( A C_ P. -> ( 2nd ` B ) = { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } )
9-Jan-2024	suplocexprlemell 7521	Lemma for suplocexpr 7533. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
|- ( B e. U. ( 1st " A ) <-> E. x e. A B e. ( 1st ` x ) )
7-Jan-2024	suplocexpr 7533	An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> E. x e. P. ( A. y e. A -. x <P y /\ A. y e. P. ( y <P x -> E. z e. A y <P z ) ) )
7-Jan-2024	suplocexprlemex 7530	Lemma for suplocexpr 7533. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> B e. P. )
7-Jan-2024	suplocexprlemmu 7526	Lemma for suplocexpr 7533. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   &    |- B = <. U. ( 1st " A ) , { u e. Q. | E. w e. |^| ( 2nd " A ) w <Q u } >.   =>    |- ( ph -> E. s e. Q. s e. ( 2nd ` B ) )
7-Jan-2024	suplocexprlemml 7524	Lemma for suplocexpr 7533. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> E. s e. Q. s e. U. ( 1st " A ) )
7-Jan-2024	suplocexprlemss 7523	Lemma for suplocexpr 7533. A is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. P. A. y e. A y <P x )   &    |- ( ph -> A. x e. P. A. y e. P. ( x <P y -> ( E. z e. A x <P z \/ A. z e. A z <P y ) ) )   =>    |- ( ph -> A C_ P. )
5-Jan-2024	dedekindicclemicc 12779	Lemma for dedekindicc 12780. Same as dedekindicc 12780, except that we merely show x to be an element of ( A [,] B ). Later we will strengthen that to ( A (,) B ). (Contributed by Jim Kingdon, 5-Jan-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> L C_ ( A [,] B ) )   &    |- ( ph -> U C_ ( A [,] B ) )   &    |- ( ph -> E. q e. ( A [,] B ) q e. L )   &    |- ( ph -> E. r e. ( A [,] B ) r e. U )   &    |- ( ph -> A. q e. ( A [,] B ) ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. ( A [,] B ) ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. ( A [,] B ) A. r e. ( A [,] B ) ( q < r -> ( q e. L \/ r e. U ) ) )   &    |- ( ph -> A < B )   =>    |- ( ph -> E! x e. ( A [,] B ) ( A. q e. L q < x /\ A. r e. U x < r ) )
5-Jan-2024	dedekindeu 12770	A Dedekind cut identifies a unique real number. Similar to df-inp 7274 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.)
|- ( ph -> L C_ RR )   &    |- ( ph -> U C_ RR )   &    |- ( ph -> E. q e. RR q e. L )   &    |- ( ph -> E. r e. RR r e. U )   &    |- ( ph -> A. q e. RR ( q e. L <-> E. r e. L q < r ) )   &    |- ( ph -> A. r e. RR ( r e. U <-> E. q e. U q < r ) )   &    |- ( ph -> ( L i^i U ) = (/) )   &    |- ( ph -> A. q e. RR A. r e. RR ( q < r -> ( q e. L \/ r e. U ) ) )   =>    |- ( ph -> E! x e. RR ( A. q e. L q < x /\ A. r e. U x < r ) )
31-Dec-2023	dvmptsubcn 12854	Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
|- ( ( ph /\ x e. CC ) -> A e. CC )   &    |- ( ( ph /\ x e. CC ) -> B e. V )   &    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )   &    |- ( ( ph /\ x e. CC ) -> C e. CC )   &    |- ( ( ph /\ x e. CC ) -> D e. W )   &    |- ( ph -> ( CC _D ( x e. CC |-> C ) ) = ( x e. CC |-> D ) )   =>    |- ( ph -> ( CC _D ( x e. CC |-> ( A - C ) ) ) = ( x e. CC |-> ( B - D ) ) )
31-Dec-2023	dvmptnegcn 12853	Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
|- ( ( ph /\ x e. CC ) -> A e. CC )   &    |- ( ( ph /\ x e. CC ) -> B e. V )   &    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )   =>    |- ( ph -> ( CC _D ( x e. CC |-> -u A ) ) = ( x e. CC |-> -u B ) )
31-Dec-2023	dvmptcmulcn 12852	Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.)
|- ( ( ph /\ x e. CC ) -> A e. CC )   &    |- ( ( ph /\ x e. CC ) -> B e. V )   &    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> B ) )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( CC _D ( x e. CC |-> ( C x. A ) ) ) = ( x e. CC |-> ( C x. B ) ) )
31-Dec-2023	brm 3978	If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.)
|- ( A R B -> E. x x e. R )
30-Dec-2023	dvmptccn 12848	Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> 0 ) )
30-Dec-2023	dvmptidcn 12847	Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.)
|- ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 )
25-Dec-2023	ctfoex 7003	A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.)
|- ( E. f f : om -onto-> ( A ⊔ 1o ) -> A e. _V )
23-Dec-2023	enct 11946	Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- ( A ~~ B -> ( E. f f : om -onto-> ( A ⊔ 1o ) <-> E. g g : om -onto-> ( B ⊔ 1o ) ) )
23-Dec-2023	enctlem 11945	Lemma for enct 11946. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- ( A ~~ B -> ( E. f f : om -onto-> ( A ⊔ 1o ) -> E. g g : om -onto-> ( B ⊔ 1o ) ) )
23-Dec-2023	omct 7002	om is countable. (Contributed by Jim Kingdon, 23-Dec-2023.)
|- E. f f : om -onto-> ( om ⊔ 1o )
21-Dec-2023	dvcoapbr 12840	The chain rule for derivatives at a point. The u # C -> ( G ` u ) # ( G ` C ) hypothesis constrains what functions work for G. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
|- ( ph -> F : X --> CC )   &    |- ( ph -> X C_ S )   &    |- ( ph -> G : Y --> X )   &    |- ( ph -> Y C_ T )   &    |- ( ph -> A. u e. Y ( u # C -> ( G ` u ) # ( G ` C ) ) )   &    |- ( ph -> S C_ CC )   &    |- ( ph -> T C_ CC )   &    |- ( ph -> ( G ` C ) ( S _D F ) K )   &    |- ( ph -> C ( T _D G ) L )   &    |- J = ( MetOpen ` ( abs o. - ) )   =>    |- ( ph -> C ( T _D ( F o. G ) ) ( K x. L ) )
19-Dec-2023	apsscn 8409	The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.)
|- { x e. A | x # B } C_ CC
19-Dec-2023	aprcl 8408	Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.)
|- ( A # B -> ( A e. CC /\ B e. CC ) )
18-Dec-2023	limccoap 12816	Composition of two limits. This theorem is only usable in the case where x # X implies R(x) # C so it is less general than might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.) (Revised by Jim Kingdon, 18-Dec-2023.)
|- ( ( ph /\ x e. { w e. A | w # X } ) -> R e. { w e. B | w # C } )   &    |- ( ( ph /\ y e. { w e. B | w # C } ) -> S e. CC )   &    |- ( ph -> C e. ( ( x e. { w e. A | w # X } |-> R ) lim CC X ) )   &    |- ( ph -> D e. ( ( y e. { w e. B | w # C } |-> S ) lim CC C ) )   &    |- ( y = R -> S = T )   =>    |- ( ph -> D e. ( ( x e. { w e. A | w # X } |-> T ) lim CC X ) )
16-Dec-2023	cnreim 10750	Complex apartness in terms of real and imaginary parts. See also apreim 8365 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.)
|- ( ( A e. CC /\ B e. CC ) -> ( A # B <-> ( ( Re ` A ) # ( Re ` B ) \/ ( Im ` A ) # ( Im ` B ) ) ) )
14-Dec-2023	cnopnap 12763	The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.)
|- ( A e. CC -> { w e. CC | w # A } e. ( MetOpen ` ( abs o. - ) ) )
14-Dec-2023	cnovex 12365	The class of all continuous functions from a topology to another is a set. (Contributed by Jim Kingdon, 14-Dec-2023.)
|- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V )