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

Theorem ennnfonelemhom 11767
Description: Lemma for ennnfone 11777. The sequences in  H increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
ennnfonelemh.f  |-  ( ph  ->  F : om -onto-> A
)
ennnfonelemh.ne  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
ennnfonelemh.g  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
ennnfonelemh.n  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
ennnfonelemh.j  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
ennnfonelemh.h  |-  H  =  seq 0 ( G ,  J )
ennnfonelemhom.m  |-  ( ph  ->  M  e.  om )
Assertion
Ref Expression
ennnfonelemhom  |-  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `
 i ) )
Distinct variable groups:    i, H, k, j, x, y    i, M    ph, i, k, x, y, j    ph, n    x, N, y, j, k   
n, N    j, G    k, F, x, y, j   
n, F, j    x, A, y, j    j, J   
x, i, y, j   
i, n, H, k
Allowed substitution hints:    A( i, k, n)    F( i)    G( x, y, i, k, n)    J( x, y, i, k, n)    M( x, y, j, k, n)    N( i)

Proof of Theorem ennnfonelemhom
Dummy variables  q  w  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ennnfonelemhom.m . 2  |-  ( ph  ->  M  e.  om )
2 eleq1 2175 . . . . 5  |-  ( w  =  (/)  ->  ( w  e.  dom  ( H `
 i )  <->  (/)  e.  dom  ( H `  i ) ) )
32rexbidv 2410 . . . 4  |-  ( w  =  (/)  ->  ( E. i  e.  NN0  w  e.  dom  ( H `  i )  <->  E. i  e.  NN0  (/)  e.  dom  ( H `  i )
) )
43imbi2d 229 . . 3  |-  ( w  =  (/)  ->  ( (
ph  ->  E. i  e.  NN0  w  e.  dom  ( H `
 i ) )  <-> 
