ILE Home Intuitionistic Logic Explorer This is the GIF version.
Change to Unicode version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 3 wff 
-.  ph
wi 4 wff  ( ph  ->  ps )
ax-1 5 |-  ( ph  ->  ( ps  ->  ph ) )
ax-2 6 |-  ( ( ph  ->  ( ps  ->  ch )
)  ->  ( ( ph  ->  ps )  -> 
( ph  ->  ch )
) )
ax-mp 7 |- 
ph   &    |-  ( ph  ->  ps )   =>    |- 
ps
wa 97 wff  ( ph  /\  ps )
wb 98 wff  ( ph  <->  ps )
ax-ia1 99 |-  ( ( ph  /\  ps )  ->  ph )
ax-ia2 100 |-  ( ( ph  /\  ps )  ->  ps )
ax-ia3 101 |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
df-bi 110 |-  ( ( ( ph  <->  ps )  ->  ( ( ph  ->  ps )  /\  ( ps  ->  ph )
) )  /\  (
( ( ph  ->  ps )  /\  ( ps 
->  ph ) )  -> 
( ph  <->  ps ) ) )
ax-in1 544 |-  ( ( ph  ->  -. 
ph )  ->  -.  ph )
ax-in2 545 |-  ( -.  ph  ->  (
ph  ->  ps ) )
wo 629 wff  ( ph  \/  ps )
ax-io 630 |-  ( ( ( ph  \/  ch )  ->  ps ) 
<->  ( ( ph  ->  ps )  /\  ( ch 
->  ps ) ) )
wstab 739 wff STAB  ph
df-stab 740 |-  (STAB 
ph 
<->  ( -.  -.  ph  ->  ph ) )
wdc 742 wff DECID  ph
df-dc 743 |-  (DECID 
ph 
<->  ( ph  \/  -.  ph ) )
w3o 884 wff  ( ph  \/  ps  \/  ch )
w3a 885 wff  ( ph  /\  ps  /\ 
ch )
df-3or 886 |-  ( ( ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/ 
ch ) )
df-3an 887 |-  ( ( ph  /\  ps  /\  ch )  <->  ( ( ph  /\  ps )  /\  ch ) )
wal 1241 wff  A. x ph
cv 1242 class  x
wceq 1243 wff 
A  =  B
wtru 1244 wff T.
df-tru 1246 |-  ( T.  <->  ( A. x  x  =  x  ->  A. x  x  =  x ) )
wfal 1248 wff F.
df-fal 1249 |-  ( F.  <->  -. T.  )
wxo 1266 wff  ( ph  \/_  ps )
df-xor 1267 |-  ( ( ph  \/_  ps ) 
<->  ( ( ph  \/  ps )  /\  -.  ( ph  /\  ps ) ) )
ax-5 1336 |-  ( A. x ( ph  ->  ps )  ->  ( A. x ph  ->  A. x ps ) )
ax-7 1337 |-  ( A. x A. y ph  ->  A. y A. x ph )
ax-gen 1338 |- 
ph   =>    |- 
A. x ph
wnf 1349 wff 
F/ x ph
df-nf 1350 |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
wex 1381 wff 
E. x ph
ax-ie1 1382 |-  ( E. x ph  ->  A. x E. x ph )
ax-ie2 1383 |-  ( A. x ( ps  ->  A. x ps )  ->  ( A. x ( ph  ->  ps )  <->  ( E. x ph  ->  ps ) ) )
wcel 1393 wff 
A  e.  B
ax-8 1395 |-  ( x  =  y  ->  ( x  =  z  ->  y  =  z ) )
ax-10 1396 |-  ( A. x  x  =  y  ->  A. y 
y  =  x )
ax-11 1397 |-  ( x  =  y  ->  ( A. y ph  ->  A. x ( x  =  y  ->  ph )
) )
ax-i12 1398 |-  ( A. z  z  =  x  \/  ( A. z  z  =  y  \/  A. z
( x  =  y  ->  A. z  x  =  y ) ) )
ax-bndl 1399 |-  ( A. z  z  =  x  \/  ( A. z  z  =  y  \/  A. x A. z ( x  =  y  ->  A. z  x  =  y )
) )
ax-4 1400 |-  ( A. x ph  ->  ph )
ax-13 1404 |-  ( x  =  y  ->  ( x  e.  z  ->  y  e.  z ) )
ax-14 1405 |-  ( x  =  y  ->  ( z  e.  x  ->  z  e.  y ) )
ax-17 1419 |-  ( ph  ->  A. x ph )
ax-i9 1423 |-  E. x  x  =  y
ax-ial 1427 |-  ( A. x ph  ->  A. x A. x ph )
ax-i5r 1428 |-  ( ( A. x ph  ->  A. x ps )  ->  A. x ( A. x ph  ->  ps )
)
ax-10o 1604 |-  ( A. x  x  =  y  ->  ( A. x ph  ->  A. y ph ) )
wsb 1645 wff 
[ y  /  x ] ph
df-sb 1646 |-  ( [ y  /  x ] ph  <->  ( ( x  =  y  ->  ph )  /\  E. x ( x  =  y  /\  ph ) ) )
ax-16 1695 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
)
ax-11o 1704 |-  ( -.  A. x  x  =  y  ->  ( x  =  y  -> 
( ph  ->  A. x
( x  =  y  ->  ph ) ) ) )
weu 1900 wff 
E! x ph
wmo 1901 wff 
E* x ph
df-eu 1903 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
df-mo 1904 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
ax-ext 2022 |-  ( A. z ( z  e.  x  <->  z  e.  y )  ->  x  =  y )
cab 2026 class  { x  |  ph }
df-clab 2027 |-  ( x  e.  {
y  |  ph }  <->  [ x  /  y ]
ph )
df-cleq 2033 |-  ( A. x ( x  e.  y  <->  x  e.  z )  ->  y  =  z )   =>    |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
df-clel 2036 |-  ( A  e.  B  <->  E. x ( x  =  A  /\  x  e.  B ) )
wnfc 2165 wff  F/_ x A
df-nfc 2167 |-  ( F/_ x A  <->  A. y F/ x  y  e.  A )
wne 2204 wff 
A  =/=  B
wnel 2205 wff 
A  e/  B
df-ne 2206 |-  ( A  =/=  B  <->  -.  A  =  B )
df-nel 2207 |-  ( A  e/  B  <->  -.  A  e.  B )
wral 2306 wff  A. x  e.  A  ph
wrex 2307 wff 
E. x  e.  A  ph
wreu 2308 wff 
E! x  e.  A  ph
wrmo 2309 wff 
E* x  e.  A  ph
crab 2310 class  { x  e.  A  |  ph }
df-ral 2311 |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
df-rex 2312 |-  ( E. x  e.  A  ph  <->  E. x
( x  e.  A  /\  ph ) )
df-reu 2313 |-  ( E! x  e.  A  ph  <->  E! x
( x  e.  A  /\  ph ) )
df-rmo 2314 |-  ( E* x  e.  A  ph  <->  E* x
( x  e.  A  /\  ph ) )
df-rab 2315 |- 
{ x  e.  A  |  ph }  =  {
x  |  ( x  e.  A  /\  ph ) }
cvv 2557 class  _V
df-v 2559 |-  _V  =  { x  |  x  =  x }
wcdeq 2747 wff CondEq ( x  =  y  ->  ph )
df-cdeq 2748 |-  (CondEq ( x  =  y  ->  ph )  <->  ( x  =  y  ->  ph )
)
wsbc 2764 wff  [. A  /  x ]. ph
df-sbc 2765 |-  ( [. A  /  x ]. ph  <->  A  e.  { x  |  ph }
)
csb 2852 class  [_ A  /  x ]_ B
df-csb 2853 |- 
[_ A  /  x ]_ B  =  {
y  |  [. A  /  x ]. y  e.  B }
cdif 2914 class  ( A  \  B )
cun 2915 class  ( A  u.  B )
cin 2916 class  ( A  i^i  B )
wss 2917 wff 
A  C_  B
wpss 2918 wff 
A  C.  B
df-dif 2920 |-  ( A  \  B
)  =  { x  |  ( x  e.  A  /\  -.  x  e.  B ) }
df-un 2922 |-  ( A  u.  B
)  =  { x  |  ( x  e.  A  \/  x  e.  B ) }
df-in 2924 |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B
) }
df-ss 2931 |-  ( A  C_  B  <->  ( A  i^i  B )  =  A )
df-pss 2933 |-  ( A  C.  B  <->  ( A  C_  B  /\  A  =/=  B ) )
c0 3224 class  (/)
df-nul 3225 |-  (/)  =  ( _V  \  _V )
cif 3331 class  if ( ph ,  A ,  B )
df-if 3332 |-  if ( ph ,  A ,  B )  =  {
x  |  ( ( x  e.  A  /\  ph )  \/  ( x  e.  B  /\  -.  ph ) ) }
cpw 3359 class  ~P A
df-pw 3361 |-  ~P A  =  {
x  |  x  C_  A }
csn 3375 class  { A }
cpr 3376 class  { A ,  B }
ctp 3377 class  { A ,  B ,  C }
cop 3378 class  <. A ,  B >.
cotp 3379 class  <. A ,  B ,  C >.
df-sn 3381 |-  { A }  =  {
x  |  x  =  A }
df-pr 3382 |-  { A ,  B }  =  ( { A }  u.  { B } )
df-tp 3383 |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
df-op 3384 |-  <. A ,  B >.  =  { x  |  ( A  e.  _V  /\  B  e.  _V  /\  x  e.  { { A } ,  { A ,  B } } ) }
df-ot 3385 |-  <. A ,  B ,  C >.  =  <. <. A ,  B >. ,  C >.
cuni 3580 class  U. A
df-uni 3581 |- 
U. A  =  {
x  |  E. y
( x  e.  y  /\  y  e.  A
) }
cint 3615 class  |^| A
df-int 3616 |- 
|^| A  =  {
x  |  A. y
( y  e.  A  ->  x  e.  y ) }
ciun 3657 class  U_ x  e.  A  B
ciin 3658 class  |^|_
x  e.  A  B
df-iun 3659 |- 
U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
df-iin 3660 |- 
|^|_ x  e.  A  B  =  { y  |  A. x  e.  A  y  e.  B }
wdisj 3745 wff Disj  x  e.  A  B
df-disj 3746 |-  (Disj  x  e.  A  B 
<-> 
A. y E* x  e.  A  y  e.  B )
wbr 3764 wff 
A R B
df-br 3765 |-  ( A R B  <->  <. A ,  B >.  e.  R )
copab 3817 class  {
<. x ,  y >.  |  ph }
cmpt 3818 class  ( x  e.  A  |->  B )
df-opab 3819 |- 
{ <. x ,  y
>.  |  ph }  =  { z  |  E. x E. y ( z  =  <. x ,  y
>.  /\  ph ) }
df-mpt 3820 |-  ( x  e.  A  |->  B )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  B ) }
wtr 3854 wff 
Tr  A
df-tr 3855 |-  ( Tr  A  <->  U. A  C_  A )
ax-coll 3872 |-  F/ b ph   =>    |-  ( A. x  e.  a  E. y ph  ->  E. b A. x  e.  a  E. y  e.  b  ph )
ax-sep 3875 |- 
E. y A. x
( x  e.  y  <-> 
( x  e.  z  /\  ph ) )
ax-nul 3883 |- 
E. x A. y  -.  y  e.  x
ax-pow 3927 |- 
E. y A. z
( A. w ( w  e.  z  ->  w  e.  x )  ->  z  e.  y )
ax-pr 3944 |-  E. z A. w ( ( w  =  x  \/  w  =  y )  ->  w  e.  z )
cep 4024 class  _E
cid 4025 class  _I
df-eprel 4026 |-  _E  =  { <. x ,  y >.  |  x  e.  y }
df-id 4030 |-  _I  =  { <. x ,  y >.  |  x  =  y }
wpo 4031 wff 
R  Po  A
wor 4032 wff 
R  Or  A
df-po 4033 |-  ( R  Po  A  <->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) ) )
df-iso 4034 |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x R y  -> 
( x R z  \/  z R y ) ) ) )
wfrfor 4064 wff FrFor  R A S
wfr 4065 wff 
R  Fr  A
wse 4066 wff 
R Se  A
wwe 4067 wff 
R  We  A
df-frfor 4068 |-  (FrFor  R A S  <-> 
( A. x  e.  A  ( A. y  e.  A  ( y R x  ->  y  e.  S )  ->  x  e.  S )  ->  A  C_  S ) )
df-frind 4069 |-  ( R  Fr  A  <->  A. sFrFor  R A s )
df-se 4070 |-  ( R Se  A  <->  A. x  e.  A  { y  e.  A  |  y R x }  e.  _V )
df-wetr 4071 |-  ( R  We  A  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  (
( x R y  /\  y R z )  ->  x R
z ) ) )
word 4099 wff 
Ord  A
con0 4100 class  On
wlim 4101 wff 
Lim  A
csuc 4102 class  suc 
A
df-iord 4103 |-  ( Ord  A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
df-on 4105 |-  On  =  { x  |  Ord  x }
df-ilim 4106 |-  ( Lim  A  <->  ( Ord  A  /\  (/)  e.  A  /\  A  =  U. A ) )
df-suc 4108 |- 
suc  A  =  ( A  u.  { A } )
ax-un 4170 |-  E. y A. z ( E. w ( z  e.  w  /\  w  e.  x )  ->  z  e.  y )
ax-setind 4262 |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-iinf 4311 |- 
E. x ( (/)  e.  x  /\  A. y
( y  e.  x  ->  suc  y  e.  x
) )
com 4313 class  om
df-iom 4314 |- 
om  =  |^| { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
cxp 4343 class  ( A  X.  B )
ccnv 4344 class  `' A
cdm 4345 class  dom 
A
crn 4346 class  ran 
A
cres 4347 class  ( A  |`  B )
cima 4348 class  ( A " B )
ccom 4349 class  ( A  o.  B )
wrel 4350 wff 
Rel  A
df-xp 4351 |-  ( A  X.  B
)  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  B ) }
df-rel 4352 |-  ( Rel  A  <->  A  C_  ( _V  X.  _V ) )
df-cnv 4353 |-  `' A  =  { <. x ,  y >.  |  y A x }
df-co 4354 |-  ( A  o.  B
)  =  { <. x ,  y >.  |  E. z ( x B z  /\  z A y ) }
df-dm 4355 |-  dom  A  =  { x  |  E. y  x A y }
df-rn 4356 |-  ran  A  =  dom  `' A
df-res 4357 |-  ( A  |`  B )  =  ( A  i^i  ( B  X.  _V )
)
df-ima 4358 |-  ( A " B
)  =  ran  ( A  |`  B )
cio 4865 class  ( iota x ph )
df-iota 4867 |-  ( iota x ph )  =  U. { y  |  { x  | 
ph }  =  {
y } }
wfun 4896 wff 
Fun  A
wfn 4897 wff 
A  Fn  B
wf 4898 wff 
F : A --> B
wf1 4899 wff 
F : A -1-1-> B
wfo 4900 wff 
F : A -onto-> B
wf1o 4901 wff 
F : A -1-1-onto-> B
cfv 4902 class  ( F `  A )
wiso 4903 wff 
H  Isom  R ,  S  ( A ,  B )
df-fun 4904 |-  ( Fun  A  <->  ( Rel  A  /\  ( A  o.  `' A )  C_  _I  ) )
df-fn 4905 |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
df-f 4906 |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
df-f1 4907 |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
df-fo 4908 |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
df-f1o 4909 |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B
) )
df-fv 4910 |-  ( F `  A )  =  ( iota x A F x )
df-isom 4911 |-  ( H  Isom  R ,  S  ( A ,  B )  <->  ( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) ) ) )
crio 5467 class  (
iota_ x  e.  A  ph )
df-riota 5468 |-  ( iota_ x  e.  A  ph )  =  ( iota
x ( x  e.  A  /\  ph )
)
co 5512 class  ( A F B )
coprab 5513 class  { <. <. x ,  y
>. ,  z >.  | 
ph }
cmpt2 5514 class  ( x  e.  A , 
y  e.  B  |->  C )
df-ov 5515 |-  ( A F B )  =  ( F `  <. A ,  B >. )
df-oprab 5516 |- 
{ <. <. x ,  y
>. ,  z >.  | 
ph }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ph ) }
df-mpt2 5517 |-  ( x  e.  A ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  A  /\  y  e.  B )  /\  z  =  C ) }
cof 5710 class  oF R
cofr 5711 class  oR R
df-of 5712 |-  oF R  =  ( f  e.  _V ,  g  e.  _V  |->  ( x  e.  ( dom  f  i^i  dom  g
)  |->  ( ( f `
 x ) R ( g `  x
) ) ) )
df-ofr 5713 |-  oR R  =  { <. f ,  g
>.  |  A. x  e.  ( dom  f  i^i 
dom  g ) ( f `  x ) R ( g `  x ) }
c1st 5765 class  1st
c2nd 5766 class  2nd
df-1st 5767 |- 
1st  =  ( x  e.  _V  |->  U. dom  { x } )
df-2nd 5768 |- 
2nd  =  ( x  e.  _V  |->  U. ran  { x } )
ctpos 5859 class tpos  F
df-tpos 5860 |- tpos  F  =  ( F  o.  ( x  e.  ( `' dom  F  u.  { (/)
} )  |->  U. `' { x } ) )
wsmo 5900 wff 
Smo  A
df-smo 5901 |-  ( Smo  A  <->  ( A : dom  A --> On  /\  Ord  dom  A  /\  A. x  e.  dom  A A. y  e.  dom  A ( x  e.  y  -> 
( A `  x
)  e.  ( A `
 y ) ) ) )
crecs 5919 class recs ( F )
df-recs 5920 |- recs
( F )  = 
U. { f  |  E. x  e.  On  ( f  Fn  x  /\  A. y  e.  x  ( f `  y
)  =  ( F `
 ( f  |`  y ) ) ) }
crdg 5956 class  rec ( F ,  I
)
df-irdg 5957 |- 
rec ( F ,  I )  = recs (
( g  e.  _V  |->  ( I  u.  U_ x  e.  dom  g ( F `
 ( g `  x ) ) ) ) )
cfrec 5977 class frec ( F ,  I )
df-frec 5978 |- frec
( F ,  I
)  =  (recs ( ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) } ) )  |`  om )
c1o 5994 class  1o
c2o 5995 class  2o
c3o 5996 class  3o
c4o 5997 class  4o
coa 5998 class  +o
comu 5999 class  .o
coei 6000 class𝑜
df-1o 6001 |-  1o  =  suc  (/)
df-2o 6002 |-  2o  =  suc  1o
df-3o 6003 |-  3o  =  suc  2o
df-4o 6004 |-  4o  =  suc  3o
df-oadd 6005 |- 
+o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  suc  z ) ,  x ) `  y
) )
df-omul 6006 |- 
.o  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e. 
_V  |->  ( z  +o  x ) ) ,  (/) ) `  y ) )
df-oexpi 6007 |-𝑜  =  ( x  e.  On ,  y  e.  On  |->  ( rec ( ( z  e.  _V  |->  ( z  .o  x ) ) ,  1o ) `  y ) )
wer 6103 wff 
R  Er  A
cec 6104 class  [ A ] R
cqs 6105 class  ( A /. R )
df-er 6106 |-  ( R  Er  A  <->  ( Rel  R  /\  dom  R  =  A  /\  ( `' R  u.  ( R  o.  R )
)  C_  R )
)
df-ec 6108 |-  [ A ] R  =  ( R " { A } )
df-qs 6112 |-  ( A /. R )  =  { y  |  E. x  e.  A  y  =  [ x ] R }
cen 6219 class  ~~
cdom 6220 class  ~<_
cfn 6221 class  Fin
df-en 6222 |-  ~~  =  { <. x ,  y >.  |  E. f  f : x -1-1-onto-> y }
df-dom 6223 |-  ~<_  =  { <. x ,  y >.  |  E. f  f : x
-1-1-> y }
df-fin 6224 |- 
Fin  =  { x  |  E. y  e.  om  x  ~~  y }
ccrd 6359 class  card
df-card 6360 |- 
card  =  ( x  e.  _V  |->  |^| { y  e.  On  |  y  ~~  x } )
cnpi 6370 class  N.
cpli 6371 class  +N
cmi 6372 class  .N
clti 6373 class  <N
cplpq 6374 class  +pQ
cmpq 6375 class  .pQ
cltpq 6376 class  <pQ
ceq 6377 class  ~Q
cnq 6378 class  Q.
c1q 6379 class  1Q
cplq 6380 class  +Q
cmq 6381 class  .Q
crq 6382 class  *Q
cltq 6383 class  <Q
ceq0 6384 class ~Q0
cnq0 6385 class Q0
c0q0 6386 class 0Q0
cplq0 6387 class +Q0
cmq0 6388 class ·Q0
cnp 6389 class  P.
c1p 6390 class  1P
cpp 6391 class  +P.
cmp 6392 class  .P.
cltp 6393 class  <P
cer 6394 class  ~R
cnr 6395 class  R.
c0r 6396 class  0R
c1r 6397 class  1R
cm1r 6398 class  -1R
cplr 6399 class  +R
cmr 6400 class  .R
cltr 6401 class  <R
df-ni 6402 |-  N.  =  ( om  \  { (/) } )
df-pli 6403 |- 
+N  =  (  +o  |`  ( N.  X.  N. ) )
df-mi 6404 |-  .N  =  (  .o  |`  ( N.  X.  N. ) )
df-lti 6405 |- 
<N  =  (  _E  i^i  ( N.  X.  N. ) )
df-plpq 6442 |- 
+pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( ( 1st `  x )  .N  ( 2nd `  y
) )  +N  (
( 1st `  y
)  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-mpq 6443 |- 
.pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |->  <. ( ( 1st `  x )  .N  ( 1st `  y ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y ) )
>. )
df-ltpq 6444 |- 
<pQ  =  { <. x ,  y >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( ( 1st `  x )  .N  ( 2nd `  y ) ) 
<N  ( ( 1st `  y
)  .N  ( 2nd `  x ) ) ) }
df-enq 6445 |- 
~Q  =  { <. x ,  y >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .N  u
)  =  ( w  .N  v ) ) ) }
df-nqqs 6446 |- 
Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
df-plqqs 6447 |- 
+Q  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~Q  /\  y  =  [ <. u ,  f
>. ]  ~Q  )  /\  z  =  [ ( <. w ,  v >.  +pQ  <. u ,  f
>. ) ]  ~Q  )
) }
df-mqqs 6448 |- 
.Q  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~Q  /\  y  =  [ <. u ,  f
>. ]  ~Q  )  /\  z  =  [ ( <. w ,  v >.  .pQ  <. u ,  f
>. ) ]  ~Q  )
) }
df-1nqqs 6449 |-  1Q  =  [ <. 1o ,  1o >. ]  ~Q
df-rq 6450 |-  *Q  =  { <. x ,  y >.  |  ( x  e.  Q.  /\  y  e.  Q.  /\  (
x  .Q  y )  =  1Q ) }
df-ltnqqs 6451 |- 
<Q  =  { <. x ,  y >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. z E. w E. v E. u ( ( x  =  [ <. z ,  w >. ]  ~Q  /\  y  =  [ <. v ,  u >. ]  ~Q  )  /\  ( z  .N  u
)  <N  ( w  .N  v ) ) ) }
df-enq0 6522 |- ~Q0  =  { <. x ,  y
>.  |  ( (
x  e.  ( om 
X.  N. )  /\  y  e.  ( om  X.  N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  .o  u
)  =  ( w  .o  v ) ) ) }
df-nq0 6523 |- Q0  =  ( ( om  X.  N. ) /. ~Q0  )
df-0nq0 6524 |- 0Q0  =  [ <. (/) ,  1o >. ] ~Q0
df-plq0 6525 |- +Q0  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e. Q0  /\  y  e. Q0 )  /\  E. w E. v E. u E. f
( ( x  =  [ <. w ,  v
>. ] ~Q0  /\  y  =  [ <. u ,  f >. ] ~Q0  )  /\  z  =  [ <. ( ( w  .o  f )  +o  (
v  .o  u ) ) ,  ( v  .o  f ) >. ] ~Q0  ) ) }
df-mq0 6526 |- ·Q0  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e. Q0  /\  y  e. Q0 )  /\  E. w E. v E. u E. f
( ( x  =  [ <. w ,  v
>. ] ~Q0  /\  y  =  [ <. u ,  f >. ] ~Q0  )  /\  z  =  [ <. ( w  .o  u
) ,  ( v  .o  f ) >. ] ~Q0  ) ) }
df-inp 6564 |- 
P.  =  { <. l ,  u >.  |  ( ( ( l  C_  Q.  /\  u  C_  Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e. 
Q.  r  e.  u
) )  /\  (
( A. q  e. 
Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )  /\  A. q  e. 
Q.  -.  ( q  e.  l  /\  q  e.  u )  /\  A. q  e.  Q.  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) ) ) ) }
df-i1p 6565 |-  1P  =  <. { l  |  l  <Q  1Q } ,  { u  |  1Q  <Q  u } >.
df-iplp 6566 |- 
+P.  =  ( x  e.  P. ,  y  e.  P.  |->  <. { q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  +Q  s ) ) } ,  {
q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  (
r  e.  ( 2nd `  x )  /\  s  e.  ( 2nd `  y
)  /\  q  =  ( r  +Q  s
) ) } >. )
df-imp 6567 |- 
.P.  =  ( x  e.  P. ,  y  e.  P.  |->  <. { q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  ( r  e.  ( 1st `  x
)  /\  s  e.  ( 1st `  y )  /\  q  =  ( r  .Q  s ) ) } ,  {
q  e.  Q.  |  E. r  e.  Q.  E. s  e.  Q.  (
r  e.  ( 2nd `  x )  /\  s  e.  ( 2nd `  y
)  /\  q  =  ( r  .Q  s
) ) } >. )
df-iltp 6568 |- 
<P  =  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
df-enr 6811 |- 
~R  =  { <. x ,  y >.  |  ( ( x  e.  ( P.  X.  P. )  /\  y  e.  ( P.  X.  P. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  =  <. v ,  u >. )  /\  ( z  +P.  u
)  =  ( w  +P.  v ) ) ) }
df-nr 6812 |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
df-plr 6813 |- 
+R  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  R.  /\  y  e.  R. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~R  /\  y  =  [ <. u ,  f
>. ]  ~R  )  /\  z  =  [ <. (
w  +P.  u ) ,  ( v  +P.  f ) >. ]  ~R  ) ) }
df-mr 6814 |-  .R  =  { <. <. x ,  y >. ,  z
>.  |  ( (
x  e.  R.  /\  y  e.  R. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ]  ~R  /\  y  =  [ <. u ,  f
>. ]  ~R  )  /\  z  =  [ <. (
( w  .P.  u
)  +P.  ( v  .P.  f ) ) ,  ( ( w  .P.  f )  +P.  (
v  .P.  u )
) >. ]  ~R  )
) }
df-ltr 6815 |- 
<R  =  { <. x ,  y >.  |  ( ( x  e.  R.  /\  y  e.  R. )  /\  E. z E. w E. v E. u ( ( x  =  [ <. z ,  w >. ]  ~R  /\  y  =  [ <. v ,  u >. ]  ~R  )  /\  ( z  +P.  u
)  <P  ( w  +P.  v ) ) ) }
df-0r 6816 |-  0R  =  [ <. 1P ,  1P >. ]  ~R
df-1r 6817 |-  1R  =  [ <. ( 1P  +P.  1P ) ,  1P >. ]  ~R
df-m1r 6818 |- 
-1R  =  [ <. 1P ,  ( 1P  +P.  1P ) >. ]  ~R
cc 6887 class  CC
cr 6888 class  RR
cc0 6889 class  0
c1 6890 class  1
ci 6891 class  _i
caddc 6892 class  +
cltrr 6893 class  <RR
cmul 6894 class  x.
df-c 6895 |-  CC  =  ( R.  X.  R. )
df-0 6896 |-  0  =  <. 0R ,  0R >.
df-1 6897 |-  1  =  <. 1R ,  0R >.
df-i 6898 |-  _i  =  <. 0R ,  1R >.
df-r 6899 |-  RR  =  ( R.  X.  { 0R } )
df-add 6900 |-  +  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  CC  /\  y  e.  CC )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( w  +R  u ) ,  ( v  +R  f ) >. )
) }
df-mul 6901 |-  x.  =  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  CC  /\  y  e.  CC )  /\  E. w E. v E. u E. f
( ( x  = 
<. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  =  <. ( ( w  .R  u
)  +R  ( -1R 
.R  ( v  .R  f ) ) ) ,  ( ( v  .R  u )  +R  ( w  .R  f
) ) >. )
) }
df-lt 6902 |-  <RR  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  E. z E. w
( ( x  = 
<. z ,  0R >.  /\  y  =  <. w ,  0R >. )  /\  z  <R  w ) ) }
ax-cnex 6975 |-  CC  e.  _V
ax-resscn 6976 |-  RR  C_  CC
ax-1cn 6977 |-  1  e.  CC
ax-1re 6978 |-  1  e.  RR
ax-icn 6979 |-  _i  e.  CC
ax-addcl 6980 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  e.  CC )
ax-addrcl 6981 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  +  B )  e.  RR )
ax-mulcl 6982 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  e.  CC )
ax-mulrcl 6983 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  x.  B )  e.  RR )
ax-addcom 6984 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B )  =  ( B  +  A ) )
ax-mulcom 6985 |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B )  =  ( B  x.  A ) )
ax-addass 6986 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
ax-mulass 6987 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
ax-distr 6988 |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
ax-i2m1 6989 |-  ( ( _i  x.  _i )  +  1
)  =  0
ax-1rid 6991 |-  ( A  e.  RR  ->  ( A  x.  1 )  =  A )
ax-0id 6992 |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
ax-rnegex 6993 |-  ( A  e.  RR  ->  E. x  e.  RR  ( A  +  x
)  =  0 )
ax-precex 6994 |-  ( ( A  e.  RR  /\  0  <RR  A )  ->  E. x  e.  RR  ( 0  <RR  x  /\  ( A  x.  x )  =  1 ) )
ax-cnre 6995 |-  ( A  e.  CC  ->  E. x  e.  RR  E. y  e.  RR  A  =  ( x  +  ( _i  x.  y
) ) )
ax-pre-ltirr 6996 |-  ( A  e.  RR  ->  -.  A  <RR  A )
ax-pre-ltwlin 6997 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( A  <RR  C  \/  C  <RR  B ) ) )
ax-pre-lttrn 6998 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <RR  B  /\  B  <RR  C )  ->  A  <RR  C ) )
ax-pre-apti 6999 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  -.  ( A  <RR  B  \/  B  <RR  A ) )  ->  A  =  B )
ax-pre-ltadd 7000 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( A  <RR  B  ->  ( C  +  A )  <RR  ( C  +  B
) ) )
ax-pre-mulgt0 7001 |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  (
( 0  <RR  A  /\  0  <RR  B )  -> 
0  <RR  ( A  x.  B ) ) )
ax-pre-mulext 7002 |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  x.  C
)  <RR  ( B  x.  C )  ->  ( A  <RR  B  \/  B  <RR  A ) ) )
ax-arch 7003 |-  ( A  e.  RR  ->  E. n  e.  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  (
y  +  1 )  e.  x ) } A  <RR  n )
ax-caucvg 7004 |-  N  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }   &    |-  ( ph  ->  F : N --> RR )   &    |-  ( ph  ->  A. n  e.  N  A. k  e.  N  (
n  <RR  k  ->  (
( F `  n
)  <RR  ( ( F `
 k )  +  ( iota_ r  e.  RR  ( n  x.  r
)  =  1 ) )  /\  ( F `
 k )  <RR  ( ( F `  n
)  +  ( iota_ r  e.  RR  ( n  x.  r )  =  1 ) ) ) ) )   =>    |-  ( ph  ->  E. y  e.  RR  A. x  e.  RR  (
0  <RR  x  ->  E. j  e.  N  A. k  e.  N  ( j  <RR  k  ->  ( ( F `  k )  <RR  ( y  +  x
)  /\  y  <RR  ( ( F `  k
)  +  x ) ) ) ) )
cpnf 7057 class +oo
cmnf 7058 class -oo
cxr 7059 class  RR*
clt 7060 class  <
cle 7061 class  <_
df-pnf 7062 |- +oo  =  ~P U. CC
df-mnf 7063 |- -oo  =  ~P +oo
df-xr 7064 |-  RR*  =  ( RR  u.  { +oo , -oo }
)
df-ltxr 7065 |- 
<  =  ( { <. x ,  y >.  |  ( x  e.  RR  /\  y  e.  RR  /\  x  <RR  y ) }  u.  (
( ( RR  u.  { -oo } )  X. 
{ +oo } )  u.  ( { -oo }  X.  RR ) ) )
df-le 7066 |-  <_  =  ( ( RR*  X. 
RR* )  \  `'  <  )
cmin 7182 class  -
cneg 7183 class  -u A
df-sub 7184 |- 
-  =  ( x  e.  CC ,  y  e.  CC  |->  ( iota_ z  e.  CC  ( y  +  z )  =  x ) )
df-neg 7185 |-  -u A  =  (
0  -  A )
creap 7565 class #
df-reap 7566 |- #  =  { <. x ,  y
>.  |  ( (
x  e.  RR  /\  y  e.  RR )  /\  ( x  <  y  \/  y  <  x ) ) }
cap 7572 class #
df-ap 7573 |- #  =  { <. x ,  y
>.  |  E. r  e.  RR  E. s  e.  RR  E. t  e.  RR  E. u  e.  RR  ( ( x  =  ( r  +  ( _i  x.  s
) )  /\  y  =  ( t  +  ( _i  x.  u
) ) )  /\  ( r #  t  \/  s #  u
) ) }
cdiv 7651 class  /
df-div 7652 |- 
/  =  ( x  e.  CC ,  y  e.  ( CC  \  { 0 } ) 
|->  ( iota_ z  e.  CC  ( y  x.  z
)  =  x ) )
cn 7914 class  NN
df-inn 7915 |-  NN  =  |^| { x  |  ( 1  e.  x  /\  A. y  e.  x  ( y  +  1 )  e.  x ) }
c2 7964 class  2
c3 7965 class  3
c4 7966 class  4
c5 7967 class  5
c6 7968 class  6
c7 7969 class  7
c8 7970 class  8
c9 7971 class  9
c10 7972 class  10
df-2 7973 |-  2  =  ( 1  +  1 )
df-3 7974 |-  3  =  ( 2  +  1 )
df-4 7975 |-  4  =  ( 3  +  1 )
df-5 7976 |-  5  =  ( 4  +  1 )
df-6 7977 |-  6  =  ( 5  +  1 )
df-7 7978 |-  7  =  ( 6  +  1 )
df-8 7979 |-  8  =  ( 7  +  1 )
df-9 7980 |-  9  =  ( 8  +  1 )
df-10 7981 |-  10  =  ( 9  +  1 )
cn0 8181 class  NN0
df-n0 8182 |-  NN0  =  ( NN  u.  { 0 } )
cz 8245 class  ZZ
df-z 8246 |-  ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
cdc 8368 class ; A B
df-dec 8369 |- ; A B  =  ( ( 10  x.  A )  +  B )
cuz 8473 class  ZZ>=
df-uz 8474 |-  ZZ>=  =  ( j  e.  ZZ  |->  { k  e.  ZZ  |  j  <_ 
k } )
cq 8554 class  QQ
df-q 8555 |-  QQ  =  (  /  " ( ZZ  X.  NN ) )
crp 8583 class  RR+
df-rp 8584 |-  RR+  =  { x  e.  RR  |  0  < 
x }
cxne 8686 class  -e A
cxad 8687 class  +e
cxmu 8688 class  xe
df-xneg 8689 |-  -e A  =  if ( A  = +oo , -oo ,  if ( A  = -oo , +oo ,  -u A
) )
df-xadd 8690 |-  +e  =  ( x  e.  RR* ,  y  e.  RR*  |->  if ( x  = +oo ,  if ( y  = -oo ,  0 , +oo ) ,  if (
x  = -oo ,  if ( y  = +oo ,  0 , -oo ) ,  if (
y  = +oo , +oo ,  if ( y  = -oo , -oo ,  ( x  +  y ) ) ) ) ) )
df-xmul 8691 |-  xe  =  ( x  e.  RR* ,  y  e.  RR*  |->  if ( ( x  =  0  \/  y  =  0 ) ,  0 ,  if ( ( ( ( 0  <  y  /\  x  = +oo )  \/  ( y  <  0  /\  x  = -oo ) )  \/  ( ( 0  < 
x  /\  y  = +oo )  \/  (
x  <  0  /\  y  = -oo )
) ) , +oo ,  if ( ( ( ( 0  <  y  /\  x  = -oo )  \/  ( y  <  0  /\  x  = +oo ) )  \/  ( ( 0  < 
x  /\  y  = -oo )  \/  (
x  <  0  /\  y  = +oo )
) ) , -oo ,  ( x  x.  y ) ) ) ) )
cioo 8757 class  (,)
cioc 8758 class  (,]
cico 8759 class  [,)
cicc 8760 class  [,]
df-ioo 8761 |- 
(,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  < 
y ) } )
df-ioc 8762 |- 
(,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <  z  /\  z  <_ 
y ) } )
df-ico 8763 |- 
[,)  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  < 
y ) } )
df-icc 8764 |- 
[,]  =  ( x  e.  RR* ,  y  e. 
RR*  |->  { z  e. 
RR*  |  ( x  <_  z  /\  z  <_ 
y ) } )
cfz 8874 class  ...
df-fz 8875 |-  ...  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  { k  e.  ZZ  |  ( m  <_  k  /\  k  <_  n ) } )
cfzo 8999 class ..^
df-fzo 9000 |- ..^ 
=  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  -  1
) ) )
cfl 9112 class  |_
cceil 9113 class
df-fl 9114 |-  |_  =  ( x  e.  RR  |->  ( iota_ y  e.  ZZ  ( y  <_  x  /\  x  <  (
y  +  1 ) ) ) )
df-ceil 9115 |- =  ( x  e.  RR  |->  -u ( |_ `  -u x ) )
cmo 9164 class  mod
df-mod 9165 |- 
mod  =  ( x  e.  RR ,  y  e.  RR+  |->  ( x  -  ( y  x.  ( |_ `  (
x  /  y ) ) ) ) )
cseq 9211 class  seq M (  .+  ,  F ,  S )
df-iseq 9212 |- 
seq M (  .+  ,  F ,  S )  =  ran frec ( (
x  e.  ( ZZ>= `  M ) ,  y  e.  S  |->  <. (
x  +  1 ) ,  ( y  .+  ( F `  ( x  +  1 ) ) ) >. ) ,  <. M ,  ( F `  M ) >. )
cexp 9254 class  ^
df-iexp 9255 |- 
^  =  ( x  e.  CC ,  y  e.  ZZ  |->  if ( y  =  0 ,  1 ,  if ( 0  <  y ,  (  seq 1 (  x.  ,  ( NN 
X.  { x }
) ,  CC ) `
 y ) ,  ( 1  /  (  seq 1 (  x.  , 
( NN  X.  {
x } ) ,  CC ) `  -u y
) ) ) ) )
cshi 9415 class  shift
df-shft 9416 |- 
shift  =  ( f  e.  _V ,  x  e.  CC  |->  { <. y ,  z >.  |  ( y  e.  CC  /\  ( y  -  x
) f z ) } )
ccj 9439 class  *
cre 9440 class  Re
cim 9441 class  Im
df-cj 9442 |-  *  =  ( x  e.  CC  |->  ( iota_ y  e.  CC  ( ( x  +  y )  e.  RR  /\  ( _i  x.  ( x  -  y ) )  e.  RR ) ) )
df-re 9443 |-  Re  =  ( x  e.  CC  |->  ( ( x  +  ( * `  x ) )  / 
2 ) )
df-im 9444 |-  Im  =  ( x  e.  CC  |->  ( Re `  ( x  /  _i ) ) )
csqrt 9594 class  sqr
cabs 9595 class  abs
df-rsqrt 9596 |- 
sqr  =  ( x  e.  RR  |->  ( iota_ y  e.  RR  ( ( y ^ 2 )  =  x  /\  0  <_  y ) ) )
df-abs 9597 |- 
abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
cli 9799 class  ~~>
df-clim 9800 |-  ~~>  =  { <. f ,  y
>.  |  ( y  e.  CC  /\  A. x  e.  RR+  E. j  e.  ZZ  A. k  e.  ( ZZ>= `  j )
( ( f `  k )  e.  CC  /\  ( abs `  (
( f `  k
)  -  y ) )  <  x ) ) }
csu 9872 class  sum_ k  e.  A  B
df-sum 9873 |- 
sum_ k  e.  A  B  =  ( iota x ( E. m  e.  ZZ  ( A  C_  ( ZZ>= `  m )  /\  seq m (  +  ,  ( n  e.  ZZ  |->  if ( n  e.  A ,  [_ n  /  k ]_ B ,  0 ) ) ,  CC )  ~~>  x )  \/  E. m  e.  NN  E. f ( f : ( 1 ... m ) -1-1-onto-> A  /\  x  =  (  seq 1 (  +  , 
( n  e.  NN  |->  [_ ( f `  n
)  /  k ]_ B ) ,  CC ) `  m )
) ) )
The list of syntax, axioms (ax-) and definitions (df-) for the starts here
wbd 9932 wff BOUNDED  ph
ax-bd0 9933 |-  ( ph  <->  ps )   =>    |-  (BOUNDED  ph  -> BOUNDED  ps )
ax-bdim 9934 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  ->  ps )
ax-bdan 9935 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  /\  ps )
ax-bdor 9936 |- BOUNDED  ph   &    |- BOUNDED  ps   =>    |- BOUNDED  ( ph  \/  ps )
ax-bdn 9937 |- BOUNDED  ph   =>    |- BOUNDED  -.  ph
ax-bdal 9938 |- BOUNDED  ph   =>    |- BOUNDED  A. x  e.  y 
ph
ax-bdex 9939 |- BOUNDED  ph   =>    |- BOUNDED  E. x  e.  y 
ph
ax-bdeq 9940 |- BOUNDED  x  =  y
ax-bdel 9941 |- BOUNDED  x  e.  y
ax-bdsb 9942 |- BOUNDED  ph   =>    |- BOUNDED  [ y  /  x ] ph
wbdc 9960 wff BOUNDED  A
df-bdc 9961 |-  (BOUNDED  A 
<-> 
A. xBOUNDED  x  e.  A )
ax-bdsep 10004 |- BOUNDED  ph   =>    |-  A. a E. b A. x
( x  e.  b  <-> 
( x  e.  a  /\  ph ) )
ax-bj-d0cl 10044 |- BOUNDED  ph   =>    |- DECID  ph
wind 10050 wff Ind  A
df-bj-ind 10051 |-  (Ind  A  <->  ( (/)  e.  A  /\  A. x  e.  A  suc  x  e.  A ) )
ax-infvn 10066 |- 
E. x (Ind  x  /\  A. y (Ind  y  ->  x  C_  y
) )
ax-bdsetind 10093 |- BOUNDED  ph   =>    |-  ( A. a ( A. y  e.  a  [ y  /  a ] ph  ->  ph )  ->  A. a ph )
ax-inf2 10101 |- 
E. a A. x
( x  e.  a  <-> 
( x  =  (/)  \/ 
E. y  e.  a  x  =  suc  y
) )
ax-strcoll 10107 |- 
A. a ( A. x  e.  a  E. y ph  ->  E. b A. y ( y  e.  b  <->  E. x  e.  a 
ph ) )
ax-sscoll 10112 |- 
A. a A. b E. c A. z ( A. x  e.  a  E. y  e.  b 
ph  ->  E. d  e.  c 
A. y ( y  e.  d  <->  E. x  e.  a  ph ) )
ax-ddkcomp 10114 |-  ( ( ( A 
C_  RR  /\  A  =/=  (/) )  /\  E. x  e.  RR  A. y  e.  A  y  <  x  /\  A. x  e.  RR  A. y  e.  RR  (
x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )  ->  E. x  e.  RR  ( A. y  e.  A  y  <_  x  /\  (
( B  e.  R  /\  A. y  e.  A  y  <_  B )  ->  x  <_  B ) ) )
walsi 10115 wff  A.! x ( ph  ->  ps )
walsc 10116 wff  A.! x  e.  A ph
df-alsi 10117 |-  ( A.! x (
ph  ->  ps )  <->  ( A. x ( ph  ->  ps )  /\  E. x ph ) )
df-alsc 10118 |-  ( A.! x  e.  A ph  <->  ( A. x  e.  A  ph  /\  E. x  x  e.  A
) )
  Copyright terms: Public domain W3C validator