Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

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

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

Color key:   Intuitionistic Logic Explorer  Intuitionistic Logic Explorer   User Mathboxes  User Mathboxes  

Last updated on 7-Dec-2022 at 10:16 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem
 
24-Nov-2022cvgratnnlembern 10878 Lemma for cvgratnn 10886. Upper bound for a geometric progression of positive ratio less than one. (Contributed by Jim Kingdon, 24-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ph  ->  M  e.  NN )   =>    |-  ( ph  ->  ( A ^ M )  < 
 ( ( 1  /  ( ( 1  /  A )  -  1
 ) )  /  M ) )
 
23-Nov-2022cvgratnnlemfm 10884 Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 23-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   &    |-  ( ph  ->  M  e.  NN )   =>    |-  ( ph  ->  ( abs `  ( F `  M ) )  < 
 ( ( ( ( 1  /  ( ( 1  /  A )  -  1 ) ) 
 /  A )  x.  ( ( abs `  ( F `  1 ) )  +  1 ) ) 
 /  M ) )
 
23-Nov-2022cvgratnnlemsumlt 10883 Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 23-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  M ) )   =>    |-  ( ph  ->  sum_ i  e.  ( ( M  +  1 ) ... N ) ( A ^
 ( i  -  M ) )  <  ( A 
 /  ( 1  -  A ) ) )
 
