From d2cd7e112d43d56e2b95655af85e430a704ef473 Mon Sep 17 00:00:00 2001
From: expln <47696142+expln@users.noreply.github.com>
Date: Mon, 22 Jan 2024 10:11:08 +0100
Subject: [PATCH] Delete and add theorems in set-mbox-ii. (#3785)

* Delete and add theorems in set-mbox-ii.

* Specify N must be even in anpnaneq0d.

* Specify N must be odd in anpnaneq0d.

* Rename anpnaneq0d to negexpidd.

* Rename and change signature of rexlimdvv3d.

---------

Co-authored-by: igorocky <123@gmail.com>
---
 set.mm | 62 +++++++++++++++++++++++++++++++---------------------------
 1 file changed, 33 insertions(+), 29 deletions(-)

diff --git a/set.mm b/set.mm
index 6c107f9113..26103e0c0f 100644
--- a/set.mm
+++ b/set.mm
@@ -630918,37 +630918,41 @@ standardize vectors to a length (norm) of one, but such definitions require
   $}
 
   ${
-    cu3addi.1 $e |- A e. CC $.
-    cu3addi.2 $e |- B e. CC $.
-    cu3addi.3 $e |- C e. CC $.
-    $( Cube of sum of three numbers.  (Contributed by Igor Ieskov,
-       14-Dec-2023.) $)
-    cu3addi $p |- ( ( ( A + B ) + C ) ^ 3 ) =
-    ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) )
-    + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) )
-    + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) )
-    + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) )
-    + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) )
-    + ( ( ( 3 x. ( A x. ( C ^ 2 ) ) )
-    + ( 3 x. ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) )
-    $=
-      ( caddc co c3 cexp c2 cmul wceq wtru cc wcel a1i cu3addd mptru ) ABGZHCTH
-      IZJZHAUAUBHUAAKZUBHZBLZHUEHTHUAABUCUBHZUEHUEHBUAUBHTHTHUAUDCUEHUEHUAUCUEH
-      ABUEHUEHCUEHTHUAUFCUEHUEHTHTHUAACUCUBHZUEHUEHUABUGUEHUEHTHCUAUBHTHTHMNZAB
-      CAOZPUHDQBUIPUHEQCUIPUHFQRS $.
+    sqnegd.1 $e |- ( ph -> A e. CC ) $.
+    $( The square of the negative of a number.  (Contributed by Igor Ieskov,
+       21-Jan-2024.) $)
+    sqnegd $p |- ( ph -> ( -u A ^ 2 ) = ( A ^ 2 ) ) $=
+      ( cc wcel cneg c2 cexp co wceq sqneg syl ) ABDEBFGZHZIBMNIJCBKL $.
+  $}
+
+  ${
+    negexpidd.1 $e |- ( ph -> A e. RR ) $.
+    negexpidd.2 $e |- ( ph -> N e. NN0 ) $.
+    negexpidd.3 $e |- ( ph -> -. 2 || N ) $.
+    $( The sum of a real number to the power of N and the negative of the
+       number to the power of N equals zero if N is a nonnegative odd integer.
+       (Contributed by Igor Ieskov, 21-Jan-2024.) $)
+    negexpidd $p |- ( ph -> ( ( A ^ N ) + ( -u A ^ N ) ) = 0 ) $=
+      ( cexp co cneg caddc cc0 wceq recnd mulm1d oveq1d wcel wi a1i mpd eqtr4d
+      reexpcld negidd c1 cmul eqcomd cz c2 cdvds wbr wn wa jctird m1expo eqtr2d
+      cn0 nn0z cc neg1cn mulexpd oveq2d eqeq1d mpbird ) ABCGZHZBIZCVCHZJZHZKZLV
+      DVDIZVGHZVILAVDAVDABCDEUAMZUBAVHVKVIAVFVJVDVGAVFUCIZBUDZHZCVCHZVJAVEVOCVC
+      AVOVEABABDMZNUEOAVJVMCVCHZVDVNHZVPAVSVMVDVNHVJAVRVMVDVNACUFPZUGCUHUIUJZUK
+      ZVRVMLZACUOPZWBEAWDVTWAWDVTQACUPRFULSWBWCQACUMRSOAVDVLNUNAVMBCVMUQPAURRVQ
+      EUSTTUTVAVB $.
+  $}
+
+  ${
+    $d B z $.  $d A y z $.  $d ph x y z $.  $d ch x y z $.
+    rexlimdv3d.1 $e |- ( ph ->
+      ( ( x e. A /\ y e. B /\ z e. C ) -> ( ps -> ch ) ) ) $.
+    $( An extended version of ~ rexlimdvv to include three set variables.
+       (Contributed by Igor Ieskov, 21-Jan-2024.) $)
+    rexlimdv3d $p |- ( ph -> ( E. x e. A E. y e. B E. z e. C ps -> ch ) ) $=
+      ( wrex cv wcel wa wi 3expd imp4d expdimp rexlimdvv rexlimdva ) ABFIKEHKCD
+      GADLGMZNBCEFHIAUAELHMZFLIMZNBCOZAUAUBUCUDAUAUBUCUDJPQRST $.
   $}
 
-  $( Cube of sum of three numbers.  (Contributed by Igor Ieskov,
-     14-Dec-2023.) $)
-  cu3add $p |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A + B ) + C ) ^ 3 )
-        = ( ( ( ( ( A ^ 3 ) + ( 3 x. ( ( A ^ 2 ) x. B ) ) )
-        + ( ( 3 x. ( A x. ( B ^ 2 ) ) ) + ( B ^ 3 ) ) )
-        + ( ( ( 3 x. ( ( A ^ 2 ) x. C ) )
-        + ( ( ( 3 x. 2 ) x. ( A x. B ) ) x. C ) )
-        + ( 3 x. ( ( B ^ 2 ) x. C ) ) ) ) + ( ( ( 3 x. ( A x. ( C ^ 2 ) ) )
-        + ( 3 x. ( B x. ( C ^ 2 ) ) ) ) + ( C ^ 3 ) ) ) ) $=
-    ( cc wcel w3a simp1 simp2 simp3 cu3addd ) ADZEZBKEZCKEZFABCLMNGLMNHLMNIJ $.
-
 $( (End of Igor Ieskov's mathbox.) $)
 $( End $[ set-mbox-ii.mm $] $)