( ph  ->  E. i  e.  NN0  (/)  e.  dom  ( H `  i )
) ) )
5 eleq1 2175 . . . . 5  |-  ( w  =  k  ->  (
w  e.  dom  ( H `  i )  <->  k  e.  dom  ( H `
 i ) ) )
65rexbidv 2410 . . . 4  |-  ( w  =  k  ->  ( E. i  e.  NN0  w  e.  dom  ( H `
 i )  <->  E. i  e.  NN0  k  e.  dom  ( H `  i ) ) )
76imbi2d 229 . . 3  |-  ( w  =  k  ->  (
( ph  ->  E. i  e.  NN0  w  e.  dom  ( H `  i ) )  <->  ( ph  ->  E. i  e.  NN0  k  e.  dom  ( H `  i ) ) ) )
8 eleq1 2175 . . . . 5  |-  ( w  =  suc  k  -> 
( w  e.  dom  ( H `  i )  <->  suc  k  e.  dom  ( H `  i ) ) )
98rexbidv 2410 . . . 4  |-  ( w  =  suc  k  -> 
( E. i  e. 
NN0  w  e.  dom  ( H `  i )  <->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) )
109imbi2d 229 . . 3  |-  ( w  =  suc  k  -> 
( ( ph  ->  E. i  e.  NN0  w  e.  dom  ( H `  i ) )  <->  ( ph  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) ) )
11 eleq1 2175 . . . . 5  |-  ( w  =  M  ->  (
w  e.  dom  ( H `  i )  <->  M  e.  dom  ( H `
 i ) ) )
1211rexbidv 2410 . . . 4  |-  ( w  =  M  ->  ( E. i  e.  NN0  w  e.  dom  ( H `
 i )  <->  E. i  e.  NN0  M  e.  dom  ( H `  i ) ) )
1312imbi2d 229 . . 3  |-  ( w  =  M  ->  (
( ph  ->  E. i  e.  NN0  w  e.  dom  ( H `  i ) )  <->  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `  i ) ) ) )
14 1nn0 8891 . . . 4  |-  1  e.  NN0
15 0ex 4013 . . . . . 6  |-  (/)  e.  _V
1615snid 3520 . . . . 5  |-  (/)  e.  { (/)
}
17 ennnfonelemh.dceq . . . . . . . 8  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
18 ennnfonelemh.f . . . . . . . 8  |-  ( ph  ->  F : om -onto-> A
)
19 ennnfonelemh.ne . . . . . . . 8  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
20 ennnfonelemh.g . . . . . . . 8  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
21 ennnfonelemh.n . . . . . . . 8  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
22 ennnfonelemh.j . . . . . . . 8  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
23 ennnfonelemh.h . . . . . . . 8  |-  H  =  seq 0 ( G ,  J )
2417, 18, 19, 20, 21, 22, 23ennnfonelem1 11759 . . . . . . 7  |-  ( ph  ->  ( H `  1
)  =  { <. (/)
,  ( F `  (/) ) >. } )
2524dmeqd 4699 . . . . . 6  |-  ( ph  ->  dom  ( H ` 
1 )  =  dom  {
<. (/) ,  ( F `
 (/) ) >. } )
26 peano1 4466 . . . . . . . 8  |-  (/)  e.  om
27 fof 5301 . . . . . . . . . 10  |-  ( F : om -onto-> A  ->  F : om --> A )
2818, 27syl 14 . . . . . . . . 9  |-  ( ph  ->  F : om --> A )
2926a1i 9 . . . . . . . . 9  |-  ( ph  -> 
(/)  e.  om )
3028, 29ffvelrnd 5508 . . . . . . . 8  |-  ( ph  ->  ( F `  (/) )  e.  A )
31 fnsng 5126 . . . . . . . 8  |-  ( (
(/)  e.  om  /\  ( F `  (/) )  e.  A )  ->  { <. (/)
,  ( F `  (/) ) >. }  Fn  { (/)
} )
3226, 30, 31sylancr 408 . . . . . . 7  |-  ( ph  ->  { <. (/) ,  ( F `
 (/) ) >. }  Fn  {
(/) } )
33 fndm 5178 . . . . . . 7  |-  ( {
<. (/) ,  ( F `
 (/) ) >. }  Fn  {
(/) }  ->  dom  { <.
(/) ,  ( F `  (/) ) >. }  =  { (/) } )
3432, 33syl 14 . . . . . 6  |-  ( ph  ->  dom  { <. (/) ,  ( F `  (/) ) >. }  =  { (/) } )
3525, 34eqtrd 2145 . . . . 5  |-  ( ph  ->  dom  ( H ` 
1 )  =  { (/)
} )
3616, 35syl5eleqr 2202 . . . 4  |-  ( ph  -> 
(/)  e.  dom  ( H `
 1 ) )
37 fveq2 5373 . . . . . . 7  |-  ( i  =  1  ->  ( H `  i )  =  ( H ` 
1 ) )
3837dmeqd 4699 . . . . . 6  |-  ( i  =  1  ->  dom  ( H `  i )  =  dom  ( H `
 1 ) )
3938eleq2d 2182 . . . . 5  |-  ( i  =  1  ->  ( (/) 
e.  dom  ( H `  i )  <->  (/)  e.  dom  ( H `  1 ) ) )
4039rspcev 2758 . . . 4  |-  ( ( 1  e.  NN0  /\  (/) 
e.  dom  ( H `  1 ) )  ->  E. i  e.  NN0  (/) 
e.  dom  ( H `  i ) )
4114, 36, 40sylancr 408 . . 3  |-  ( ph  ->  E. i  e.  NN0  (/) 
e.  dom  ( H `  i ) )
4217ad3antrrr 481 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
4318ad3antrrr 481 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  F : om -onto-> A )
4419ad3antrrr 481 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  A. n  e.  om  E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )
)
45 fveq2 5373 . . . . . . . . . . . . . 14  |-  ( k  =  a  ->  ( F `  k )  =  ( F `  a ) )
4645neeq1d 2298 . . . . . . . . . . . . 13  |-  ( k  =  a  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  a )  =/=  ( F `  j )
) )
4746ralbidv 2409 . . . . . . . . . . . 12  |-  ( k  =  a  ->  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. j  e.  suc  n
( F `  a
)  =/=  ( F `
 j ) ) )
4847cbvrexv 2627 . . . . . . . . . . 11  |-  ( E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  E. a  e.  om  A. j  e. 
suc  n ( F `
 a )  =/=  ( F `  j
) )
4948ralbii 2413 . . . . . . . . . 10  |-  ( A. n  e.  om  E. k  e.  om  A. j  e. 
suc  n ( F `
 k )  =/=  ( F `  j
)  <->  A. n  e.  om  E. a  e.  om  A. j  e.  suc  n ( F `  a )  =/=  ( F `  j ) )
5044, 49sylib 121 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  A. n  e.  om  E. a  e. 
om  A. j  e.  suc  n ( F `  a )  =/=  ( F `  j )
)
51 simplr 502 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  i  e.  NN0 )
5242, 43, 50, 20, 21, 22, 23, 51ennnfonelemex 11766 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  E. q  e.  NN0  dom  ( H `  i )  e.  dom  ( H `  q ) )
5342ad2antrr 477 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
5443ad2antrr 477 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  F : om -onto-> A )
5544ad2antrr 477 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  A. n  e.  om  E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )
)
56 simplr 502 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  q  e.  NN0 )
5753, 54, 55, 20, 21, 22, 23, 56ennnfonelemom 11760 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  dom  ( H `
 q )  e. 
om )
58 nnord 4483 . . . . . . . . . . . . 13  |-  ( dom  ( H `  q
)  e.  om  ->  Ord 
dom  ( H `  q ) )
5957, 58syl 14 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  Ord  dom  ( H `  q )
)
60 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  dom  ( H `
 i )  e. 
dom  ( H `  q ) )
61 ordsucss 4378 . . . . . . . . . . . 12  |-  ( Ord 
dom  ( H `  q )  ->  ( dom  ( H `  i
)  e.  dom  ( H `  q )  ->  suc  dom  ( H `  i )  C_  dom  ( H `  q ) ) )
6259, 60, 61sylc 62 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  suc  dom  ( H `  i )  C_ 
dom  ( H `  q ) )
63 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  k  e.  dom  ( H `  i
) )
6442, 43, 44, 20, 21, 22, 23, 51ennnfonelemom 11760 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  dom  ( H `
 i )  e. 
om )
65 nnsucelsuc 6339 . . . . . . . . . . . . . 14  |-  ( dom  ( H `  i
)  e.  om  ->  ( k  e.  dom  ( H `  i )  <->  suc  k  e.  suc  dom  ( H `  i ) ) )
6664, 65syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  ( k  e.  dom  ( H `  i )  <->  suc  k  e. 
suc  dom  ( H `  i ) ) )
6763, 66mpbid 146 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  suc  k  e. 
suc  dom  ( H `  i ) )
6867ad2antrr 477 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  suc  k  e. 
suc  dom  ( H `  i ) )
6962, 68sseldd 3062 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  suc  k  e. 
dom  ( H `  q ) )
7069ex 114 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e. 
NN0 )  ->  ( dom  ( H `  i
)  e.  dom  ( H `  q )  ->  suc  k  e.  dom  ( H `  q ) ) )
7170reximdva 2506 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  ( E. q  e.  NN0  dom  ( H `  i )  e.  dom  ( H `  q )  ->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) ) )
7252, 71mpd 13 . . . . . . 7  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) )
7372rexlimdva2 2524 . . . . . 6  |-  ( (
ph  /\  k  e.  om )  ->  ( E. i  e.  NN0  k  e. 
dom  ( H `  i )  ->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) ) )
74 fveq2 5373 . . . . . . . . 9  |-  ( i  =  q  ->  ( H `  i )  =  ( H `  q ) )
7574dmeqd 4699 . . . . . . . 8  |-  ( i  =  q  ->  dom  ( H `  i )  =  dom  ( H `
 q ) )
7675eleq2d 2182 . . . . . . 7  |-  ( i  =  q  ->  ( suc  k  e.  dom  ( H `  i )  <->  suc  k  e.  dom  ( H `  q ) ) )
7776cbvrexv 2627 . . . . . 6  |-  ( E. i  e.  NN0  suc  k  e.  dom  ( H `
 i )  <->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) )
