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

Theorem addclnq 7203
Description: Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
Assertion
Ref Expression
addclnq  |-  ( ( A  e.  Q.  /\  B  e.  Q. )  ->  ( A  +Q  B
)  e.  Q. )

Proof of Theorem addclnq
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nqqs 7176 . . 3  |-  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
2 oveq1 5785 . . . 4  |-  ( [
<. x ,  y >. ]  ~Q  =  A  -> 
( [ <. x ,  y >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  =  ( A  +Q  [ <. z ,  w >. ]  ~Q  ) )
32eleq1d 2209 . . 3  |-  ( [
<. x ,  y >. ]  ~Q  =  A  -> 
( ( [ <. x ,  y >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  e.  ( ( N.  X.  N. ) /.  ~Q  )  <->  ( A  +Q  [ <. z ,  w >. ]  ~Q  )  e.  ( ( N.  X.  N. ) /.  ~Q  ) ) )
4 oveq2 5786 . . . 4  |-  ( [
<. z ,  w >. ]  ~Q  =  B  -> 
( A  +Q  [ <. z ,  w >. ]  ~Q  )  =  ( A  +Q  B ) )
54eleq1d 2209 . . 3  |-  ( [
<. z ,  w >. ]  ~Q  =  B  -> 
( ( A  +Q  [
<. z ,  w >. ]  ~Q  )  e.  ( ( N.  X.  N. ) /.  ~Q  )  <->  ( A  +Q  B )  e.  ( ( N.  X.  N. ) /.  ~Q  ) ) )
6 addpipqqs 7198 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( [ <. x ,  y >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  =  [ <. (
( x  .N  w
)  +N  ( y  .N  z ) ) ,  ( y  .N  w ) >. ]  ~Q  )
7 mulclpi 7156 . . . . . . . 8  |-  ( ( x  e.  N.  /\  w  e.  N. )  ->  ( x  .N  w
)  e.  N. )
8 mulclpi 7156 . . . . . . . 8  |-  ( ( y  e.  N.  /\  z  e.  N. )  ->  ( y  .N  z
)  e.  N. )
9 addclpi 7155 . . . . . . . 8  |-  ( ( ( x  .N  w
)  e.  N.  /\  ( y  .N  z
)  e.  N. )  ->  ( ( x  .N  w )  +N  (
y  .N  z ) )  e.  N. )
107, 8, 9syl2an 287 . . . . . . 7  |-  ( ( ( x  e.  N.  /\  w  e.  N. )  /\  ( y  e.  N.  /\  z  e.  N. )
)  ->  ( (
x  .N  w )  +N  ( y  .N  z ) )  e. 
N. )
1110an42s 579 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( (
x  .N  w )  +N  ( y  .N  z ) )  e. 
N. )
12 mulclpi 7156 . . . . . . 7  |-  ( ( y  e.  N.  /\  w  e.  N. )  ->  ( y  .N  w
)  e.  N. )
1312ad2ant2l 500 . . . . . 6  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( y  .N  w )  e.  N. )
1411, 13jca 304 . . . . 5  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( (
( x  .N  w
)  +N  ( y  .N  z ) )  e.  N.  /\  (
y  .N  w )  e.  N. ) )
15 opelxpi 4575 . . . . 5  |-  ( ( ( ( x  .N  w )  +N  (
y  .N  z ) )  e.  N.  /\  ( y  .N  w
)  e.  N. )  -> 
<. ( ( x  .N  w )  +N  (
y  .N  z ) ) ,  ( y  .N  w ) >.  e.  ( N.  X.  N. ) )
16 enqex 7188 . . . . . 6  |-  ~Q  e.  _V
1716ecelqsi 6487 . . . . 5  |-  ( <.
( ( x  .N  w )  +N  (
y  .N  z ) ) ,  ( y  .N  w ) >.  e.  ( N.  X.  N. )  ->  [ <. (
( x  .N  w
)  +N  ( y  .N  z ) ) ,  ( y  .N  w ) >. ]  ~Q  e.  ( ( N.  X.  N. ) /.  ~Q  )
)
1814, 15, 173syl 17 . . . 4  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  [ <. (
( x  .N  w
)  +N  ( y  .N  z ) ) ,  ( y  .N  w ) >. ]  ~Q  e.  ( ( N.  X.  N. ) /.  ~Q  )
)
196, 18eqeltrd 2217 . . 3  |-  ( ( ( x  e.  N.  /\  y  e.  N. )  /\  ( z  e.  N.  /\  w  e.  N. )
)  ->  ( [ <. x ,  y >. ]  ~Q  +Q  [ <. z ,  w >. ]  ~Q  )  e.  ( ( N.  X.  N. ) /.  ~Q  ) )
201, 3, 5, 192ecoptocl 6521 . 2  |-  ( ( A  e.  Q.  /\  B  e.  Q. )  ->  ( A  +Q  B
)  e.  ( ( N.  X.  N. ) /.  ~Q  ) )
2120, 1eleqtrrdi 2234 1  |-  ( ( A  e.  Q.  /\  B  e.  Q. )  ->  ( A  +Q  B
)  e.  Q. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1332    e. wcel 1481   <.cop 3531    X. cxp 4541  (class class class)co 5778   [cec 6431   /.cqs 6432   N.cnpi 7100    +N cpli 7101    .N cmi 7102    ~Q ceq 7107   Q.cnq 7108    +Q cplq 7110
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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4047  ax-sep 4050  ax-nul 4058  ax-pow 4102  ax-pr 4135  ax-un 4359  ax-setind 4456  ax-iinf 4506
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2689  df-sbc 2911  df-csb 3005  df-dif 3074  df-un 3076  df-in 3078  df-ss 3085  df-nul 3365  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-iun 3819  df-br 3934  df-opab 3994  df-mpt 3995  df-tr 4031  df-id 4219  df-iord 4292  df-on 4294  df-suc 4297  df-iom 4509  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-rn 4554  df-res 4555  df-ima 4556  df-iota 5092  df-fun 5129  df-fn 5130  df-f 5131  df-f1 5132  df-fo 5133  df-f1o 5134  df-fv 5135  df-ov 5781  df-oprab 5782  df-mpo 5783  df-1st 6042  df-2nd 6043  df-recs 6206  df-irdg 6271  df-oadd 6321  df-omul 6322  df-er 6433  df-ec 6435  df-qs 6439  df-ni 7132  df-pli 7133  df-mi 7134  df-plpq 7172  df-enq 7175  df-nqqs 7176  df-plqqs 7177
This theorem is referenced by:  ltaddnq  7235  halfnqq  7238  ltbtwnnqq  7243  prarloclemcalc  7330  addnqprl  7357  addnqpru  7358  addlocprlemeqgt  7360  addlocprlemgt  7362  addlocprlem  7363  addclpr  7365  plpvlu  7366  dmplp  7368  addnqprlemrl  7385  addnqprlemru  7386  addnqprlemfl  7387  addnqprlemfu  7388  addnqpr  7389  addassprg  7407  distrlem1prl  7410  distrlem1pru  7411  distrlem4prl  7412  distrlem4pru  7413  distrlem5prl  7414  distrlem5pru  7415  ltaddpr  7425  ltexprlemloc  7435  ltexprlemfl  7437  ltexprlemrl  7438  ltexprlemfu  7439  ltexprlemru  7440  addcanprleml  7442  addcanprlemu  7443  recexprlemm  7452  aptiprleml  7467  aptiprlemu  7468  caucvgprlemcanl  7472  cauappcvgprlemm  7473  cauappcvgprlemdisj  7479  cauappcvgprlemloc  7480  cauappcvgprlemladdfu  7482  cauappcvgprlemladdfl  7483  cauappcvgprlemladdru  7484  cauappcvgprlemladdrl  7485  cauappcvgprlem1  7487  cauappcvgprlem2  7488  caucvgprlemnkj  7494  caucvgprlemnbj  7495  caucvgprlemm  7496  caucvgprlemloc  7503  caucvgprlemladdfu  7505  caucvgprlemladdrl  7506  caucvgprlem2  7508  caucvgprprlemloccalc  7512  caucvgprprlemml  7522  caucvgprprlemmu  7523  caucvgprprlemopl  7525  caucvgprprlemloc  7531  suplocexprlemmu  7546
  Copyright terms: Public domain W3C validator