21-Nov-2022cvgratnnlemrate 10885 Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 21-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  M ) )   =>    |-  ( ph  ->  ( abs `  ( (  seq 1
 (  +  ,  F ) `  N )  -  (  seq 1 (  +  ,  F ) `  M ) ) )  < 
 ( ( ( ( ( 1  /  (
 ( 1  /  A )  -  1 ) ) 
 /  A )  x.  ( ( abs `  ( F `  1 ) )  +  1 ) )  x.  ( A  /  ( 1  -  A ) ) )  /  M ) )
 
21-Nov-2022cvgratnnlemabsle 10882 Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 21-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  M ) )   =>    |-  ( ph  ->  ( abs ` 
 sum_ i  e.  (
 ( M  +  1 ) ... N ) ( F `  i
 ) )  <_  (
 ( abs `  ( F `  M ) )  x. 
 sum_ i  e.  (
 ( M  +  1 ) ... N ) ( A ^ (
 i  -  M ) ) ) )
 
21-Nov-2022cvgratnnlemseq 10881 Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 21-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  M ) )   =>    |-  ( ph  ->  ( (  seq 1 (  +  ,  F ) `  N )  -  (  seq 1
 (  +  ,  F ) `  M ) )  =  sum_ i  e.  (
 ( M  +  1 ) ... N ) ( F `  i
 ) )
 
15-Nov-2022cvgratnnlemmn 10880 Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 15-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  e.  ( ZZ>=
 `  M ) )   =>    |-  ( ph  ->  ( abs `  ( F `  N ) )  <_  ( ( abs `  ( F `  M ) )  x.  ( A ^ ( N  -  M ) ) ) )
 
15-Nov-2022cvgratnnlemnexp 10879 Lemma for cvgratnn 10886. (Contributed by Jim Kingdon, 15-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   &    |-  ( ph  ->  N  e.  NN )   =>    |-  ( ph  ->  ( abs `  ( F `  N ) )  <_  ( ( abs `  ( F `  1 ) )  x.  ( A ^
 ( N  -  1
 ) ) ) )
 
12-Nov-2022cvgratnn 10886 Ratio test for convergence of a complex infinite series. If the ratio  A of the absolute values of successive terms in an infinite sequence  F is less than 1 for all terms, then the infinite sum of the terms of  F converges to a complex number. Although this theorem is similar to cvgratz 10887 and cvgratgt0 10888, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 10703 is sensitive to how a sequence is indexed. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 12-Nov-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   =>    |-  ( ph  ->  seq 1
 (  +  ,  F )  e.  dom  ~~>  )
 
12-Nov-2022fsum3cvg 10731 The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 12-Nov-2022.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  0 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  -> DECID  k  e.  A )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ph  ->  A 
 C_  ( M ... N ) )   =>    |-  ( ph  ->  seq M (  +  ,  F ) 
 ~~>  (  seq M (  +  ,  F ) `
  N ) )
 
12-Nov-2022seq3id2 9905 The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for  .+) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 12-Nov-2022.)
 |-  ( ( ph  /\  x  e.  S )  ->  ( x  .+  Z )  =  x )   &    |-  ( ph  ->  K  e.  ( ZZ>= `  M ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  K ) )   &    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ) `  K )  e.  S )   &    |-  (
 ( ph  /\  x  e.  ( ( K  +  1 ) ... N ) )  ->  ( F `
  x )  =  Z )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  e.  S )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ) `  K )  =  (  seq M (  .+  ,  F ) `  N ) )
 
11-Nov-2022cvgratgt0 10888 Ratio test for convergence of a complex infinite series. If the ratio  A of the absolute values of successive terms in an infinite sequence  F is less than 1 for all terms beyond some index  B, then the infinite sum of the terms of 
F converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  W  =  (
 ZZ>= `  N )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  ( ph  ->  N  e.  Z )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  W ) 
 ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   =>    |-  ( ph  ->  seq M (  +  ,  F )  e.  dom  ~~>  )
 
11-Nov-2022cvgratz 10887 Ratio test for convergence of a complex infinite series. If the ratio  A of the absolute values of successive terms in an infinite sequence  F is less than 1 for all terms, then the infinite sum of the terms of  F converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <  A )   &    |-  (
 ( ph  /\  k  e.  Z )  ->  ( F `  k )  e. 
 CC )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  ( abs `  ( F `  ( k  +  1 ) ) ) 
 <_  ( A  x.  ( abs `  ( F `  k ) ) ) )   =>    |-  ( ph  ->  seq M (  +  ,  F )  e.  dom  ~~>  )
 
4-Nov-2022seq3val 9839 Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 9845, seq3-1 9842 and seq3p1 9849, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  R  = frec (
 ( x  e.  ( ZZ>=
 `  M ) ,  y  e.  _V  |->  <.
 ( x  +  1 ) ,  ( x ( z  e.  ( ZZ>=
 `  M ) ,  w  e.  S  |->  ( w  .+  ( F `
  ( z  +  1 ) ) ) ) y ) >. ) ,  <. M ,  ( F `  M ) >. )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  seq M (  .+  ,  F )  =  ran  R )
 
4-Nov-2022dfseq3-2 9820 Define a general-purpose operation that builds a recursive sequence (i.e. a function on an upper integer set such as  NN or  NN0) whose value at an index is a function of its previous value and the value of an input sequence at that index. This definition is complicated, but fortunately it is not intended to be used directly. Instead, the only purpose of this definition is to provide us with an object that has the properties expressed by seqf 9845, seq3-1 9842 and seq3p1 9849. Typically, those are the main theorems that would be used in practice.

The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation  +, an input sequence  F with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence  seq 1 (  +  ,  F ) with values 1, 3/2, 7/4, 15/8,.., so that  (  seq 1
(  +  ,  F
) `  1 )  =  1,  (  seq 1 (  +  ,  F ) `  2
)  = 3/2, etc. In other words,  seq M (  +  ,  F ) transforms a sequence  F into an infinite series.

Internally, the frec function generates as its values a set of ordered pairs starting at 
<. M ,  ( F `
 M ) >., with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain.

Eventually, this will be the definition of  seq, replacing df-iseq 9818 and df-seq3 9819.

(Contributed by NM, 18-Apr-2005.) (Revised by Jim Kingdon, 4-Nov-2022.)

 |- 
 seq M (  .+  ,  F )  =  ran frec ( ( x  e.  ( ZZ>=
 `  M ) ,  y  e.  _V  |->  <.
 ( x  +  1 ) ,  ( y 
 .+  ( F `  ( x  +  1
 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. )
 
3-Nov-2022seq3f1o 9898 Rearrange a sum via an arbitrary bijection on  ( M ... N ). (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 3-Nov-2022.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  =  ( y  .+  x ) )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S ) )  ->  ( ( x  .+  y ) 
 .+  z )  =  ( x  .+  (
 y  .+  z )
 ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ph  ->  F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( G `  x )  e.  S )   &    |-  (
 ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( H `  x )  e.  S )   &    |-  ( ( ph  /\  k  e.  ( M ... N ) )  ->  ( H `
  k )  =  ( G `  ( F `  k ) ) )   =>    |-  ( ph  ->  (  seq M (  .+  ,  H ) `  N )  =  (  seq M (  .+  ,  G ) `  N ) )
 
3-Nov-2022seq3m1 9854 Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 3-Nov-2022.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1 )
 ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  e.  S )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ) `  N )  =  ( (  seq M (  .+  ,  F ) `  ( N  -  1 ) ) 
 .+  ( F `  N ) ) )
 
29-Oct-2022absgtap 10865 Greater-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  RR+ )   &    |-  ( ph  ->  B  <  ( abs `  A ) )   =>    |-  ( ph  ->  A #  B )
 
29-Oct-2022absltap 10864 Less-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  RR )   &    |-  ( ph  ->  ( abs `  A )  <  B )   =>    |-  ( ph  ->  A #  B )
 
29-Oct-20221ap2 8593 1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.)
 |-  1 #  2
 
28-Oct-2022expcnv 10859 A sequence of powers of a complex number  A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 28-Oct-2022.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  ( abs `  A )  <  1 )   =>    |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
 
28-Oct-2022expcnvre 10858 A sequence of powers of a nonnegative real number less than one converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  A  <  1 )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
 
24-Oct-2022pwm1geoserap1 10863 The n-th power of a number decreased by 1 expressed by the finite geometric series  1  +  A ^ 1  +  A ^ 2  +...  +  A ^ ( N  - 
1 ). (Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon, 24-Oct-2022.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  N  e.  NN0 )   &    |-  ( ph  ->  A #  1 )   =>    |-  ( ph  ->  (
 ( A ^ N )  -  1 )  =  ( ( A  -  1 )  x.  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( A ^ k
 ) ) )
 
24-Oct-2022geoserap 10862 The value of the finite geometric series  1  +  A ^
1  +  A ^
2  +...  +  A ^
( N  -  1 ). This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A #  1 )   &    |-  ( ph  ->  N  e.  NN0 )   =>    |-  ( ph  ->  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( A ^ k
 )  =  ( ( 1  -  ( A ^ N ) ) 
 /  ( 1  -  A ) ) )
 
24-Oct-2022geosergap 10861 The value of the finite geometric series  A ^ M  +  A ^ ( M  + 
1 )  +...  +  A ^
( N  -  1 ). (Contributed by Mario Carneiro, 2-May-2016.) (Revised by Jim Kingdon, 24-Oct-2022.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  A #  1 )   &    |-  ( ph  ->  M  e.  NN0 )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   =>    |-  ( ph  ->  sum_ k  e.  ( M..^ N ) ( A ^ k
 )  =  ( ( ( A ^ M )  -  ( A ^ N ) )  /  ( 1  -  A ) ) )
 
23-Oct-2022expcnvap0 10857 A sequence of powers of a complex number  A with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 23-Oct-2022.)
 |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  ( abs `  A )  <  1 )   &    |-  ( ph  ->  A #  0 )   =>    |-  ( ph  ->  ( n  e.  NN0  |->  ( A ^ n ) )  ~~>  0 )
 
22-Oct-2022divcnv 10852 The sequence of reciprocals of positive integers, multiplied by the factor  A, converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Jim Kingdon, 22-Oct-2022.)
 |-  ( A  e.  CC  ->  ( n  e.  NN  |->  ( A  /  n ) )  ~~>  0 )
 
21-Oct-2022isumsplit 10847 Split off the first  N terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.)
 |-  Z  =  ( ZZ>= `  M )   &    |-  W  =  (
 ZZ>= `  N )   &    |-  ( ph  ->  N  e.  Z )   &    |-  ( ( ph  /\  k  e.  Z )  ->  ( F `  k )  =  A )   &    |-  ( ( ph  /\  k  e.  Z ) 
 ->  A  e.  CC )   &    |-  ( ph  ->  seq M (  +  ,  F )  e.  dom  ~~>  )   =>    |-  ( ph  ->  sum_ k  e.  Z  A  =  (
 sum_ k  e.  ( M ... ( N  -  1 ) ) A  +  sum_ k  e.  W  A ) )
 
21-Oct-2022seq3split 9872 Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S )
 )  ->  ( ( x  .+  y )  .+  z )  =  ( x  .+  ( y  .+  z ) ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1 ) ) )   &    |-  ( ph  ->  M  e.  ( ZZ>= `  K ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  K ) )  ->  ( F `  x )  e.  S )   =>    |-  ( ph  ->  ( 
 seq K (  .+  ,  F ) `  N )  =  ( (  seq K (  .+  ,  F ) `  M )  .+  (  seq ( M  +  1 )
 (  .+  ,  F ) `  N ) ) )
 
20-Oct-2022fidcenumlemrk 6642 Lemma for fidcenum 6644. (Contributed by Jim Kingdon, 20-Oct-2022.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  N  e.  om )   &    |-  ( ph  ->  F : N -onto-> A )   &    |-  ( ph  ->  K  e.  om )   &    |-  ( ph  ->  K 
 C_  N )   &    |-  ( ph  ->  X  e.  A )   =>    |-  ( ph  ->  ( X  e.  ( F " K )  \/  -.  X  e.  ( F " K ) ) )
 
20-Oct-2022fidcenumlemrks 6641 Lemma for fidcenum 6644. Induction step for fidcenumlemrk 6642. (Contributed by Jim Kingdon, 20-Oct-2022.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  N  e.  om )   &    |-  ( ph  ->  F : N -onto-> A )   &    |-  ( ph  ->  J  e.  om )   &    |-  ( ph  ->  suc 
 J  C_  N )   &    |-  ( ph  ->  ( X  e.  ( F " J )  \/  -.  X  e.  ( F " J ) ) )   &    |-  ( ph  ->  X  e.  A )   =>    |-  ( ph  ->  ( X  e.  ( F
 " suc  J )  \/  -.  X  e.  ( F " suc  J ) ) )
 
19-Oct-2022fidcenum 6644 A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as  E. n  e. 
om E. f f : n -onto-> A is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.)
 |-  ( A  e.  Fin  <->  ( A. x  e.  A  A. y  e.  A DECID  x  =  y  /\  E. n  e.  om  E. f  f : n -onto-> A ) )
 
19-Oct-2022fidcenumlemr 6643 Lemma for fidcenum 6644. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.)
 |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )   &    |-  ( ph  ->  N  e.  om )   &    |-  ( ph  ->  F : N -onto-> A )   =>    |-  ( ph  ->  A  e.  Fin )
 
