P. 384 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38301-38400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	volicon0 38301	The measure of a nonempty left-closed, right-open interval. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( vol ` ( A [,) B ) ) = ( B - A ) )
Theorem	hsphoif 38302*	H is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29 (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- H = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> X e. V )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( ( H ` A ) ` B ) : X --> RR )
Theorem	hoidmvval 38303*	The dimensional volume of a multidimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> X e. Fin )   =>    |- ( ph -> ( A ( L ` X ) B ) = if ( X = (/) , 0 , prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) ) )
Theorem	hoissrrn2 38304*	A half-open interval is a subset of R^n . (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ( ph /\ k e. X ) -> A e. RR )   &    |- ( ( ph /\ k e. X ) -> B e. RR* )   =>    |- ( ph -> X_ k e. X ( A [,) B ) C_ ( RR ^m X ) )
Theorem	hsphoival 38305*	H is a function (that returns the representation of the right side of a half-open interval intersected with a half-space). Step (b) in Lemma 115B of [Fremlin1] p. 29 (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- H = ( x e. RR |-> ( a e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( a ` j ) , if ( ( a ` j ) <_ x , ( a ` j ) , x ) ) ) ) )   &    |- ( ph -> A e. RR )   &    |- ( ph -> X e. V )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> K e. X )   =>    |- ( ph -> ( ( ( H ` A ) ` B ) ` K ) = if ( K e. Y , ( B ` K ) , if ( ( B ` K ) <_ A , ( B ` K ) , A ) ) )
Theorem	hoiprodcl3 38306*	The pre-measure of half-open intervals is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> X e. Fin )   &    |- ( ( ph /\ k e. X ) -> A e. RR )   &    |- ( ( ph /\ k e. X ) -> B e. RR )   =>    |- ( ph -> prod_ k e. X ( vol ` ( A [,) B ) ) e. ( 0 [,) +oo ) )
Theorem	volicore 38307	The Lebesgue measure of a left-closed right-open interval is a real number. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A [,) B ) ) e. RR )
Theorem	hoidmvcl 38308*	The dimensional volume of a multidimensional half-open interval is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) B ) e. ( 0 [,) +oo ) )
Theorem	hoidmv0val 38309*	The dimensional volume of a 0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> A : (/) --> RR )   &    |- ( ph -> B : (/) --> RR )   =>    |- ( ph -> ( A ( L ` (/) ) B ) = 0 )
Theorem	hoidmvn0val 38310*	The dimensional volume of a non 0-dimensional half-open interval. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) B ) = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
Theorem	hsphoidmvle2 38311*	The dimensional volume of a half-open interval intersected with a two half-spaces. Used in the last inequality of step (c) of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- X = ( Y u. { Z } )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> C <_ D )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) ( ( H ` D ) ` B ) ) )
Theorem	hsphoidmvle 38312*	The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- X = ( Y u. { Z } )   &    |- ( ph -> C e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( j e. X |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) ( ( H ` C ) ` B ) ) <_ ( A ( L ` X ) B ) )
Theorem	hoidmvval0 38313*	The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ j ph   &    |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> E. j e. X ( B ` j ) <_ ( A ` j ) )   =>    |- ( ph -> ( A ( L ` X ) B ) = 0 )
Theorem	hoiprodp1 38314*	The dimensional volume of a half-open interval with dimension n + 1. Used in the first equality of step (e) of Lemma 115B of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> Z e. V )   &    |- ( ph -> -. Z e. Y )   &    |- X = ( Y u. { Z } )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- G = prod_ k e. Y ( vol ` ( ( A ` k ) [,) ( B ` k ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) = ( G x. ( vol ` ( ( A ` Z ) [,) ( B ` Z ) ) ) ) )
Theorem	sge0hsphoire 38315*	If the generalized sum of dimensional volumes of n-dimensional half-open intervals is finite, then the sum stays finite if every half-open interval is intersected with a half-space. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> Y e. Fin )   &    |- ( ph -> Z e. ( W \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- ( ph -> S e. RR )   =>    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
Theorem	hoidmvval0b 38316*	The dimensional volume of the (half-open interval) empty set. Definition 115A (c) of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   =>    |- ( ph -> ( A ( L ` X ) A ) = 0 )
Theorem	hoidmv1lelem1 38317*	The supremum of U belongs to U. This is the last part of step (a) and the whole step (b) in the proof of Lemma 114B of [Fremlin1] p. 23 (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> C : NN --> RR )   &    |- ( ph -> D : NN --> RR )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )   &    |- U = { z e. ( A [,] B ) | ( z - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   =>    |- ( ph -> ( S e. U /\ A e. U /\ E. x e. RR A. y e. U y <_ x ) )
Theorem	hoidmv1lelem2 38318*	This is the contradiction proven in step (c) in the proof of Lemma 114B of [Fremlin1] p. 23 (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C : NN --> RR )   &    |- ( ph -> D : NN --> RR )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )   &    |- U = { z e. ( A [,] B ) | ( z - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }   &    |- ( ph -> S e. U )   &    |- ( ph -> A <_ S )   &    |- ( ph -> S < B )   &    |- ( ph -> K e. NN )   &    |- ( ph -> S e. ( ( C ` K ) [,) ( D ` K ) ) )   &    |- M = if ( ( D ` K ) <_ B , ( D ` K ) , B )   =>    |- ( ph -> E. u e. U S < u )
Theorem	hoidmv1lelem3 38319*	The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the non-empty, finite generalized sum, sub case in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> C : NN --> RR )   &    |- ( ph -> D : NN --> RR )   &    |- ( ph -> ( A [,) B ) C_ U_ j e. NN ( ( C ` j ) [,) ( D ` j ) ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) e. RR )   &    |- U = { z e. ( A [,] B ) | ( z - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) if ( ( D ` j ) <_ z , ( D ` j ) , z ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   =>    |- ( ph -> ( B - A ) <_ (Σ^ ` ( j e. NN |-> ( vol ` ( ( C ` j ) [,) ( D ` j ) ) ) ) ) )
Theorem	hoidmv1le 38320*	The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of [Fremlin1] p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of [Fremlin1] p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> Z e. V )   &    |- X = { Z }   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> C : NN --> ( RR ^m X ) )   &    |- ( ph -> D : NN --> ( RR ^m X ) )   &    |- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
Theorem	hoidmvlelem1 38321*	The supremum of U belongs to U. Step (c) in the proof of Lemma 115B of [Fremlin1] p. 29 (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   &    |- ( ph -> ( A ` Z ) < ( B ` Z ) )   =>    |- ( ph -> S e. U )
Theorem	hoidmvlelem2 38322*	This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- F = ( y e. Y |-> 0 )   &    |- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- ( ph -> S e. U )   &    |- ( ph -> S < ( B ` Z ) )   &    |- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )   &    |- ( ph -> M e. NN )   &    |- ( ph -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) )   &    |- O = ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )   &    |- V = ( { ( B ` Z ) } u. O )   &    |- Q = inf ( V , RR , < )   =>    |- ( ph -> E. u e. U S < u )
Theorem	hoidmvlelem3 38323*	This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )   &    |- F = ( y e. Y |-> 0 )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- ( ph -> S e. U )   &    |- ( ph -> S < ( B ` Z ) )   &    |- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )   &    |- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ (Σ^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )   &    |- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   &    |- O = ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) |-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )   =>    |- ( ph -> E. u e. U S < u )
Theorem	hoidmvlelem4 38324*	The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29, case nonempty interval and dimension of the space greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Y =/= (/) )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )   &    |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )   &    |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )   &    |- ( ph -> E e. RR+ )   &    |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }   &    |- S = sup ( U , RR , < )   &    |- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ (Σ^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )   &    |- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   =>    |- ( ph -> ( A ( L ` W ) B ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) ) )
Theorem	hoidmvlelem5 38325*	The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Z e. ( X \ Y ) )   &    |- W = ( Y u. { Z } )   &    |- ( ph -> A : W --> RR )   &    |- ( ph -> B : W --> RR )   &    |- ( ph -> C : NN --> ( RR ^m W ) )   &    |- ( ph -> D : NN --> ( RR ^m W ) )   &    |- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ (Σ^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )   &    |- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   &    |- ( ph -> Y =/= (/) )   =>    |- ( ph -> ( A ( L ` W ) B ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) )
Theorem	hoidmvle 38326*	The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- ( ph -> C : NN --> ( RR ^m X ) )   &    |- ( ph -> D : NN --> ( RR ^m X ) )   &    |- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) <_ (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
Theorem	ovnhoilem1 38327*	The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   &    |- H = ( j e. NN |-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )   =>    |- ( ph -> ( (voln* ` X ) ` I ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
Theorem	ovnhoilem2 38328*	The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )   &    |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   &    |- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = (Σ^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }   &    |- F = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 1st ` ( ( i ` n ) ` l ) ) ) ) )   &    |- S = ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) |-> ( n e. NN |-> ( l e. X |-> ( 2nd ` ( ( i ` n ) ` l ) ) ) ) )   =>    |- ( ph -> ( A ( L ` X ) B ) <_ ( (voln* ` X ) ` I ) )
Theorem	ovnhoi 38329*	The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of [Fremlin1] p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> A : X --> RR )   &    |- ( ph -> B : X --> RR )   &    |- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )   &    |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )   =>    |- ( ph -> ( (voln* ` X ) ` I ) = ( A ( L ` X ) B ) )
21.31  Mathbox for Saveliy Skresanov
21.31.1  Ceva's theorem
Theorem	sigarval 38330*	Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A G B ) = ( Im ` ( ( * ` A ) x. B ) ) )
Theorem	sigarim 38331*	Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A G B ) e. RR )
Theorem	sigarac 38332*	Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC ) -> ( A G B ) = -u ( B G A ) )
Theorem	sigaraf 38333*	Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) G B ) = ( ( A G B ) + ( C G B ) ) )
Theorem	sigarmf 38334*	Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G B ) = ( ( A G B ) - ( C G B ) ) )
Theorem	sigaras 38335*	Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B + C ) ) = ( ( A G B ) + ( A G C ) ) )
Theorem	sigarms 38336*	Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A G ( B - C ) ) = ( ( A G B ) - ( A G C ) ) )
Theorem	sigarls 38337*	Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. RR ) -> ( A G ( B x. C ) ) = ( ( A G B ) x. C ) )
Theorem	sigarid 38338*	Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( A e. CC -> ( A G A ) = 0 )
Theorem	sigarexp 38339*	Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( ( A G B ) - ( A G C ) ) - ( C G B ) ) )
Theorem	sigarperm 38340*	Signed area ( A - C ) G ( B - C ) acts as a double area of a triangle A B C. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) G ( B - C ) ) = ( ( B - A ) G ( C - A ) ) )
Theorem	sigardiv 38341*	If signed area between vectors B - A and C - A is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> -. C = A )   &    |- ( ph -> ( ( B - A ) G ( C - A ) ) = 0 )   =>    |- ( ph -> ( ( B - A ) / ( C - A ) ) e. RR )
Theorem	sigarimcd 38342*	Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC ) )   =>    |- ( ph -> ( A G B ) e. CC )
Theorem	sigariz 38343*	If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. ( Contributed by Saveliy Skresanov, 23-Sep-2017.) (Contributed by Saveliy Skresanov, 24-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC ) )   &    |- ( ph -> ( A G B ) = 0 )   =>    |- ( ph -> ( B G A ) = 0 )
Theorem	sigarcol 38344*	Given three points A, B and C such that -. A = B, the point C lies on the line going through A and B iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> -. A = B )   =>    |- ( ph -> ( ( ( A - C ) G ( B - C ) ) = 0 <-> E. t e. RR C = ( B + ( t x. ( A - B ) ) ) ) )
Theorem	sharhght 38345*	Let A B C be a triangle, and let D lie on the line A B. Then (doubled) areas of triangles A D C and C D B relate as lengths of corresponding bases A D and D B. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( D e. CC /\ ( ( A - D ) G ( B - D ) ) = 0 ) )   =>    |- ( ph -> ( ( ( C - A ) G ( D - A ) ) x. ( B - D ) ) = ( ( ( C - B ) G ( D - B ) ) x. ( A - D ) ) )
Theorem	sigaradd 38346*	Subtracting (double) area of A D C from A B C yields the (double) area of D B C. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( D e. CC /\ ( ( A - D ) G ( B - D ) ) = 0 ) )   =>    |- ( ph -> ( ( ( B - C ) G ( A - C ) ) - ( ( D - C ) G ( A - C ) ) ) = ( ( B - C ) G ( D - C ) ) )
Theorem	cevathlem1 38347	Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
|- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( D e. CC /\ E e. CC /\ F e. CC ) )   &    |- ( ph -> ( G e. CC /\ H e. CC /\ K e. CC ) )   &    |- ( ph -> ( A =/= 0 /\ E =/= 0 /\ C =/= 0 ) )   &    |- ( ph -> ( ( A x. B ) = ( C x. D ) /\ ( E x. F ) = ( A x. G ) /\ ( C x. H ) = ( E x. K ) ) )   =>    |- ( ph -> ( ( B x. F ) x. H ) = ( ( D x. G ) x. K ) )
Theorem	cevathlem2 38348*	Ceva's theorem second lemma. Relate (doubled) areas of triangles C A O and A B O with of segments B D and D C. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) )   &    |- ( ph -> O e. CC )   &    |- ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) )   =>    |- ( ph -> ( ( ( C - O ) G ( A - O ) ) x. ( B - D ) ) = ( ( ( A - O ) G ( B - O ) ) x. ( D - C ) ) )
Theorem	cevath 38349*	Ceva's theorem. Let A B C be a triangle and let points F, D and E lie on sides A B, B C, C A correspondingly. Suppose that cevians A D, B E and C F intersect at one point O. Then triangle's sides are partitioned into segments and their lengths satisfy a certain identity. Here we obtain a bit stronger version by using complex numbers themselves instead of their absolute values. The proof goes by applying cevathlem2 38348 three times and then using cevathlem1 38347 to multiply obtained identities and prove the theorem. In the theorem statement we are using function G as a collinearity indicator. For justification of that use, see sigarcol 38344. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
|- G = ( x e. CC , y e. CC |-> ( Im ` ( ( * ` x ) x. y ) ) )   &    |- ( ph -> ( A e. CC /\ B e. CC /\ C e. CC ) )   &    |- ( ph -> ( F e. CC /\ D e. CC /\ E e. CC ) )   &    |- ( ph -> O e. CC )   &    |- ( ph -> ( ( ( A - O ) G ( D - O ) ) = 0 /\ ( ( B - O ) G ( E - O ) ) = 0 /\ ( ( C - O ) G ( F - O ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - F ) G ( B - F ) ) = 0 /\ ( ( B - D ) G ( C - D ) ) = 0 /\ ( ( C - E ) G ( A - E ) ) = 0 ) )   &    |- ( ph -> ( ( ( A - O ) G ( B - O ) ) =/= 0 /\ ( ( B - O ) G ( C - O ) ) =/= 0 /\ ( ( C - O ) G ( A - O ) ) =/= 0 ) )   =>    |- ( ph -> ( ( ( A - F ) x. ( C - E ) ) x. ( B - D ) ) = ( ( ( F - B ) x. ( E - A ) ) x. ( D - C ) ) )
21.32  Mathbox for Jarvin Udandy
Theorem	hirstL-ax3 38350	The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.)
|- ( ( -. ph -> -. ps ) -> ( ( -. ph -> ps ) -> ph ) )
Theorem	ax3h 38351	Recovery of ax-3 8 from hirstL-ax3 38350. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )
Theorem	aibandbiaiffaiffb 38352	A closed form showing (a implies b and b implies a) same-as (a same-as b) (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( ph <-> ps ) )
Theorem	aibandbiaiaiffb 38353	A closed form showing (a implies b and b implies a) implies (a same-as b) (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) -> ( ph <-> ps ) )
Theorem	notatnand 38354	Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- -. ph   =>    |- -. ( ph /\ ps )
Theorem	aistia 38355	Given a is equivalent to T., there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
|- ( ph <-> T. )   =>    |- ph
Theorem	aisfina 38356	Given a is equivalent to F., there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
|- ( ph <-> F. )   =>    |- -. ph
Theorem	bothtbothsame 38357	Given both a, b are equivalent to T., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> T. )   =>    |- ( ph <-> ps )
Theorem	bothfbothsame 38358	Given both a, b are equivalent to F., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> F. )   =>    |- ( ph <-> ps )
Theorem	aiffbbtat 38359	Given a is equivalent to b, b is equivalent to T. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ph <-> ps )   &    |- ( ps <-> T. )   =>    |- ( ph <-> T. )
Theorem	aisbbisfaisf 38360	Given a is equivalent to b, b is equivalent to F. there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.)
|- ( ph <-> ps )   &    |- ( ps <-> F. )   =>    |- ( ph <-> F. )
Theorem	axorbtnotaiffb 38361	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1401 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ps )   =>    |- -. ( ph <-> ps )
Theorem	aiffnbandciffatnotciffb 38362	Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> -. ps )   &    |- ( ch <-> ph )   =>    |- -. ( ch <-> ps )
Theorem	axorbciffatcxorb 38363	Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ) . (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ps )   &    |- ( ch <-> ph )   =>    |- ( ch \/_ ps )
Theorem	aibnbna 38364	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
|- ( ph -> ps )   &    |- -. ps   =>    |- -. ph
Theorem	aibnbaif 38365	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
|- ( ph -> ps )   &    |- -. ps   =>    |- ( ph <-> F. )
Theorem	aiffbtbat 38366	Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ph <-> ps )   &    |- ( T. <-> ps )   =>    |- ( ph <-> T. )
Theorem	astbstanbst 38367	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> T. )   =>    |- ( ( ph /\ ps ) <-> T. )
Theorem	aistbistaandb 38368	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> T. )   =>    |- ( ph /\ ps )
Theorem	aisbnaxb 38369	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
|- ( ph <-> ps )   =>    |- -. ( ph \/_ ps )
Theorem	iatbtatnnb 38370	Given a implies b, there exists a proof for a implies not not b. (Contributed by Jarvin Udandy, 2-Sep-2016.)
|- ( ph -> ps )   =>    |- ( ph -> -. -. ps )
Theorem	atbiffatnnb 38371	If a implies b, then a implies not not b (Contributed by Jarvin Udandy, 28-Aug-2016.)
|- ( ( ph -> ps ) -> ( ph -> -. -. ps ) )
Theorem	bisaiaisb 38372	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ( ps <-> ph ) -> ( ph <-> ps ) )
Theorem	atbiffatnnbalt 38373	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ( ( ph -> ps ) -> ( ph -> -. -. ps ) )
Theorem	abnotbtaxb 38374	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ph   &    |- -. ps   =>    |- ( ph \/_ ps )
Theorem	abnotataxb 38375	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- -. ph   &    |- ps   =>    |- ( ph \/_ ps )
Theorem	conimpf 38376	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.)
|- ph   &    |- -. ps   &    |- ( ph -> ps )   =>    |- ( ph <-> F. )
Theorem	conimpfalt 38377	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.)
|- ph   &    |- -. ps   &    |- ( ph -> ps )   =>    |- ( ph <-> F. )
Theorem	aistbisfiaxb 38378	Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> T. )   &    |- ( ps <-> F. )   =>    |- ( ph \/_ ps )
Theorem	aisfbistiaxb 38379	Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   =>    |- ( ph \/_ ps )
Theorem	aifftbifffaibif 38380	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( ph <-> T. )   &    |- ( ps <-> F. )   =>    |- ( ( ph -> ps ) <-> F. )
Theorem	aifftbifffaibifff 38381	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( ph <-> T. )   &    |- ( ps <-> F. )   =>    |- ( ( ph <-> ps ) <-> F. )
Theorem	atnaiana 38382	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ph   =>    |- -. ( ph -> ( ph /\ -. ph ) )
Theorem	ainaiaandna 38383	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ph   =>    |- ( ph -> -. ( ph -> ( ph /\ -. ph ) ) )
Theorem	abcdta 38384	Given (((a and b) and c) and d), there exists a proof for a (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- ph
Theorem	abcdtb 38385	Given (((a and b) and c) and d), there exists a proof for b (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- ps
Theorem	abcdtc 38386	Given (((a and b) and c) and d), there exists a proof for c (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- ch
Theorem	abcdtd 38387	Given (((a and b) and c) and d), there exists a proof for d (Contributed by Jarvin Udandy, 3-Sep-2016.)
|- ( ( ( ph /\ ps ) /\ ch ) /\ th )   =>    |- th
Theorem	abciffcbatnabciffncba 38388	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( -. ( ( ph /\ ps ) /\ ch ) -> -. ( ( ch /\ ps ) /\ ph ) )
Theorem	abciffcbatnabciffncbai 38389	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ( ( ( ph /\ ps ) /\ ch ) <-> ( ( ch /\ ps ) /\ ph ) )   =>    |- ( -. ( ( ph /\ ps ) /\ ch ) -> -. ( ( ch /\ ps ) /\ ph ) )
Theorem	nabctnabc 38390	not ( a -> ( b /\ c ) ) we can show: not a implies ( b /\ c ) (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- -. ( ph -> ( ps /\ ch ) )   =>    |- ( -. ph -> ( ps /\ ch ) )
Theorem	jabtaib 38391	For when pm3.4 lacks a pm3.4i. (Contributed by Jarvin Udandy, 9-Sep-2020.)
|- ( ph /\ ps )   =>    |- ( ph -> ps )
Theorem	onenotinotbothi 38392	From one negated implication it is not the case its non negated form and a random others are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.)
|- -. ( ph -> ps )   =>    |- -. ( ( ph -> ps ) /\ ( ch -> th ) )
Theorem	twonotinotbothi 38393	From these two negated implications it is not the case their non negated forms are both true. (Contributed by Jarvin Udandy, 11-Sep-2020.)
|- -. ( ph -> ps )   &    |- -. ( ch -> th )   =>    |- -. ( ( ph -> ps ) /\ ( ch -> th ) )
Theorem	clifte 38394	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
|- ( ph /\ -. ch )   &    |- th   =>    |- ( th <-> ( ( ph /\ -. ch ) \/ ( ps /\ ch ) ) )
Theorem	cliftet 38395	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
|- ( ph /\ ch )   &    |- th   =>    |- ( th <-> ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) )
Theorem	clifteta 38396	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
|- ( ( ph /\ -. ch ) \/ ( ps /\ ch ) )   &    |- th   =>    |- ( th <-> ( ( ph /\ -. ch ) \/ ( ps /\ ch ) ) )
Theorem	cliftetb 38397	show d is the same as an if-else involving a,b. (Contributed by Jarvin Udandy, 20-Sep-2020.)
|- ( ( ph /\ ch ) \/ ( ps /\ -. ch ) )   &    |- th   =>    |- ( th <-> ( ( ph /\ ch ) \/ ( ps /\ -. ch ) ) )
Theorem	confun 38398	Given the hypotheses there exists a proof for (c implies ( d iff a ) ) (Contributed by Jarvin Udandy, 6-Sep-2020.)
|- ph   &    |- ( ch -> ps )   &    |- ( ch -> th )   &    |- ( ph -> ( ph -> ps ) )   =>    |- ( ch -> ( th <-> ph ) )
Theorem	confun2 38399	Confun simplified to two propositions. (Contributed by Jarvin Udandy, 6-Sep-2020.)
|- ( ps -> ph )   &    |- ( ps -> -. ( ps -> ( ps /\ -. ps ) ) )   &    |- ( ( ps -> ph ) -> ( ( ps -> ph ) -> ph ) )   =>    |- ( ps -> ( -. ( ps -> ( ps /\ -. ps ) ) <-> ( ps -> ph ) ) )
Theorem	confun3 38400	Confun's more complex form where both a,d have been "defined". (Contributed by Jarvin Udandy, 6-Sep-2020.)
|- ( ph <-> ( ch -> ps ) )   &    |- ( th <-> -. ( ch -> ( ch /\ -. ch ) ) )   &    |- ( ch -> ps )   &    |- ( ch -> -. ( ch -> ( ch /\ -. ch ) ) )   &    |- ( ( ch -> ps ) -> ( ( ch -> ps ) -> ps ) )   =>    |- ( ch -> ( -. ( ch -> ( ch /\ -. ch ) ) <-> ( ch -> ps ) ) )