ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isummolem2a Unicode version

Theorem isummolem2a 10735
Description: Lemma for isummo 10737. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 3-Sep-2022.)
Hypotheses
Ref Expression
isummo.1  |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )
isummo.2  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  CC )
isummolem2a.dc  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  -> DECID  k  e.  A
)
isummolem2a.g  |-  G  =  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
isummolem2a.h  |-  H  =  ( n  e.  NN  |->  if ( n  <_  N ,  [_ ( K `  n )  /  k ]_ B ,  0 ) )
summolem2.5  |-  ( ph  ->  N  e.  NN )
summolem2.6  |-  ( ph  ->  M  e.  ZZ )
summolem2.7  |-  ( ph  ->  A  C_  ( ZZ>= `  M ) )
summolem2.8  |-  ( ph  ->  f : ( 1 ... N ) -1-1-onto-> A )
summolem2.9  |-  ( ph  ->  K  Isom  <  ,  <  ( ( 1 ... ( `  A ) ) ,  A ) )
Assertion
Ref Expression
isummolem2a  |-  ( ph  ->  seq M (  +  ,  F ,  CC ) 
~~>  (  seq 1
(  +  ,  G ,  CC ) `  N
) )
Distinct variable groups:    k, n, A   
n, F    k, N, n    ph, k, n    k, M, n    B, n    k, F    k, K, n    f,
k, n
Allowed substitution hints:    ph( f)    A( f)    B( f, k)    F( f)    G( f, k, n)    H( f, k, n)    K( f)    M( f)    N( f)

Proof of Theorem isummolem2a
Dummy variables  m  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isummo.1 . . 3  |-  F  =  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )
2 isummo.2 . . 3  |-  ( (
ph  /\  k  e.  A )  ->  B  e.  CC )
3 isummolem2a.dc . . 3  |-  ( (
ph  /\  k  e.  ( ZZ>= `  M )
)  -> DECID  k  e.  A
)
4 summolem2.7 . . . 4  |-  ( ph  ->  A  C_  ( ZZ>= `  M ) )
5 summolem2.9 . . . . . . . 8  |-  ( ph  ->  K  Isom  <  ,  <  ( ( 1 ... ( `  A ) ) ,  A ) )
6 1zzd 8747 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  ZZ )
7 summolem2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN )
87nnzd 8837 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ZZ )
96, 8fzfigd 9803 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
10 summolem2.8 . . . . . . . . . . . 12  |-  ( ph  ->  f : ( 1 ... N ) -1-1-onto-> A )
119, 10fihasheqf1od 10163 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  ( `  A )
)
12 nnnn0 8650 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  NN0 )
13 hashfz1 10156 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( `  (
1 ... N ) )  =  N )
147, 12, 133syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  N )
1511, 14eqtr3d 2122 . . . . . . . . . 10  |-  ( ph  ->  ( `  A )  =  N )
1615oveq2d 5650 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( `  A ) )  =  ( 1 ... N
) )
17 isoeq4 5565 . . . . . . . . 9  |-  ( ( 1 ... ( `  A
) )  =  ( 1 ... N )  ->  ( K  Isom  <  ,  <  ( ( 1 ... ( `  A
) ) ,  A
)  <->  K  Isom  <  ,  <  ( ( 1 ... N ) ,  A
) ) )
1816, 17syl 14 . . . . . . . 8  |-  ( ph  ->  ( K  Isom  <  ,  <  ( ( 1 ... ( `  A
) ) ,  A
)  <->  K  Isom  <  ,  <  ( ( 1 ... N ) ,  A
) ) )
195, 18mpbid 145 . . . . . . 7  |-  ( ph  ->  K  Isom  <  ,  <  ( ( 1 ... N
) ,  A ) )
20 isof1o 5568 . . . . . . 7  |-  ( K 
Isom  <  ,  <  (
( 1 ... N
) ,  A )  ->  K : ( 1 ... N ) -1-1-onto-> A )
2119, 20syl 14 . . . . . 6  |-  ( ph  ->  K : ( 1 ... N ) -1-1-onto-> A )
22 f1of 5237 . . . . . 6  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  K :
( 1 ... N
) --> A )
2321, 22syl 14 . . . . 5  |-  ( ph  ->  K : ( 1 ... N ) --> A )
24 nnuz 9023 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
257, 24syl6eleq 2180 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
26 eluzfz2 9415 . . . . . 6  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
2725, 26syl 14 . . . . 5  |-  ( ph  ->  N  e.  ( 1 ... N ) )
2823, 27ffvelrnd 5419 . . . 4  |-  ( ph  ->  ( K `  N
)  e.  A )
294, 28sseldd 3024 . . 3  |-  ( ph  ->  ( K `  N
)  e.  ( ZZ>= `  M ) )
304sselda 3023 . . . . . 6  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ( ZZ>= `  M )
)
31 f1ocnvfv2 5539 . . . . . . . . 9  |-  ( ( K : ( 1 ... N ) -1-1-onto-> A  /\  n  e.  A )  ->  ( K `  ( `' K `  n ) )  =  n )
3221, 31sylan 277 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  ( `' K `  n )
)  =  n )
33 f1ocnv 5250 . . . . . . . . . . . 12  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  `' K : A -1-1-onto-> ( 1 ... N
) )
34 f1of 5237 . . . . . . . . . . . 12  |-  ( `' K : A -1-1-onto-> ( 1 ... N )  ->  `' K : A --> ( 1 ... N ) )
3521, 33, 343syl 17 . . . . . . . . . . 11  |-  ( ph  ->  `' K : A --> ( 1 ... N ) )
3635ffvelrnda 5418 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  ( `' K `  n )  e.  ( 1 ... N ) )
37 elfzle2 9411 . . . . . . . . . 10  |-  ( ( `' K `  n )  e.  ( 1 ... N )  ->  ( `' K `  n )  <_  N )
3836, 37syl 14 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  A )  ->  ( `' K `  n )  <_  N )
3919adantr 270 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  K  Isom  <  ,  <  (
( 1 ... N
) ,  A ) )
40 fzssuz 9447 . . . . . . . . . . . . 13  |-  ( 1 ... N )  C_  ( ZZ>= `  1 )
41 uzssz 9007 . . . . . . . . . . . . . 14  |-  ( ZZ>= ` 
1 )  C_  ZZ
42 zssre 8727 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
4341, 42sstri 3032 . . . . . . . . . . . . 13  |-  ( ZZ>= ` 
1 )  C_  RR
4440, 43sstri 3032 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  RR
45 ressxr 7510 . . . . . . . . . . . 12  |-  RR  C_  RR*
4644, 45sstri 3032 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  RR*
4746a1i 9 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  (
1 ... N )  C_  RR* )
484adantr 270 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  A )  ->  A  C_  ( ZZ>= `  M )
)
49 uzssz 9007 . . . . . . . . . . . . 13  |-  ( ZZ>= `  M )  C_  ZZ
5049, 42sstri 3032 . . . . . . . . . . . 12  |-  ( ZZ>= `  M )  C_  RR
5148, 50syl6ss 3035 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  A )  ->  A  C_  RR )
5251, 45syl6ss 3035 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  A  C_ 
RR* )
5327adantr 270 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  N  e.  ( 1 ... N
) )
54 leisorel 10207 . . . . . . . . . 10  |-  ( ( K  Isom  <  ,  <  ( ( 1 ... N
) ,  A )  /\  ( ( 1 ... N )  C_  RR* 
/\  A  C_  RR* )  /\  ( ( `' K `  n )  e.  ( 1 ... N )  /\  N  e.  ( 1 ... N ) ) )  ->  (
( `' K `  n )  <_  N  <->  ( K `  ( `' K `  n ) )  <_  ( K `  N ) ) )
5539, 47, 52, 36, 53, 54syl122anc 1183 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  A )  ->  (
( `' K `  n )  <_  N  <->  ( K `  ( `' K `  n ) )  <_  ( K `  N ) ) )
5638, 55mpbid 145 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  ( `' K `  n )
)  <_  ( K `  N ) )
5732, 56eqbrtrrd 3859 . . . . . . 7  |-  ( (
ph  /\  n  e.  A )  ->  n  <_  ( K `  N
) )
58 eluzelz 8997 . . . . . . . . 9  |-  ( n  e.  ( ZZ>= `  M
)  ->  n  e.  ZZ )
5930, 58syl 14 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ZZ )
60 eluzelz 8997 . . . . . . . . . 10  |-  ( ( K `  N )  e.  ( ZZ>= `  M
)  ->  ( K `  N )  e.  ZZ )
6129, 60syl 14 . . . . . . . . 9  |-  ( ph  ->  ( K `  N
)  e.  ZZ )
6261adantr 270 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  N )  e.  ZZ )
63 eluz 9001 . . . . . . . 8  |-  ( ( n  e.  ZZ  /\  ( K `  N )  e.  ZZ )  -> 
( ( K `  N )  e.  (
ZZ>= `  n )  <->  n  <_  ( K `  N ) ) )
6459, 62, 63syl2anc 403 . . . . . . 7  |-  ( (
ph  /\  n  e.  A )  ->  (
( K `  N
)  e.  ( ZZ>= `  n )  <->  n  <_  ( K `  N ) ) )
6557, 64mpbird 165 . . . . . 6  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  N )  e.  ( ZZ>= `  n )
)
66 elfzuzb 9403 . . . . . 6  |-  ( n  e.  ( M ... ( K `  N ) )  <->  ( n  e.  ( ZZ>= `  M )  /\  ( K `  N
)  e.  ( ZZ>= `  n ) ) )
6730, 65, 66sylanbrc 408 . . . . 5  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ( M ... ( K `  N )
) )
6867ex 113 . . . 4  |-  ( ph  ->  ( n  e.  A  ->  n  e.  ( M ... ( K `  N ) ) ) )
6968ssrdv 3029 . . 3  |-  ( ph  ->  A  C_  ( M ... ( K `  N
) ) )
701, 2, 3, 29, 69fisumcvg 10730 . 2  |-  ( ph  ->  seq M (  +  ,  F ,  CC ) 
~~>  (  seq M (  +  ,  F ,  CC ) `  ( K `
 N ) ) )