19-Oct-2022fidcenumlemim 6640 Lemma for fidcenum 6644. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.)
 |-  ( A  e.  Fin  ->  ( A. x  e.  A  A. y  e.  A DECID  x  =  y  /\  E. n  e.  om  E. f  f : n -onto-> A ) )
 
17-Oct-2022iser3shft 10699 Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.)
 |-  ( ph  ->  F  e.  V )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ZZ )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  (  seq M (  .+  ,  F )  ~~>  A  <->  seq ( M  +  N ) (  .+  ,  ( F  shift  N ) )  ~~>  A ) )
 
17-Oct-2022seq3shft 10237 Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 17-Oct-2022.)
 |-  ( ph  ->  F  e.  V )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  N  e.  ZZ )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  ( M  -  N ) ) ) 
 ->  ( F `  x )  e.  S )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  seq
 M (  .+  ,  ( F  shift  N ) )  =  (  seq ( M  -  N ) (  .+  ,  F )  shift  N ) )
 
17-Oct-2022seq3shft2 9864 Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 17-Oct-2022.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ph  ->  K  e.  ZZ )   &    |-  ( ( ph  /\  k  e.  ( M
 ... N ) ) 
 ->  ( F `  k
 )  =  ( G `
  ( k  +  K ) ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  ( M  +  K ) ) ) 
 ->  ( G `  x )  e.  S )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ) `  N )  =  (  seq ( M  +  K ) (  .+  ,  G ) `  ( N  +  K ) ) )
 
16-Oct-2022resqrexlemf1 10406 Lemma for resqrex 10424. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ph  ->  ( F `  1 )  =  ( 1  +  A ) )
 
16-Oct-2022resqrexlemf 10405 Lemma for resqrex 10424. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
 |-  F  =  seq 1
 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) ,  ( NN  X.  { ( 1  +  A ) }
 ) )   &    |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0  <_  A )   =>    |-  ( ph  ->  F : NN --> RR+ )
 
16-Oct-2022resqrexlemp1rp 10404 Lemma for resqrex 10424. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 9845 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0 
 <_  A )   =>    |-  ( ( ph  /\  ( B  e.  RR+  /\  C  e.  RR+ ) )  ->  ( B ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y
 ) )  /  2
 ) ) C )  e.  RR+ )
 
16-Oct-2022resqrexlem1arp 10403 Lemma for resqrex 10424.  1  +  A is a positive real (expressed in a way that will help apply seqf 9845 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
 |-  ( ph  ->  A  e.  RR )   &    |-  ( ph  ->  0 
 <_  A )   =>    |-  ( ( ph  /\  N  e.  NN )  ->  (
 ( NN  X.  {
 ( 1  +  A ) } ) `  N )  e.  RR+ )
 
