Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 4a9d622, also available here: set.mm (32MB) or set.mm.bz2 (compressed, 9MB).

The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 13-Jul-2018 .    Syndication: RSS feed (courtesy of Dan Getz).    Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.

Recent news items    (10-May-2018) George Szpiro, journalist and author of several books on popular mathematics such as Poincare's Prize and Numbers Rule, used a genetic algorithm to find shorter D-proofs of "*3.37" and "meredith" in our Shortest known proofs... file.

(19-Apr-2018) The EMetamath Eclipse plugin has undergone many improvements since its initial release as the change log indicates. Thierry uses it as his main proof assistant and writes, "I added support for mmj2's auto-transformations, which allows it to infer several steps when building proofs. This added a lot of comfort for writing proofs.... I can now switch back and forth between the proof assistant and editing the Metamath file.... I think no other proof assistant has this feature."

(11-Apr-2018) Benoît Jubin solved an open problem about the "Axiom of Twoness", showing that it is necessary for completeness. See item 14 on the "Open problems and miscellany" page.

(30-Mar-2018) Filip Cernatescu's Milpgame has been updated to version 0.6, which reduces the set.mm load time to about 40 seconds. A new how-to has also been added to its web page.

(25-Mar-2018) Giovanni Mascellani has announced mmpp, a new proof editing environment for the Metamath language.

(27-Feb-2018) Bill Hale has released an app for the Apple iPad and desktop computer that allows you to browse Metamath theorems and their proofs.

(17-Jan-2018) Dylan Houlihan has kindly provided a new mirror site. He has also provided an rsync server; type "rsync uk.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").

(15-Jan-2018) The metamath program, version 0.157, has been updated to implement the file inclusion conventions described in the 21-Dec-2017 entry of mmnotes.txt.

(11-Dec-2017) I added a paragraph, suggested by Gérard Lang, to the distinct variable description here.

(10-Dec-2017) Per FL's request, his mathbox will be removed from set.mm. If you wish to export any of his theorems, today's version (master commit 1024a3a) is the last one that will contain it.

(11-Nov-2017) Alan Sare updated his completeusersproof program.

(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript. He also wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.

(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)

(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.

(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.

(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.

(7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.

(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).

   Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 15-Jul-2018 at 12:38 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 1-Jan-2018 )
DateLabelDescription
Theorem
 
14-Jul-2018sbie 2150 Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Revised by Wolf Lammen, 14-Jul-2018.)
 |- 
 F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( [ y  /  x ] ph  <->  ps )
 
14-Jul-2018sbequi 2111 An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Jul-2018.)
 |-  ( x  =  y 
 ->  ( [ x  /  z ] ph  ->  [ y  /  z ] ph )
 )
 
14-Jul-20184syl 20 Inference chaining three syllogisms. The use of this theorem is marked "discouraged" because it causes the "minimize" command to have very long run times. However, feel free to override it to use directly or in small "minimize" runs. (Contributed by BJ, 14-Jul-2018.) (New usage is discouraged.)
 |-  ( ph  ->  ps )   &    |-  ( ps  ->  ch )   &    |-  ( ch  ->  th )   &    |-  ( th  ->  ta )   =>    |-  ( ph  ->  ta )
 
13-Jul-2018mblfinlem4 26247 Backward direction of ismblfin 26248. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
 |-  (
 ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  A  e.  dom  vol )  ->  ( vol * `
  A )  = 
 sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  A  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  ) )
 
13-Jul-2018mblfinlem3 26246 The difference between two sets measurable by the criterion in ismblfin 26248 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
 |-  (
 ( ( A  C_  RR  /\  ( vol * `  A )  e.  RR )  /\  ( B  C_  RR  /\  ( vol * `  B )  e.  RR )  /\  ( ( vol
 * `  A )  =  sup ( { y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  A  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  )  /\  ( vol * `  B )  =  sup ( {
 y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  B  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  ) ) )  ->  sup ( {
 y  |  E. b  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( b 
 C_  ( A  \  B )  /\  y  =  ( vol `  b
 ) ) } ,  RR ,  <  )  =  ( vol * `  ( A  \  B ) ) )
 
13-Jul-2018mblfinlem2 26245 Lemma for ismblfin 26248, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
 |-  (
 ( A  e.  ( topGen `
  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol * `  A ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
 C_  A  /\  M  <  ( vol * `  s ) ) )
 
13-Jul-2018mblfinlem1 26244 Lemma for ismblfin 26248, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in  A. (Contributed by Brendan Leahy, 13-Jul-2018.)
 |-  (
 ( A  e.  ( topGen `
  ran  (,) )  /\  A  =/=  (/) )  ->  E. f  f : NN -1-1-onto-> { a  e.  {
 b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  ( 2 ^ y
 ) ) ,  (
 ( x  +  1 )  /  ( 2 ^ y ) )
 >. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x 
 /  ( 2 ^
 y ) ) ,  ( ( x  +  1 )  /  (
 2 ^ y ) ) >. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c
 )  ->  a  =  c ) } )
 
13-Jul-2018opnmbllem0 26243 Lemma for ismblfin 26248; could also be used to shorten proof of opnmbllem 19494. (Contributed by Brendan Leahy, 13-Jul-2018.)
 |-  ( A  e.  ( topGen `  ran  (,) )  ->  U. ( [,] " { z  e. 
 ran  ( x  e. 
 ZZ ,  y  e. 
 NN0  |->  <. ( x  /  ( 2 ^ y
 ) ) ,  (
 ( x  +  1 )  /  ( 2 ^ y ) )
 >. )  |  ( [,] `  z )  C_  A } )  =  A )
 
11-Jul-2018areacirc 26298 The area of a circle of radius  R is  pi  x.  R ^ 2. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
 |-  S  =  { <. x ,  y >.  |  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
 ( x ^ 2
 )  +  ( y ^ 2 ) ) 
 <_  ( R ^ 2
 ) ) }   =>    |-  ( ( R  e.  RR  /\  0  <_  R )  ->  (area `  S )  =  ( pi  x.  ( R ^ 2 ) ) )
 
11-Jul-2018areacirclem5 26297 Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
 |-  S  =  { <. x ,  y >.  |  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
 ( x ^ 2
 )  +  ( y ^ 2 ) ) 
 <_  ( R ^ 2
 ) ) }   =>    |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e. 
 RR )  ->  ( S " { t }
 )  =  if (
 ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2
 ) ) ) [,] ( sqr `  (
 ( R ^ 2
 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )
 
11-Jul-2018areacirclem4 26296 Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
 |-  ( R  e.  RR+  ->  (
 t  e.  ( -u R [,] R )  |->  ( ( R ^ 2
 )  x.  ( (arcsin `  ( t  /  R ) )  +  (
 ( t  /  R )  x.  ( sqr `  (
 1  -  ( ( t  /  R ) ^ 2 ) ) ) ) ) ) )  e.  ( (
 -u R [,] R ) -cn-> CC ) )
 
11-Jul-2018areacirclem3 26295 Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
 |-  (
 ( R  e.  RR  /\  0  <_  R )  ->  ( t  e.  ( -u R [,] R ) 
 |->  ( 2  x.  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2
 ) ) ) ) )  e.  L ^1 )
 
11-Jul-2018areacirclem2 26294 Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
 |-  (
 ( R  e.  RR  /\  0  <_  R )  ->  ( t  e.  ( -u R [,] R ) 
 |->  ( sqr `  (
 ( R ^ 2
 )  -  ( t ^ 2 ) ) ) )  e.  (
 ( -u R [,] R ) -cn-> CC ) )
 
11-Jul-2018areacirclem1 26293 Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.)
 |-  ( R  e.  RR+  ->  ( RR  _D  ( t  e.  ( -u R (,) R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  (
 t  /  R )
 )  +  ( ( t  /  R )  x.  ( sqr `  (
 1  -  ( ( t  /  R ) ^ 2 ) ) ) ) ) ) ) )  =  ( t  e.  ( -u R (,) R )  |->  ( 2  x.  ( sqr `  ( ( R ^
 2 )  -  (
 t ^ 2 ) ) ) ) ) )
 
10-Jul-2018cusgraisrusgra 28378 A complete undirected simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.)
 |-  (
 ( V ComplUSGrph  E  /\  V  e.  Fin  /\  V  =/=  (/) )  ->  <. V ,  E >. RegUSGrph  ( ( # `  V )  -  1 ) )
 
10-Jul-20180vgrargra 28377 A graph with no vertices is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.)
 |-  ( E  e.  V  ->  A. k  e.  NN0  <. (/) ,  E >. RegGrph 
 k )
 
9-Jul-2018vdcusgra 28365 In a finite complete undirected simple graph with n vertices every vertex has degree (n-1). (Contributed by Alexander van der Vekens, 9-Jul-2018.)
 |-  (
 ( V ComplUSGrph  E  /\  V  e.  Fin )  ->  A. v  e.  V  ( ( V VDeg 
 E ) `  v
 )  =  ( ( # `  V )  -  1 ) )
 
9-Jul-2018usgrauvtxvd 28364 In a finite complete undirected simple graph with n vertices every vertex has degree (n-1). (Contributed by Alexander van der Vekens, 9-Jul-2018.)
 |-  (
 ( V USGrph  E  /\  V  e.  Fin )  ->  ( K  e.  ( V UnivVertex  E )  ->  (
 ( V VDeg  E ) `  K )  =  ( ( # `  V )  -  1 ) ) )
 
9-Jul-2018vdusgravaledg 28363 The value of the vertex degree function for simple undirected graphs in terms of edges. (Contributed by Alexander van der Vekens, 9-Jul-2018.)
 |-  (
 ( V USGrph  E  /\  U  e.  V )  ->  ( ( V VDeg  E ) `  U )  =  ( # `  { x  e.  V  |  { U ,  x }  e.  ran  E } ) )
 
8-Jul-20180egra0rgra 28376 A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
 |-  A. v <. v ,  (/) >. RegGrph  0
 
8-Jul-2018rusisusgra 28375 Any k-regular undirected simple graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
 |-  ( <. V ,  E >. RegUSGrph  K  ->  V USGrph  E )
 
8-Jul-2018rusgrargra 28374 A k-regular undirected simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
 |-  ( <. V ,  E >. RegUSGrph  K  -> 
 <. V ,  E >. RegGrph  K )
 
8-Jul-2018rusgraprop 28373 The properties of a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
 |-  ( <. V ,  E >. RegUSGrph  K  ->  ( V USGrph  E  /\  K  e.  NN0  /\  A. p  e.  V  (
 ( V VDeg  E ) `  p )  =  K ) )
 
8-Jul-2018rgraprop 28372 The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
 |-  ( <. V ,  E >. RegGrph  K  ->  ( K  e.  NN0  /\ 
 A. p  e.  V  ( ( V VDeg  E ) `  p )  =  K ) )
 
8-Jul-2018oprabv 28086 If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
 |-  ( <. X ,  Y >. {
 <. <. x ,  y >. ,  z >.  |  ph } Z  ->  ( X  e.  _V  /\  Y  e.  _V 
 /\  Z  e.  _V ) )
 
8-Jul-2018opelopabgf 28072 The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 4474 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Alexander van der Vekens, 8-Jul-2018.)
 |-  F/ x ps   &    |-  F/ y ch   &    |-  ( x  =  A  ->  ( ph  <->  ps ) )   &    |-  (
 y  =  B  ->  ( ps  <->  ch ) )   =>    |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( <. A ,  B >.  e. 
 { <. x ,  y >.  |  ph }  <->  ch ) )
 
7-Jul-2018isrusgra 28371 The property of being a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y  /\  K  e.  Z )  ->  ( <. V ,  E >. RegUSGrph  K 
 <->  ( V USGrph  E  /\  K  e.  NN0  /\  A. p  e.  V  (
 ( V VDeg  E ) `  p )  =  K ) ) )
 
7-Jul-2018isrgra 28370 The property of being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y  /\  K  e.  Z )  ->  ( <. V ,  E >. RegGrph  K 
 <->  ( K  e.  NN0  /\ 
 A. p  e.  V  ( ( V VDeg  E ) `  p )  =  K ) ) )
 
7-Jul-2018breqn0 28070 If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
 |-  ( A R B  ->  R  =/= 
 (/) )
 
7-Jul-2018nelir 2699 Inference associated with df-nel 2603. (Contributed by BJ, 7-Jul-2018.)
 |- 
 -.  A  e.  B   =>    |-  A  e/  B
 
7-Jul-2018neli 2698 Inference associated with df-nel 2603. (Contributed by BJ, 7-Jul-2018.)
 |-  A  e/  B   =>    |-  -.  A  e.  B
 
7-Jul-2018nesymir 2643 Inference associated with nesym 2641. (Contributed by BJ, 7-Jul-2018.)
 |- 
 -.  A  =  B   =>    |-  B  =/=  A
 
