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

Theorem summodclem2a 11162
Description: Lemma for summodc 11164. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)
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
summodclem2a  |-  ( ph  ->  seq M (  +  ,  F )  ~~>  (  seq 1 (  +  ,  G ) `  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 summodclem2a
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 9093 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  ZZ )
7 summolem2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN )
87nnzd 9184 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ZZ )
96, 8fzfigd 10216 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
10 summolem2.8 . . . . . . . . . . . 12  |-  ( ph  ->  f : ( 1 ... N ) -1-1-onto-> A )
119, 10fihasheqf1od 10548 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  ( `  A )
)
12 nnnn0 8996 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  NN0 )
13 hashfz1 10541 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( `  (
1 ... N ) )  =  N )
147, 12, 133syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  N )
1511, 14eqtr3d 2174 . . . . . . . . . 10  |-  ( ph  ->  ( `  A )  =  N )
1615oveq2d 5790 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( `  A ) )  =  ( 1 ... N
) )
17 isoeq4 5705 . . . . . . . . 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 146 . . . . . . 7  |-  ( ph  ->  K  Isom  <  ,  <  ( ( 1 ... N
) ,  A ) )
20 isof1o 5708 . . . . . . 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 5367 . . . . . 6  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  K :
( 1 ... N
) --> A )
2321, 22syl 14 . . . . 5  |-  ( ph  ->  K : ( 1 ... N ) --> A )
24 nnuz 9373 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
257, 24eleqtrdi 2232 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
26 eluzfz2 9824 . . . . . 6  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
2725, 26syl 14 . . . . 5  |-  ( ph  ->  N  e.  ( 1 ... N ) )
2823, 27ffvelrnd 5556 . . . 4  |-  ( ph  ->  ( K `  N
)  e.  A )
294, 28sseldd 3098 . . 3  |-  ( ph  ->  ( K `  N
)  e.  ( ZZ>= `  M ) )
304sselda 3097 . . . . . 6  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ( ZZ>= `  M )
)
31 f1ocnvfv2 5679 . . . . . . . . 9  |-  ( ( K : ( 1 ... N ) -1-1-onto-> A  /\  n  e.  A )  ->  ( K `  ( `' K `  n ) )  =  n )
3221, 31sylan 281 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  ( `' K `  n )
)  =  n )
33 f1ocnv 5380 . . . . . . . . . . . 12  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  `' K : A -1-1-onto-> ( 1 ... N
) )
34 f1of 5367 . . . . . . . . . . . 12  |-  ( `' K : A -1-1-onto-> ( 1 ... N )  ->  `' K : A --> ( 1 ... N ) )
3521, 33, 343syl 17 . . . . . . . . . . 11  |-  ( ph  ->  `' K : A --> ( 1 ... N ) )
3635ffvelrnda 5555 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  ( `' K `  n )  e.  ( 1 ... N ) )
37 elfzle2 9820 . . . . . . . . . 10  |-  ( ( `' K `  n )  e.  ( 1 ... N )  ->  ( `' K `  n )  <_  N )
3836, 37syl 14 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  A )  ->  ( `' K `  n )  <_  N )
3919adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  K  Isom  <  ,  <  (
( 1 ... N
) ,  A ) )
40 fzssuz 9857 . . . . . . . . . . . . 13  |-  ( 1 ... N )  C_  ( ZZ>= `  1 )
41 uzssz 9357 . . . . . . . . . . . . . 14  |-  ( ZZ>= ` 
1 )  C_  ZZ
42 zssre 9073 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
4341, 42sstri 3106 . . . . . . . . . . . . 13  |-  ( ZZ>= ` 
1 )  C_  RR
4440, 43sstri 3106 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  RR
45 ressxr 7821 . . . . . . . . . . . 12  |-  RR  C_  RR*
4644, 45sstri 3106 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  RR*
4746a1i 9 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  (
1 ... N )  C_  RR* )
484adantr 274 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  A )  ->  A  C_  ( ZZ>= `  M )
)
49 uzssz 9357 . . . . . . . . . . . . 13  |-  ( ZZ>= `  M )  C_  ZZ
5049, 42sstri 3106 . . . . . . . . . . . 12  |-  ( ZZ>= `  M )  C_  RR
5148, 50sstrdi 3109 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  A )  ->  A  C_  RR )
5251, 45sstrdi 3109 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  A  C_ 
RR* )
5327adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  N  e.  ( 1 ... N
) )
54 leisorel 10592 . . . . . . . . . 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 1225 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  A )  ->  (
( `' K `  n )  <_  N  <->  ( K `  ( `' K `  n ) )  <_  ( K `  N ) ) )
5638, 55mpbid 146 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  ( `' K `  n )
)  <_  ( K `  N ) )
5732, 56eqbrtrrd 3952 . . . . . . 7  |-  ( (
ph  /\  n  e.  A )  ->  n  <_  ( K `  N
) )
58 eluzelz 9347 . . . . . . . . 9  |-  ( n  e.  ( ZZ>= `  M
)  ->  n  e.  ZZ )
5930, 58syl 14 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ZZ )
60 eluzelz 9347 . . . . . . . . . 10  |-  ( ( K `  N )  e.  ( ZZ>= `  M
)  ->  ( K `  N )  e.  ZZ )
6129, 60syl 14 . . . . . . . . 9  |-  ( ph  ->  ( K `  N
)  e.  ZZ )
6261adantr 274 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  N )  e.  ZZ )
63 eluz 9351 . . . . . . . 8  |-  ( ( n  e.  ZZ  /\  ( K `  N )  e.  ZZ )  -> 
( ( K `  N )  e.  (
ZZ>= `  n )  <->  n  <_  ( K `  N ) ) )
6459, 62, 63syl2anc 408 . . . . . . 7  |-  ( (
ph  /\  n  e.  A )  ->  (
( K `  N
)  e.  ( ZZ>= `  n )  <->  n  <_  ( K `  N ) ) )
6557, 64mpbird 166 . . . . . 6  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  N )  e.  ( ZZ>= `  n )
)
66 elfzuzb 9812 . . . . . 6  |-  ( n  e.  ( M ... ( K `  N ) )  <->  ( n  e.  ( ZZ>= `  M )  /\  ( K `  N
)  e.  ( ZZ>= `  n ) ) )
6730, 65, 66sylanbrc 413 . . . . 5  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ( M ... ( K `  N )
) )
6867ex 114 . . . 4  |-  ( ph  ->  ( n  e.  A  ->  n  e.  ( M ... ( K `  N ) ) ) )
6968ssrdv 3103 . . 3  |-  ( ph  ->  A  C_  ( M ... ( K `  N
) ) )
701, 2, 3, 29, 69fsum3cvg 11159 . 2  |-  ( ph  ->  seq M (  +  ,  F )  ~~>  (  seq M (  +  ,  F ) `  ( K `  N )
) )
71 addid2 7913 . . . . 5  |-  ( m  e.  CC  ->  (
0  +  m )  =  m )
7271adantl 275 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( 0  +  m )  =  m )
73 addid1 7912 . . . . 5  |-  ( m  e.  CC  ->  (
m  +  0 )  =  m )
7473adantl 275 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( m  +  0 )  =  m )
75 addcl 7757 . . . . 5  |-  ( ( m  e.  CC  /\  x  e.  CC )  ->  ( m  +  x
)  e.  CC )
7675adantl 275 . . . 4  |-  ( (
ph  /\  ( m  e.  CC  /\  x  e.  CC ) )  -> 
( m  +  x
)  e.  CC )
77 0cnd 7771 . . . 4  |-  ( ph  ->  0  e.  CC )
7827, 16eleqtrrd 2219 . . . 4  |-  ( ph  ->  N  e.  ( 1 ... ( `  A
) ) )
79 iftrue 3479 . . . . . . . . . . . 12  |-  ( k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  =  B )
8079adantl 275 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  =  B )
8180, 2eqeltrd 2216 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8281adantlr 468 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8382adantlr 468 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>=
`  M ) )  /\  k  e.  A
)  ->  if (
k  e.  A ,  B ,  0 )  e.  CC )
84 iffalse 3482 . . . . . . . . . 10  |-  ( -.  k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  =  0 )
85 0cn 7770 . . . . . . . . . 10  |-  0  e.  CC
8684, 85eqeltrdi 2230 . . . . . . . . 9  |-  ( -.  k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8786adantl 275 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>=
`  M ) )  /\  -.  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
883adantlr 468 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  -> DECID  k  e.  A
)
89 exmiddc 821 . . . . . . . . 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 787 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  e.  A ,  B ,  0 )  e.  CC )
92 simpll 518 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  ph )
93 simpr 109 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  -.  k  e.  ( ZZ>=
`  M ) )
944ssneld 3099 . . . . . . . . 9  |-  ( ph  ->  ( -.  k  e.  ( ZZ>= `  M )  ->  -.  k  e.  A
) )
9592, 93, 94sylc 62 . . . . . . . 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 9416 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  -> DECID  k  e.  ( ZZ>= `  M
) )
9997, 98sylan 281 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ZZ )  -> DECID  k  e.  ( ZZ>=
`  M ) )
100 exmiddc 821 . . . . . . . 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 787 . . . . . 6  |-  ( (
ph  /\  k  e.  ZZ )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
103102, 1fmptd 5574 . . . . 5  |-  ( ph  ->  F : ZZ --> CC )
104 eluzelz 9347 . . . . 5  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
105 ffvelrn 5553 . . . . 5  |-  ( ( F : ZZ --> CC  /\  m  e.  ZZ )  ->  ( F `  m
)  e.  CC )
106103, 104, 105syl2an 287 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( F `  m )  e.  CC )
107 elnnuz 9374 . . . . . . . 8  |-  ( m  e.  NN  <->  m  e.  ( ZZ>= `  1 )
)
108107biimpri 132 . . . . . . 7  |-  ( m  e.  ( ZZ>= `  1
)  ->  m  e.  NN )
109108adantl 275 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  m  e.  NN )
110 isof1o 5708 . . . . . . . . . . . 12  |-  ( K 
Isom  <  ,  <  (
( 1 ... ( `  A ) ) ,  A )  ->  K : ( 1 ... ( `  A )
)
-1-1-onto-> A )
111 f1of 5367 . . . . . . . . . . . 12  |-  ( K : ( 1 ... ( `  A )
)
-1-1-onto-> A  ->  K : ( 1 ... ( `  A
) ) --> A )
1125, 110, 1113syl 17 . . . . . . . . . . 11  |-  ( ph  ->  K : ( 1 ... ( `  A
) ) --> A )
113112ad2antrr 479 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  K :
( 1 ... ( `  A ) ) --> A )
114 1zzd 9093 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  1  e.  ZZ )
11515, 8eqeltrd 2216 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `  A )  e.  ZZ )
116115ad2antrr 479 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( `  A
)  e.  ZZ )
117 eluzelz 9347 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  m  e.  ZZ )
118117ad2antlr 480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ZZ )
119114, 116, 1183jca 1161 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  m  e.  ZZ ) )
120 eluzle 9350 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  1  <_  m )
121120ad2antlr 480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  1  <_  m )
122 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  <_  N )
12315breq2d 3941 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  <_  ( `  A )  <->  m  <_  N ) )
124123ad2antrr 479 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( m  <_  ( `  A )  <->  m  <_  N ) )
125122, 124mpbird 166 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  <_  ( `  A ) )
126121, 125jca 304 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( 1  <_  m  /\  m  <_  ( `  A )
) )
127 elfz2 9809 . . . . . . . . . . 11  |-  ( m  e.  ( 1 ... ( `  A )
)  <->  ( ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  m  e.  ZZ )  /\  ( 1  <_  m  /\  m  <_  ( `  A ) ) ) )
128119, 126, 127sylanbrc 413 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ( 1 ... ( `  A ) ) )
129113, 128ffvelrnd 5556 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
130129iftrued 3481 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  if (
( K `  m
)  e.  A ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  =  [_ ( K `
 m )  / 
k ]_ B )
1314ad2antrr 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  A  C_  ( ZZ>=
`  M ) )
13223ad2antrr 479 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  K :
( 1 ... N
) --> A )
13316eleq2d 2209 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  e.  ( 1 ... ( `  A
) )  <->  m  e.  ( 1 ... N
) ) )
134133ad2antrr 479 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( m  e.  ( 1 ... ( `  A ) )  <->  m  e.  ( 1 ... N
) ) )
135128, 134mpbid 146 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ( 1 ... N
) )
136132, 135ffvelrnd 5556 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
137131, 136sseldd 3098 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  (
ZZ>= `  M ) )
13849, 137sseldi 3095 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  ZZ )
139102ralrimiva 2505 . . . . . . . . . 10  |-  ( ph  ->  A. k  e.  ZZ  if ( k  e.  A ,  B ,  0 )  e.  CC )
140139ad2antrr 479 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  A. k  e.  ZZ  if ( k  e.  A ,  B ,  0 )  e.  CC )
141 nfv 1508 . . . . . . . . . . . 12  |-  F/ k ( K `  m
)  e.  A
142 nfcsb1v 3035 . . . . . . . . . . . 12  |-  F/_ k [_ ( K `  m
)  /  k ]_ B
143 nfcv 2281 . . . . . . . . . . . 12  |-  F/_ k
0
144141, 142, 143nfif 3500 . . . . . . . . . . 11  |-  F/_ k if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )
145144nfel1 2292 . . . . . . . . . 10  |-  F/ k if ( ( K `
 m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )  e.  CC
146 eleq1 2202 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  (
k  e.  A  <->  ( K `  m )  e.  A
) )
147 csbeq1a 3012 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  B  =  [_ ( K `  m )  /  k ]_ B )
148146, 147ifbieq1d 3494 . . . . . . . . . . 11  |-  ( k  =  ( K `  m )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
149148eleq1d 2208 . . . . . . . . . 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 2783 . . . . . . . . 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 62 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  if (
( K `  m
)  e.  A ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  e.  CC )
152130, 151eqeltrrd 2217 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  [_ ( K `
 m )  / 
k ]_ B  e.  CC )
153 0cnd 7771 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  -.  m  <_  N )  ->  0  e.  CC )
154109nnzd 9184 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  m  e.  ZZ )
1558adantr 274 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  N  e.  ZZ )
156 zdcle 9139 . . . . . . . 8  |-  ( ( m  e.  ZZ  /\  N  e.  ZZ )  -> DECID  m  <_  N )
157154, 155, 156syl2anc 408 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  -> DECID  m  <_  N )
158152, 153, 157ifcldadc 3501 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  if (
m  <_  N ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  e.  CC )
159 breq1 3932 . . . . . . . 8  |-  ( n  =  m  ->  (
n  <_  N  <->  m  <_  N ) )
160 fveq2 5421 . . . . . . . . 9  |-  ( n  =  m  ->  ( K `  n )  =  ( K `  m ) )
161160csbeq1d 3010 . . . . . . . 8  |-  ( n  =  m  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  m )  /  k ]_ B )
162159, 161ifbieq1d 3494 . . . . . . 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 5497 . . . . . 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 408 . . . . 5  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  ( H `  m )  =  if ( m  <_  N ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
166165, 158eqeltrd 2216 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  ( H `  m )  e.  CC )
167 fveqeq2 5430 . . . . . 6  |-  ( k  =  m  ->  (
( F `  k
)  =  0  <->  ( F `  m )  =  0 ) )
168 eldifi 3198 . . . . . . . . 9  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ( M ... ( K `
 ( `  A
) ) ) )
169 elfzelz 9818 . . . . . . . . 9  |-  ( k  e.  ( M ... ( K `  ( `  A
) ) )  -> 
k  e.  ZZ )
170168, 169syl 14 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ZZ )
171 eldifn 3199 . . . . . . . . . 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, 85eqeltrdi 2230 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
1741fvmpt2 5504 . . . . . . . 8  |-  ( ( k  e.  ZZ  /\  if ( k  e.  A ,  B ,  0 )  e.  CC )  -> 
( F `  k
)  =  if ( k  e.  A ,  B ,  0 ) )
175170, 173, 174syl2anc 408 . . . . . . 7  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  k )  =  if ( k  e.  A ,  B ,  0 ) )
176175, 172eqtrd 2172 . . . . . 6  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  k )  =  0 )
177167, 176vtoclga 2752 . . . . 5  |-  ( m  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  m )  =  0 )
178177adantl 275 . . . 4  |-  ( (
ph  /\  m  e.  ( ( M ... ( K `  ( `  A
) ) )  \  A ) )  -> 
( F `  m
)  =  0 )
179112ffvelrnda 5555 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  A
)
180179iftrued 3481 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  = 
[_ ( K `  x )  /  k ]_ B )
1814adantr 274 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  A  C_  ( ZZ>=
`  M ) )
182181, 179sseldd 3098 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  (
ZZ>= `  M ) )
183 eluzelz 9347 . . . . . . 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 108 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ph )
186185, 184jca 304 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( ph  /\  ( K `  x )  e.  ZZ ) )
187 nfv 1508 . . . . . . . . 9  |-  F/ k ( ph  /\  ( K `  x )  e.  ZZ )
188 nfv 1508 . . . . . . . . . . 11  |-  F/ k ( K `  x
)  e.  A
189 nfcsb1v 3035 . . . . . . . . . . 11  |-  F/_ k [_ ( K `  x
)  /  k ]_ B
190188, 189, 143nfif 3500 . . . . . . . . . 10  |-  F/_ k if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )
191190nfel1 2292 . . . . . . . . 9  |-  F/ k if ( ( K `
 x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC
192187, 191nfim 1551 . . . . . . . 8  |-  F/ k ( ( ph  /\  ( K `  x )  e.  ZZ )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
193 eleq1 2202 . . . . . . . . . 10  |-  ( k  =  ( K `  x )  ->  (
k  e.  ZZ  <->  ( K `  x )  e.  ZZ ) )
194193anbi2d 459 . . . . . . . . 9  |-  ( k  =  ( K `  x )  ->  (
( ph  /\  k  e.  ZZ )  <->  ( ph  /\  ( K `  x
)  e.  ZZ ) ) )
195 eleq1 2202 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  (
k  e.  A  <->  ( K `  x )  e.  A
) )
196 csbeq1a 3012 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  B  =  [_ ( K `  x )  /  k ]_ B )
197195, 196ifbieq1d 3494 . . . . . . . . . 10  |-  ( k  =  ( K `  x )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
198197eleq1d 2208 . . . . . . . . 9  |-  ( k  =  ( K `  x )  ->  ( if ( k  e.  A ,  B ,  0 )  e.  CC  <->  if (
( K `  x
)  e.  A ,  [_ ( K `  x
)  /  k ]_ B ,  0 )  e.  CC ) )
199194, 198imbi12d 233 . . . . . . . 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 ) ) )
200192, 199, 102vtoclg1f 2745 . . . . . . 7  |-  ( ( K `  x )  e.  A  ->  (
( ph  /\  ( K `  x )  e.  ZZ )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC ) )
201179, 186, 200sylc 62 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
202 eleq1 2202 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  (
n  e.  A  <->  ( K `  x )  e.  A
) )
203 csbeq1 3006 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  [_ n  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
204202, 203ifbieq1d 3494 . . . . . . 7  |-  ( n  =  ( K `  x )  ->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
205 nfcv 2281 . . . . . . . . 9  |-  F/_ n if ( k  e.  A ,  B ,  0 )
206 nfv 1508 . . . . . . . . . 10  |-  F/ k  n  e.  A
207 nfcsb1v 3035 . . . . . . . . . 10  |-  F/_ k [_ n  /  k ]_ B
208206, 207, 143nfif 3500 . . . . . . . . 9  |-  F/_ k if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
209 eleq1 2202 . . . . . . . . . 10  |-  ( k  =  n  ->  (
k  e.  A  <->  n  e.  A ) )
210 csbeq1a 3012 . . . . . . . . . 10  |-  ( k  =  n  ->  B  =  [_ n  /  k ]_ B )
211209, 210ifbieq1d 3494 . . . . . . . . 9  |-  ( k  =  n  ->  if ( k  e.  A ,  B ,  0 )  =  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
212205, 208, 211cbvmpt 4023 . . . . . . . 8  |-  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2131, 212eqtri 2160 . . . . . . 7  |-  F  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
214204, 213fvmptg 5497 . . . . . 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 ) )
215184, 201, 214syl2anc 408 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( F `  ( K `  x ) )  =  if ( ( K `  x
)  e.  A ,  [_ ( K `  x
)  /  k ]_ B ,  0 ) )
216 elfznn 9846 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  e.  NN )
217216adantl 275 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  e.  NN )
218 elfzle2 9820 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  <_  ( `  A ) )
219218adantl 275 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  <_  ( `  A ) )
22015breq2d 3941 . . . . . . . . . . 11  |-  ( ph  ->  ( x  <_  ( `  A )  <->  x  <_  N ) )
221220adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( x  <_ 
( `  A )  <->  x  <_  N ) )
222219, 221mpbid 146 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  <_  N
)
223222iftrued 3481 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  = 
[_ ( K `  x )  /  k ]_ B )
224180, 201eqeltrrd 2217 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  [_ ( K `  x )  /  k ]_ B  e.  CC )
225223, 224eqeltrd 2216 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
226 breq1 3932 . . . . . . . . 9  |-  ( n  =  x  ->  (
n  <_  N  <->  x  <_  N ) )
227 fveq2 5421 . . . . . . . . . 10  |-  ( n  =  x  ->  ( K `  n )  =  ( K `  x ) )
228227csbeq1d 3010 . . . . . . . . 9  |-  ( n  =  x  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
229226, 228ifbieq1d 3494 . . . . . . . 8  |-  ( n  =  x  ->  if ( n  <_  N ,  [_ ( K `  n
)  /  k ]_ B ,  0 )  =  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
230229, 163fvmptg 5497 . . . . . . 7  |-  ( ( x  e.  NN  /\  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )  -> 
( H `  x
)  =  if ( x  <_  N ,  [_ ( K `  x
)  /  k ]_ B ,  0 ) )
231217, 225, 230syl2anc 408 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
232231, 223eqtrd 2172 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  [_ ( K `  x )  /  k ]_ B
)
233180, 215, 2323eqtr4rd 2183 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  ( F `  ( K `
 x ) ) )
23472, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233seq3coll 10597 . . 3  |-  ( ph  ->  (  seq M (  +  ,  F ) `
 ( K `  N ) )  =  (  seq 1 (  +  ,  H ) `
 N ) )
23515, 7eqeltrd 2216 . . . . 5  |-  ( ph  ->  ( `  A )  e.  NN )
236235, 7jca 304 . . . 4  |-  ( ph  ->  ( ( `  A
)  e.  NN  /\  N  e.  NN )
)
23716eqcomd 2145 . . . . . 6  |-  ( ph  ->  ( 1 ... N
)  =  ( 1 ... ( `  A
) ) )
238 f1oeq2 5357 . . . . . 6  |-  ( ( 1 ... N )  =  ( 1 ... ( `  A )
)  ->  ( f : ( 1 ... N ) -1-1-onto-> A  <->  f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )
239237, 238syl 14 . . . . 5  |-  ( ph  ->  ( f : ( 1 ... N ) -1-1-onto-> A  <-> 
f : ( 1 ... ( `  A
) ) -1-1-onto-> A ) )
24010, 239mpbid 146 . . . 4  |-  ( ph  ->  f : ( 1 ... ( `  A
) ) -1-1-onto-> A )
241 isummolem2a.g . . . 4  |-  G  =  ( n  e.  NN  |->  if ( n  <_  ( `  A ) ,  [_ ( f `  n
)  /  k ]_ B ,  0 ) )
2421, 2, 236, 240, 21, 241, 163summodclem3 11161 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ) `
 ( `  A
) )  =  (  seq 1 (  +  ,  H ) `  N ) )
24315fveq2d 5425 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ) `
 ( `  A
) )  =  (  seq 1 (  +  ,  G ) `  N ) )
244234, 242, 2433eqtr2d 2178 . 2  |-  ( ph  ->  (  seq M (  +  ,  F ) `
 ( K `  N ) )  =  (  seq 1 (  +  ,  G ) `
 N ) )
24570, 244breqtrd 3954 1  |-  ( ph  ->  seq M (  +  ,  F )  ~~>  (  seq 1 (  +  ,  G ) `  N
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 697  DECID wdc 819    /\ w3a 962    = wceq 1331    e. wcel 1480   A.wral 2416   [_csb 3003    \ cdif 3068    C_ wss 3071   ifcif 3474   class class class wbr 3929    |-> cmpt 3989   `'ccnv 4538   -->wf 5119   -1-1-onto->wf1o 5122   ` cfv 5123    Isom wiso 5124  (class class class)co 5774   CCcc 7630   RRcr 7631   0cc0 7632   1c1 7633    + caddc 7635   RR*cxr 7811    < clt 7812    <_ cle 7813   NNcn 8732   NN0cn0 8989   ZZcz 9066   ZZ>=cuz 9338   ...cfz 9802    seqcseq 10230  ♯chash 10533    ~~> cli 11059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7723  ax-resscn 7724  ax-1cn 7725  ax-1re 7726  ax-icn 7727  ax-addcl 7728  ax-addrcl 7729  ax-mulcl 7730  ax-mulrcl 7731  ax-addcom 7732  ax-mulcom 7733  ax-addass 7734  ax-mulass 7735  ax-distr 7736  ax-i2m1 7737  ax-0lt1 7738  ax-1rid 7739  ax-0id 7740  ax-rnegex 7741  ax-precex 7742  ax-cnre 7743  ax-pre-ltirr 7744  ax-pre-ltwlin 7745  ax-pre-lttrn 7746  ax-pre-apti 7747  ax-pre-ltadd 7748  ax-pre-mulgt0 7749  ax-pre-mulext 7750
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-1o 6313  df-er 6429  df-en 6635  df-dom 6636  df-fin 6637  df-pnf 7814  df-mnf 7815  df-xr 7816  df-ltxr 7817  df-le 7818  df-sub 7947  df-neg 7948  df-reap 8349  df-ap 8356  df-div 8445  df-inn 8733  df-2 8791  df-n0 8990  df-z 9067  df-uz 9339  df-rp 9454  df-fz 9803  df-fzo 9932  df-seqfrec 10231  df-exp 10305  df-ihash 10534  df-cj 10626  df-rsqrt 10782  df-abs 10783  df-clim 11060
This theorem is referenced by:  summodclem2  11163  zsumdc  11165
  Copyright terms: Public domain W3C validator