16-Oct-2022seq3feq 9862 Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 16-Oct-2022.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  e.  S )   &    |-  (
 ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  =  ( G `  k ) )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x 
 .+  y )  e.  S )   =>    |-  ( ph  ->  seq M (  .+  ,  F )  =  seq M ( 
 .+  ,  G )
 )
 
15-Oct-2022inffz 11574 The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
 |-  ( N  e.  ( ZZ>= `  M )  -> inf ( ( M ... N ) ,  ZZ ,  <  )  =  M )
 
15-Oct-2022supfz 11573 The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.)
 |-  ( N  e.  ( ZZ>= `  M )  ->  sup (
 ( M ... N ) ,  ZZ ,  <  )  =  N )
 
12-Oct-2022fsumlessfi 10817 A shorter sum of nonnegative terms is no greater than a longer one. (Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon, 12-Oct-2022.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  RR )   &    |-  (
 ( ph  /\  k  e.  A )  ->  0  <_  B )   &    |-  ( ph  ->  C 
 C_  A )   &    |-  ( ph  ->  C  e.  Fin )   =>    |-  ( ph  ->  sum_ k  e.  C  B  <_  sum_ k  e.  A  B )
 
12-Oct-2022modfsummodlemstep 10814 Induction step for modfsummod 10815. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.)
 |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  A. k  e.  ( A  u.  { z }
 ) B  e.  ZZ )   &    |-  ( ph  ->  -.  z  e.  A )   &    |-  ( ph  ->  (
 sum_ k  e.  A  B  mod  N )  =  ( sum_ k  e.  A  ( B  mod  N ) 
 mod  N ) )   =>    |-  ( ph  ->  (
 sum_ k  e.  ( A  u.  { z }
 ) B  mod  N )  =  ( sum_ k  e.  ( A  u.  { z } ) ( B  mod  N ) 
 mod  N ) )
 
10-Oct-2022fsum3 10743 The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
 |-  ( k  =  ( F `  n ) 
 ->  B  =  C )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 M ) -1-1-onto-> A )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  n  e.  ( 1 ... M ) )  ->  ( G `
  n )  =  C )   =>    |-  ( ph  ->  sum_ k  e.  A  B  =  ( 
 seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 )
 ) ) `  M ) )
 
10-Oct-2022fsumgcl 10741 Closure for a function used to describe a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.)
 |-  ( k  =  ( F `  n ) 
 ->  B  =  C )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 M ) -1-1-onto-> A )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  n  e.  ( 1 ... M ) )  ->  ( G `
  n )  =  C )   =>    |-  ( ph  ->  A. n  e.  ( 1 ... M ) ( G `  n )  e.  CC )
 
10-Oct-2022seq3distr 9911 The distributive property for series. (Contributed by Jim Kingdon, 10-Oct-2022.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( C T ( x  .+  y ) )  =  ( ( C T x )  .+  ( C T y ) ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( G `  x )  e.  S )   &    |-  (
 ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  =  ( C T ( G `
  x ) ) )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x T y )  e.  S )   &    |-  ( ph  ->  C  e.  S )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ) `  N )  =  ( C T (  seq M ( 
 .+  ,  G ) `  N ) ) )
 
10-Oct-2022seq3homo 9909 Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 10-Oct-2022.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  S )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( H `  ( x  .+  y
 ) )  =  ( ( H `  x ) Q ( H `  y ) ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( H `  ( F `  x ) )  =  ( G `  x ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( G `  x )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x Q y )  e.  S )   =>    |-  ( ph  ->  ( H `  (  seq M (  .+  ,  F ) `
  N ) )  =  (  seq M ( Q ,  G ) `
  N ) )
 
8-Oct-2022fsum2dlemstep 10791 Lemma for fsum2d 10792- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.)
 |-  ( z  =  <. j ,  k >.  ->  D  =  C )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  j  e.  A )  ->  B  e.  Fin )   &    |-  ( ( ph  /\  ( j  e.  A  /\  k  e.  B ) )  ->  C  e.  CC )   &    |-  ( ph  ->  -.  y  e.  x )   &    |-  ( ph  ->  ( x  u.  { y } )  C_  A )   &    |-  ( ph  ->  x  e.  Fin )   &    |-  ( ps 
 <-> 
 sum_ j  e.  x  sum_
 k  e.  B  C  =  sum_ z  e.  U_  j  e.  x  ( { j }  X.  B ) D )   =>    |-  ( ( ph  /\  ps )  ->  sum_ j  e.  ( x  u.  { y }
 ) sum_ k  e.  B  C  =  sum_ z  e.  U_  j  e.  ( x  u.  { y }
 ) ( { j }  X.  B ) D )
 
7-Oct-2022iunfidisj 6634 The finite union of disjoint finite sets is finite. Note that  B depends on  x, i.e. can be thought of as  B ( x ). (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.)
 |-  ( ( A  e.  Fin  /\  A. x  e.  A  B  e.  Fin  /\ Disj  x  e.  A  B )  ->  U_ x  e.  A  B  e.  Fin )
 
7-Oct-2022disjnims 3829 If a collection  B ( i ) for  i  e.  A is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Jim Kingdon, 7-Oct-2022.)
 |-  (Disj  x  e.  A  B  ->  A. i  e.  A  A. j  e.  A  ( i  =/=  j  ->  ( [_ i  /  x ]_ B  i^i  [_ j  /  x ]_ B )  =  (/) ) )
 
6-Oct-2022disjnim 3828 If a collection  B ( i ) for  i  e.  A is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.)
 |-  ( i  =  j 
 ->  B  =  C )   =>    |-  (Disj  i  e.  A  B  ->  A. i  e.  A  A. j  e.  A  ( i  =/=  j  ->  ( B  i^i  C )  =  (/) ) )
 
5-Oct-2022dcun 3388 The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.)
 |-  ( ph  -> DECID  k  e.  A )   &    |-  ( ph  -> DECID  k  e.  B )   =>    |-  ( ph  -> DECID  k  e.  ( A  u.  B ) )
 
4-Oct-2022ser3add 9900 The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 4-Oct-2022.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( H `  k )  =  ( ( F `  k
 )  +  ( G `
  k ) ) )   =>    |-  ( ph  ->  (  seq M (  +  ,  H ) `  N )  =  ( (  seq M (  +  ,  F ) `  N )  +  (  seq M (  +  ,  G ) `  N ) ) )
 
4-Oct-2022iseqseq3 9867 Equality of  seq M (  +  ,  F ,  CC ) and  seq M (  +  ,  F ). (Contributed by Jim Kingdon, 4-Oct-2022.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  e.  CC )   =>    |-  ( ph  ->  seq
 M (  +  ,  F ,  CC )  =  seq M (  +  ,  F ) )
 
3-Oct-2022ser3le 9918 Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Jim Kingdon, 3-Oct-2022.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  e.  RR )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( G `  k )  e.  RR )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  <_  ( G `  k ) )   =>    |-  ( ph  ->  (  seq M (  +  ,  F ) `  N )  <_  (  seq M (  +  ,  G ) `  N ) )
 
3-Oct-2022seq3-1 9842 Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.)
 |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( F `  x )  e.  S )   &    |-  (
 ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x  .+  y )  e.  S )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ) `  M )  =  ( F `  M ) )
 
