P. 82 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rexri 8101	A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.)
|- A e. RR   =>    |- A e. RR*
Theorem	1xr 8102	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- 1 e. RR*
Theorem	renfdisj 8103	The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( RR i^i { +oo , -oo } ) = (/)
Theorem	ltrelxr 8104	'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- < C_ ( RR* X. RR* )
Theorem	ltrel 8105	'Less than' is a relation. (Contributed by NM, 14-Oct-2005.)
|- Rel <
Theorem	lerelxr 8106	'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.)
|- <_ C_ ( RR* X. RR* )
Theorem	lerel 8107	'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- Rel <_
Theorem	xrlenlt 8108	'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
Theorem	ltxrlt 8109	The standard less-than <RR and the extended real less-than < are identical when restricted to the non-extended reals RR. (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A <RR B ) )
4.2.3  Restate the ordering postulates with extended real "less than"
Theorem	axltirr 8110	Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 8008 with ordering on the extended reals. New proofs should use ltnr 8120 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.)
|- ( A e. RR -> -. A < A )
Theorem	axltwlin 8111	Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 8009 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( A < C \/ C < B ) ) )
Theorem	axlttrn 8112	Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 8010 with ordering on the extended reals. New proofs should use lttr 8117 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	axltadd 8113	Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 8012 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( C + A ) < ( C + B ) ) )
Theorem	axapti 8114	Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 8011 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ( ( A e. RR /\ B e. RR /\ -. ( A < B \/ B < A ) ) -> A = B )
Theorem	axmulgt0 8115	The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 8013 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) ) )
Theorem	axsuploc 8116*	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 8017 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 ) ) )
4.2.4  Ordering on reals
Theorem	lttr 8117	Alias for axlttrn 8112, for naming consistency with lttri 8148. New proofs should generally use this instead of ax-pre-lttrn 8010. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	mulgt0 8118	The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A x. B ) )
Theorem	lenlt 8119	'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> -. B < A ) )
Theorem	ltnr 8120	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> -. A < A )
Theorem	ltso 8121	'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.)
|- < Or RR
Theorem	gtso 8122	'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.)
|- `' < Or RR
Theorem	lttri3 8123	Tightness of real apartness. (Contributed by NM, 5-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	letri3 8124	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	ltleletr 8125	Transitive law, weaker form of ( A < B /\ B <_ C ) -> A < C. (Contributed by AV, 14-Oct-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A <_ C ) )
Theorem	letr 8126	Transitive law. (Contributed by NM, 12-Nov-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )
Theorem	leid 8127	'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.)
|- ( A e. RR -> A <_ A )
Theorem	ltne 8128	'Less than' implies not equal. See also ltap 8677 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- ( ( A e. RR /\ A < B ) -> B =/= A )
Theorem	ltnsym 8129	'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> -. B < A ) )
Theorem	eqlelt 8130	Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.)
|- ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )
Theorem	ltle 8131	'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
Theorem	lelttr 8132	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
Theorem	ltletr 8133	Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
Theorem	ltnsym2 8134	'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- ( ( A e. RR /\ B e. RR ) -> -. ( A < B /\ B < A ) )
Theorem	eqle 8135	Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.)
|- ( ( A e. RR /\ A = B ) -> A <_ B )
Theorem	ltnri 8136	'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.)
|- A e. RR   =>    |- -. A < A
Theorem	eqlei 8137	Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.)
|- A e. RR   =>    |- ( A = B -> A <_ B )
Theorem	eqlei2 8138	Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- A e. RR   =>    |- ( B = A -> B <_ A )
Theorem	gtneii 8139	'Less than' implies not equal. See also gtapii 8678 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.)
|- A e. RR   &    |- A < B   =>    |- B =/= A
Theorem	ltneii 8140	'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- A e. RR   &    |- A < B   =>    |- A =/= B
Theorem	lttri3i 8141	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( -. A < B /\ -. B < A ) )
Theorem	letri3i 8142	Tightness of real apartness. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A = B <-> ( A <_ B /\ B <_ A ) )
Theorem	ltnsymi 8143	'Less than' is not symmetric. (Contributed by NM, 6-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> -. B < A )
Theorem	lenlti 8144	'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A <_ B <-> -. B < A )
Theorem	ltlei 8145	'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> A <_ B )
Theorem	ltleii 8146	'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)
|- A e. RR   &    |- B e. RR   &    |- A < B   =>    |- A <_ B
Theorem	ltnei 8147	'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( A < B -> B =/= A )
Theorem	lttri 8148	'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A < B /\ B < C ) -> A < C )
Theorem	lelttri 8149	'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B < C ) -> A < C )
Theorem	ltletri 8150	'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A < B /\ B <_ C ) -> A < C )
Theorem	letri 8151	'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B <_ C ) -> A <_ C )
Theorem	le2tri3i 8152	Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   =>    |- ( ( A <_ B /\ B <_ C /\ C <_ A ) <-> ( A = B /\ B = C /\ C = A ) )
Theorem	mulgt0i 8153	The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.)
|- A e. RR   &    |- B e. RR   =>    |- ( ( 0 < A /\ 0 < B ) -> 0 < ( A x. B ) )
Theorem	mulgt0ii 8154	The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.)
|- A e. RR   &    |- B e. RR   &    |- 0 < A   &    |- 0 < B   =>    |- 0 < ( A x. B )
Theorem	ltnrd 8155	'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> -. A < A )
Theorem	gtned 8156	'Less than' implies not equal. See also gtapd 8681 which is the same but for apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> B =/= A )
Theorem	ltned 8157	'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	lttri3d 8158	Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	letri3d 8159	Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	eqleltd 8160	Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )
Theorem	lenltd 8161	'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A <_ B <-> -. B < A ) )
Theorem	ltled 8162	'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> A <_ B )
Theorem	ltnsymd 8163	'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> -. B < A )
Theorem	nltled 8164	'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> -. B < A )   =>    |- ( ph -> A <_ B )
Theorem	lensymd 8165	'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> -. B < A )
Theorem	mulgt0d 8166	The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 < A )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> 0 < ( A x. B ) )
Theorem	letrd 8167	Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> A <_ C )
Theorem	lelttrd 8168	Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	lttrd 8169	Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	0lt1 8170	0 is less than 1. Theorem I.21 of [Apostol] p. 20. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 17-Jan-1997.)
|- 0 < 1
Theorem	ltntri 8171	Negative trichotomy property for real numbers. It is well known that we cannot prove real number trichotomy, A < B \/ A = B \/ B < A. Does that mean there is a pair of real numbers where none of those hold (that is, where we can refute each of those three relationships)? Actually, no, as shown here. This is another example of distinguishing between being unable to prove something, or being able to refute it. (Contributed by Jim Kingdon, 13-Aug-2023.)
|- ( ( A e. RR /\ B e. RR ) -> -. ( -. A < B /\ -. A = B /\ -. B < A ) )
4.2.5  Initial properties of the complex numbers
Theorem	mul12 8172	Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )
Theorem	mul32 8173	Commutative/associative law. (Contributed by NM, 8-Oct-1999.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )
Theorem	mul31 8174	Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( ( C x. B ) x. A ) )
Theorem	mul4 8175	Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) ) )
Theorem	muladd11 8176	A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( 1 + A ) x. ( 1 + B ) ) = ( ( 1 + A ) + ( B + ( A x. B ) ) ) )
Theorem	1p1times 8177	Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( A e. CC -> ( ( 1 + 1 ) x. A ) = ( A + A ) )
Theorem	peano2cn 8178	A theorem for complex numbers analogous the second Peano postulate peano2 4632. (Contributed by NM, 17-Aug-2005.)
|- ( A e. CC -> ( A + 1 ) e. CC )
Theorem	peano2re 8179	A theorem for reals analogous the second Peano postulate peano2 4632. (Contributed by NM, 5-Jul-2005.)
|- ( A e. RR -> ( A + 1 ) e. RR )
Theorem	addcom 8180	Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
Theorem	addrid 8181	0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Theorem	addlid 8182	0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( A e. CC -> ( 0 + A ) = A )
Theorem	readdcan 8183	Cancellation law for addition over the reals. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C + A ) = ( C + B ) <-> A = B ) )
Theorem	00id 8184	0 is its own additive identity. (Contributed by Scott Fenton, 3-Jan-2013.)
|- ( 0 + 0 ) = 0
Theorem	addridi 8185	0 is an additive identity. (Contributed by NM, 23-Nov-1994.) (Revised by Scott Fenton, 3-Jan-2013.)
|- A e. CC   =>    |- ( A + 0 ) = A
Theorem	addlidi 8186	0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
|- A e. CC   =>    |- ( 0 + A ) = A
Theorem	addcomi 8187	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) = ( B + A )
Theorem	addcomli 8188	Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. CC   &    |- B e. CC   &    |- ( A + B ) = C   =>    |- ( B + A ) = C
Theorem	mul12i 8189	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by NM, 11-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( A x. ( B x. C ) ) = ( B x. ( A x. C ) )
Theorem	mul32i 8190	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by NM, 11-May-1999.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   =>    |- ( ( A x. B ) x. C ) = ( ( A x. C ) x. B )
Theorem	mul4i 8191	Rearrangement of 4 factors. (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &    |- B e. CC   &    |- C e. CC   &    |- D e. CC   =>    |- ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) )
Theorem	addridd 8192	0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A + 0 ) = A )
Theorem	addlidd 8193	0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 0 + A ) = A )
Theorem	addcomd 8194	Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A + B ) = ( B + A ) )
Theorem	mul12d 8195	Commutative/associative law that swaps the first two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B x. C ) ) = ( B x. ( A x. C ) ) )
Theorem	mul32d 8196	Commutative/associative law that swaps the last two factors in a triple product. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A x. B ) x. C ) = ( ( A x. C ) x. B ) )
Theorem	mul31d 8197	Commutative/associative law. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A x. B ) x. C ) = ( ( C x. B ) x. A ) )
Theorem	mul4d 8198	Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A x. B ) x. ( C x. D ) ) = ( ( A x. C ) x. ( B x. D ) ) )
Theorem	muladd11r 8199	A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + 1 ) x. ( B + 1 ) ) = ( ( ( A x. B ) + ( A + B ) ) + 1 ) )
Theorem	comraddd 8200	Commute RHS addition, in deduction form. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> A = ( B + C ) )   =>    |- ( ph -> A = ( C + B ) )