7873, 77syl6ibr 161 . . . . 5  |-  ( (
ph  /\  k  e.  om )  ->  ( E. i  e.  NN0  k  e. 
dom  ( H `  i )  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i
) ) )
7978expcom 115 . . . 4  |-  ( k  e.  om  ->  ( ph  ->  ( E. i  e.  NN0  k  e.  dom  ( H `  i )  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) ) )
8079a2d 26 . . 3  |-  ( k  e.  om  ->  (
( ph  ->  E. i  e.  NN0  k  e.  dom  ( H `  i ) )  ->  ( ph  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) ) )
814, 7, 10, 13, 41, 80finds 4472 . 2  |-  ( M  e.  om  ->  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `
 i ) ) )
821, 81mpcom 36 1  |-  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `
 i ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104  DECID wdc 802    = wceq 1312    e. wcel 1461    =/= wne 2280   A.wral 2388   E.wrex 2389    u. cun 3033    C_ wss 3035   (/)c0 3327   ifcif 3438   {csn 3491   <.cop 3494    |-> cmpt 3947   Ord word 4242   suc csuc 4245   omcom 4462   `'ccnv 4496   dom cdm 4497   "cima 4500    Fn wfn 5074   -->wf 5075   -onto->wfo 5077   ` cfv 5079  (class class class)co 5726    e. cmpo 5728  freccfrec 6239    ^pm cpm 6495   0cc0 7541   1c1 7542    + caddc 7544    - cmin 7850   NN0cn0 8875   ZZcz 8952    seqcseq 10105
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-13 1472  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-coll 4001  ax-sep 4004  ax-nul 4012  ax-pow 4056  ax-pr 4089  ax-un 4313  ax-setind 4410  ax-iinf 4460  ax-cnex 7630  ax-resscn 7631  ax-1cn 7632  ax-1re 7633  ax-icn 7634  ax-addcl 7635  ax-addrcl 7636  ax-mulcl 7637  ax-addcom 7639  ax-addass 7641  ax-distr 7643  ax-i2m1 7644  ax-0lt1 7645  ax-0id 7647  ax-rnegex 7648  ax-cnre 7650  ax-pre-ltirr 7651  ax-pre-ltwlin 7652  ax-pre-lttrn 7653  ax-pre-ltadd 7655
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 944  df-3an 945  df-tru 1315  df-fal 1318  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ne 2281  df-nel 2376  df-ral 2393  df-rex 2394  df-reu 2395  df-rab 2397  df-v 2657  df-sbc 2877  df-csb 2970  df-dif 3037  df-un 3039  df-in 3041  df-ss 3048  df-nul 3328  df-if 3439  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-int 3736  df-iun 3779  df-br 3894  df-opab 3948  df-mpt 3949  df-tr 3985  df-id 4173  df-iord 4246  df-on 4248  df-ilim 4249  df-suc 4251  df-iom 4463  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-res 4509  df-ima 4510  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-f1 5084  df-fo 5085  df-f1o 5086  df-fv 5087  df-riota 5682  df-ov 5729  df-oprab 5730  df-mpo 5731  df-1st 5990  df-2nd 5991  df-recs 6154  df-frec 6240  df-pm 6497  df-pnf 7720  df-mnf 7721  df-xr 7722  df-ltxr 7723  df-le 7724  df-sub 7852  df-neg 7853  df-inn 8625  df-n0 8876  df-z 8953  df-uz 9223  df-seqfrec 10106
This theorem is referenced by:  ennnfonelemdm  11772
  Copyright terms: Public domain W3C validator