3-Oct-2022df-seq3 9819 Define a three-argument version of 
seq. By theorems such as iseqsst 9851, it should be capable of doing pretty much everything that the four-argument version can, and may eventually replace the four-argument version entirely. (Contributed by Jim Kingdon, 3-Oct-2022.)
 |- 
 seq M (  .+  ,  F )  =  seq M (  .+  ,  F ,  _V )
 
3-Oct-2022brrelex12i 4469 Two classes that are related by a binary relation are sets. (An artifact of our ordered pair definition.) (Contributed by BJ, 3-Oct-2022.)
 |- 
 Rel  R   =>    |-  ( A R B  ->  ( A  e.  _V  /\  B  e.  _V )
 )
 
1-Oct-2022fsum3ser 10754 A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 10769 and fsump1 10777, which should make our notation clear and from which, along with closure fsumcl 10757, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.)
 |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  =  A )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  A  e.  CC )   =>    |-  ( ph  ->  sum_ k  e.  ( M ... N ) A  =  (  seq M (  +  ,  F ) `  N ) )
 
1-Oct-2022fisumser 10753 A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 10769 and fsump1 10777, which should make our notation clear and from which, along with closure fsumcl 10757, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.) Use fsum3ser 10754 instead. (New usage is discouraged.)
 |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  ( F `  k )  =  A )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M )
 )  ->  A  e.  CC )   =>    |-  ( ph  ->  sum_ k  e.  ( M ... N ) A  =  (  seq M (  +  ,  F ,  CC ) `  N ) )
 
1-Oct-2022tpfidisj 6618 A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ph  ->  B  e.  W )   &    |-  ( ph  ->  C  e.  X )   &    |-  ( ph  ->  A  =/=  B )   &    |-  ( ph  ->  A  =/=  C )   &    |-  ( ph  ->  B  =/=  C )   =>    |-  ( ph  ->  { A ,  B ,  C }  e.  Fin )
 
28-Sep-2022seq3clss 9852 Closure property of the recursive sequence builder. (Contributed by Jim Kingdon, 28-Sep-2022.)
 |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( F `  x )  e.  T )   &    |-  ( ( ph  /\  x  e.  ( M ... N ) )  ->  ( F `
  x )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S ) )  ->  ( x 
 .+  y )  e.  S )   &    |-  ( ph  ->  S 
 C_  T )   &    |-  (
 ( ph  /\  ( x  e.  T  /\  y  e.  T ) )  ->  ( x  .+  y )  e.  T )   =>    |-  ( ph  ->  ( 
 seq M (  .+  ,  F ) `  N )  e.  S )
 
27-Sep-2022zmaxcl 10621 The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.)
 |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  sup ( { A ,  B } ,  RR ,  <  )  e.  ZZ )
 
24-Sep-2022isumss2 10749 Change the index set of a sum by adding zeroes. The nonzero elements are in the contained set  A and the added zeroes compose the rest of the containing set  B which needs to be summable. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ph  ->  A. j  e.  B DECID  j  e.  A )   &    |-  ( ph  ->  A. k  e.  A  C  e.  CC )   &    |-  ( ph  ->  ( ( M  e.  ZZ  /\  B  C_  ( ZZ>= `  M )  /\  A. j  e.  ( ZZ>= `  M )DECID  j  e.  B )  \/  B  e.  Fin ) )   =>    |-  ( ph  ->  sum_
 k  e.  A  C  =  sum_ k  e.  B  if ( k  e.  A ,  C ,  0 ) )
 
