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

Theorem summodclem2a 11105
Description: Lemma for summodc 11107. (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 9039 . . . . . . . . . . . . 13  |-  ( ph  ->  1  e.  ZZ )
7 summolem2.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  NN )
87nnzd 9130 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ZZ )
96, 8fzfigd 10159 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1 ... N
)  e.  Fin )
10 summolem2.8 . . . . . . . . . . . 12  |-  ( ph  ->  f : ( 1 ... N ) -1-1-onto-> A )
119, 10fihasheqf1od 10491 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  ( `  A )
)
12 nnnn0 8942 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  NN0 )
13 hashfz1 10484 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  ( `  (
1 ... N ) )  =  N )
147, 12, 133syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( `  ( 1 ... N ) )  =  N )
1511, 14eqtr3d 2152 . . . . . . . . . 10  |-  ( ph  ->  ( `  A )  =  N )
1615oveq2d 5758 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... ( `  A ) )  =  ( 1 ... N
) )
17 isoeq4 5673 . . . . . . . . 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 5676 . . . . . . 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 5335 . . . . . 6  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  K :
( 1 ... N
) --> A )
2321, 22syl 14 . . . . 5  |-  ( ph  ->  K : ( 1 ... N ) --> A )
24 nnuz 9317 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
257, 24eleqtrdi 2210 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
26 eluzfz2 9767 . . . . . 6  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
2725, 26syl 14 . . . . 5  |-  ( ph  ->  N  e.  ( 1 ... N ) )
2823, 27ffvelrnd 5524 . . . 4  |-  ( ph  ->  ( K `  N
)  e.  A )
294, 28sseldd 3068 . . 3  |-  ( ph  ->  ( K `  N
)  e.  ( ZZ>= `  M ) )
304sselda 3067 . . . . . 6  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ( ZZ>= `  M )
)
31 f1ocnvfv2 5647 . . . . . . . . 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 5348 . . . . . . . . . . . 12  |-  ( K : ( 1 ... N ) -1-1-onto-> A  ->  `' K : A -1-1-onto-> ( 1 ... N
) )
34 f1of 5335 . . . . . . . . . . . 12  |-  ( `' K : A -1-1-onto-> ( 1 ... N )  ->  `' K : A --> ( 1 ... N ) )
3521, 33, 343syl 17 . . . . . . . . . . 11  |-  ( ph  ->  `' K : A --> ( 1 ... N ) )
3635ffvelrnda 5523 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  ( `' K `  n )  e.  ( 1 ... N ) )
37 elfzle2 9763 . . . . . . . . . 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 9800 . . . . . . . . . . . . 13  |-  ( 1 ... N )  C_  ( ZZ>= `  1 )
41 uzssz 9301 . . . . . . . . . . . . . 14  |-  ( ZZ>= ` 
1 )  C_  ZZ
42 zssre 9019 . . . . . . . . . . . . . 14  |-  ZZ  C_  RR
4341, 42sstri 3076 . . . . . . . . . . . . 13  |-  ( ZZ>= ` 
1 )  C_  RR
4440, 43sstri 3076 . . . . . . . . . . . 12  |-  ( 1 ... N )  C_  RR
45 ressxr 7777 . . . . . . . . . . . 12  |-  RR  C_  RR*
4644, 45sstri 3076 . . . . . . . . . . 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 9301 . . . . . . . . . . . . 13  |-  ( ZZ>= `  M )  C_  ZZ
5049, 42sstri 3076 . . . . . . . . . . . 12  |-  ( ZZ>= `  M )  C_  RR
5148, 50sstrdi 3079 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  A )  ->  A  C_  RR )
5251, 45sstrdi 3079 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  A  C_ 
RR* )
5327adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  A )  ->  N  e.  ( 1 ... N
) )
54 leisorel 10535 . . . . . . . . . 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 1210 . . . . . . . . 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 3922 . . . . . . 7  |-  ( (
ph  /\  n  e.  A )  ->  n  <_  ( K `  N
) )
58 eluzelz 9291 . . . . . . . . 9  |-  ( n  e.  ( ZZ>= `  M
)  ->  n  e.  ZZ )
5930, 58syl 14 . . . . . . . 8  |-  ( (
ph  /\  n  e.  A )  ->  n  e.  ZZ )
60 eluzelz 9291 . . . . . . . . . 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 9295 . . . . . . . 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 9755 . . . . . 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 3073 . . 3  |-  ( ph  ->  A  C_  ( M ... ( K `  N
) ) )
701, 2, 3, 29, 69fsum3cvg 11101 . 2  |-  ( ph  ->  seq M (  +  ,  F )  ~~>  (  seq M (  +  ,  F ) `  ( K `  N )
) )
71 addid2 7869 . . . . 5  |-  ( m  e.  CC  ->  (
0  +  m )  =  m )
7271adantl 275 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( 0  +  m )  =  m )
73 addid1 7868 . . . . 5  |-  ( m  e.  CC  ->  (
m  +  0 )  =  m )
7473adantl 275 . . . 4  |-  ( (
ph  /\  m  e.  CC )  ->  ( m  +  0 )  =  m )
75 addcl 7713 . . . . 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 7727 . . . 4  |-  ( ph  ->  0  e.  CC )
7827, 16eleqtrrd 2197 . . . 4  |-  ( ph  ->  N  e.  ( 1 ... ( `  A
) ) )
79 iftrue 3449 . . . . . . . . . . . 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 2194 . . . . . . . . . 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 3452 . . . . . . . . . 10  |-  ( -.  k  e.  A  ->  if ( k  e.  A ,  B ,  0 )  =  0 )
85 0cn 7726 . . . . . . . . . 10  |-  0  e.  CC
8684, 85syl6eqel 2208 . . . . . . . . 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 806 . . . . . . . . 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 772 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  ZZ )  /\  k  e.  ( ZZ>= `  M )
)  ->  if (
k  e.  A ,  B ,  0 )  e.  CC )
92 simpll 503 . . . . . . . . 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 3069 . . . . . . . . 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 9360 . . . . . . . . 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 806 . . . . . . . 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 772 . . . . . 6  |-  ( (
ph  /\  k  e.  ZZ )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
103102, 1fmptd 5542 . . . . 5  |-  ( ph  ->  F : ZZ --> CC )
104 eluzelz 9291 . . . . 5  |-  ( m  e.  ( ZZ>= `  M
)  ->  m  e.  ZZ )
105 ffvelrn 5521 . . . . 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 9318 . . . . . . . 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 5676 . . . . . . . . . . . 12  |-  ( K 
Isom  <  ,  <  (
( 1 ... ( `  A ) ) ,  A )  ->  K : ( 1 ... ( `  A )
)
-1-1-onto-> A )
111 f1of 5335 . . . . . . . . . . . 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 9039 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  1  e.  ZZ )
11515, 8eqeltrd 2194 . . . . . . . . . . . . 13  |-  ( ph  ->  ( `  A )  e.  ZZ )
116115ad2antrr 479 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( `  A
)  e.  ZZ )
117 eluzelz 9291 . . . . . . . . . . . . 13  |-  ( m  e.  ( ZZ>= `  1
)  ->  m  e.  ZZ )
118117ad2antlr 480 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  m  e.  ZZ )
119114, 116, 1183jca 1146 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( 1  e.  ZZ  /\  ( `  A )  e.  ZZ  /\  m  e.  ZZ ) )
120 eluzle 9294 . . . . . . . . . . . . 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 3911 . . . . . . . . . . . . . 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 9752 . . . . . . . . . . 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 5524 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
130129iftrued 3451 . . . . . . . 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 2187 . . . . . . . . . . . . . 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 5524 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  A
)
137131, 136sseldd 3068 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  (
ZZ>= `  M ) )
13849, 137sseldi 3065 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  ( K `  m )  e.  ZZ )
139102ralrimiva 2482 . . . . . . . . . 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 1493 . . . . . . . . . . . 12  |-  F/ k ( K `  m
)  e.  A
142 nfcsb1v 3005 . . . . . . . . . . . 12  |-  F/_ k [_ ( K `  m
)  /  k ]_ B
143 nfcv 2258 . . . . . . . . . . . 12  |-  F/_ k
0
144141, 142, 143nfif 3470 . . . . . . . . . . 11  |-  F/_ k if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )
145144nfel1 2269 . . . . . . . . . 10  |-  F/ k if ( ( K `
 m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 )  e.  CC
146 eleq1 2180 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  (
k  e.  A  <->  ( K `  m )  e.  A
) )
147 csbeq1a 2983 . . . . . . . . . . . 12  |-  ( k  =  ( K `  m )  ->  B  =  [_ ( K `  m )  /  k ]_ B )
148146, 147ifbieq1d 3464 . . . . . . . . . . 11  |-  ( k  =  ( K `  m )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  m )  e.  A ,  [_ ( K `  m )  /  k ]_ B ,  0 ) )
149148eleq1d 2186 . . . . . . . . . 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 2757 . . . . . . . . 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 2195 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  m  <_  N )  ->  [_ ( K `
 m )  / 
k ]_ B  e.  CC )
153 0cnd 7727 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  1 )
)  /\  -.  m  <_  N )  ->  0  e.  CC )
154109nnzd 9130 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  m  e.  ZZ )
1558adantr 274 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  N  e.  ZZ )
156 zdcle 9085 . . . . . . . 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 3471 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  if (
m  <_  N ,  [_ ( K `  m
)  /  k ]_ B ,  0 )  e.  CC )
159 breq1 3902 . . . . . . . 8  |-  ( n  =  m  ->  (
n  <_  N  <->  m  <_  N ) )
160 fveq2 5389 . . . . . . . . 9  |-  ( n  =  m  ->  ( K `  n )  =  ( K `  m ) )
161160csbeq1d 2981 . . . . . . . 8  |-  ( n  =  m  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  m )  /  k ]_ B )
162159, 161ifbieq1d 3464 . . . . . . 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 5465 . . . . . 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 2194 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  1 )
)  ->  ( H `  m )  e.  CC )
167 fveqeq2 5398 . . . . . 6  |-  ( k  =  m  ->  (
( F `  k
)  =  0  <->  ( F `  m )  =  0 ) )
168 eldifi 3168 . . . . . . . . 9  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ( M ... ( K `
 ( `  A
) ) ) )
169 elfzelz 9761 . . . . . . . . 9  |-  ( k  e.  ( M ... ( K `  ( `  A
) ) )  -> 
k  e.  ZZ )
170168, 169syl 14 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  k  e.  ZZ )
171 eldifn 3169 . . . . . . . . . 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 2208 . . . . . . . 8  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  if ( k  e.  A ,  B ,  0 )  e.  CC )
1741fvmpt2 5472 . . . . . . . 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 2150 . . . . . 6  |-  ( k  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  k )  =  0 )
177167, 176vtoclga 2726 . . . . 5  |-  ( m  e.  ( ( M ... ( K `  ( `  A ) ) )  \  A )  ->  ( F `  m )  =  0 )
178177adantl 275 . . . 4  |-  ( (
ph  /\  m  e.  ( ( M ... ( K `  ( `  A
) ) )  \  A ) )  -> 
( F `  m
)  =  0 )
179112ffvelrnda 5523 . . . . . 6  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  A
)
180179iftrued 3451 . . . . 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 3068 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( K `  x )  e.  (
ZZ>= `  M ) )
183 eluzelz 9291 . . . . . . 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 1493 . . . . . . . . 9  |-  F/ k ( ph  /\  ( K `  x )  e.  ZZ )
188 nfv 1493 . . . . . . . . . . 11  |-  F/ k ( K `  x
)  e.  A
189 nfcsb1v 3005 . . . . . . . . . . 11  |-  F/_ k [_ ( K `  x
)  /  k ]_ B
190188, 189, 143nfif 3470 . . . . . . . . . 10  |-  F/_ k if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )
191190nfel1 2269 . . . . . . . . 9  |-  F/ k if ( ( K `
 x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC
192187, 191nfim 1536 . . . . . . . 8  |-  F/ k ( ( ph  /\  ( K `  x )  e.  ZZ )  ->  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
193 eleq1 2180 . . . . . . . . . 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 2180 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  (
k  e.  A  <->  ( K `  x )  e.  A
) )
196 csbeq1a 2983 . . . . . . . . . . 11  |-  ( k  =  ( K `  x )  ->  B  =  [_ ( K `  x )  /  k ]_ B )
197195, 196ifbieq1d 3464 . . . . . . . . . 10  |-  ( k  =  ( K `  x )  ->  if ( k  e.  A ,  B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
198197eleq1d 2186 . . . . . . . . 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 2719 . . . . . . 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 2180 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  (
n  e.  A  <->  ( K `  x )  e.  A
) )
203 csbeq1 2978 . . . . . . . 8  |-  ( n  =  ( K `  x )  ->  [_ n  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
204202, 203ifbieq1d 3464 . . . . . . 7  |-  ( n  =  ( K `  x )  ->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )  =  if ( ( K `  x )  e.  A ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
205 nfcv 2258 . . . . . . . . 9  |-  F/_ n if ( k  e.  A ,  B ,  0 )
206 nfv 1493 . . . . . . . . . 10  |-  F/ k  n  e.  A
207 nfcsb1v 3005 . . . . . . . . . 10  |-  F/_ k [_ n  /  k ]_ B
208206, 207, 143nfif 3470 . . . . . . . . 9  |-  F/_ k if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 )
209 eleq1 2180 . . . . . . . . . 10  |-  ( k  =  n  ->  (
k  e.  A  <->  n  e.  A ) )
210 csbeq1a 2983 . . . . . . . . . 10  |-  ( k  =  n  ->  B  =  [_ n  /  k ]_ B )
211209, 210ifbieq1d 3464 . . . . . . . . 9  |-  ( k  =  n  ->  if ( k  e.  A ,  B ,  0 )  =  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
212205, 208, 211cbvmpt 3993 . . . . . . . 8  |-  ( k  e.  ZZ  |->  if ( k  e.  A ,  B ,  0 ) )  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
2131, 212eqtri 2138 . . . . . . 7  |-  F  =  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) )
214204, 213fvmptg 5465 . . . . . 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 9789 . . . . . . . 8  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  e.  NN )
217216adantl 275 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  e.  NN )
218 elfzle2 9763 . . . . . . . . . . 11  |-  ( x  e.  ( 1 ... ( `  A )
)  ->  x  <_  ( `  A ) )
219218adantl 275 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  x  <_  ( `  A ) )
22015breq2d 3911 . . . . . . . . . . 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 3451 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  = 
[_ ( K `  x )  /  k ]_ B )
224180, 201eqeltrrd 2195 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  [_ ( K `  x )  /  k ]_ B  e.  CC )
225223, 224eqeltrd 2194 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 )  e.  CC )
226 breq1 3902 . . . . . . . . 9  |-  ( n  =  x  ->  (
n  <_  N  <->  x  <_  N ) )
227 fveq2 5389 . . . . . . . . . 10  |-  ( n  =  x  ->  ( K `  n )  =  ( K `  x ) )
228227csbeq1d 2981 . . . . . . . . 9  |-  ( n  =  x  ->  [_ ( K `  n )  /  k ]_ B  =  [_ ( K `  x )  /  k ]_ B )
229226, 228ifbieq1d 3464 . . . . . . . 8  |-  ( n  =  x  ->  if ( n  <_  N ,  [_ ( K `  n
)  /  k ]_ B ,  0 )  =  if ( x  <_  N ,  [_ ( K `  x )  /  k ]_ B ,  0 ) )
230229, 163fvmptg 5465 . . . . . . 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 2150 . . . . 5  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  [_ ( K `  x )  /  k ]_ B
)
233180, 215, 2323eqtr4rd 2161 . . . 4  |-  ( (
ph  /\  x  e.  ( 1 ... ( `  A ) ) )  ->  ( H `  x )  =  ( F `  ( K `
 x ) ) )
23472, 74, 76, 77, 5, 78, 4, 106, 166, 178, 233seq3coll 10540 . . 3  |-  ( ph  ->  (  seq M (  +  ,  F ) `
 ( K `  N ) )  =  (  seq 1 (  +  ,  H ) `
 N ) )
23515, 7eqeltrd 2194 . . . . 5  |-  ( ph  ->  ( `  A )  e.  NN )
236235, 7jca 304 . . . 4  |-  ( ph  ->  ( ( `  A
)  e.  NN  /\  N  e.  NN )
)
23716eqcomd 2123 . . . . . 6  |-  ( ph  ->  ( 1 ... N
)  =  ( 1 ... ( `  A
) ) )
238 f1oeq2 5327 . . . . . 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 11104 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ) `
 ( `  A
) )  =  (  seq 1 (  +  ,  H ) `  N ) )
24315fveq2d 5393 . . 3  |-  ( ph  ->  (  seq 1 (  +  ,  G ) `
 ( `  A
) )  =  (  seq 1 (  +  ,  G ) `  N ) )
244234, 242, 2433eqtr2d 2156 . 2  |-  ( ph  ->  (  seq M (  +  ,  F ) `
 ( K `  N ) )  =  (  seq 1 (  +  ,  G ) `
 N ) )
24570, 244breqtrd 3924 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 682  DECID wdc 804    /\ w3a 947    = wceq 1316    e. wcel 1465   A.wral 2393   [_csb 2975    \ cdif 3038    C_ wss 3041   ifcif 3444   class class class wbr 3899    |-> cmpt 3959   `'ccnv 4508   -->wf 5089   -1-1-onto->wf1o 5092   ` cfv 5093    Isom wiso 5094  (class class class)co 5742   CCcc 7586   RRcr 7587   0cc0 7588   1c1 7589    + caddc 7591   RR*cxr 7767    < clt 7768    <_ cle 7769   NNcn 8684   NN0cn0 8935   ZZcz 9012   ZZ>=cuz 9282   ...cfz 9745    seqcseq 10173  ♯chash 10476    ~~> cli 11002
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-isom 5102  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-frec 6256  df-1o 6281  df-er 6397  df-en 6603  df-dom 6604  df-fin 6605  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8304  df-ap 8311  df-div 8400  df-inn 8685  df-2 8743  df-n0 8936  df-z 9013  df-uz 9283  df-rp 9398  df-fz 9746  df-fzo 9875  df-seqfrec 10174  df-exp 10248  df-ihash 10477  df-cj 10569  df-rsqrt 10725  df-abs 10726  df-clim 11003
This theorem is referenced by:  summodclem2  11106  zsumdc  11108
  Copyright terms: Public domain W3C validator