7-Jul-2018nesymi 2642 Inference associated with nesym 2641. (Contributed by BJ, 7-Jul-2018.)
 |-  A  =/=  B   =>    |-  -.  B  =  A
 
7-Jul-2018nesym 2641 Characterization of inequality in terms of reversed equality (see bicom 193). (Contributed by BJ, 7-Jul-2018.)
 |-  ( A  =/=  B  <->  -.  B  =  A )
 
7-Jul-2018neir 2605 Inference associated with df-ne 2602. (Contributed by BJ, 7-Jul-2018.)
 |- 
 -.  A  =  B   =>    |-  A  =/=  B
 
7-Jul-2018neii 2604 Inference associated with df-ne 2602. (Contributed by BJ, 7-Jul-2018.)
 |-  A  =/=  B   =>    |-  -.  A  =  B
 
6-Jul-2018df-rusgra 28369 Define the set of k-regular undirected simple graphs. (Contributed by Alexander van der Vekens, 6-Jul-2018.)
 |- RegUSGrph  =  { <.
 <. v ,  e >. ,  k >.  |  (
 v USGrph  e  /\  <. v ,  e >. RegGrph  k ) }
 
6-Jul-2018df-rgra 28368 Define the set of k-regular "graphs". (Contributed by Alexander van der Vekens, 6-Jul-2018.)
 |- RegGrph  =  { <.
 <. v ,  e >. ,  k >.  |  (
 k  e.  NN0  /\  A. p  e.  v  (
 ( v VDeg  e ) `
  p )  =  k ) }
 
5-Jul-2018swdeq 28197 If two words have the same prefix, their symbols are identical with this prefix. (Contributed by Alexander van der Vekens, 5-Jul-2018.)
 |-  (
 ( ( U  e. Word  V 
 /\  W  e. Word  V )  /\  ( N  e.  NN0  /\  N  <_  ( # `  U )  /\  N  <_  ( # `
  W ) ) )  ->  ( ( U substr 
 <. 0 ,  N >. )  =  ( W substr  <. 0 ,  N >. )  ->  A. i  e.  ( 0..^ N ) ( U `  i
 )  =  ( W `
  i ) ) )
 