24-Sep-2022preimaf1ofi 6639 The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.)
 |-  ( ph  ->  C  C_  B )   &    |-  ( ph  ->  F : A -1-1-onto-> B )   &    |-  ( ph  ->  C  e.  Fin )   =>    |-  ( ph  ->  ( `' F " C )  e.  Fin )
 
24-Sep-2022ifmdc 3424 If a conditional class is inhabited, then the condition is decidable. This shows that conditionals are not very useful unless one can prove the condition decidable. (Contributed by BJ, 24-Sep-2022.)
 |-  ( A  e.  if ( ph ,  B ,  C )  -> DECID  ph )
 
23-Sep-2022fisumss 10748 Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  C  e.  CC )   &    |-  (
 ( ph  /\  k  e.  ( B  \  A ) )  ->  C  =  0 )   &    |-  ( ph  ->  A. j  e.  B DECID  j  e.  A )   &    |-  ( ph  ->  B  e.  Fin )   =>    |-  ( ph  ->  sum_
 k  e.  A  C  =  sum_ k  e.  B  C )
 
21-Sep-2022pw1dom2 11546 The power set of  1o dominates  2o. (Contributed by Jim Kingdon, 21-Sep-2022.)
 |-  2o  ~<_  ~P 1o
 
21-Sep-2022isumss 10747 Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 21-Sep-2022.)
 |-  ( ph  ->  A  C_  B )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  C  e.  CC )   &    |-  (
 ( ph  /\  k  e.  ( B  \  A ) )  ->  C  =  0 )   &    |-  ( ph  ->  A. j  e.  ( ZZ>= `  M )DECID  j  e.  A )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  B 
 C_  ( ZZ>= `  M ) )   &    |-  ( ph  ->  A. j  e.  ( ZZ>= `  M )DECID  j  e.  B )   =>    |-  ( ph  ->  sum_ k  e.  A  C  =  sum_ k  e.  B  C )
 
18-Sep-2022sumfct 10727 A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.)
 |-  ( A. k  e.  A  B  e.  CC  -> 
 sum_ j  e.  A  ( ( k  e.  A  |->  B ) `  j )  =  sum_ k  e.  A  B )
 
16-Sep-2022isumz 10745 Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 16-Sep-2022.)
 |-  ( ( ( M  e.  ZZ  /\  A  C_  ( ZZ>= `  M )  /\  A. j  e.  ( ZZ>=
 `  M )DECID  j  e.  A )  \/  A  e.  Fin )  ->  sum_ k  e.  A  0  =  0 )
 
16-Sep-2022fser0const 9916 Simplifying an expression which turns out just to be a constant zero sequence. (Contributed by Jim Kingdon, 16-Sep-2022.)
 |-  Z  =  ( ZZ>= `  M )   =>    |-  ( N  e.  Z  ->  ( n  e.  Z  |->  if ( n  <_  N ,  ( ( Z  X.  { 0 } ) `  n ) ,  0 ) )  =  ( Z  X.  { 0 } ) )
 
14-Sep-2022fisum 10742 The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 14-Sep-2022.) Use fsum3 10743 instead. (New usage is discouraged.)
 |-  ( k  =  ( F `  n ) 
 ->  B  =  C )   &    |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  F : ( 1 ...
 M ) -1-1-onto-> A )   &    |-  ( ( ph  /\  k  e.  A ) 
 ->  B  e.  CC )   &    |-  (
 ( ph  /\  n  e.  ( 1 ... M ) )  ->  ( G `
  n )  =  C )   =>    |-  ( ph  ->  sum_ k  e.  A  B  =  ( 
 seq 1 (  +  ,  ( n  e.  NN  |->  if ( n  <_  M ,  ( G `  n ) ,  0 )
 ) ,  CC ) `  M ) )
 
10-Sep-2022isummo 10737 A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 10-Sep-2022.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  0 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  G  =  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n )  /  k ]_ B ,  0 ) )   =>    |-  ( ph  ->  E* x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  ,  F ,  CC )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m )
 -1-1-onto-> A  /\  x  =  ( 
 seq 1 (  +  ,  G ,  CC ) `  m ) ) ) )
 
8-Sep-2022isummolem2 10736 Lemma for isummo 10737. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 8-Sep-2022.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  0 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  G  =  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n )  /  k ]_ B ,  0 ) )   =>    |-  ( ( ph  /\  E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  A. j  e.  ( ZZ>= `  m )DECID  j  e.  A  /\  seq m (  +  ,  F ,  CC )  ~~>  x )
 )  ->  ( E. m  e.  NN  E. f
 ( f : ( 1 ... m ) -1-1-onto-> A 
 /\  y  =  ( 
 seq 1 (  +  ,  G ,  CC ) `  m ) )  ->  x  =  y )
 )
 
8-Sep-2022zfz1isolemiso 10209 Lemma for zfz1iso 10211. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  X 
 C_  ZZ )   &    |-  ( ph  ->  M  e.  X )   &    |-  ( ph  ->  A. z  e.  X  z  <_  M )   &    |-  ( ph  ->  G  Isom  <  ,  <  ( ( 1
 ... ( `  ( X  \  { M } )
 ) ) ,  ( X  \  { M }
 ) ) )   &    |-  ( ph  ->  A  e.  (
 1 ... ( `  X ) ) )   &    |-  ( ph  ->  B  e.  (
 1 ... ( `  X ) ) )   =>    |-  ( ph  ->  ( A  <  B  <->  ( ( G  u.  { <. ( `  X ) ,  M >. } ) `  A )  <  ( ( G  u.  { <. ( `  X ) ,  M >. } ) `  B ) ) )
 
8-Sep-2022zfz1isolemsplit 10208 Lemma for zfz1iso 10211. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.)
 |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  M  e.  X )   =>    |-  ( ph  ->  ( 1 ... ( `  X ) )  =  (
 ( 1 ... ( `  ( X  \  { M } ) ) )  u.  { ( `  X ) } ) )
 
