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

Theorem summodclem2a 11524
Description: Lemma for summodc 11526. (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 9344 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  ZZ )
7 summolem2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN )
87nnzd 9438 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ZZ )
96, 8fzfigd 10502 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
10 summolem2.8 . . . . . . . . . . . 12  |-  ( ph  ->  f : ( 1 ... N ) -1-1-onto-> A )
119, 10fihasheqf1od 10860 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  ( `  A )
)
12 nnnn0 9247 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  NN0 )
13 hashfz1 10854 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( `  (
1 ... N ) )  =  N )
147, 12, 133syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  N )
1511, 14eqtr3d 2228 . . . . . . . . . 10  |-  ( ph  ->  ( `  A )  =  N )
1615oveq2d 5934 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( `  A ) )  =  ( 1 ... N
) )
17 isoeq4 5847 . . . . . . . . 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 147 . . . . . . 7  |-  ( ph  ->  K  Isom  <  ,  <  ( ( 1 ... N
) ,  A ) )
20 isof1o 5850 . . . . . . 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 5500 . . . . . 6  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  K :
( 1 ... N
) --> A )
2321, 22syl 14 . . . . 5  |-  ( ph  ->  K : ( 1 ... N ) --> A )
24 nnuz 9628 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
257, 24eleqtrdi 2286 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
26 eluzfz2 10098 . . . . . 6  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
2725, 26syl 14 . . . . 5  |-  ( ph  ->  N  e.  ( 1 ... N ) )
2823, 27ffvelcdmd 5694 . . . 4  |-  ( ph  ->  ( K `  N
)  e.  A )
294, 28sseldd 3180 . . 3  |-  ( ph  ->  ( K `  N
)  e.  ( ZZ>= `  M ) )
304sselda 3179 . . . . . 6  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ( ZZ>= `  M )
)
31 f1ocnvfv2 5821 . . . . . . . . 9  |-  ( ( K : ( 1 ... N ) -1-1-onto-> A  /\  n  e.  A )  ->  ( K `  ( `' K `  n ) )  =  n )
3221, 31sylan 283 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  ( `' K `  n )
)  =  n )
33 f1ocnv 5513 . . . . . . . . . . . 12  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  `' K : A -1-1-onto-> ( 1 ... N
) )
34 f1of 5500 . . . . . . . . . . . 12  |-  ( `' K : A -1-1-onto-> ( 1 ... N )  ->  `' K : A --> ( 1 ... N ) )
3521, 33, 343syl 17 . . . . . . . . . . 11  |-  ( ph  ->  `' K : A --> ( 1 ... N ) )
3635ffvelcdmda 5693 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  ( `' K `  n )  e.  ( 1 ... N ) )
37 elfzle2 10094 . . . . . . . . . 10  |-  ( ( `' K `  n )  e.  ( 1 ... N )  ->  ( `' K `  n )  <_  N )
3836, 37syl 14 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  A )  ->  ( `' K `  n )  <_  N )
3919adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  K  Isom  <  ,  <  (
( 1 ... N
) ,  A ) )
40 fzssuz 10131 . . . . . . . . . . . . 13  |-  ( 1 ... N )  C_  ( ZZ>= `  1 )
41 uzssz 9612 . . . . . . . . . . . . . 14  |-  ( ZZ>= ` 
1 )  C_  ZZ
42 zssre 9324 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
4341, 42sstri 3188 . . . . . . . . . . . . 13  |-  ( ZZ>= ` 
1 )  C_  RR
4440, 43sstri 3188 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  RR
45 ressxr 8063 . . . . . . . . . . . 12  |-  RR  C_  RR*
4644, 45sstri 3188 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  RR*
4746a1i 9 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  (
1 ... N )  C_  RR* )
484adantr 276 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  A )  ->  A  C_  ( ZZ>= `  M )
)
49 uzssz 9612 . . . . . . . . . . . . 13  |-  ( ZZ>= `  M )  C_  ZZ
5049, 42sstri 3188 . . . . . . . . . . . 12  |-  ( ZZ>= `  M )  C_  RR
5148, 50sstrdi 3191 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  A )  ->  A  C_  RR )
5251, 45sstrdi 3191 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  A  C_ 
RR* )
5327adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  N  e.  ( 1 ... N
) )
54 leisorel 10908 . . . . . . . . . 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 1258 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  A )  ->  (
( `' K `  n )  <_  N  <->  ( K `  ( `' K `  n ) )  <_  ( K `  N ) ) )
5638, 55mpbid 147 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  ( `' K `  n )
)  <_  ( K `  N ) )
5732, 56eqbrtrrd 4053 . . . . . . 7  |-  ( (
ph  /\  n  e.  A )  ->  n  <_  ( K `  N
) )
58 eluzelz 9601 . . . . . . . . 9  |-  ( n  e.  ( ZZ>= `  M
)  ->  n  e.  ZZ )
5930, 58syl 14 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ZZ )
60 eluzelz 9601 . . . . . . . . . 10  |-  ( ( K `  N )  e.  ( ZZ>= `  M
)  ->  ( K `  N )  e.  ZZ )
6129, 60syl 14 . . . . . . . . 9  |-  ( ph  ->  ( K `  N
)  e.  ZZ )
6261adantr 276 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  N )  e.  ZZ )
63 eluz 9605 . . . . . . . 8  |-  ( ( n  e.  ZZ  /\  ( K `  N )  e.  ZZ )  -> 
( ( K `  N )  e.  (
ZZ>= `  n )  <->  n  <_  ( K `  N ) ) )
6459, 62, 63syl2anc 411 . . . . . . 7  |-  ( (
ph  /\  n  e.  A )  ->  (
( K `  N
)  e.  ( ZZ>= `  n )  <->  n  <_  ( K `  N ) ) )
6557, 64mpbird 167 . . . . . 6  |-  ( (
ph  /\  n  e.  A )  ->  ( K `  N )  e.  ( ZZ>= `  n )
)
66 elfzuzb 10085 . . . . . 6  |-  ( n  e.  ( M ... ( K `  N ) )  <->  ( n  e.  ( ZZ>= `  M )  /\  ( K `  N
)  e.  ( ZZ>= `  n ) ) )
6730, 65, 66sylanbrc 417 . . . . 5  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ( M ... ( K `  N )
) )
6867ex 115 . . . 4  |-  ( ph  ->  ( n  e.  A  ->  n  e.  ( M ... ( K `  N ) ) ) )
6968ssrdv 3185 . . 3  |-  ( ph  ->  A  C_  ( M ... ( K `  N
) ) )
701, 2, 3, 29, 69fsum3cvg 11521 . 2  |-  ( ph  ->  seq M (  +  ,  F )  ~~>  (  seq M (  +  ,  F ) `  ( K `  N )
) )
71 addlid 8158 . . . . 5  |-  ( m  e.  CC  ->  (
0  +  m )  =  m )
7271adantl 277 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( 0  +  m )  =  m )
73 addrid 8157 . . . . 5  |-  ( m  e.  CC  ->  (
m  +  0 )  =  m )
7473adantl 277 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( m  +  0 )  =  m )
75 addcl 7997 . . . . 5  |-  ( ( m  e.  CC  /\  x  e.  CC )  ->  ( m  +  x
)  e.  CC )
7675adantl 277 . . . 4  |-  ( (
ph  /\  ( m  e.  CC  /\  x  e.  CC ) )  -> 
( m  +  x
)  e.  CC )
77 0cnd 8012 . . . 4  |-  ( ph  ->  0  e.  CC )
7827, 16eleqtrrd 2273 . . . 4  |-  ( ph  ->  N  e.  ( 1 ... ( `  A
) ) )
79 iftrue 3562 . . . . . . . . . . . 12  |-  ( k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  =  B )
8079adantl 277 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  =  B )
8180, 2eqeltrd 2270 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8281adantlr 477 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8382adantlr 477 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>=
`  M ) )  /\  k  e.  A
)  ->  if (
k  e.  A ,  B ,  0 )  e.  CC )
84 iffalse 3565 . . . . . . . . . 10  |-  ( -.  k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  =  0 )
85 0cn 8011 . . . . . . . . . 10  |-  0  e.  CC
8684, 85eqeltrdi 2284 . . . . . . . . 9  |-  ( -.  k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
8786adantl 277 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>=
`  M ) )  /\  -.  k  e.  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
883adantlr 477 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  -> DECID  k  e.  A
)
89 exmiddc 837 . . . . . . . . 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 799 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  e.  A ,  B ,  0 )  e.  CC )
92 simpll 527 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  ph )
93 simpr 110 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  -.  k  e.  ( ZZ>= `  M ) )  ->  -.  k  e.  ( ZZ>=
`  M ) )
944ssneld 3181 . . . . . . . . 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 9675 . . . . . . . . 9  |-  ( ( M  e.  ZZ  /\  k  e.  ZZ )  -> DECID  k  e.  ( ZZ>= `  M
) )
9997, 98sylan 283 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ZZ )  -> DECID  k  e.  ( ZZ>=
`  M ) )
100 exmiddc 837 . . . . . . . 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 799 . . . . . 6  |-  ( (
ph  /\  k  e.  ZZ )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
103102, 1fmptd 5712 . . . . 5  |-  ( ph  ->  F : ZZ --> CC )
104 eluzelz 9601 . . . . 5  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
105 ffvelcdm 5691 . . . . 5  |-  ( ( F : ZZ --> CC  /\  m  e.  ZZ )  ->  ( F `  m
)  e.  CC )
106103, 104, 105syl2an 289 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  M )
)  ->  ( F `  m )  e.  CC )
107 elnnuz 9629 . . . . . . . 8  |-  ( m  e.  NN  <->  m  e.  ( ZZ>= `  1 )
)
108107biimpri 133 . . . . . . 7  |-  ( m  e.  ( ZZ>= `  1
)  ->  m  e.  NN )
109108adantl 277 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  m  e.  NN )
110 isof1o 5850 . . . . . . . . . . . 12  |-  ( K 
Isom  <  ,  <  (
( 1 ... ( `  A ) ) ,  A )  ->  K : ( 1 ... ( `  A )
)
-1-1-onto-> A )
111 f1of 5500 . . . . . . . . . . . 12  |-  ( K : ( 1 ... ( `  A )
)
-1-1-onto-> A  ->  K : ( 1 ... ( `  A
) ) --> A )
1125, 110, 1113syl 17 . . . . . . . . . . 11  |-  ( ph  ->  K : ( 1 ... ( `  A
) ) --> A )
113112ad2antrr 488 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  K :
( 1 ... ( `  A ) ) --> A )
114 1zzd 9344 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  1  e.  ZZ )
11515, 8eqeltrd 2270 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `  A )  e.  ZZ )
116115ad2antrr 488 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( `  A
)  e.  ZZ )
117 eluzelz 9601 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  m  e.  ZZ )
118117ad2antlr 489 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ZZ )
119114, 116, 1183jca 1179 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  m  e.  ZZ ) )
120 eluzle 9604 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  1  <_  m )
121120ad2antlr 489 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  1  <_  m )
122 simpr 110 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  <_  N )
12315breq2d 4041 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  <_  ( `  A )  <->  m  <_  N ) )
124123ad2antrr 488 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( m  <_  ( `  A )  <->  m  <_  N ) )
125122, 124mpbird 167 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  <_  ( `  A ) )
126121, 125jca 306 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( 1  <_  m  /\  m  <_  ( `  A )
) )
127 elfz2 10081 . . . . . . . . . . 11  |-  ( m  e.  ( 1 ... ( `  A )
)  <->  ( ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  m  e.  ZZ )  /\  ( 1  <_  m  /\  m  <_  ( `  A ) ) ) )
128119, 126, 127sylanbrc 417 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ( 1 ... ( `  A ) ) )
129113, 128ffvelcdmd 5694 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
130129iftrued 3564 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  if (
( K `  m
)  e.  A ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  =  [_ ( K `
 m )  / 
k ]_ B )
1314ad2antrr 488 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  A  C_  ( ZZ>=
`  M ) )
13223ad2antrr 488 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  K :
( 1 ... N
) --> A )
13316eleq2d 2263 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( m  e.  ( 1 ... ( `  A
) )  <->  m  e.  ( 1 ... N
) ) )
134133ad2antrr 488 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( m  e.  ( 1 ... ( `  A ) )  <->  m  e.  ( 1 ... N
) ) )
135128, 134mpbid 147 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ( 1 ... N
) )
136132, 135ffvelcdmd 5694 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
137131, 136sseldd 3180 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  (
ZZ>= `  M ) )
13849, 137sselid 3177 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  ZZ )
139102ralrimiva 2567 . . . . . . . . . 10  |-  ( ph  ->  A. k  e.  ZZ  if ( k  e.  A ,  B ,  0 )  e.  CC )
140139ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  A. k  e.  ZZ  if ( k  e.  A ,  B ,  0 )  e.  CC )
141 nfv 1539 . . . . . . . . . . . 12  |-  F/ k ( K `  m
)  e.  A
142 nfcsb1v 3113 . . . . . . . . . . . 12  |-  F/_ k [_ ( K `  m
)  /  k ]_ B
143 nfcv 2336 . . . . . . . . . . . 12  |-  F/_ k
0
144141, 142, 143nfif 3585 . . . . . . . . . . 11  |-  F/_ k if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )
145144nfel1 2347 . . . . . . . . . 10  |-  F/ k if ( ( K `
 m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )  e.  CC
146 eleq1 2256 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  (
k  e.  A  <->  ( K `  m )  e.  A
) )
147 csbeq1a 3089 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  B  =  [_ ( K `  m )  /  k ]_ B )
148146, 147ifbieq1d 3579 . . . . . . . . . . 11  |-  ( k  =  ( K `  m )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
149148eleq1d 2262 . . . . . . . . . 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 2858 . . . . . . . . 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 2271 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  [_ ( K `
 m )  / 
k ]_ B  e.  CC )
153 0cnd 8012 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  -.  m  <_  N )  ->  0  e.  CC )
154109nnzd 9438 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  m  e.  ZZ )
1558adantr 276 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  N  e.  ZZ )
156 zdcle 9393 . . . . . . . 8  |-  ( ( m  e.  ZZ  /\  N  e.  ZZ )  -> DECID  m  <_  N )
157154, 155, 156syl2anc 411 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  -> DECID  m  <_  N )
158152, 153, 157ifcldadc 3586 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  if (
m  <_  N ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  e.  CC )
159 breq1 4032 . . . . . . . 8  |-  ( n  =  m  ->  (
n  <_  N  <->  m  <_  N ) )
160 fveq2 5554 . . . . . . . . 9  |-  ( n  =  m  ->  ( K `  n )  =  ( K `  m ) )
161160csbeq1d 3087 . . . . . . . 8  |-  ( n  =  m  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  m )  /  k ]_ B )
162159, 161ifbieq1d 3579 . . . . . . 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 5633 . . . . . 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 411 . . . . 5  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  ( H `  m )  =  if ( m  <_  N ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
166165, 158eqeltrd 2270 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  ( H `  m )  e.  CC )
167 fveqeq2 5563 . . . . . 6  |-  ( k  =  m  ->  (
( F `  k
)  =  0  <->  ( F `  m )  =  0 ) )
168 eldifi 3281 . . . . . . . . 9  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ( M ... ( K `
 ( `  A
) ) ) )
169 elfzelz 10091 . . . . . . . . 9  |-  ( k  e.  ( M ... ( K `  ( `  A
) ) )  -> 
k  e.  ZZ )
170168, 169syl 14 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ZZ )
171 eldifn 3282 . . . . . . . . . 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 2284 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
1741fvmpt2 5641 . . . . . . . 8  |-  ( ( k  e.  ZZ  /\  if ( k  e.  A ,  B ,  0 )  e.  CC )  -> 
( F `  k
)  =  if ( k  e.  A ,  B ,  0 ) )
175170, 173, 174syl2anc 411 . . . . . . 7  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  k )  =  if ( k  e.  A ,  B ,  0 ) )
176175, 172eqtrd 2226 . . . . . 6  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  k )  =  0 )
177167, 176vtoclga 2826 . . . . 5  |-  ( m  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  m )  =  0 )
178177adantl 277 . . . 4  |-  ( (
ph  /\  m  e.  ( ( M ... ( K `  ( `  A
) ) )  \  A ) )  -> 
( F `  m
)  =  0 )
179112ffvelcdmda 5693 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  A
)
180179iftrued 3564 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  = 
[_ ( K `  x )  /  k ]_ B )
1814adantr 276 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  A  C_  ( ZZ>=
`  M ) )
182181, 179sseldd 3180 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  (
ZZ>= `  M ) )
183 eluzelz 9601 . . . . . . 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 109 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ph )
186185, 184jca 306 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( ph  /\  ( K `  x )  e.  ZZ ) )
187 nfv 1539 . . . . . . . . 9  |-  F/ k ( ph  /\  ( K `  x )  e.  ZZ )
188 nfv 1539 . . . . . . . . . . 11  |-  F/ k ( K `  x
)  e.  A
189 nfcsb1v 3113 . . . . . . . . . . 11  |-  F/_ k [_ ( K `  x
)  /  k ]_ B
190188, 189, 143nfif 3585 . . . . . . . . . 10  |-  F/_ k if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )
191190nfel1 2347 . . . . . . . . 9  |-  F/ k if ( ( K `
 x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC
192187, 191nfim 1583 . . . . . . . 8  |-  F/ k ( ( ph  /\  ( K `  x )  e.  ZZ )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
193 eleq1 2256 . . . . . . . . . 10  |-  ( k  =  ( K `  x )  ->  (
k  e.  ZZ  <->  ( K `  x )  e.  ZZ ) )
194193anbi2d 464 . . . . . . . . 9  |-  ( k  =  ( K `  x )  ->  (
( ph  /\  k  e.  ZZ )  <->  ( ph  /\  ( K `  x
)  e.  ZZ ) ) )
195 eleq1 2256 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  (
k  e.  A  <->  ( K `  x )  e.  A
) )
196 csbeq1a 3089 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  B  =  [_ ( K `  x )  /  k ]_ B )
197195, 196ifbieq1d 3579 . . . . . . . . . 10  |-  ( k  =  ( K `  x )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
198197eleq1d 2262 . . . . . . . . 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 234 . . . . . . . 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 2819 . . . . . . 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 2256 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  (
n  e.  A  <->  ( K `  x )  e.  A
) )
203 csbeq1 3083 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  [_ n  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
204202, 203ifbieq1d 3579 . . . . . . 7  |-  ( n  =  ( K `  x )  ->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
205 nfcv 2336 . . . . . . . . 9  |-  F/_ n if ( k  e.  A ,  B ,  0 )
206 nfv 1539 . . . . . . . . . 10  |-  F/ k  n  e.  A
207 nfcsb1v 3113 . . . . . . . . . 10  |-  F/_ k [_ n  /  k ]_ B
208206, 207, 143nfif 3585 . . . . . . . . 9  |-  F/_ k if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
209 eleq1 2256 . . . . . . . . . 10  |-  ( k  =  n  ->  (
k  e.  A  <->  n  e.  A ) )
210 csbeq1a 3089 . . . . . . . . . 10  |-  ( k  =  n  ->  B  =  [_ n  /  k ]_ B )
211209, 210ifbieq1d 3579 . . . . . . . . 9  |-  ( k  =  n  ->  if ( k  e.  A ,  B ,  0 )  =  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
212205, 208, 211cbvmpt 4124 . . . . . . . 8  |-  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2131, 212eqtri 2214 . . . . . . 7  |-  F  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
214204, 213fvmptg 5633 . . . . . 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 411 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( F `  ( K `  x ) )  =  if ( ( K `  x
)  e.  A ,  [_ ( K `  x
)  /  k ]_ B ,  0 ) )
216 elfznn 10120 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  e.  NN )
217216adantl 277 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  e.  NN )
218 elfzle2 10094 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  <_  ( `  A ) )
219218adantl 277 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  <_  ( `  A ) )
22015breq2d 4041 . . . . . . . . . . 11  |-  ( ph  ->  ( x  <_  ( `  A )  <->  x  <_  N ) )
221220adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( x  <_ 
( `  A )  <->  x  <_  N ) )
222219, 221mpbid 147 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  <_  N
)
223222iftrued 3564 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  = 
[_ ( K `  x )  /  k ]_ B )
224180, 201eqeltrrd 2271 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  [_ ( K `  x )  /  k ]_ B  e.  CC )
225223, 224eqeltrd 2270 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
226 breq1 4032 . . . . . . . . 9  |-  ( n  =  x  ->  (
n  <_  N  <->  x  <_  N ) )
227 fveq2 5554 . . . . . . . . . 10  |-  ( n  =  x  ->  ( K `  n )  =  ( K `  x ) )
228227csbeq1d 3087 . . . . . . . . 9  |-  ( n  =  x  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
229226, 228ifbieq1d 3579 . . . . . . . 8  |-  ( n  =  x  ->  if ( n  <_  N ,  [_ ( K `  n
)  /  k ]_ B ,  0 )  =  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
230229, 163fvmptg 5633 . . . . . . 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 411 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
232231, 223eqtrd 2226 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  [_ ( K `  x )  /  k ]_ B
)
233180, 215, 2323eqtr4rd 2237 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  ( F `  ( K `
 x ) ) )
23472, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233seq3coll 10913 . . 3  |-  ( ph  ->  (  seq M (  +  ,  F ) `
 ( K `  N ) )  =  (  seq 1 (  +  ,  H ) `
 N ) )
23515, 7eqeltrd 2270 . . . . 5  |-  ( ph  ->  ( `  A )  e.  NN )
236235, 7jca 306 . . . 4  |-  ( ph  ->  ( ( `  A
)  e.  NN  /\  N  e.  NN )
)
23716eqcomd 2199 . . . . . 6  |-  ( ph  ->  ( 1 ... N
)  =  ( 1 ... ( `  A
) ) )
238 f1oeq2 5489 . . . . . 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 147 . . . 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 11523 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ) `
 ( `  A
) )  =  (  seq 1 (  +  ,  H ) `  N ) )
24315fveq2d 5558 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ) `
 ( `  A
) )  =  (  seq 1 (  +  ,  G ) `  N ) )
244234, 242, 2433eqtr2d 2232 . 2  |-  ( ph  ->  (  seq M (  +  ,  F ) `
 ( K `  N ) )  =  (  seq 1 (  +  ,  G ) `
 N ) )
24570, 244breqtrd 4055 1  |-  ( ph  ->  seq M (  +  ,  F )  ~~>  (  seq 1 (  +  ,  G ) `  N
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709  DECID wdc 835    /\ w3a 980    = wceq 1364    e. wcel 2164   A.wral 2472   [_csb 3080    \ cdif 3150    C_ wss 3153   ifcif 3557   class class class wbr 4029    |-> cmpt 4090   `'ccnv 4658   -->wf 5250   -1-1-onto->wf1o 5253   ` cfv 5254    Isom wiso 5255  (class class class)co 5918   CCcc 7870   RRcr 7871   0cc0 7872   1c1 7873    + caddc 7875   RR*cxr 8053    < clt 8054    <_ cle 8055   NNcn 8982   NN0cn0 9240   ZZcz 9317   ZZ>=cuz 9592   ...cfz 10074    seqcseq 10518  ♯chash 10846    ~~> cli 11421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-nul 4155  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-iinf 4620  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-mulrcl 7971  ax-addcom 7972  ax-mulcom 7973  ax-addass 7974  ax-mulass 7975  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-1rid 7979  ax-0id 7980  ax-rnegex 7981  ax-precex 7982  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-apti 7987  ax-pre-ltadd 7988  ax-pre-mulgt0 7989  ax-pre-mulext 7990
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-if 3558  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-tr 4128  df-id 4324  df-po 4327  df-iso 4328  df-iord 4397  df-on 4399  df-ilim 4400  df-suc 4402  df-iom 4623  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-isom 5263  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-recs 6358  df-frec 6444  df-1o 6469  df-er 6587  df-en 6795  df-dom 6796  df-fin 6797  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-reap 8594  df-ap 8601  df-div 8692  df-inn 8983  df-2 9041  df-n0 9241  df-z 9318  df-uz 9593  df-rp 9720  df-fz 10075  df-fzo 10209  df-seqfrec 10519  df-exp 10610  df-ihash 10847  df-cj 10986  df-rsqrt 11142  df-abs 11143  df-clim 11422
This theorem is referenced by:  summodclem2  11525  zsumdc  11527
  Copyright terms: Public domain W3C validator