3-Jul-2018usg2wlkeq 28305 Conditions for which two walks within the same undirected simple graph are the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 3-Jul-2018.)
 |-  (
 ( V USGrph  E  /\  ( A  e.  ( V Walks  E )  /\  B  e.  ( V Walks  E ) )  /\  N  =  ( # `  ( 1st `  A ) ) ) 
 ->  ( A  =  B  <->  ( N  =  ( # `  ( 1st `  B ) )  /\  A. y  e.  ( 0 ... N ) ( ( 2nd `  A ) `  y
 )  =  ( ( 2nd `  B ) `  y ) ) ) )
 
1-Jul-20182wlkeq 28304 Conditions for which two walks (within the same graph) are the same. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
 |-  (
 ( A  e.  ( V Walks  E )  /\  B  e.  ( V Walks  E ) 
 /\  N  =  ( # `  ( 1st `  A ) ) )  ->  ( A  =  B  <->  ( N  =  ( # `  ( 1st `  B ) )  /\  A. x  e.  ( 0..^ N ) ( ( 1st `  A ) `  x )  =  ( ( 1st `  B ) `  x )  /\  A. y  e.  ( 0
 ... N ) ( ( 2nd `  A ) `  y )  =  ( ( 2nd `  B ) `  y ) ) ) )
 
1-Jul-2018wlklenfislenpm1 28300 The number of edges of a walk (in an undirected graph) is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
 |-  ( F ( V Walks  E ) P  ->  ( # `  F )  =  ( ( # `  P )  -  1 ) )
 
1-Jul-20182wrdeq 28176 Two words are equal if and only if they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
 |-  (
 ( W  e. Word  V  /\  S  e. Word  V )  ->  ( W  =  S  <->  ( ( # `  W )  =  ( # `  S )  /\  A. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =  ( S `  i ) ) ) )
 
1-Jul-20182ffzoeq 28141 Two functions over a zero-based half-open integer range are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
 |-  (
 ( ( M  e.  NN0  /\  N  e.  NN0 )  /\  ( F : ( 0..^ M ) --> X  /\  P : ( 0..^ N )
 --> Y ) )  ->  ( F  =  P  <->  ( M  =  N  /\  A. i  e.  ( 0..^ M ) ( F `
  i )  =  ( P `  i
 ) ) ) )
 
1-Jul-2018fzoopth 28140 A half-open range of integers can represent an ordered pair, analogous to fzopth 11090. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
 |-  (
 ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <  N )  ->  ( ( M..^ N )  =  ( J..^ K )  <->  ( M  =  J  /\  N  =  K ) ) )
 
1-Jul-2018el2fzo 28139 The lower limit of a half-open range of integers which is equal to a non-empty empty half-open range of integers is element of the half-open range. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
 |-  (
 ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <  N )  ->  ( ( M..^ N )  =  ( J..^ K )  ->  J  e.  ( J..^ K ) ) )
 
30-Jun-2018wlkop 28298 A walk (in an undirected simple graph) is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.)
 |-  ( W  e.  ( V Walks  E )  ->  W  =  <. ( 1st `  W ) ,  ( 2nd `  W ) >. )
 
30-Jun-2018relwlk 28297 The walks (in an undirected simple graph) are (ordered) pairs. (Contributed by Alexander van der Vekens, 30-Jun-2018.)
 |-  Rel  ( V Walks  E )
 
30-Jun-20182ffzeq 28122 Two functions over a zero-based finite interval of integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 30-Jun-2018.)
 |-  (
 ( M  e.  NN0  /\  F : ( 0
 ... M ) --> X  /\  P : ( 0 ...
 N ) --> Y ) 
 ->  ( F  =  P  <->  ( M  =  N  /\  A. i  e.  ( 0
 ... M ) ( F `  i )  =  ( P `  i ) ) ) )
 
30-Jun-2018f0bi 28076 A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018.)
 |-  ( F : (/) --> X  <->  F  =  (/) )
 
30-Jun-2018sbceq1dd 3168 Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)
 |-  ( ph  ->  A  =  B )   &    |-  ( ph  ->  [. A  /  x ]. ps )   =>    |-  ( ph  ->  [. B  /  x ]. ps )
 
30-Jun-2018sbceq1d 3167 Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  ( [. A  /  x ].
 ps 
 <-> 
 [. B  /  x ].
 ps ) )
 
29-Jun-2018wlklenpislenfp1 28299 The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.)
 |-  ( F ( V Walks  E ) P  ->  ( # `  P )  =  ( ( # `  F )  +  1 )
 )
 
28-Jun-2018lstccats1fst 28264 The last symbol of a non-empty word concatenated with its first symbol is the first symbol. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
 |-  (
 ( P  e. Word  V  /\  1  <_  ( # `  P ) )  ->  ( LastS  `  ( P concat  <" ( P `  0 ) "> ) )  =  ( ( P concat  <" ( P `  0 ) "> ) `  0 ) )
 
28-Jun-2018ccats1swrdid 28192 A non-empty word is the prefix of the word concatenated with its first symbol. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
 |-  (
 ( P  e. Word  V  /\  1  <_  ( # `  P ) )  ->  P  =  ( ( P concat  <" ( P `
  0 ) "> ) substr  <. 0 ,  ( # `
  P ) >. ) )
 
28-Jun-2018wrdlenccats1lenm1 28181 The length of a non-empty word is the length of the word concatenated with its first symbol minus 1. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
 |-  (
 ( P  e. Word  V  /\  1  <_  ( # `  P ) )  ->  ( # `  P )  =  ( ( # `  ( P concat  <" ( P `  0 ) "> ) )  -  1
 ) )
 
28-Jun-2018wrdsymb1 28175 The first symbol within a non-empty word over a set belongs to this set. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
 |-  (
 ( P  e. Word  V  /\  1  <_  ( # `  P ) )  ->  ( P `  0 )  e.  V )
 
28-Jun-2018wrdsymb 28174 A symbol within a word over a set belongs to this set. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
 |-  (
 ( P  e. Word  V  /\  I  e.  (
 0..^ ( # `  P ) ) )  ->  ( P `  I )  e.  V )
 
25-Jun-2018fz0hash 28169 The value of the size function on a finite 0-based sequence. (Contributed by Alexander van der Vekens, 25-Jun-2018.)
 |-  (
 ( N  e.  NN0  /\  F  Fn  ( 0
 ... N ) ) 
 ->  ( # `  F )  =  ( N  +  1 ) )
 
24-Jun-2018swrd0fvls 28265 The last symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
 |-  (
 ( S  e. Word  A  /\  L  e.  ( 1
 ... ( # `  S ) ) )  ->  ( LastS  `  ( S substr  <. 0 ,  L >. ) )  =  ( S `  ( L  -  1 ) ) )
 
24-Jun-20183an4anass 28050 Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
 |-  (
 ( ( ph  /\  ps  /\ 
 ch )  /\  th ) 
 <->  ( ( ph  /\  ps )  /\  ( ch  /\  th ) ) )
 
24-Jun-2018sbcom 2165 A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 24-Jun-2018.)
 |-  ( [ y  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ y  /  z ] ph )
 
24-Jun-2018sbied 2151 Conversion of implicit substitution to explicit substitution (deduction version of sbie 2150). (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.)
 |- 
 F/ x ph   &    |-  ( ph  ->  F/ x ch )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( ph  ->  ( [ y  /  x ] ps  <->  ch ) )
 
23-Jun-2018wlkcompim 28303 Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.)
 |-  F  =  ( 1st `  W )   &    |-  P  =  ( 2nd `  W )   =>    |-  ( W  e.  ( V Walks  E )  ->  ( F  e. Word  dom  E  /\  P : ( 0 ... ( # `  F ) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F ) ) ( E `
  ( F `  k ) )  =  { ( P `  k ) ,  ( P `  ( k  +  1 ) ) }
 ) )
 
23-Jun-2018wlkcomp 28302 A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018.)
 |-  F  =  ( 1st `  W )   &    |-  P  =  ( 2nd `  W )   =>    |-  ( ( V  e.  X  /\  E  e.  Y  /\  W  e.  ( S  X.  T ) ) 
 ->  ( W  e.  ( V Walks  E )  <->  ( F  e. Word  dom 
 E  /\  P :
 ( 0 ... ( # `
  F ) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F ) ) ( E `  ( F `
  k ) )  =  { ( P `
  k ) ,  ( P `  (
 k  +  1 ) ) } ) ) )
 
23-Jun-2018iswlkg 28301 Generalisation of iswlk 21528: Properties of a pair of functions to be a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( F ( V Walks  E ) P  <->  ( F  e. Word  dom 
 E  /\  P :
 ( 0 ... ( # `
  F ) ) --> V  /\  A. k  e.  ( 0..^ ( # `  F ) ) ( E `  ( F `
  k ) )  =  { ( P `
  k ) ,  ( P `  (
 k  +  1 ) ) } ) ) )
 
23-Jun-2018wlkelwrd 28296 The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.)
 |-  ( W  e.  ( V Walks  E )  ->  ( ( 1st `  W )  e. Word  dom  E  /\  ( 2nd `  W ) : ( 0 ... ( # `  ( 1st `  W ) ) ) --> V ) )
 
23-Jun-2018elopaelxp 28071 Membership in an ordered pair class builder implies membership in a cross product. (Contributed by Alexander van der Vekens, 23-Jun-2018.)
 |-  ( A  e.  { <. x ,  y >.  |  ps }  ->  A  e.  ( _V 
 X.  _V ) )
 
19-Jun-2018ftc2nc 26290 Choice-free proof of ftc2 19929. (Contributed by Brendan Leahy, 19-Jun-2018.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A 
 <_  B )   &    |-  ( ph  ->  ( RR  _D  F )  e.  ( ( A (,) B ) -cn-> CC ) )   &    |-  ( ph  ->  ( RR  _D  F )  e.  L ^1 )   &    |-  ( ph  ->  F  e.  (
 ( A [,] B ) -cn-> CC ) )   =>    |-  ( ph  ->  S. ( A (,) B ) ( ( RR 
 _D  F ) `  t )  _d t  =  ( ( F `  B )  -  ( F `  A ) ) )
 
19-Jun-2018ftc1anclem2 26282 Lemma for ftc1anc 26289- restriction of an integrable function to the absolute value of its real or imaginary part. (Contributed by Brendan Leahy, 19-Jun-2018.)
 |-  (
 ( F : A --> CC  /\  F  e.  L ^1  /\  Z  e.  {
 0 ,  1 } )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  A ,  ( abs `  ( Re `  ( ( F `
  t )  /  ( _i ^ Z ) ) ) ) ,  0 ) ) )  e.  RR )
 
19-Jun-2018itgabsnc 26275 Choice-free analogue of itgabs 19727. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.)
 |-  (
 ( ph  /\  x  e.  A )  ->  B  e.  V )   &    |-  ( ph  ->  ( x  e.  A  |->  B )  e.  L ^1 )   &    |-  ( ph  ->  ( x  e.  A  |->  ( abs `  B )
 )  e. MblFn )   &    |-  ( ph  ->  ( y  e.  A  |->  ( ( * `  S. A B  _d x )  x.  [_ y  /  x ]_ B ) )  e. MblFn
 )   =>    |-  ( ph  ->  ( abs `  S. A B  _d x )  <_  S. A ( abs `  B )  _d x )
 
18-Jun-2018wrdlenge2n0 28177 A word with length at least 2 is not empty. (Contributed by Alexander van der Vekens, 18-Jun-2018.)
 |-  (
 ( P  e. Word  V  /\  2  <_  ( # `  P ) )  ->  P  =/=  (/) )
 
18-Jun-2018ftc1anclem1 26281 Lemma for ftc1anc 26289- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 19551, but this proof avoids ax-cc 8316. (Contributed by Brendan Leahy, 18-Jun-2018.)
 |-  (
 ( F : A --> RR  /\  F  e. MblFn )  ->  ( abs  o.  F )  e. MblFn )
 
17-Jun-2018uzletr 28104 An upper integer is also an upper integer with a smaller bound. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
 |-  (
 ( A  e.  ZZ  /\  A  <_  B )  ->  ( N  e.  ( ZZ>=
 `  B )  ->  N  e.  ( ZZ>= `  A ) ) )
 
17-Jun-2018ftc1anclem5 26285 Lemma for ftc1anc 26289, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( F `  t )  _d t
 )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  ( A (,) B )  C_  D )   &    |-  ( ph  ->  D 
 C_  RR )   &    |-  ( ph  ->  F  e.  L ^1 )   &    |-  ( ph  ->  F : D --> CC )   =>    |-  ( ( ph  /\  Y  e.  RR+ )  ->  E. f  e.  dom  S.1 ( S.2 `  (
 t  e.  RR  |->  ( abs `  ( ( Re `  if ( t  e.  D ,  ( F `  t ) ,  0 ) )  -  ( f `  t
 ) ) ) ) )  <  Y )
 
17-Jun-2018ftc1anclem4 26284 Lemma for ftc1anc 26289. (Contributed by Brendan Leahy, 17-Jun-2018.)
 |-  (
 ( F  e.  dom  S.1  /\  G  e.  L ^1 
 /\  G : RR --> RR )  ->  ( S.2 `  ( t  e.  RR  |->  ( abs `  ( ( G `  t )  -  ( F `  t ) ) ) ) )  e.  RR )
 
16-Jun-2018swrdtrcfvl 28266 The last symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
 |-  (
 ( S  e. Word  A  /\  2  <_  ( # `  S ) )  ->  ( LastS  `  ( S substr  <. 0 ,  ( ( # `  S )  -  1 ) >. ) )  =  ( S `
  ( ( # `  S )  -  2
 ) ) )
 
16-Jun-2018swrdtrcfv0 28196 The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
 |-  (
 ( S  e. Word  A  /\  2  <_  ( # `  S ) )  ->  ( ( S substr  <. 0 ,  ( ( # `  S )  -  1 ) >. ) `
  0 )  =  ( S `  0
 ) )
 
16-Jun-2018swrdtrcfv 28195 A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
 |-  (
 ( S  e. Word  A  /\  S  =/=  (/)  /\  X  e.  ( 0..^ ( ( # `  S )  -  1 ) ) ) 
 ->  ( ( S substr  <. 0 ,  ( ( # `  S )  -  1 ) >. ) `
  X )  =  ( S `  X ) )
 
16-Jun-2018swrd0fv0 28194 The first symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
 |-  (
 ( S  e. Word  A  /\  L  e.  ( 1
 ... ( # `  S ) ) )  ->  ( ( S substr  <. 0 ,  L >. ) `  0
 )  =  ( S `
  0 ) )
 
16-Jun-2018swrd0fv 28193 A symbol in an left-anchored subword, indexed using the subword's indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.)
 |-  (
 ( S  e. Word  A  /\  L  e.  ( 0
 ... ( # `  S ) )  /\  X  e.  ( 0..^ L ) ) 
 ->  ( ( S substr  <. 0 ,  L >. ) `  X )  =  ( S `  X ) )
 
16-Jun-2018wlimss 25581 The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.)
 |- WLim ( R ,  A )  C_  A
 
16-Jun-2018wsuclb 25580 A well-founded successor is a lower bound on points after  X. (Contributed by Scott Fenton, 16-Jun-2018.)
 |-  ( ph  ->  R  We  A )   &    |-  ( ph  ->  R Se  A )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  Y  e.  A )   &    |-  ( ph  ->  X R Y )   =>    |-  ( ph  ->  -.  Y Rwsuc ( R ,  A ,  X ) )
 
16-Jun-2018wsucex 25578 Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.)
 |-  ( ph  ->  R  Or  A )   =>    |-  ( ph  -> wsuc ( R ,  A ,  X )  e.  _V )
 
15-Jun-2018fzisfzounsn 28138 A finite interval of integers as union of a half-open range of integers and a singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
 |-  ( B  e.  ( ZZ>= `  A )  ->  ( A
 ... B )  =  ( ( A..^ B )  u.  { B }
 ) )
 
15-Jun-2018fzofzim 28137 If a non-negative integer in a finite interval of integers is not the upper bound of the interval, it is contained in the corresponding half-open range of integers. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
 |-  (
 ( K  =/=  M  /\  K  e.  ( 0
 ... M ) ) 
 ->  K  e.  ( 0..^ M ) )
 
15-Jun-2018wsuccl 25579 If  X is a set with an  R successor in  A, then its well-founded successor is a member of  A. (Contributed by Scott Fenton, 15-Jun-2018.)
 |-  ( ph  ->  R  We  A )   &    |-  ( ph  ->  R Se  A )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  E. y  e.  A  X R y )   =>    |-  ( ph  -> wsuc ( R ,  A ,  X )  e.  A )
 
15-Jun-2018wsuclem 25577 Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.)
 |-  ( ph  ->  R  We  A )   &    |-  ( ph  ->  R Se  A )   &    |-  ( ph  ->  X  e.  V )   &    |-  ( ph  ->  E. w  e.  A  X R w )   =>    |-  ( ph  ->  E. x  e.  A  (
 A. y  e.  Pred  ( `' R ,  A ,  X )  -.  x `' R y  /\  A. y  e.  A  (
 y `' R x 
 ->  E. z  e.  Pred  ( `' R ,  A ,  X ) y `' R z ) ) )
 
15-Jun-2018elwlim 25575 Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
 |-  ( X  e. WLim ( R ,  A )  <->  ( X  e.  A  /\  X  =/=  sup ( A ,  A ,  `' R )  /\  X  =  sup ( Pred ( R ,  A ,  X ) ,  A ,  R ) ) )
 
15-Jun-2018nfwlim 25574 Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
 |-  F/_ x R   &    |-  F/_ x A   =>    |-  F/_ xWLim ( R ,  A )
 
15-Jun-2018wlimeq2 25573 Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
 |-  ( A  =  B  -> WLim ( R ,  A )  = WLim ( R ,  B ) )
 
15-Jun-2018wlimeq1 25572 Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
 |-  ( R  =  S  -> WLim ( R ,  A )  = WLim ( S ,  A ) )
 
15-Jun-2018wlimeq12 25571 Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.)
 |-  (
 ( R  =  S  /\  A  =  B ) 
 -> WLim ( R ,  A )  = WLim ( S ,  B ) )
 
15-Jun-2018df-wlim 25565 Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.)
 |- WLim ( R ,  A )  =  { x  e.  A  |  ( x  =/=  sup ( A ,  A ,  `' R )  /\  x  =  sup ( Pred ( R ,  A ,  x ) ,  A ,  R ) ) }
 
13-Jun-2018sineq0ALT 29050 A complex number whose sine is zero is an integer multiple of  pi. The Virtual Deduction form of the proof is http://www.virtualdeduction.com/sineq0altvd.html. The Metamath form of the proof is sineq0ALT 29050. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 20430. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of http://www.virtualdeduction.com/sineq0altro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.)
 |-  ( A  e.  CC  ->  ( ( sin `  A )  =  0  <->  ( A  /  pi )  e.  ZZ ) )
 
13-Jun-2018not12an2impnot1 28660 If a double conjunction is false and the second conjunct is true, then the first conjunct is false. http://www.virtualdeduction.com/not12an2impnot1vd.html is the Virtual Deduction proof verified by automatically transforming it into the Metamath proof of not12an2impnot1 28660 using completeusersproof, which is verified by the Metamath program. http://www.virtualdeduction.com/not12an2impnot1ro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.)
 |-  (
 ( -.  ( ph  /\ 
 ps )  /\  ps )  ->  -.  ph )
 
13-Jun-2018wzel 25576 The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  (
 ( R  We  A  /\  R Se  A  /\  A  =/= 
 (/) )  ->  sup ( A ,  A ,  `' R )  e.  A )
 
13-Jun-2018nfwsuc 25570 Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  F/_ x R   &    |-  F/_ x A   &    |-  F/_ x X   =>    |-  F/_ xwsuc ( R ,  A ,  X )
 
13-Jun-2018wsuceq3 25569 Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  ( X  =  Y  -> wsuc ( R ,  A ,  X )  = wsuc ( R ,  A ,  Y ) )
 
13-Jun-2018wsuceq2 25568 Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  ( A  =  B  -> wsuc ( R ,  A ,  X )  = wsuc ( R ,  B ,  X ) )
 
13-Jun-2018wsuceq1 25567 Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  ( R  =  S  -> wsuc ( R ,  A ,  X )  = wsuc ( S ,  A ,  X ) )
 
13-Jun-2018wsuceq123 25566 Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  (
 ( R  =  S  /\  A  =  B  /\  X  =  Y )  -> wsuc ( R ,  A ,  X )  = wsuc ( S ,  B ,  Y ) )
 
13-Jun-2018df-wsuc 25564 Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.)
 |- wsuc ( R ,  A ,  X )  =  sup ( Pred ( `' R ,  A ,  X ) ,  A ,  `' R )
 
13-Jun-2018dfpred3g 25451 An alternate definition of predecessor class when  X is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  ( X  e.  V  ->  Pred
 ( R ,  A ,  X )  =  {
 y  e.  A  |  y R X } )
 
13-Jun-2018dfpred3 25450 An alternate definition of predecessor class when  X is a set. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  X  e.  _V   =>    |- 
 Pred ( R ,  A ,  X )  =  { y  e.  A  |  y R X }
 
13-Jun-2018predeq123 25441 Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  (
 ( R  =  S  /\  A  =  B  /\  X  =  Y )  -> 
 Pred ( R ,  A ,  X )  =  Pred ( S ,  B ,  Y )
 )
 
13-Jun-2018socnv 25389 The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  ( R  Or  A  ->  `' R  Or  A )
 
13-Jun-2018pocnv 25388 The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  ( R  Po  A  ->  `' R  Po  A )
 
13-Jun-2018supeq3 7455 Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.)
 |-  ( R  =  S  ->  sup ( A ,  B ,  R )  =  sup ( A ,  B ,  S )
 )
 
12-Jun-2018suctr 4666 The sucessor of a transitive class is transitive. The proof of http://www.virtualdeduction.com/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctr 4666 using completeusersproof, which is verified by the Metamath program. The proof of http://www.virtualdeduction.com/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 11-Apr-2009.) See suctrALT 4665 for the original proof before this revision. (Revised by Alan Sare, 12-Jun-2018.) (Proof modification is discouraged.)
 |-  ( Tr  A  ->  Tr 
 suc  A )
 
9-Jun-2018fz0addcom 28114 The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.)
 |-  (
 ( A  e.  (
 0 ... N )  /\  B  e.  ( 0 ... N ) )  ->  ( A  +  B )  =  ( B  +  A ) )
 
9-Jun-2018nfwrecs 25534 Bound-variable hypothesis builder for the well-founded recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018.)
 |-  F/_ x R   &    |-  F/_ x A   &    |-  F/_ x F   =>    |-  F/_ xwrecs ( R ,  A ,  F )
 
9-Jun-2018nfpred 25445 Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.)
 |-  F/_ x R   &    |-  F/_ x A   &    |-  F/_ x X   =>    |-  F/_ x Pred ( R ,  A ,  X )
 
8-Jun-2018cshwsexa 28292 The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   &    |-  M  =  { w  e. Word  V  |  E. n  e.  ( 0..^ ( # `  W ) ) ( W CyclShift  n )  =  w }   =>    |-  M  e.  _V
 
8-Jun-2018cshwssize 28291 If a word has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word or 1. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   &    |-  M  =  { w  e. Word  V  |  E. n  e.  ( 0..^ ( # `  W ) ) ( W CyclShift  n )  =  w }   =>    |-  ( ph  ->  (
 ( # `  M )  =  ( # `  W )  \/  ( # `  M )  =  1 )
 )
 
8-Jun-2018cshwssizensame 28290 If a word (not consisting of identical symbols) has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   &    |-  M  =  { w  e. Word  V  |  E. n  e.  ( 0..^ ( # `  W ) ) ( W CyclShift  n )  =  w }   =>    |-  ( ph  ->  ( E. i  e.  (
 0..^ ( # `  W ) ) ( W `
  i )  =/=  ( W `  0
 )  ->  ( # `  M )  =  ( # `  W ) ) )
 
8-Jun-2018cshwssizesame 28289 If a word consists of identical symbols, the size of the set of (different!) words resulting by cyclically shifting the original word (not necessarily of length being a prime number) equals 1. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   &    |-  M  =  { w  e. Word  V  |  E. n  e.  ( 0..^ ( # `  W ) ) ( W CyclShift  n )  =  w }   =>    |-  ( ph  ->  ( A. i  e.  (
 0..^ ( # `  W ) ) ( W `
  i )  =  ( W `  0
 )  ->  ( # `  M )  =  1 )
 )
 
8-Jun-2018cshwsex 28288 The class of (different!) words resulting by cyclically shifting a given word (not necessarily of length being a prime number) is a set. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   &    |-  M  =  { w  e. Word  V  |  E. n  e.  ( 0..^ ( # `  W ) ) ( W CyclShift  n )  =  w }   =>    |-  ( ph  ->  M  e.  _V )
 
8-Jun-2018cshwsiun 28287 The set of (different!) words resulting by cyclically shifting a given word (not necessarily of length being a prime number) is an indexed union. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   &    |-  M  =  { w  e. Word  V  |  E. n  e.  ( 0..^ ( # `  W ) ) ( W CyclShift  n )  =  w }   =>    |-  ( ph  ->  M  =  U_ n  e.  (
 0..^ ( # `  W ) ) { ( W CyclShift  n ) } )
 
8-Jun-2018cshwsdisj 28286 The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   =>    |-  ( ( ph  /\  E. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =/=  ( W `  0 ) ) 
 -> Disj 
 n  e.  ( 0..^ ( # `  W ) ) { ( W CyclShift  n ) } )
 
8-Jun-2018cshwssizelem4 28285 If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   =>    |-  ( ( ph  /\  E. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =/=  ( W `  0 ) ) 
 ->  ( ( L  e.  ( 0..^ ( # `  W ) )  /\  K  e.  ( 0..^ ( # `  W ) )  /\  K  =/=  L )  ->  ( W CyclShift  L )  =/=  ( W CyclShift  K ) ) )
 
8-Jun-2018cshwssizelem4a 28284 If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   =>    |-  ( ( ph  /\  E. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =/=  ( W `  0 ) ) 
 ->  ( ( L  e.  ( 0..^ ( # `  W ) )  /\  K  e.  ( 0..^ ( # `  W ) )  /\  K  <  L )  ->  ( W CyclShift  L )  =/=  ( W CyclShift  K ) ) )
 
8-Jun-2018cshwssizelem3 28283 If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   =>    |-  ( ( ph  /\  E. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =/=  ( W `  0 )  /\  L  e.  ( 1..^ ( # `  W ) ) )  ->  ( W CyclShift  L )  =/=  W )
 
8-Jun-2018cshwssizelem2 28282 If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 or by as much positions as the length of the word or the word must be build of identical symbols. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   =>    |-  ( ( ph  /\  L  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( W CyclShift  L )  =  W )  ->  ( L  =  0  \/  L  =  ( # `  W )  \/  A. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =  ( W `  0 ) ) )
 
8-Jun-2018cshwssizelem1 28281 If cyclically shifting a word of length being a prime number by at least two positions (and not by as many positions as the length of the word) results in the word itself, the word is build of identical symbols. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   =>    |-  ( ( ph  /\  L  e.  ( 2..^ ( # `  W ) ) ) 
 ->  ( ( W CyclShift  L )  =  W  ->  A. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =  ( W `  0 ) ) )
 
8-Jun-2018cshwssizelem1a 28280 If cyclically shifting a word of length being a prime number by at least two positions (and not by as much positions as the length of the word) results in the word itself, the word is build of identical symbols, with the possible exception of the first one. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( ph  ->  ( W  e. Word  V 
 /\  ( # `  W )  e.  Prime ) )   =>    |-  ( ( ph  /\  L  e.  ( 2..^ ( # `  W ) ) ) 
 ->  ( ( W CyclShift  L )  =  W  ->  A. i  e.  ( 1..^ ( # `  W ) ) ( W `  i )  =  ( W `  0 ) ) )
 
8-Jun-2018cshwsame0 28279 If cyclically shifting a word consisting of identical symbols by different amounts of positions, the resulting words are identical. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  A. i  e.  (
 0..^ ( # `  W ) ) ( W `
  i )  =  ( W `  0
 ) )  ->  (
 ( L  e.  (
 0..^ ( # `  W ) )  /\  K  e.  ( 0..^ ( # `  W ) ) )  ->  ( W CyclShift  L )  =  ( W CyclShift  K )
 ) )
 
8-Jun-2018cshwsame 28278 Cyclically shifting a word consisting of identical symbols results in the word itself. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  A. i  e.  (
 0..^ ( # `  W ) ) ( W `
  i )  =  ( W `  0
 ) )  ->  ( L  e.  ( 0..^ ( # `  W ) )  ->  ( W CyclShift  L )  =  W ) )
 
8-Jun-20182cshwmod 28258 Cyclically shifting a word two times using  mod. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  W  =/=  (/) )  ->  ( ( M  e.  ( 0 ... ( # `
  W ) ) 
 /\  N  e.  (
 0 ... ( # `  W ) ) )  ->  ( ( W CyclShift  M ) CyclShift  N )  =  ( W CyclShift  ( ( M  +  N )  mod  ( # `  W ) ) ) ) )
 
8-Jun-20182txmodxeq0 28163 Two times a positive real number module the real number is zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( X  e.  RR+  ->  (
 ( 2  x.  X )  mod  X )  =  0 )
 
8-Jun-2018fz0addge0 28121 The sum of two integers in zero based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  (
 ( A  e.  (
 0 ... M )  /\  B  e.  ( 0 ... N ) )  -> 
 0  <_  ( A  +  B ) )
 
8-Jun-20182eluzge1 28103 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  2  e.  ( ZZ>= `  1 )
 
8-Jun-20182eluzge0 28102 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  2  e.  ( ZZ>= `  0 )
 
8-Jun-20181eluzge0 28101 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  1  e.  ( ZZ>= `  0 )
 
8-Jun-2018ltnltne 28095 Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  ( -.  B  <  A  /\  -.  B  =  A ) ) )
 
8-Jun-20182txmxeqx 28091 Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
 |-  ( X  e.  CC  ->  ( ( 2  x.  X )  -  X )  =  X )
 
8-Jun-2018wfrlem6 25544 Lemma for well-founded recursion. The definition generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018.)
 |-  F  = wrecs ( R ,  A ,  G )   =>    |- 
 Rel  F
 
7-Jun-2018cshw1v 28277 If cyclically shifting a (not empty) word by 1 position results in the word itself, the word is build of identical symbols. (Contributed by Alexander van der Vekens, 14-May-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  W  =/=  (/)  /\  ( W CyclShift  1 )  =  W )  ->  E. v  e.  V  A. i  e.  ( 0..^ ( # `  W ) ) ( W `
  i )  =  v )
 
7-Jun-2018cshw1 28276 If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by Alexander van der Vekens, 13-May-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  ( W CyclShift  1 )  =  W )  ->  A. i  e.  ( 0..^ ( # `  W ) ) ( W `  i )  =  ( W `  0 ) )
 
7-Jun-2018cshweqrep 28275 If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by Alexander van der Vekens, 13-May-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  L  e.  ( 0..^ ( # `  W ) ) )  ->  ( ( ( W CyclShift  L )  =  W  /\  I  e.  (
 0..^ ( # `  W ) ) )  ->  A. j  e.  NN0  ( W `  I )  =  ( W `  (
 ( I  +  (
 j  x.  L ) )  mod  ( # `  W ) ) ) ) )
 
7-Jun-2018cshwsym 28274 If cyclically shifting a word A by n positions results in word B, then cyclically shifting the word B by (N-n) positions results in word A. (Contributed by Alexander van der Vekens, 22-Apr-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) ) )  ->  ( ( W CyclShift  N )  =  B  ->  ( B CyclShift  ( ( # `  W )  -  N ) )  =  W ) )
 
7-Jun-2018cshweqdifid 28273 If cyclically shifting a word by two positions results in the same word, cyclically shifting the word by the difference of these two positions results in the original word itself. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) )  /\  M  e.  ( N ... ( # `  W ) ) ) 
 ->  ( ( W CyclShift  N )  =  ( W CyclShift  M ) 
 ->  ( W CyclShift  ( M  -  N ) )  =  W ) )
 
7-Jun-2018cshweqdif2s 28272 If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by Alexander van der Vekens, 22-Apr-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.)
 |-  (
 ( ( W  e. Word  V 
 /\  U  e. Word  V )  /\  ( N  e.  ( 0 ... ( # `
  W ) ) 
 /\  M  e.  ( N ... ( # `  U ) ) ) ) 
 ->  ( ( W CyclShift  N )  =  ( U CyclShift  M ) 
 ->  ( U CyclShift  ( M  -  N ) )  =  W ) )
 
7-Jun-2018wrecseq3 25537 Equality theorem for the well-founded recusive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
 |-  ( F  =  G  -> wrecs ( R ,  A ,  F )  = wrecs ( R ,  A ,  G ) )
 
7-Jun-2018wrecseq2 25536 Equality theorem for the well-founded recusive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
 |-  ( A  =  B  -> wrecs ( R ,  A ,  F )  = wrecs ( R ,  B ,  F ) )
 
7-Jun-2018wrecseq1 25535 Equality theorem for the well-founded recusive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
 |-  ( R  =  S  -> wrecs ( R ,  A ,  F )  = wrecs ( S ,  A ,  F ) )
 
7-Jun-2018wrecseq123 25533 General equality theorem for the well-founded recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.)
 |-  (
 ( R  =  S  /\  A  =  B  /\  F  =  G )  -> wrecs ( R ,  A ,  F )  = wrecs ( S ,  B ,  G ) )
 
7-Jun-2018df-wrecs 25532 Here we define the well-founded recusive function generator. This is similar to recs, but works with arbitrary well-founded relationships. (Contributed by Scott Fenton, 7-Jun-2018.) (New usage is discouraged.)
 |- wrecs ( R ,  A ,  F )  =  U. { f  |  E. x ( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x ) 
 /\  A. y  e.  x  ( f `  y
 )  =  ( F `
  ( f  |`  Pred
 ( R ,  A ,  y ) ) ) ) }
 
6-Jun-2018cshweqdif2 28271 If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 6-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  U  e. Word  V  /\  ( # `  W )  =  ( # `  U ) )  ->  ( ( N  e.  ( 0
 ... ( # `  W ) )  /\  M  e.  ( N ... ( # `  W ) )  /\  ( W CyclShift  N )  =  ( U CyclShift  M )
 )  ->  ( U CyclShift  ( M  -  N ) )  =  W ) )
 
6-Jun-20183cshw 28270 Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by Alexander van der Vekens, 6-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) )  /\  M  e.  ( 0 ... ( # `
  W ) ) )  ->  ( W CyclShift  N )  =  ( ( ( W CyclShift  M ) CyclShift  N ) CyclShift  ( ( # `  W )  -  M ) ) )
 
6-Jun-2018fz0fzdiffz0 28120 The difference of a nonnegative integer in a finite set of sequential integers and a member of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential integers. (Contributed by Alexander van der Vekens, 6-Jun-2018.)
 |-  (
 ( M  e.  (
 0 ... N )  /\  K  e.  ( M ... N ) )  ->  ( K  -  M )  e.  ( 0 ... N ) )
 
5-Jun-2018cshwleneq 28269 If the results of cyclically shifting two words are equal, the length of the two words was equal. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.)
 |-  (
 ( ( W  e. Word  V 
 /\  U  e. Word  V )  /\  ( N  e.  ( 0 ... ( # `
  W ) ) 
 /\  M  e.  (
 0 ... ( # `  U ) ) )  /\  ( W CyclShift  N )  =  ( U CyclShift  M )
 )  ->  ( # `  W )  =  ( # `  U ) )
 
5-Jun-20182cshwcom 28268 Cyclically shifting a word two times is commutative. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  ( N  e.  (
 0 ... ( # `  W ) )  /\  M  e.  ( 0 ... ( # `
  W ) ) ) )  ->  (
 ( W CyclShift  N ) CyclShift  M )  =  ( ( W CyclShift  M ) CyclShift  N ) )
 
5-Jun-2018lswrdcshw 28267 The last symbol of a word cyclically shifted by N positions is the symbol at index (N-1) of the original word. (Contributed by Alexander van der Vekens, 21-Mar-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 1..^ ( # `  W ) ) )  ->  ( LastS  `  ( W CyclShift  N ) )  =  ( W `
  ( N  -  1 ) ) )
 
5-Jun-20182cshwid 28259 Cyclically shifting a word two times resulting in the word itself. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) ) )  ->  ( ( W CyclShift  N ) CyclShift  ( ( # `  W )  -  N ) )  =  W )
 
4-Jun-20182cshw 28257 Cyclically shifting a word two times. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 4-Jun-2018.)
 |-  ( W  e. Word  V  ->  (
 ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) )  ->  ( ( W CyclShift  M ) CyclShift  N )  =  if ( ( M  +  N )  <_  ( # `  W ) ,  ( W CyclShift  ( M  +  N ) ) ,  ( W CyclShift  ( ( M  +  N )  -  ( # `  W ) ) ) ) ) )
 
4-Jun-20182cshw2 28256 Cyclically shifting a word two times (with "overflow"). (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 4-Jun-2018.)
 |-  ( W  e. Word  V  ->  (
 ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( # `  W )  <  ( M  +  N ) )  ->  ( ( W CyclShift  M ) CyclShift  N )  =  ( W CyclShift  ( ( M  +  N )  -  ( # `
  W ) ) ) ) )
 
4-Jun-20182cshw2lem3 28255 Lemma 3 for 2cshw2 28256. (Contributed by Alexander van der Vekens, 6-Apr-2018.) (Revised by Alexander van der Vekens, 4-Jun-2018.)
 |-  (
 ( W  e. Word  V  /\  ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( # `  W )  <  ( M  +  N ) ) ) 
 ->  ( ( W substr  <. ( ( M  +  N )  -  ( # `  W ) ) ,  M >. ) concat  ( ( W substr  <. M ,  ( # `  W ) >. ) concat  ( W substr 
 <. 0 ,  ( ( M  +  N )  -  ( # `  W ) ) >. ) ) )  =  ( W CyclShift  ( ( M  +  N )  -  ( # `
  W ) ) ) )
 
1-Jun-20182cshw2lem2 28254 Lemma 2 for 2cshw2 28256. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 1-Jun-2018.)
 |-  ( W  e. Word  V  ->  (
 ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( # `  W )  <  ( M  +  N ) )  ->  ( ( ( W substr  <. M ,  ( # `  W ) >. ) concat  ( W substr 
 <. 0 ,  M >. ) ) substr  <. 0 ,  N >. )  =  ( ( W substr  <. M ,  ( # `
  W ) >. ) concat 
 ( W substr  <. 0 ,  ( ( M  +  N )  -  ( # `
  W ) )
 >. ) ) ) )
 
31-May-20182cshw2lem1 28253 Lemma 1 for 2cshw2 28256. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
 |-  ( W  e. Word  V  ->  (
 ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( # `  W )  <  ( M  +  N ) )  ->  ( ( ( W substr  <. M ,  ( # `  W ) >. ) concat  ( W substr 
 <. 0 ,  M >. ) ) substr  <. N ,  ( # `
  W ) >. )  =  ( W substr  <. ( ( M  +  N )  -  ( # `  W ) ) ,  M >. ) ) )
 
31-May-20182cshw1 28252 Cyclically shifting a word two times (without "overflow"). (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
 |-  ( W  e. Word  V  ->  (
 ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( M  +  N )  <_  ( # `  W ) )  ->  ( ( W CyclShift  M ) CyclShift  N )  =  ( W CyclShift  ( M  +  N ) ) ) )
 
31-May-20182cshw1lem2 28250 Lemma 2 for 2cshw1 28252. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
 |-  ( W  e. Word  V  ->  (
 ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( M  +  N )  <_  ( # `  W ) )  ->  ( ( ( W substr  <. M ,  ( # `  W ) >. ) concat  ( W substr 
 <. 0 ,  M >. ) ) substr  <. 0 ,  N >. )  =  ( W substr  <. M ,  ( N  +  M ) >. ) ) )
 
31-May-20182cshw1lem1 28249 Lemma 1 for 2cshw1 28252. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
 |-  ( W  e. Word  V  ->  (
 ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( M  +  N )  <_  ( # `  W ) )  ->  ( ( ( W substr  <. M ,  ( # `  W ) >. ) concat  ( W substr 
 <. 0 ,  M >. ) ) substr  <. N ,  ( # `
  W ) >. )  =  ( ( W substr  <. ( N  +  M ) ,  ( # `  W ) >. ) concat  ( W substr  <.
 0 ,  M >. ) ) ) )
 
31-May-2018swrdccatin12d 28223 The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 31-May-2018.)
 |-  ( ph  ->  ( # `  A )  =  L )   &    |-  ( ph  ->  ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ...
 L )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) ) )   =>    |-  ( ph  ->  (
 ( A concat  B ) substr  <. M ,  N >. )  =  ( ( A substr  <. M ,  L >. ) concat 
 ( B substr  <. 0 ,  ( N  -  L ) >. ) ) )
 
31-May-2018swrdccatin2d 28222 The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 31-May-2018.)
 |-  ( ph  ->  ( # `  A )  =  L )   &    |-  ( ph  ->  ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( L ... N )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) ) )   =>    |-  ( ph  ->  (
 ( A concat  B ) substr  <. M ,  N >. )  =  ( B substr  <. ( M  -  L ) ,  ( N  -  L ) >. ) )
 
31-May-2018swrdccatin1d 28221 The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 31-May-2018.)
 |-  ( ph  ->  ( # `  A )  =  L )   &    |-  ( ph  ->  ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ...
 N )  /\  N  e.  ( 0 ... L ) ) ) )   =>    |-  ( ph  ->  ( ( A concat  B ) substr  <. M ,  N >. )  =  ( A substr  <. M ,  N >. ) )
 
31-May-20182elfz2melfz 28118 If the sum of two integers of a finite set of sequential nonnegative integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the finite set of sequential nonnegative integers right bounded by the first integer. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
 |-  (
 ( A  e.  (
 0 ... N )  /\  B  e.  ( 0 ... N ) )  ->  ( N  <  ( A  +  B )  ->  ( B  -  ( N  -  A ) )  e.  ( 0 ...
 A ) ) )
 
31-May-2018elfzubelfz 28117 If there is a member in a finite set of sequential integers, the upper bound is also a member of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-May-2018.)
 |-  ( K  e.  ( M ... N )  ->  N  e.  ( M ... N ) )
 
31-May-2018ftc1anclem6 26286 Lemma for ftc1anc 26289- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued  F. (Contributed by Brendan Leahy, 31-May-2018.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( F `  t )  _d t
 )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  ( A (,) B )  C_  D )   &    |-  ( ph  ->  D 
 C_  RR )   &    |-  ( ph  ->  F  e.  L ^1 )   &    |-  ( ph  ->  F : D --> CC )   =>    |-  ( ( ph  /\  Y  e.  RR+ )  ->  E. f  e.  dom  S.1 E. g  e. 
 dom  S.1 ( S.2 `  (
 t  e.  RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t
 ) ,  0 )  -  ( ( f `
  t )  +  ( _i  x.  (
 g `  t )
 ) ) ) ) ) )  <  Y )
 
30-May-20184an4132 28583 A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)
 |-  (
 ( ( ( th  /\ 
 ch )  /\  ps )  /\  ph )  ->  ta )   =>    |-  (
 ( ( ( ph  /\ 
 ps )  /\  ch )  /\  th )  ->  ta )
 
30-May-20184an31 28582 A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)
 |-  (
 ( ( ( ch 
 /\  ps )  /\  ph )  /\  th )  ->  ta )   =>    |-  (
 ( ( ( ph  /\ 
 ps )  /\  ch )  /\  th )  ->  ta )
 
30-May-20184animp1 28581 A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018.)
 |-  (
 ( ph  /\  ps  /\  ch )  ->  ( ta  <->  th ) )   =>    |-  ( ( ( (
 ph  /\  ps )  /\  ch )  /\  th )  ->  ta )
 
30-May-2018swrdccat3b 28220 A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 30-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( A  e. Word  V 
 /\  B  e. Word  V )  ->  ( M  e.  ( 0 ... ( L  +  ( # `  B ) ) )  ->  ( ( A concat  B ) substr 
 <. M ,  ( L  +  ( # `  B ) ) >. )  =  if ( L  <_  M ,  ( B substr  <. ( M  -  L ) ,  ( # `  B ) >. ) ,  (
 ( A substr  <. M ,  L >. ) concat  B )
 ) ) )
 
30-May-2018swrdccat3blem 28219 Lemma for swrdccat3b 28220. (Contributed by Alexander van der Vekens, 30-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  M  e.  ( 0 ... ( L  +  ( # `
  B ) ) ) )  /\  ( L  +  ( # `  B ) )  <_  L ) 
 ->  if ( L  <_  M ,  ( B substr  <. ( M  -  L ) ,  ( # `  B ) >. ) ,  (
 ( A substr  <. M ,  L >. ) concat  B )
 )  =  ( A substr  <. M ,  ( L  +  ( # `  B ) ) >. ) )
 
30-May-2018leaddle0 28094 If adding a real number to a real number results in a value less then the second real number, the first real number must be not positive. (Contributed by Alexander van der Vekens, 30-May-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR )  ->  ( ( A  +  B )  <_  A  <->  B  <_  0 ) )
 
29-May-2018swrdccat3a 28218 A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 29-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( A  e. Word  V 
 /\  B  e. Word  V )  ->  ( N  e.  ( 0 ... ( L  +  ( # `  B ) ) )  ->  ( ( A concat  B ) substr 
 <. 0 ,  N >. )  =  if ( N 
 <_  L ,  ( A substr  <. 0 ,  N >. ) ,  ( A concat  ( B substr 
 <. 0 ,  ( N  -  L ) >. ) ) ) ) )
 
29-May-2018swrdccat 28217 The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( A  e. Word  V 
 /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ...
 N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) ) 
 ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( ( A substr  <. M ,  if ( N  <_  L ,  N ,  L ) >. ) concat  ( B substr 
 <. if ( 0  <_  ( M  -  L ) ,  ( M  -  L ) ,  0 ) ,  ( N  -  L ) >. ) ) ) )
 
29-May-2018ftc1anclem8 26288 Lemma for ftc1anc 26289. (Contributed by Brendan Leahy, 29-May-2018.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( F `  t )  _d t
 )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  ( A (,) B )  C_  D )   &    |-  ( ph  ->  D 
 C_  RR )   &    |-  ( ph  ->  F  e.  L ^1 )   &    |-  ( ph  ->  F : D --> CC )   =>    |-  ( ( ( ( ( ( ( ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( S.2 `  ( t  e. 
 RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t
 ) ,  0 )  -  ( ( f `
  t )  +  ( _i  x.  (
 g `  t )
 ) ) ) ) ) )  <  (
 y  /  2 )
 )  /\  E. r  e.  ( ran  f  u. 
 ran  g ) r  =/=  0 )  /\  y  e.  RR+ )  /\  ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  ( abs `  ( w  -  u ) )  < 
 ( ( y  / 
 2 )  /  (
 2  x.  sup (
 ( abs " ( ran  f  u.  ran  g
 ) ) ,  RR ,  <  ) ) ) )  ->  ( S.2 `  ( t  e.  RR  |->  if ( t  e.  ( u (,) w ) ,  ( ( abs `  (
 ( F `  t
 )  -  ( ( f `  t )  +  ( _i  x.  ( g `  t
 ) ) ) ) )  +  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t ) ) ) ) ) ,  0 ) ) )  < 
 y )
 
28-May-2018swrdccat3 28216 The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 28-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( A  e. Word  V 
 /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ...
 N )  /\  N  e.  ( 0 ... ( L  +  ( # `  B ) ) ) ) 
 ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  if ( N 
 <_  L ,  ( A substr  <. M ,  N >. ) ,  if ( L 
 <_  M ,  ( B substr  <. ( M  -  L ) ,  ( N  -  L ) >. ) ,  ( ( A substr  <. M ,  L >. ) concat  ( B substr  <.
 0 ,  ( N  -  L ) >. ) ) ) ) ) )
 
27-May-2018swrdccatin12 28215 The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( A  e. Word  V 
 /\  B  e. Word  V )  ->  ( ( M  e.  ( 0 ...
 L )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) 
 ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( ( A substr  <. M ,  L >. ) concat 
 ( B substr  <. 0 ,  ( N  -  L ) >. ) ) ) )
 
27-May-2018swrdccatin12lem4 28214 Lemma 4 for swrdccatin12 28215. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ...
 L )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) )  ->  ( ( K  e.  ( 0..^ ( N  -  M ) )  /\  K  e.  ( 0..^ ( L  -  M ) ) ) 
 ->  ( ( ( A concat  B ) substr  <. M ,  N >. ) `  K )  =  ( ( A substr 
 <. M ,  L >. ) `
  K ) ) )
 
27-May-2018swrdccatin12lem3 28213 Lemma 3 for swrdccatin12 28215. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ...
 L )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) )  ->  ( ( K  e.  ( 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  ( (
 ( A concat  B ) substr  <. M ,  N >. ) `
  K )  =  ( ( B substr  <. 0 ,  ( N  -  L ) >. ) `  ( K  -  ( # `  ( A substr 
 <. M ,  L >. ) ) ) ) ) )
 
27-May-2018swrdccatin12lem3c 28212 Lemma for swrdccatin12lem3 28213 and swrdccatin12lem4 28214. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( ( A  e. Word  V  /\  B  e. Word  V )  /\  ( M  e.  ( 0 ...
 L )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) )  ->  ( ( A concat  B )  e. Word  V  /\  M  e.  ( 0
 ... N )  /\  N  e.  ( 0 ... ( # `  ( A concat  B ) ) ) ) )
 
27-May-2018swrdccatin2 28211 The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
 |-  L  =  ( # `  A )   =>    |-  ( ( A  e. Word  V 
 /\  B  e. Word  V )  ->  ( ( M  e.  ( L ... N )  /\  N  e.  ( L ... ( L  +  ( # `  B ) ) ) ) 
 ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( B substr  <. ( M  -  L ) ,  ( N  -  L ) >. ) ) )
 
27-May-2018swrdccatin12lem3b 28210 Lemma 2 for swrdccatin12lem3 28213. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
 |-  (
 ( M  e.  (
 0 ... L )  /\  N  e.  ( L ... X ) )  ->  ( ( K  e.  ( 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  ( K  -  ( L  -  M ) )  e.  ( 0..^ ( ( N  -  L )  -  0 ) ) ) )
 
27-May-2018swrdccatin12lem3a 28209 Lemma 1 for swrdccatin12lem3 28213. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
 |-  (
 ( M  e.  (
 0 ... L )  /\  N  e.  ( L ... X ) )  ->  ( ( K  e.  ( 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  ( K  +  M )  e.  ( L..^ X ) ) )
 
27-May-2018swrdccatfn 28205 The subword of a concatenation as function. (Contributed by Alexander van der Vekens, 27-May-2018.)
 |-  (
 ( ( A  e. Word  V 
 /\  B  e. Word  V )  /\  ( M  e.  ( 0 ... N )  /\  N  e.  (
 0 ... ( ( # `  A )  +  ( # `
  B ) ) ) ) )  ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  Fn  ( 0..^ ( N  -  M ) ) )
 
27-May-2018fzmmmeqm 28116 Subtracting the difference of a member of a finite range of integers and the lower bound of the range from the difference of the upper bound and the lower bound of the range equals the difference of the upper bound of the range and the member. (Contributed by Alexander van der Vekens, 27-May-2018.)
 |-  ( M  e.  ( L ... N )  ->  (
 ( N  -  L )  -  ( M  -  L ) )  =  ( N  -  M ) )
 
27-May-2018elfz0fzfz0 28115 A member of a finite set of sequential integers starting at 0 is a member of a finite set of sequential integers from 0 to a member of a finite set of sequential integers starting at the right border of the first finite set of sequential integers. (Contributed by Alexander van der Vekens, 27-May-2018.)
 |-  (
 ( M  e.  (
 0 ... L )  /\  N  e.  ( L ... X ) )  ->  M  e.  ( 0 ... N ) )
 
27-May-2018ftc1anclem3 26283 Lemma for ftc1anc 26289- the absolute value of the sum of a simple function and  _i times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.)
 |-  (
 ( F  e.  dom  S.1  /\  G  e.  dom  S.1 )  ->  ( abs  o.  ( F  o F  +  ( ( RR  X.  { _i } )  o F  x.  G ) ) )  e.  dom  S.1 )
 
26-May-2018swrdvalodm2 28189 Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 26-May-2018.)
 |-  (
 ( W  e. Word  V  /\  A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( B  <_  A  \/  ( # `  W )  <  B  \/  A  <  0 )  ->  ( W substr 
 <. A ,  B >. )  =  (/) ) )
 
26-May-2018ccatsymb 28180 The symbol at a given position in a concatenated word. (Contributed by Alexander van der Vekens, 26-May-2018.)
 |-  (
 ( S  e. Word  B  /\  T  e. Word  B  /\  I  e.  ZZ )  ->  ( ( S concat  T ) `  I )  =  if ( I  < 
 ( # `  S ) ,  ( S `  I ) ,  ( T `  ( I  -  ( # `  S ) ) ) ) )
 
26-May-2018wrdsymb0 28171 A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.)
 |-  (
 ( W  e. Word  V  /\  I  e.  ZZ )  ->  ( ( I  <  0  \/  ( # `
  W )  <_  I )  ->  ( W `
  I )  =  (/) ) )
 
25-May-2018elfz2z 28106 Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.)
 |-  (
 ( K  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  (
 0 ... N )  <->  ( 0  <_  K  /\  K  <_  N ) ) )
 
25-May-2018jaoi3 28049 Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.)
 |-  ( ph  ->  ps )   &    |-  ( ( -.  ph  /\  ch )  ->  ps )   =>    |-  ( ( ph  \/  ch )  ->  ps )
 
24-May-2018ax7w18AUX7 29678 Weak version of ax-7 1750 not requiring ax-7 1750. (Contributed by NM, 24-May-2018.)
 |-  ( A. u  u  =  v  ->  ( A. x A. y ph  ->  A. y A. x ph ) )
 
24-May-2018ax7w17lem2AUX7 29677 Experimental lemma with the goal of deriving hbae 2041 from ax-7v 29443. Looks like a dead end because we apparently need hbae 2041 to eliminate the first 2 hypotheses for those  ph that satisfy the 3rd and 4th hypotheses. (Contributed by NM, 24-May-2018.)
 |-  F/ x ph   &    |-  F/ z ph   &    |-  ( ph  ->  F/ x  u  =  y )   &    |-  ( ph  ->  F/ z  u  =  y )   =>    |-  ( ph  ->  (
 A. x A. z  x  =  y  ->  A. z A. x  x  =  y ) )
 
24-May-2018ax7w17lem1AUX7 29676 Lemma for ax7w17lem2AUX7 29677. (Contributed by NM, 24-May-2018.)
 |-  ( [ x  /  u ] [ z  /  v ] u  =  y  <->  x  =  y )
 
24-May-2018ax7w16AUX7 29675 Special case of ax-7 1750 derived from ax-7v 29443. This is the "easy" direction. The other direction is still conjectured. (Contributed by NM, 24-May-2018.)
 |-  ( A. z A. x  x  =  y  ->  A. x A. z  x  =  y )
 
24-May-2018nfsbdwAUX7 29579 Deduction version of nfsbwAUX7 29666. (Contributed by NM, 24-May-2018.)
 |-  F/ x ph   &    |-  ( ph  ->  F/ z ps )   =>    |-  ( ph  ->  F/ z [ y  /  x ] ps )
 
24-May-2018swrdvalodm 28190 Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.)
 |-  (
 ( W  e. Word  V  /\  A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( B  <_  A  \/  ( # `  W )  <_  A  \/  B  <_  0 )  ->  ( W substr 
 <. A ,  B >. )  =  (/) ) )
 
24-May-2018swrdvalodmlem1 28188 Lemma for swrdvalodm 28190. (Contributed by Alexander van der Vekens, 24-May-2018.)
 |-  (
 ( N  e.  NN0  /\  A  e.  ZZ  /\  B  e.  ZZ )  ->  ( ( N  <_  A  \/  B  <_  0
 )  ->  ( ( A..^ B )  C_  (
 0..^ N )  ->  B  <_  A ) ) )
 
23-May-2018ax7w15lemxAUX7 29667 Lemma for ax7w14AUX7 29671. (Contributed by NM, 23-May-2018.)
 |-  F/ x ph   &    |-  F/ y ph   =>    |-  ( -.  A. x  x  =  y  ->  ( A. x A. y [ x  /  u ] [ y  /  v ] ph  ->  A. s A. t [
 s  /  u ] [ t  /  v ] ph ) )
 
23-May-2018swrdccatin12lem2 28208 Lemma 2 for swrdccatin12 28215. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.)
 |-  (
 ( L  e.  NN0  /\  M  e.  NN0  /\  N  e.  ZZ )  ->  (
 ( K  e.  (
 0..^ ( N  -  M ) )  /\  -.  K  e.  ( 0..^ ( L  -  M ) ) )  ->  K  e.  ( ( L  -  M )..^ ( ( L  -  M )  +  ( N  -  L ) ) ) ) )
 
23-May-2018swrdccat3a0 28204 The subword of a concatenation of an empty word with another word is the subword of the second concatenated word. (Contributed by Alexander van der Vekens, 27-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.)
 |-  (
 ( A  =  (/)  /\  B  e. Word  V )  ->  ( ( A concat  B ) substr 
 <. M ,  N >. )  =  ( B substr  <. M ,  N >. ) )
 
22-May-2018ax7w14AUX7 29671 Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 22-May-2018.)
 |-  F/ x ph   &    |-  F/ y ph   =>    |-  ( A. x A. y [ x  /  u ] [
 y  /  v ] ph  ->  A. y A. x [ x  /  u ] [ y  /  v ] ph )
 
22-May-2018ax7w14lemAUX7 29670 Lemma for ax7w14AUX7 29671. (Contributed by NM, 22-May-2018.)
 |-  F/ x ph   &    |-  F/ y ph   =>    |-  ( -.  A. x  x  =  y  ->  ( A. x A. y [ x  /  u ] [ y  /  v ] ph  <->  A. s A. t [ s  /  u ] [ t  /  v ] ph ) )
 
22-May-2018ax7w15AUX7 29669 Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 22-May-2018.)
 |-  F/ x ph   &    |-  F/ y ph   &    |-  ( ph  ->  F/ x ps )   &    |-  ( ph  ->  F/ y ps )   =>    |-  ( ph  ->  ( A. x A. y [ x  /  u ] [
 y  /  v ] ps  ->  A. y A. x [ x  /  u ] [ y  /  v ] ps ) )
 
22-May-2018ax7w15lemAUX7 29668 Lemma for ax7w15AUX7 29669. (Contributed by NM, 22-May-2018.)
 |-  F/ x ph   &    |-  F/ y ph   &    |-  ( ph  ->  F/ x ps )   &    |-  ( ph  ->  F/ y ps )   =>    |-  ( ( ph  /\  -.  A. x  x  =  y )  ->  ( A. x A. y [ x  /  u ] [ y  /  v ] ps  <->  A. s A. t [ s  /  u ] [ t  /  v ] ps ) )
 
22-May-2018nfsbwAUX7 29666 If  z is not free in  ph, it is not free in  [ y  /  x ] ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by NM, 22-May-2018.)
 |-  F/ z ph   =>    |- 
 F/ z [ y  /  x ] ph
 
22-May-2018dvelimfwAUX7 29665 Version of dvelimvNEW7 29463. (Contributed by Mario Carneiro, 6-Oct-2016.) (Revised by NM, 22-May-2018.)
 |-  F/ x ph   &    |-  F/ z ps   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  F/ x ps )
 
22-May-2018sb8dwAUX7 29591 Weak version of sb8 2169 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.)
 |-  F/ x ph   &    |-  F/ y ph   &    |-  ( ph  ->  F/ y ps )   =>    |-  ( ph  ->  ( A. x ps  <->  A. y [ y  /  x ] ps )
 )
 
22-May-2018sb8iwAUX7 29590 Version of sb8 2169 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.)
 |-  ( -.  A. x  x  =  y  ->  F/ y ps )   =>    |-  ( -.  A. x  x  =  y  ->  (
 A. y [ y  /  x ] ps  ->  A. x ps ) )
 
22-May-2018cbv3dwAUX7 29517 Weak deduction version of cbv3 1972 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.)
 |-  F/ x ph   &    |-  F/ y ph   &    |-  ( ph  ->  F/ y ps )   &    |-  ( ph  ->  F/ x ch )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  ->  ch ) ) )   =>    |-  ( ph  ->  ( A. x ps  ->  A. y ch ) )
 
22-May-2018cbvaldwAUX7 29516 Weak version of cbvald 1987 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.)
 |-  F/ y ph   &    |-  ( ph  ->  F/ y ps )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( ph  ->  (
 A. x ps  <->  A. y ch )
 )
 
22-May-20182cshw1lem3 28251 Lemma 3 for 2cshw1 28252. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by Alexander van der Vekens, 22-May-2018.)
 |-  (
 ( W  e. Word  V  /\  ( M  e.  (
 0 ... ( # `  W ) )  /\  N  e.  ( 0 ... ( # `
  W ) ) 
 /\  ( M  +  N )  <_  ( # `  W ) ) ) 
 ->  ( ( ( W substr  <. ( N  +  M ) ,  ( # `  W ) >. ) concat  ( W substr  <.
 0 ,  M >. ) ) concat  ( W substr  <. M ,  ( N  +  M ) >. ) )  =  ( W CyclShift  ( M  +  N ) ) )
 
21-May-2018ax7w13AUX7 29674 Special case of ax-7 1750 derived from ax-7v 29443. Example illustrating use of ax7w12AUX7 29672. (Contributed by NM, 21-May-2018.)
 |-  ( A. x A. y  x  e.  y  ->  A. y A. x  x  e.  y )
 
21-May-2018elsb34AUX7 29673 Substitution applied to an atomic membership wff. (Contributed by NM, 21-May-2018.)
 |-  ( [ x  /  u ] [ y  /  v ] u  e.  v  <->  x  e.  y )
 
21-May-2018ax7w12AUX7 29672 Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 21-May-2018.)
 |-  ( A. x A. y [ x  /  u ] [
 y  /  v ] ph  ->  A. y A. x [ x  /  u ] [ y  /  v ] ph )
 
21-May-2018cshwidxn 28248 The symbol at index (n-1) of a cyclically shifted word of length n (not 0) is the symbol at index (N-1) of the original word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( N  e.  (
 1..^ ( # `  W ) )  /\  W  e. Word  V )  ->  ( ( W CyclShift  N ) `  (
 ( # `  W )  -  1 ) )  =  ( W `  ( N  -  1
 ) ) )
 
21-May-2018cshwidxm 28247 The symbol at index (n-N) of a cyclically shifted word of length n (not 0) is the symbol at index 0 of the original word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 1..^ ( # `  W ) ) )  ->  ( ( W CyclShift  N ) `
  ( ( # `  W )  -  N ) )  =  ( W `  0 ) )
 
21-May-2018cshwidxm1 28246 The symbol at index ((n-N)-1) of a cyclically shifted word of length n (not 0) is the symbol at index (n-1) of the original word. (Contributed by Alexander van der Vekens, 23-Mar-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 1..^ ( # `  W ) ) )  ->  ( ( W CyclShift  N ) `
  ( ( ( # `  W )  -  N )  -  1
 ) )  =  ( W `  ( ( # `  W )  -  1 ) ) )
 
21-May-2018cshwidx0 28245 The symbol at index 0 of a cyclically shifted word is the symbol at index N of the original word. (Contributed by Alexander van der Vekens, 15-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0..^ ( # `  W ) ) )  ->  ( ( W CyclShift  N ) `
  0 )  =  ( W `  N ) )
 
21-May-2018cshwidxmod 28244 The symbol at a given index of a cyclically shifted word is the symbol at the shifted index of the original word. (Contributed by Alexander van der Vekens, 13-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0..^ ( # `  W ) ) )  ->  ( I  e.  (
 0..^ ( # `  W ) )  ->  ( ( W CyclShift  N ) `  I
 )  =  ( W `
  ( ( I  +  N )  mod  ( # `  W ) ) ) ) )
 
21-May-2018cshwidx 28243 The symbol at a given index of a cyclically shifted word is the symbol at the shifted index of the original word. (Contributed by Alexander van der Vekens, 17-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0..^ ( # `  W ) ) )  ->  ( I  e.  (
 0..^ ( # `  W ) )  ->  ( ( W CyclShift  N ) `  I
 )  =  if ( I  <  ( ( # `  W )  -  N ) ,  ( W `  ( I  +  N ) ) ,  ( W `  ( ( I  +  N )  -  ( # `  W ) ) ) ) ) )
 
21-May-2018cshwcl 28241 A cyclically shifted word is a word over the same set as for the original word. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  ( W  e. Word  V  ->  ( W CyclShift  N )  e. Word  V )
 
21-May-2018cshwoor 28238 A cyclically shifted word is the empty set if the number of shifts is out of the range of the word. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  NN0 )  ->  ( ( # `  W )  <  N  ->  ( W CyclShift  N )  =  (/) ) )
 
21-May-2018cshnnn0 28237 A cyclical shift is the empty set if the number of shifts is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
 |-  ( -.  N  e.  NN0  ->  ( W CyclShift  N )  =  (/) )
 
21-May-2018modifeq2int 28162 If a nonnegative integer is less than the double of a positive integer, the nonnegative integer modulo the positive integer equals the nonnegative integer or the nonnegative integer minus the positive integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( A  e.  NN0  /\  B  e.  NN  /\  A  <  ( 2  x.  B ) )  ->  ( A  mod  B )  =  if ( A  <  B ,  A ,  ( A  -  B ) ) )
 
21-May-2018subsubelfzo0 28136 Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( A  e.  (
 0..^ N )  /\  I  e.  ( 0..^ N )  /\  -.  I  <  ( N  -  A ) )  ->  ( I  -  ( N  -  A ) )  e.  ( 0..^ A ) )
 
21-May-2018elfzonn0 28123 A member of a half-open integer range starting at 0 is a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
 |-  ( K  e.  ( 0..^ N )  ->  K  e.  NN0 )
 
21-May-20182leaddle2 28093 If two real numbers are less than a third real number, the sum of the real numbers is less then twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( ( A  <  C 
 /\  B  <  C )  ->  ( A  +  B )  <  ( 2  x.  C ) ) )
 
21-May-2018fvifeq 28077 Equality of function values with conditional arguments, see also fvif 5744. (Contributed by Alexander van der Vekens, 21-May-2018.)
 |-  ( A  =  if ( ph ,  B ,  C )  ->  ( F `  A )  =  if ( ph ,  ( F `
  B ) ,  ( F `  C ) ) )
 
21-May-2018axio 2408 Definition of 'or' (intuitionistic logic axiom ax-io). (Contributed by Jim Kingdon, 21-May-2018.)
 |-  ( ( ( ph  \/  ch )  ->  ps )  <->  ( ( ph  ->  ps )  /\  ( ch  ->  ps )
 ) )
 
21-May-2018axin2 2407 'Not' elimination (intuitionistic logic axiom ax-in2). (Contributed by Jim Kingdon, 21-May-2018.)
 |-  ( -.  ph  ->  (
 ph  ->  ps ) )
 
21-May-2018axin1 2406 'Not' introduction (intuitionistic logic axiom ax-in1). (Contributed by Jim Kingdon, 21-May-2018.)
 |-  ( ( ph  ->  -.  ph )  ->  -.  ph )
 
21-May-2018axia3 2405 'And' introduction (intuitionistic logic axiom ax-ia3). (Contributed by Jim Kingdon, 21-May-2018.)
 |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
 
21-May-2018axia2 2404 Right 'and' elimination (intuitionistic logic axiom ax-ia2). (Contributed by Jim Kingdon, 21-May-2018.)
 |-  ( ( ph  /\  ps )  ->  ps )
 
21-May-2018axia1 2403 Left 'and' elimination (intuitionistic logic axiom ax-ia1). (Contributed by Jim Kingdon, 21-May-2018.)
 |-  ( ( ph  /\  ps )  ->  ph )
 
20-May-2018ax7w11AUX7 29664 Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 20-May-2018.)
 |-  ( A. x A. y ( -.  x  =  y 
 /\  ph )  ->  A. y A. x ( -.  x  =  y  /\  ph )
 )
 
20-May-2018ax7w10AUX7 29663 Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 20-May-2018.)
 |-  ( A. x A. y ( x  =  y  /\  ph )  ->  A. y A. x ( x  =  y  /\  ph )
 )
 
20-May-2018cshwlen 28242 The length of a cyclically shifted word is the same as the length of the original word. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 20-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  ( 0
 ... ( # `  W ) ) )  ->  ( # `  ( W CyclShift  N ) )  =  ( # `  W ) )
 
20-May-2018cshwn 28240 A word cyclically shifted by its length is the word itself. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 20-May-2018.)
 |-  ( W  e. Word  V  ->  ( W CyclShift  ( # `  W ) )  =  W )
 
20-May-2018cshw0 28239 A word cyclically shifted by 0 is the word itself. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 20-May-2018.)
 |-  ( W  e. Word  V  ->  ( W CyclShift  0 )  =  W )
 
20-May-2018cshword 28236 Perform a cyclic shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018.)
 |-  (
 ( W  e. Word  V  /\  N  e.  NN0 )  ->  ( W CyclShift  N )  =  ( ( W substr  <. N ,  ( # `  W )
 >. ) concat  ( W substr  <. 0 ,  N >. ) ) )
 
20-May-2018cshfn 28235 Perform a cyclic shift for a function over a range of nonnegative integers. (Contributed by Alexander van der Vekens, 20-May-2018.)
 |-  (
 ( W  e.  {
 f  |  E. l  e.  NN0  f  Fn  (
 0..^ l ) }  /\  N  e.  NN0 )  ->  ( W CyclShift  N )  =  ( ( W substr  <. N ,  ( # `  W )
 >. ) concat  ( W substr  <. 0 ,  N >. ) ) )
 
20-May-2018df-csh 28233 Perform a cyclic shift for an arbitrary class. Meaningful only for words  w  e. Word  S or at least functions over an half-open range of nonnegative integers. The result is also only meaningful if  0  <_  n  <_  ( # `  w
). (Contributed by Alexander van der Vekens, 20-May-2018.)
 |- CyclShift  =  ( w  e.  { f  |  E. l  e.  NN0  f  Fn  ( 0..^ l ) } ,  n  e.  NN0  |->  ( ( w substr  <. n ,  ( # `  w ) >. ) concat  ( w substr 
 <. 0 ,  n >. ) ) )
 
19-May-2018fzonmapblen 28135 The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one, is less then the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018.)
 |-  (
 ( A  e.  (
 0..^ N )  /\  B  e.  ( 0..^ N )  /\  B  <  A )  ->  ( B  +  ( N  -  A ) )  <  N )
 
18-May-2018fzo0sn0fzo1 28126 A half open integer range starting from 0 is the union of the singleton set containing 0 and a half open integer range starting from 1. (Contributed by Alexander van der Vekens, 18-May-2018.)
 |-  ( N  e.  NN  ->  ( 0..^ N )  =  ( { 0 }  u.  ( 1..^ N ) ) )
 
17-May-2018modprm0g 28230 For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  A. p  e.  Prime  A. n  e.  (
 1..^ p ) A. i  e.  ( 1..^ p ) E. j  e.  ( 0..^ p ) ( ( i  +  ( j  x.  n ) )  mod  p )  =  0
 
17-May-2018modprm0 28229 For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( P  e.  Prime  /\  N  e.  ( 1..^ P )  /\  I  e.  ( 1..^ P ) )  ->  E. j  e.  ( 0..^ P ) ( ( I  +  ( j  x.  N ) )  mod  P )  =  0 )
 
17-May-2018modprminveq 28227 The modular inverse of  A  mod  P is unique. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  R  =  ( ( A ^
 ( P  -  2
 ) )  mod  P )   =>    |-  ( ( P  e.  Prime  /\  A  e.  ZZ  /\ 
 -.  P  ||  A )  ->  ( ( S  e.  ( 0 ... ( P  -  1
 ) )  /\  (
 ( A  x.  S )  mod  P )  =  1 )  <->  S  =  R ) )
 
17-May-2018modprm1div 28225 A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( P  e.  Prime  /\  A  e.  ZZ )  ->  ( ( A  mod  P )  =  1  <->  P  ||  ( A  -  1 ) ) )
 
17-May-2018prmgt1 28224 A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  ( P  e.  Prime  ->  1  <  P )
 
17-May-2018modidmul0 28161 The product of an integer and a positive integer is 0 modulo the positive integer. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( A  e.  ZZ  /\  N  e.  NN )  ->  ( ( A  x.  N )  mod  N )  =  0 )
 
17-May-2018modaddmulmod 28159 The sum of a real number and the product of a second real number modulo a positive real number and an integer equals the sum of the real number and the product of the other real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  ZZ )  /\  M  e.  RR+ )  ->  ( ( A  +  ( ( B  mod  M )  x.  C ) )  mod  M )  =  ( ( A  +  ( B  x.  C ) )  mod  M ) )
 
17-May-2018modmulmod 28158 The product of a real number modulo a positive real number and an integer equals the product of the real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  ZZ  /\  M  e.  RR+ )  ->  ( ( ( A 
 mod  M )  x.  B )  mod  M )  =  ( ( A  x.  B )  mod  M ) )
 
17-May-2018modsubmodmod 28157 The difference of a real number modulo a positive real number and another real number modulo this positive real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  M  e.  RR+ )  ->  ( ( ( A 
 mod  M )  -  ( B  mod  M ) ) 
 mod  M )  =  ( ( A  -  B )  mod  M ) )
 
17-May-2018modsubmod 28156 The difference of a real number modulo a positive real number and another real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  M  e.  RR+ )  ->  ( ( ( A 
 mod  M )  -  B )  mod  M )  =  ( ( A  -  B )  mod  M ) )
 
17-May-2018modadd2mod 28155 The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  M  e.  RR+ )  ->  ( ( B  +  ( A  mod  M ) )  mod  M )  =  ( ( B  +  A )  mod  M ) )
 
15-May-2018modprminv 28226 Show an explicit expression for the modular inverse of  A  mod  P. This is an application of prmdiv 13175. (Contributed by Alexander van der Vekens, 15-May-2018.)
 |-  R  =  ( ( A ^
 ( P  -  2
 ) )  mod  P )   =>    |-  ( ( P  e.  Prime  /\  A  e.  ZZ  /\ 
 -.  P  ||  A )  ->  ( R  e.  ( 1 ... ( P  -  1 ) ) 
 /\  ( ( A  x.  R )  mod  P )  =  1 ) )
 
15-May-2018modid0 28160 A positive real number modulo itself is 0 . (Contributed by Alexander van der Vekens, 15-May-2018.)
 |-  ( N  e.  RR+  ->  ( N  mod  N )  =  0 )
 
14-May-2018exdistrf 2067 Distribution of existential quantifiers, with a bound-variable hypothesis saying that  y is not free in  ph, but  x can be free in  ph (and there is no distinct variable condition on  x and  y). (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.)
 |-  ( -.  A. x  x  =  y  ->  F/ y ph )   =>    |-  ( E. x E. y ( ph  /\  ps )  ->  E. x ( ph  /\ 
 E. y ps )
 )
 
13-May-2018modaddmod 28154 The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.)
 |-  (
 ( A  e.  RR  /\  B  e.  RR  /\  M  e.  RR+ )  ->  ( ( ( A 
 mod  M )  +  B )  mod  M )  =  ( ( A  +  B )  mod  M ) )
 
13-May-20182submod 28153 If a real number is between a positive real number and the double of the positive real number, the real number modulo the positive real number equals the real number minus the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.)
 |-  (
 ( ( A  e.  RR  /\  B  e.  RR+ )  /\  ( B  <_  A 
 /\  A  <  (
 2  x.  B ) ) )  ->  ( A  mod  B )  =  ( A  -  B ) )
 
13-May-2018fzossnn0 28125 A half open integer range starting from a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018.)
 |-  ( M  e.  NN0  ->  ( M..^ N )  C_  NN0 )
 
13-May-2018ftc1anclem7 26287 Lemma for ftc1anc 26289. (Contributed by Brendan Leahy, 13-May-2018.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( F `  t )  _d t
 )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  ( A (,) B )  C_  D )   &    |-  ( ph  ->  D 
 C_  RR )   &    |-  ( ph  ->  F  e.  L ^1 )   &    |-  ( ph  ->  F : D --> CC )   =>    |-  ( ( ( ( ( ( ( ph  /\  ( f  e.  dom  S.1  /\  g  e.  dom  S.1 ) )  /\  ( S.2 `  ( t  e. 
 RR  |->  ( abs `  ( if ( t  e.  D ,  ( F `  t
 ) ,  0 )  -  ( ( f `
  t )  +  ( _i  x.  (
 g `  t )
 ) ) ) ) ) )  <  (
 y  /  2 )
 )  /\  E. r  e.  ( ran  f  u. 
 ran  g ) r  =/=  0 )  /\  y  e.  RR+ )  /\  ( u  e.  ( A [,] B )  /\  w  e.  ( A [,] B )  /\  u  <_  w ) )  /\  ( abs `  ( w  -  u ) )  < 
 ( ( y  / 
 2 )  /  (
 2  x.  sup (
 ( abs " ( ran  f  u.  ran  g
 ) ) ,  RR ,  <  ) ) ) )  ->  ( ( S.2 `  ( t  e. 
 RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( f `  t )  +  ( _i  x.  ( g `  t ) ) ) ) ,  0 ) ) )  +  ( S.2 `  ( t  e. 
 RR  |->  if ( t  e.  ( u (,) w ) ,  ( abs `  ( ( F `  t )  -  (
 ( f `  t
 )  +  ( _i 
 x.  ( g `  t ) ) ) ) ) ,  0 ) ) ) )  <  ( ( y 
 /  2 )  +  ( y  /  2
 ) ) )
 
13-May-2018cbvald 1987 Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2074. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
 |- 
 F/ y ph   &    |-  ( ph  ->  F/ y ps )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( ph  ->  (
 A. x ps  <->  A. y ch )
 )
 
13-May-2018cbv2 1981 Rule used to change bound variables, using implicit substitution. Revised to align format of hypotheses to common style. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
 |- 
 F/ x ph   &    |-  F/ y ph   &    |-  ( ph  ->  F/ y ps )   &    |-  ( ph  ->  F/ x ch )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( ph  ->  (
 A. x ps  <->  A. y ch )
 )
 
13-May-2018cbv1h 1975 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.)
 |-  ( ph  ->  ( ps  ->  A. y ps )
 )   &    |-  ( ph  ->  ( ch  ->  A. x ch )
 )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  ->  ch )
 ) )   =>    |-  ( A. x A. y ph  ->  ( A. x ps  ->  A. y ch ) )
 
13-May-2018cbv1 1974 Rule used to change bound variables, using implicit substitution. Revised to format hypotheses to common style. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
 |- 
 F/ x ph   &    |-  F/ y ph   &    |-  ( ph  ->  F/ y ps )   &    |-  ( ph  ->  F/ x ch )   &    |-  ( ph  ->  ( x  =  y  ->  ( ps  ->  ch ) ) )   =>    |-  ( ph  ->  ( A. x ps  ->  A. y ch ) )
 
12-May-2018reumodprminv 28228 For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018.)
 |-  (
 ( P  e.  Prime  /\  N  e.  ( 1..^ P ) )  ->  E! i  e.  (
 1 ... ( P  -  1 ) ) ( ( N  x.  i
 )  mod  P )  =  1 )
 
12-May-2018cbv3h 1973 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.)
 |-  ( ph  ->  A. y ph )   &    |-  ( ps  ->  A. x ps )   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  A. y ps )
 
12-May-2018cbv3 1972 Rule used to change bound variables, using implicit substitution, that does not use ax-12o 2220. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.)
 |- 
 F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  A. y ps )
 
12-May-2018spei 1967 Inference from existential specialization, using implicit substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   &    |-  ps   =>    |-  E. x ph
 
11-May-2018ftc1anc 26289 ftc1a 19922 holds for functions that obey the triangle inequality in the absence of ax-cc 8316. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.)
 |-  G  =  ( x  e.  ( A [,] B )  |->  S. ( A (,) x ) ( F `  t )  _d t
 )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  A  <_  B )   &    |-  ( ph  ->  ( A (,) B )  C_  D )   &    |-  ( ph  ->  D 
 C_  RR )   &    |-  ( ph  ->  F  e.  L ^1 )   &    |-  ( ph  ->  F : D --> CC )   &    |-  ( ph  ->  A. s  e.  ( (,) " ( ( A [,] B )  X.  ( A [,] B ) ) ) ( abs `  S. s ( F `
  t )  _d t )  <_  ( S.2 `  ( t  e. 
 RR  |->  if ( t  e.  s ,  ( abs `  ( F `  t
 ) ) ,  0 ) ) ) )   =>    |-  ( ph  ->  G  e.  ( ( A [,] B ) -cn-> CC ) )
 
11-May-2018nfsb4t 2128 A variable not free remains so after substitution with a distinct variable (closed form of nfsb4 2130). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
 |-  ( A. x F/ z ph  ->  ( -.  A. z  z  =  y  ->  F/ z [ y  /  x ] ph ) )
 
11-May-2018dvelimh 2072 Version of dvelim 2074 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. z ps )   &    |-  (
 z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
11-May-2018dvelimdf 2071 Deduction form of dvelimf 2069. This version may be useful if we want to avoid ax-17 1627 and use ax-16 2222 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
 |- 
 F/ x ph   &    |-  F/ z ph   &    |-  ( ph  ->  F/ x ps )   &    |-  ( ph  ->  F/ z ch )   &    |-  ( ph  ->  ( z  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( ph  ->  ( -.  A. x  x  =  y 
 ->  F/ x ch )
 )
 
11-May-2018dvelimf 2069 Version of dvelimv 2075 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
 |- 
 F/ x ph   &    |-  F/ z ps   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  F/ x ps )
 
8-May-2018elima4 25405 Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
 |-  ( A  e.  ( R " B )  <->  ( R  i^i  ( B  X.  { A } ) )  =/=  (/) )
 
8-May-2018snnzb 25403 A singleton is non-empty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.)
 |-  ( A  e.  _V  <->  { A }  =/=  (/) )
 
6-May-2018opelco3 25404 Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.)
 |-  ( <. A ,  B >.  e.  ( C  o.  D ) 
 <->  B  e.  ( C
 " ( D " { A } ) ) )
 
5-May-2018wl-nfnbi 26234 Being free does not depend on an outside negation in an expression. This theorem is slightly more general than nfn 1812 or nfnd 1810. (Contributed by Wolf Lammen, 5-May-2018.)
 |-  ( F/ x ph  <->  F/ x  -.  ph )
 
5-May-2018drnf2 2063 Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.)
 |-  ( A. x  x  =  y  ->  ( ph 
 <->  ps ) )   =>    |-  ( A. x  x  =  y  ->  ( F/ z ph  <->  F/ z ps )
 )
 
3-May-2018brlb 25801 Binary relationship form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.)
 |-  S  e.  _V   &    |-  A  e.  _V   =>    |-  ( SLB R A  <->  A. x  e.  S  A R x )
 
3-May-2018brub 25800 Binary relationship form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.)
 |-  S  e.  _V   &    |-  A  e.  _V   =>    |-  ( SUB R A  <->  A. x  e.  S  x R A )
 
3-May-2018df-lb 25722 Define the lower bound relationship functor. See brlb 25801 for value. (Contributed by Scott Fenton, 3-May-2018.)
 |- LB R  = UB `' R
 
3-May-2018df-ub 25721 Define the upper bound relationship functor. See brub 25800 for value. (Contributed by Scott Fenton, 3-May-2018.)
 |- UB R  =  ( ( _V  X.  _V )  \  ( ( _V  \  R )  o.  `'  _E  )
 )
 
3-May-2018sbft 2116 Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.)
 |-  ( F/ x ph  ->  ( [ y  /  x ] ph  <->  ph ) )
 
3-May-2018spsbe 1664 A specialization theorem. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.)
 |-  ( [ y  /  x ] ph  ->  E. x ph )
 
30-Apr-2018sbn 2131 Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.)
 |-  ( [ y  /  x ]  -.  ph  <->  -.  [ y  /  x ] ph )
 
30-Apr-2018dvelimv 2075 Similar to dvelim 2074 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.)
 |-  ( z  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
29-Apr-2018dveeq1 2022 Quantifier introduction when one pair of variables is distinct. Revised to be independent of dvelimv 2075. (Contributed by NM, 2-Jan-2002.) (Revised by Wolf Lammen, 29-Apr-2018.)
 |-  ( -.  A. x  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z ) )
 
29-Apr-2018ax12o 2011 Derive set.mm's original ax-12o 2220 from the shorter ax-12 1951. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.)
 |-  ( -.  A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y ) ) )
 
29-Apr-2018nfeqf 2010 A variable is effectively not free in an equality if it is not either of the involved variables.  F/ version of ax-12o 2220. (Contributed by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 29-Apr-2018.)
 |-  ( ( -.  A. z  z  =  x  /\  -.  A. z  z  =  y )  ->  F/ z  x  =  y )
 
29-Apr-2018ax12olem4 2009 Lemma for nfeqf 2010. A technical step to remove a distinct variable constraint from ax12v 1952. (Contributed by Wolf Lammen, 29-Apr-2018.)
 |-  ( ph  ->  F/ x  y  =  w )   &    |-  ( ps  ->  F/ x  z  =  w )   =>    |-  ( ( ph  /\ 
 ps )  ->  F/ x  y  =  z )
 
29-Apr-2018ax12olem3 2008 Lemma for nfeqf 2010 and dveeq1 2022. Convert ax12olem2 2007 into a more general form. (Contributed by Wolf Lammen, 29-Apr-2018.)
 |-  ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 )   =>    |-  ( -.  A. x  x  =  y  ->  F/ x  y  =  z )
 
29-Apr-2018ax12olem2 2007 Lemma for nfeqf 2010 and dveeq1 2022. This lemma is equivalent to ax12v 1952 with one distinct variable constraint removed. (Contributed by Wolf Lammen, 29-Apr-2018.)
 |-  ( -.  x  =  y  ->  ( E. x  y  =  z  ->  y  =  z ) )
 
27-Apr-2018wl-aleq 26236 The semantics of  A. x y  =  z. (Contributed by Wolf Lammen, 27-Apr-2018.)
 |-  ( A. x  y  =  z 
 <->  ( y  =  z 
 /\  ( A. x  x  =  y  <->  A. x  x  =  z ) ) )
 
27-Apr-2018wl-exeq 26235 The semantics of  E. x y  =  z. (Contributed by Wolf Lammen, 27-Apr-2018.)
 |-  ( E. x  y  =  z 
 <->  ( y  =  z  \/  A. x  x  =  y  \/  A. x <