7-Sep-2022zfz1isolem1 10210 Lemma for zfz1iso 10211. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.)
 |-  ( ph  ->  K  e.  om )   &    |-  ( ph  ->  A. y ( ( ( y  C_  ZZ  /\  y  e.  Fin )  /\  y  ~~  K )  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( `  y ) ) ,  y ) ) )   &    |-  ( ph  ->  X  C_  ZZ )   &    |-  ( ph  ->  X  e.  Fin )   &    |-  ( ph  ->  X 
 ~~  suc  K )   &    |-  ( ph  ->  M  e.  X )   &    |-  ( ph  ->  A. z  e.  X  z  <_  M )   =>    |-  ( ph  ->  E. f  f  Isom  <  ,  <  ( ( 1 ... ( `  X ) ) ,  X ) )
 
6-Sep-2022fimaxq 10200 A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.)
 |-  ( ( A  C_  QQ  /\  A  e.  Fin  /\  A  =/=  (/) )  ->  E. x  e.  A  A. y  e.  A  y 
 <_  x )
 
5-Sep-2022fimax2gtri 6597 A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.)
 |-  ( ph  ->  R  Po  A )   &    |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  A  =/= 
 (/) )   =>    |-  ( ph  ->  E. x  e.  A  A. y  e.  A  -.  x R y )
 
5-Sep-2022fimax2gtrilemstep 6596 Lemma for fimax2gtri 6597. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.)
 |-  ( ph  ->  R  Po  A )   &    |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )   &    |-  ( ph  ->  A  e.  Fin )   &    |-  ( ph  ->  A  =/= 
 (/) )   &    |-  ( ph  ->  U  e.  Fin )   &    |-  ( ph  ->  U  C_  A )   &    |-  ( ph  ->  Z  e.  A )   &    |-  ( ph  ->  V  e.  A )   &    |-  ( ph  ->  -.  V  e.  U )   &    |-  ( ph  ->  A. y  e.  U  -.  Z R y )   =>    |-  ( ph  ->  E. x  e.  A  A. y  e.  ( U  u.  { V } )  -.  x R y )
 
5-Sep-2022tridc 6595 A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.)
 |-  ( ph  ->  R  Po  A )   &    |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )   &    |-  ( ph  ->  B  e.  A )   &    |-  ( ph  ->  C  e.  A )   =>    |-  ( ph  -> DECID  B R C )
 
3-Sep-2022isummolem2a 10735 Lemma for isummo 10737. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 3-Sep-2022.)
 |-  F  =  ( k  e.  ZZ  |->  if (
 k  e.  A ,  B ,  0 )
 )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  CC )   &    |-  ( ( ph  /\  k  e.  ( ZZ>= `  M ) )  -> DECID  k  e.  A )   &    |-  G  =  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n )  /  k ]_ B ,  0 ) )   &    |-  H  =  ( n  e.  NN  |->  if ( n  <_  N ,  [_ ( K `
  n )  /  k ]_ B ,  0 ) )   &    |-  ( ph  ->  N  e.  NN )   &    |-  ( ph  ->  M  e.  ZZ )   &    |-  ( ph  ->  A  C_  ( ZZ>= `  M )
 )   &    |-  ( ph  ->  f : ( 1 ...
 N ) -1-1-onto-> A )   &    |-  ( ph  ->  K 
 Isom  <  ,  <  (
 ( 1 ... ( `  A ) ) ,  A ) )   =>    |-  ( ph  ->  seq
 M (  +  ,  F ,  CC )  ~~>  (  seq 1 (  +  ,  G ,  CC ) `  N ) )
 
3-Sep-2022zfz1iso 10211 A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
 |-  ( ( A  C_  ZZ  /\  A  e.  Fin )  ->  E. f  f  Isom  <  ,  <  ( ( 1
 ... ( `  A )
 ) ,  A ) )
 
1-Sep-2022ssidd 3043 Weakening of ssid 3042. (Contributed by BJ, 1-Sep-2022.)
 |-  ( ph  ->  A  C_  A )
 
31-Aug-2022fveqeq2 5298 Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.)
 |-  ( A  =  B  ->  ( ( F `  A )  =  C  <->  ( F `  B )  =  C ) )
 
30-Aug-2022iseqf1olemfvp 9891 Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 30-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  T : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ph  ->  A  e.  ( M ... N ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( G `  x )  e.  S )   &    |-  P  =  ( x  e.  ( ZZ>=
 `  M )  |->  if ( x  <_  N ,  ( G `  (
 f `  x )
 ) ,  ( G `
  M ) ) )   =>    |-  ( ph  ->  ( [_ T  /  f ]_ P `  A )  =  ( G `  ( T `  A ) ) )
 
30-Aug-2022fveqeq2d 5297 Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.)
 |-  ( ph  ->  A  =  B )   =>    |-  ( ph  ->  (
 ( F `  A )  =  C  <->  ( F `  B )  =  C ) )
 