71 addid2 7600 . . . . 5  |-  ( m  e.  CC  ->  (
0  +  m )  =  m )
7271adantl 271 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( 0  +  m )  =  m )
73 addid1 7599 . . . . 5  |-  ( m  e.  CC  ->  (
m  +  0 )  =  m )
7473adantl 271 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( m  +  0 )  =  m )
75 addcl 7446 . . . . 5  |-  ( ( m  e.  CC  /\  x  e.  CC )  ->  ( m  +  x
)  e.  CC )
7675adantl 271 . . . 4  |-  ( (
ph  /\  ( m  e.  CC  /\  x  e.  CC ) )  -> 
( m  +  x
)  e.  CC )
77 0cnd 7460 . . . 4  |-  ( ph  ->  0  e.  CC )
7827, 16eleqtrrd 2167 . . . 4  |-  ( ph  ->  N  e.  ( 1 ... ( `  A
) ) )
79 iftrue 3394 . . . . . . . . . . . 12  |-  ( k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  =  B )
8079adantl 271 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  =  B )
8180, 2eqeltrd 2164 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8281adantlr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8382adantlr 461 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>=
`  M ) )  /\  k  e.  A
)  ->  if (
k  e.  A ,  B ,  0 )  e.  CC )
84 iffalse 3397 . . . . . . . . . 10  |-  ( -.  k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  =  0 )
85 0cn 7459 . . . . . . . . . 10  |-  0  e.  CC
8684, 85syl6eqel 2178 . . . . . . . . 9  |-  ( -.  k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8786adantl 271 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>=
`  M ) )  /\  -.  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
883adantlr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  -> DECID  k  e.  A
)
89 exmiddc 782 . . . . . . . . 9  |-  (DECID  k  e.  A  ->  ( k  e.  A  \/  -.  k  e.  A )
)
9088, 89syl 14 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  ->  ( k  e.  A  \/  -.  k  e.  A )
)
9183, 87, 90mpjaodan 747 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  e.  A ,  B ,  0 )  e.  CC )
92 simpll 496 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  ph )
93 simpr 108 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  -.  k  e.  ( ZZ>=
`  M ) )
944ssneld 3025 . . . . . . . . 9  |-  ( ph  ->  ( -.  k  e.  ( ZZ>= `  M )  ->  -.  k  e.  A
) )
9592, 93, 94sylc 61 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  -.  k  e.  A
)
9695, 86syl 14 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
97 summolem2.6 . . . . . . . . 9  |-  ( ph  ->  M  e.  ZZ )
98 eluzdc 9066 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  -> DECID  k  e.  ( ZZ>= `  M
) )
9997, 98sylan 277 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ZZ )  -> DECID  k  e.  ( ZZ>=
`  M ) )
100 exmiddc 782 . . . . . . . 8  |-  (DECID  k  e.  ( ZZ>= `  M )  ->  ( k  e.  (
ZZ>= `  M )  \/ 
-.  k  e.  (
ZZ>= `  M ) ) )
10199, 100syl 14 . . . . . . 7  |-  ( (
ph  /\  k  e.  ZZ )  ->  ( k  e.  ( ZZ>= `  M
)  \/  -.  k  e.  ( ZZ>= `  M )
) )
10291, 96, 101mpjaodan 747 . . . . . 6  |-  ( (
ph  /\  k  e.  ZZ )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
103102, 1fmptd 5436 . . . . 5  |-  ( ph  ->  F : ZZ --> CC )
104 eluzelz 8997 . . . . 5  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
105 ffvelrn 5416 . . . . 5  |-  ( ( F : ZZ --> CC  /\  m  e.  ZZ )  ->  ( F `  m
)  e.  CC )
106103, 104, 105syl2an 283 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( F `  m )  e.  CC )
107 elnnuz 9024 . . . . . . . 8  |-  ( m  e.  NN  <->  m  e.  ( ZZ>= `  1 )
)
108107biimpri 131 . . . . . . 7  |-  ( m  e.  ( ZZ>= `  1
)  ->  m  e.  NN )
109108adantl 271 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  m  e.  NN )
110 isof1o 5568 . . . . . . . . . . . 12  |-  ( K 
Isom  <  ,  <  (
( 1 ... ( `  A ) ) ,  A )  ->  K : ( 1 ... ( `  A )
)
-1-1-onto-> A )
111 f1of 5237 . . . . . . . . . . . 12  |-  ( K : ( 1 ... ( `  A )
)
-1-1-onto-> A  ->  K : ( 1 ... ( `  A
) ) --> A )
1125, 110, 1113syl 17 . . . . . . . . . . 11  |-  ( ph  ->  K : ( 1 ... ( `  A
) ) --> A )
113112ad2antrr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  K :
( 1 ... ( `  A ) ) --> A )
114 1zzd 8747 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  1  e.  ZZ )
11515, 8eqeltrd 2164 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `  A )  e.  ZZ )
116115ad2antrr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( `  A
)  e.  ZZ )
117 eluzelz 8997 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  m  e.  ZZ )
118117ad2antlr 473 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ZZ )
119114, 116, 1183jca 1123 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  m  e.  ZZ ) )
120 eluzle 9000 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  1  <_  m )
121120ad2antlr 473 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  1  <_  m )
122 simpr 108 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  <_  N )
12315breq2d 3849 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  <_  ( `  A )  <->  m  <_  N ) )
124123ad2antrr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( m  <_  ( `  A )  <->  m  <_  N ) )
125122, 124mpbird 165 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  <_  ( `  A ) )
126121, 125jca 300 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( 1  <_  m  /\  m  <_  ( `  A )
) )
127 elfz2 9400 . . . . . . . . . . 11  |-  ( m  e.  ( 1 ... ( `  A )
)  <->  ( ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  m  e.  ZZ )  /\  ( 1  <_  m  /\  m  <_  ( `  A ) ) ) )
128119, 126, 127sylanbrc 408 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ( 1 ... ( `  A ) ) )
129113, 128ffvelrnd 5419 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
130129iftrued 3396 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  if (
( K `  m
)  e.  A ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  =  [_ ( K `
 m )  / 
k ]_ B )
1314ad2antrr 472 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  A  C_  ( ZZ>=
`  M ) )
13223ad2antrr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  K :
( 1 ... N
) --> A )
13316eleq2d 2157 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  e.  ( 1 ... ( `  A
) )  <->  m  e.  ( 1 ... N
) ) )
134133ad2antrr 472 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( m  e.  ( 1 ... ( `  A ) )  <->  m  e.  ( 1 ... N
) ) )
135128, 134mpbid 145 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ( 1 ... N
) )
136132, 135ffvelrnd 5419 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
137131, 136sseldd 3024 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  (
ZZ>= `  M ) )
13849, 137sseldi 3021 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  ZZ )
139102ralrimiva 2446 . . . . . . . . . 10  |-  ( ph  ->  A. k  e.  ZZ  if ( k  e.  A ,  B ,  0 )  e.  CC )
140139ad2antrr 472 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  A. k  e.  ZZ  if ( k  e.  A ,  B ,  0 )  e.  CC )
141 nfv 1466 . . . . . . . . . . . 12  |-  F/ k ( K `  m
)  e.  A
142 nfcsb1v 2961 . . . . . . . . . . . 12  |-  F/_ k [_ ( K `  m
)  /  k ]_ B
143 nfcv 2228 . . . . . . . . . . . 12  |-  F/_ k
0
144141, 142, 143nfif 3415 . . . . . . . . . . 11  |-  F/_ k if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )
145144nfel1 2239 . . . . . . . . . 10  |-  F/ k if ( ( K `
 m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )  e.  CC
146 eleq1 2150 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  (
k  e.  A  <->  ( K `  m )  e.  A
) )
147 csbeq1a 2939 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  B  =  [_ ( K `  m )  /  k ]_ B )
148146, 147ifbieq1d 3409 . . . . . . . . . . 11  |-  ( k  =  ( K `  m )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
149148eleq1d 2156 . . . . . . . . . 10  |-  ( k  =  ( K `  m )  ->  ( if ( k  e.  A ,  B ,  0 )  e.  CC  <->  if (
( K `  m
)  e.  A ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  e.  CC ) )
150145, 149rspc 2716 . . . . . . . . 9  |-  ( ( K `  m )  e.  ZZ  ->  ( A. k  e.  ZZ  if ( k  e.  A ,  B ,  0 )  e.  CC  ->  if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )  e.  CC ) )
151138, 140, 150sylc 61 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  if (
( K `  m
)  e.  A ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  e.  CC )
152130, 151eqeltrrd 2165 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  [_ ( K `
 m )  / 
k ]_ B  e.  CC )
153 0cnd 7460 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  -.  m  <_  N )  ->  0  e.  CC )
154109nnzd 8837 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  m  e.  ZZ )
1558adantr 270 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  N  e.  ZZ )
156 zdcle 8793 . . . . . . . 8  |-  ( ( m  e.  ZZ  /\  N  e.  ZZ )  -> DECID  m  <_  N )
157154, 155, 156syl2anc 403 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  -> DECID  m  <_  N )
158152, 153, 157ifcldadc 3416 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  if (
m  <_  N ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  e.  CC )
159 breq1 3840 . . . . . . . 8  |-  ( n  =  m  ->  (
n  <_  N  <->  m  <_  N ) )
160 fveq2 5289 . . . . . . . . 9  |-  ( n  =  m  ->  ( K `  n )  =  ( K `  m ) )
161160csbeq1d 2937 . . . . . . . 8  |-  ( n  =  m  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  m )  /  k ]_ B )
162159, 161ifbieq1d 3409 . . . . . . 7  |-  ( n  =  m  ->  if ( n  <_  N ,  [_ ( K `  n
)  /  k ]_ B ,  0 )  =  if ( m  <_  N ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
163 isummolem2a.h . . . . . . 7  |-  H  =  ( n  e.  NN  |->  if ( n  <_  N ,  [_ ( K `  n )  /  k ]_ B ,  0 ) )
164162, 163fvmptg 5364 . . . . . 6  |-  ( ( m  e.  NN  /\  if ( m  <_  N ,  [_ ( K `  m )  /  k ]_ B ,  0 )  e.  CC )  -> 
( H `  m
)  =  if ( m  <_  N ,  [_ ( K `  m
)  /  k ]_ B ,  0 ) )
165109, 158, 164syl2anc 403 . . . . 5  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  ( H `  m )  =  if ( m  <_  N ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
166165, 158eqeltrd 2164 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  ( H `  m )  e.  CC )
167 fveqeq2 5298 . . . . . 6  |-  ( k  =  m  ->  (
( F `  k
)  =  0  <->  ( F `  m )  =  0 ) )
168 eldifi 3120 . . . . . . . . 9  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ( M ... ( K `
 ( `  A
) ) ) )
169 elfzelz 9409 . . . . . . . . 9  |-  ( k  e.  ( M ... ( K `  ( `  A
) ) )  -> 
k  e.  ZZ )
170168, 169syl 14 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ZZ )
171 eldifn 3121 . . . . . . . . . 10  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  -.  k  e.  A )
172171, 84syl 14 . . . . . . . . 9  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  if ( k  e.  A ,  B ,  0 )  =  0 )
173172, 85syl6eqel 2178 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
1741fvmpt2 5370 . . . . . . . 8  |-  ( ( k  e.  ZZ  /\  if ( k  e.  A ,  B ,  0 )  e.  CC )  -> 
( F `  k
)  =  if ( k  e.  A ,  B ,  0 ) )
175170, 173, 174syl2anc 403 . . . . . . 7  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  k )  =  if ( k  e.  A ,  B ,  0 ) )
176175, 172eqtrd 2120 . . . . . 6  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  k )  =  0 )
177167, 176vtoclga 2685 . . . . 5  |-  ( m  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  m )  =  0 )
178177adantl 271 . . . 4  |-  ( (
ph  /\  m  e.  ( ( M ... ( K `  ( `  A
) ) )  \  A ) )  -> 
( F `  m
)  =  0 )
179112ffvelrnda 5418 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  A
)
180179iftrued 3396 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  = 
[_ ( K `  x )  /  k ]_ B )
1814adantr 270 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  A  C_  ( ZZ>=
`  M ) )
182181, 179sseldd 3024 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  (
ZZ>= `  M ) )
183 eluzelz 8997 . . . . . . 7  |-  ( ( K `  x )  e.  ( ZZ>= `  M
)  ->  ( K `  x )  e.  ZZ )
184182, 183syl 14 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  ZZ )
185 simpl 107 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ph )
186185, 184jca 300 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( ph  /\  ( K `  x )  e.  ZZ ) )
187 nfcv 2228 . . . . . . . 8  |-  F/_ k
( K `  x
)
188 nfv 1466 . . . . . . . . 9  |-  F/ k ( ph  /\  ( K `  x )  e.  ZZ )
189 nfv 1466 . . . . . . . . . . 11  |-  F/ k ( K `  x
)  e.  A
190 nfcsb1v 2961 . . . . . . . . . . 11  |-  F/_ k [_ ( K `  x
)  /  k ]_ B
191189, 190, 143nfif 3415 . . . . . . . . . 10  |-  F/_ k if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )
192191nfel1 2239 . . . . . . . . 9  |-  F/ k if ( ( K `
 x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC
193188, 192nfim 1509 . . . . . . . 8  |-  F/ k ( ( ph  /\  ( K `  x )  e.  ZZ )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
194 eleq1 2150 . . . . . . . . . 10  |-  ( k  =  ( K `  x )  ->  (
k  e.  ZZ  <->  ( K `  x )  e.  ZZ ) )
195194anbi2d 452 . . . . . . . . 9  |-  ( k  =  ( K `  x )  ->  (
( ph  /\  k  e.  ZZ )  <->  ( ph  /\  ( K `  x
)  e.  ZZ ) ) )
196 eleq1 2150 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  (
k  e.  A  <->  ( K `  x )  e.  A
) )
197 csbeq1a 2939 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  B  =  [_ ( K `  x )  /  k ]_ B )
198196, 197ifbieq1d 3409 . . . . . . . . . 10  |-  ( k  =  ( K `  x )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
199198eleq1d 2156 . . . . . . . . 9  |-  ( k  =  ( K `  x )  ->  ( if ( k  e.  A ,  B ,  0 )  e.  CC  <->  if (
( K `  x
)  e.  A ,  [_ ( K `  x
)  /  k ]_ B ,  0 )  e.  CC ) )
200195, 199imbi12d 232 . . . . . . . 8  |-  ( k  =  ( K `  x )  ->  (
( ( ph  /\  k  e.  ZZ )  ->  if ( k  e.  A ,  B , 
0 )  e.  CC ) 
<->  ( ( ph  /\  ( K `  x )  e.  ZZ )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC ) ) )
201187, 193, 200, 102vtoclgf 2677 . . . . . . 7  |-  ( ( K `  x )  e.  A  ->  (
( ph  /\  ( K `  x )  e.  ZZ )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC ) )
202179, 186, 201sylc 61 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
203 eleq1 2150 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  (
n  e.  A  <->  ( K `  x )  e.  A
) )
204 csbeq1 2934 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  [_ n  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
205203, 204ifbieq1d 3409 . . . . . . 7  |-  ( n  =  ( K `  x )  ->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
206 nfcv 2228 . . . . . . . . 9  |-  F/_ n if ( k  e.  A ,  B ,  0 )
207 nfv 1466 . . . . . . . . . 10  |-  F/ k  n  e.  A
208 nfcsb1v 2961 . . . . . . . . . 10  |-  F/_ k [_ n  /  k ]_ B
209207, 208, 143nfif 3415 . . . . . . . . 9  |-  F/_ k if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
210 eleq1 2150 . . . . . . . . . 10  |-  ( k  =  n  ->  (
k  e.  A  <->  n  e.  A ) )
211 csbeq1a 2939 . . . . . . . . . 10  |-  ( k  =  n  ->  B  =  [_ n  /  k ]_ B )
212210, 211ifbieq1d 3409 . . . . . . . . 9  |-  ( k  =  n  ->  if ( k  e.  A ,  B ,  0 )  =  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
213206, 209, 212cbvmpt 3925 . . . . . . . 8  |-  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2141, 213eqtri 2108 . . . . . . 7  |-  F  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
215205, 214fvmptg 5364 . . . . . 6  |-  ( ( ( K `  x
)  e.  ZZ  /\  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )  -> 
( F `  ( K `  x )
)  =  if ( ( K `  x
)  e.  A ,  [_ ( K `  x
)  /  k ]_ B ,  0 ) )
216184, 202, 215syl2anc 403 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( F `  ( K `  x ) )  =  if ( ( K `  x
)  e.  A ,  [_ ( K `  x
)  /  k ]_ B ,  0 ) )
217 elfznn 9437 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  e.  NN )
218217adantl 271 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  e.  NN )
219 elfzle2 9411 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  <_  ( `  A ) )
220219adantl 271 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  <_  ( `  A ) )
22115breq2d 3849 . . . . . . . . . . 11  |-  ( ph  ->  ( x  <_  ( `  A )  <->  x  <_  N ) )
222221adantr 270 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( x  <_ 
( `  A )  <->  x  <_  N ) )
223220, 222mpbid 145 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  <_  N
)
224223iftrued 3396 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  = 
[_ ( K `  x )  /  k ]_ B )
225180, 202eqeltrrd 2165 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  [_ ( K `  x )  /  k ]_ B  e.  CC )
226224, 225eqeltrd 2164 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
227 breq1 3840 . . . . . . . . 9  |-  ( n  =  x  ->  (
n  <_  N  <->  x  <_  N ) )
228 fveq2 5289 . . . . . . . . . 10  |-  ( n  =  x  ->  ( K `  n )  =  ( K `  x ) )
229228csbeq1d 2937 . . . . . . . . 9  |-  ( n  =  x  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
230227, 229ifbieq1d 3409 . . . . . . . 8  |-  ( n  =  x  ->  if ( n  <_  N ,  [_ ( K `  n
)  /  k ]_ B ,  0 )  =  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
231230, 163fvmptg 5364 . . . . . . 7  |-  ( ( x  e.  NN  /\  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )  -> 
( H `  x
)  =  if ( x  <_  N ,  [_ ( K `  x
)  /  k ]_ B ,  0 ) )
232218, 226, 231syl2anc 403 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
233232, 224eqtrd 2120 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  [_ ( K `  x )  /  k ]_ B
)
234180, 216, 2333eqtr4rd 2131 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  ( F `  ( K `
 x ) ) )
23572, 74, 76, 77, 5, 78, 4, 106, 166, 178, 234iseqcoll 10212 . . 3  |-  ( ph  ->  (  seq M (  +  ,  F ,  CC ) `  ( K `
 N ) )  =  (  seq 1
(  +  ,  H ,  CC ) `  N
) )
23615, 7eqeltrd 2164 . . . . 5  |-  ( ph  ->  ( `  A )  e.  NN )
237236, 7jca 300 . . . 4  |-  ( ph  ->  ( ( `  A
)  e.  NN  /\  N  e.  NN )
)
23816eqcomd 2093 . . . . . 6  |-  ( ph  ->  ( 1 ... N
)  =  ( 1 ... ( `  A
) ) )
239 f1oeq2 5229 . . . . . 6  |-  ( ( 1 ... N )  =  ( 1 ... ( `  A )
)  ->  ( f : ( 1 ... N ) -1-1-onto-> A  <->  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )
240238, 239syl 14 . . . . 5  |-  ( ph  ->  ( f : ( 1 ... N ) -1-1-onto-> A  <-> 
f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )
24110, 240mpbid 145 . . . 4  |-  ( ph  ->  f : ( 1 ... ( `  A
) ) -1-1-onto-> A )
242 isummolem2a.g . . . 4  |-  G  =  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
2431, 2, 237, 241, 21, 242, 163isummolem3 10734 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ,  CC ) `  ( `  A
) )  =  (  seq 1 (  +  ,  H ,  CC ) `  N )
)
24415fveq2d 5293 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ,  CC ) `  ( `  A
) )  =  (  seq 1 (  +  ,  G ,  CC ) `  N )
)
245235, 243, 2443eqtr2d 2126 . 2  |-  ( ph  ->  (  seq M (  +  ,  F ,  CC ) `  ( K `
 N ) )  =  (  seq 1
(  +  ,  G ,  CC ) `  N
) )
24670, 245breqtrd 3861 1  |-  ( ph  ->  seq M (  +  ,  F ,  CC ) 
~~>  (  seq 1
(  +  ,  G ,  CC ) `  N
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 102    <-> wb 103    \/ wo 664  DECID wdc 780    /\ w3a 924    = wceq 1289    e. wcel 1438   A.wral 2359   [_csb 2931    \ cdif 2994    C_ wss 2997   ifcif 3389   class class class wbr 3837    |-> cmpt 3891   `'ccnv 4427   -->wf 4998   -1-1-onto->wf1o 5001   ` cfv 5002    Isom wiso 5003  (class class class)co 5634   CCcc 7327   RRcr 7328   0cc0 7329   1c1 7330    + caddc 7332   RR*cxr 7500    < clt 7501    <_ cle 7502   NNcn 8394   NN0cn0 8643   ZZcz 8720   ZZ>=cuz 8988   ...cfz 9393    seqcseq4 9816  ♯chash 10148    ~~> cli 10630
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3946  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027  ax-un 4251  ax-setind 4343  ax-iinf 4393  ax-cnex 7415  ax-resscn 7416  ax-1cn 7417  ax-1re 7418  ax-icn 7419  ax-addcl 7420  ax-addrcl 7421  ax-mulcl 7422  ax-mulrcl 7423  ax-addcom 7424  ax-mulcom 7425  ax-addass 7426  ax-mulass 7427  ax-distr 7428  ax-i2m1 7429  ax-0lt1 7430  ax-1rid 7431  ax-0id 7432  ax-rnegex 7433  ax-precex 7434  ax-cnre 7435  ax-pre-ltirr 7436  ax-pre-ltwlin 7437  ax-pre-lttrn 7438  ax-pre-apti 7439  ax-pre-ltadd 7440  ax-pre-mulgt0 7441  ax-pre-mulext 7442
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-reu 2366  df-rmo 2367  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-if 3390  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-int 3684  df-iun 3727  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-id 4111  df-po 4114  df-iso 4115  df-iord 4184  df-on 4186  df-ilim 4187  df-suc 4189  df-iom 4396  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-rn 4439  df-res 4440  df-ima 4441  df-iota 4967  df-fun 5004  df-fn 5005  df-f 5006  df-f1 5007  df-fo 5008  df-f1o 5009  df-fv 5010  df-isom 5011  df-riota 5590  df-ov 5637  df-oprab 5638  df-mpt2 5639  df-1st 5893  df-2nd 5894  df-recs 6052  df-frec 6138  df-1o 6163  df-er 6272  df-en 6438  df-dom 6439  df-fin 6440  df-pnf 7503  df-mnf 7504  df-xr 7505  df-ltxr 7506  df-le 7507  df-sub 7634  df-neg 7635  df-reap 8028  df-ap 8035  df-div 8114  df-inn 8395  df-2 8452  df-n0 8644  df-z 8721  df-uz 8989  df-rp 9104  df-fz 9394  df-fzo 9519  df-iseq 9818  df-seq3 9819  df-exp 9920  df-ihash 10149  df-cj 10241  df-rsqrt 10396  df-abs 10397  df-clim 10631
This theorem is referenced by:  isummolem2  10736  zisum  10738
  Copyright terms: Public domain W3C validator