29-Aug-2022seq3f1olemqsumkj 9892 Lemma for seq3f1o 9898. 
Q gives the same sum as 
J in the range  ( K ... ( `' J `  K ) ). (Contributed by Jim Kingdon, 29-Aug-2022.)
 |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  e.  S )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S )
 )  ->  ( x  .+  y )  =  ( y  .+  x ) )   &    |-  ( ( ph  /\  ( x  e.  S  /\  y  e.  S  /\  z  e.  S ) )  ->  ( ( x  .+  y ) 
 .+  z )  =  ( x  .+  (
 y  .+  z )
 ) )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )   &    |-  ( ph  ->  F : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( G `  x )  e.  S )   &    |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J :
 ( M ... N )
 -1-1-onto-> ( M ... N ) )   &    |-  ( ph  ->  A. x  e.  ( M..^ K ) ( J `
  x )  =  x )   &    |-  ( ph  ->  K  =/=  ( `' J `  K ) )   &    |-  Q  =  ( u  e.  ( M ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   &    |-  P  =  ( x  e.  ( ZZ>= `  M )  |->  if ( x  <_  N ,  ( G `  ( f `  x ) ) ,  ( G `  M ) ) )   =>    |-  ( ph  ->  ( 
 seq K (  .+  , 
 [_ J  /  f ]_ P ) `  ( `' J `  K ) )  =  (  seq K (  .+  ,  [_ Q  /  f ]_ P ) `  ( `' J `  K ) ) )
 
29-Aug-2022iseqf1olemqpcl 9890 Lemma for seq3f1o 9898. A closure lemma involving  Q and  P. (Contributed by Jim Kingdon, 29-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  Q  =  ( u  e.  ( M
 ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( G `  x )  e.  S )   &    |-  P  =  ( x  e.  ( ZZ>=
 `  M )  |->  if ( x  <_  N ,  ( G `  (
 f `  x )
 ) ,  ( G `
  M ) ) )   =>    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( [_ Q  /  f ]_ P `  x )  e.  S )
 
29-Aug-2022iseqf1olemjpcl 9889 Lemma for seq3f1o 9898. A closure lemma involving  J and  P. (Contributed by Jim Kingdon, 29-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  Q  =  ( u  e.  ( M
 ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   &    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M ) )  ->  ( G `  x )  e.  S )   &    |-  P  =  ( x  e.  ( ZZ>=
 `  M )  |->  if ( x  <_  N ,  ( G `  (
 f `  x )
 ) ,  ( G `
  M ) ) )   =>    |-  ( ( ph  /\  x  e.  ( ZZ>= `  M )
 )  ->  ( [_ J  /  f ]_ P `  x )  e.  S )
 
28-Aug-2022iseqf1olemqval 9881 Lemma for seq3f1o 9898. Value of the function  Q. (Contributed by Jim Kingdon, 28-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ph  ->  A  e.  ( M ... N ) )   &    |-  Q  =  ( u  e.  ( M
 ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   =>    |-  ( ph  ->  ( Q `  A )  =  if ( A  e.  ( K ... ( `' J `  K ) ) ,  if ( A  =  K ,  K ,  ( J `  ( A  -  1
 ) ) ) ,  ( J `  A ) ) )
 
27-Aug-2022iseqf1olemmo 9886 Lemma for seq3f1o 9898. Showing that  Q is one-to-one. (Contributed by Jim Kingdon, 27-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  Q  =  ( u  e.  ( M
 ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   &    |-  ( ph  ->  A  e.  ( M ... N ) )   &    |-  ( ph  ->  B  e.  ( M ... N ) )   &    |-  ( ph  ->  ( Q `  A )  =  ( Q `  B ) )   =>    |-  ( ph  ->  A  =  B )
 
27-Aug-2022iseqf1olemnanb 9884 Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ph  ->  A  e.  ( M ... N ) )   &    |-  ( ph  ->  B  e.  ( M ... N ) )   &    |-  ( ph  ->  ( Q `  A )  =  ( Q `  B ) )   &    |-  Q  =  ( u  e.  ( M ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   &    |-  ( ph  ->  -.  A  e.  ( K
 ... ( `' J `  K ) ) )   &    |-  ( ph  ->  -.  B  e.  ( K ... ( `' J `  K ) ) )   =>    |-  ( ph  ->  A  =  B )
 
27-Aug-2022iseqf1olemab 9883 Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ph  ->  A  e.  ( M ... N ) )   &    |-  ( ph  ->  B  e.  ( M ... N ) )   &    |-  ( ph  ->  ( Q `  A )  =  ( Q `  B ) )   &    |-  Q  =  ( u  e.  ( M ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   &    |-  ( ph  ->  A  e.  ( K ... ( `' J `  K ) ) )   &    |-  ( ph  ->  B  e.  ( K ... ( `' J `  K ) ) )   =>    |-  ( ph  ->  A  =  B )
 
27-Aug-2022iseqf1olemnab 9882 Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ph  ->  A  e.  ( M ... N ) )   &    |-  ( ph  ->  B  e.  ( M ... N ) )   &    |-  ( ph  ->  ( Q `  A )  =  ( Q `  B ) )   &    |-  Q  =  ( u  e.  ( M ... N )  |->  if ( u  e.  ( K ... ( `' J `  K ) ) ,  if ( u  =  K ,  K ,  ( J `  ( u  -  1 ) ) ) ,  ( J `
  u ) ) )   =>    |-  ( ph  ->  -.  ( A  e.  ( K ... ( `' J `  K ) )  /\  -.  B  e.  ( K
 ... ( `' J `  K ) ) ) )
 
27-Aug-2022iseqf1olemqcl 9880 Lemma for seq3f1o 9898. (Contributed by Jim Kingdon, 27-Aug-2022.)
 |-  ( ph  ->  K  e.  ( M ... N ) )   &    |-  ( ph  ->  J : ( M ... N ) -1-1-onto-> ( M ... N ) )   &    |-  ( ph  ->  A  e.  ( M ... N ) )   =>    |-  ( ph  ->  if ( A  e.  ( K ... ( `' J `  K ) ) ,  if ( A  =  K ,  K ,  ( J `  ( A  -  1 ) ) ) ,  ( J `
  A ) )  e.  ( M ... N ) )

  Copyright terms: Public domain W3C HTML validation [external]