Theorem 1sr 7717

Description: The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.)

Assertion

Ref	Expression
1sr	|- 1R e. R.

Proof of Theorem 1sr

Step	Hyp	Ref	Expression
1		1pr 7520	. . . . 5 |- 1P e. P.
2		addclpr 7503	. . . . 5 |- ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
3	1, 1, 2	mp2an 424	. . . 4 |- ( 1P +P. 1P ) e. P.
4		opelxpi 4644	. . . 4 |- ( ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) -> <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. ) )
5	3, 1, 4	mp2an 424	. . 3 |- <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. )
6		enrex 7703	. . . 4 |- ~R e. _V
7	6	ecelqsi 6571	. . 3 |- ( <. ( 1P +P. 1P ) , 1P >. e. ( P. X. P. ) -> [ <. ( 1P +P. 1P ) , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
8	5, 7	ax-mp 5	. 2 |- [ <. ( 1P +P. 1P ) , 1P >. ] ~R e. ( ( P. X. P. ) /. ~R )
9		df-1r 7698	. 2 |- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
10		df-nr 7693	. 2 |- R. = ( ( P. X. P. ) /. ~R )
11	8, 9, 10	3eltr4i 2253	1 |- 1R e. R.

Syntax hints:   e. wcel 2142   <.cop 3587   X. cxp 4610  (class class class)co 5857   [cec 6515   /.cqs 6516   P.cnp 7257   1Pc1p 7258   +P. cpp 7259   ~R cer 7262   R.cnr 7263   1Rc1r 7265

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 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-13 2144  ax-14 2145  ax-ext 2153  ax-coll 4105  ax-sep 4108  ax-nul 4116  ax-pow 4161  ax-pr 4195  ax-un 4419  ax-setind 4522  ax-iinf 4573

This theorem depends on definitions:  df-bi 116  df-dc 831  df-3or 975  df-3an 976  df-tru 1352  df-fal 1355  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-ral 2454  df-rex 2455  df-reu 2456  df-rab 2458  df-v 2733  df-sbc 2957  df-csb 3051  df-dif 3124  df-un 3126  df-in 3128  df-ss 3135  df-nul 3416  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-int 3833  df-iun 3876  df-br 3991  df-opab 4052  df-mpt 4053  df-tr 4089  df-eprel 4275  df-id 4279  df-po 4282  df-iso 4283  df-iord 4352  df-on 4354  df-suc 4357  df-iom 4576  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-res 4624  df-ima 4625  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-f1 5205  df-fo 5206  df-f1o 5207  df-fv 5208  df-ov 5860  df-oprab 5861  df-mpo 5862  df-1st 6123  df-2nd 6124  df-recs 6288  df-irdg 6353  df-1o 6399  df-2o 6400  df-oadd 6403  df-omul 6404  df-er 6517  df-ec 6519  df-qs 6523  df-ni 7270  df-pli 7271  df-mi 7272  df-lti 7273  df-plpq 7310  df-mpq 7311  df-enq 7313  df-nqqs 7314  df-plqqs 7315  df-mqqs 7316  df-1nqqs 7317  df-rq 7318  df-ltnqqs 7319  df-enq0 7390  df-nq0 7391  df-0nq0 7392  df-plq0 7393  df-mq0 7394  df-inp 7432  df-i1p 7433  df-iplp 7434  df-enr 7692  df-nr 7693  df-1r 7698

This theorem is referenced by:  1ne0sr  7732  pn0sr  7737  ltadd1sr  7742  ltm1sr  7743  caucvgsrlemoffval  7762  caucvgsrlemofff  7763  caucvgsrlemoffcau  7764  caucvgsrlemoffgt1  7765  caucvgsrlemoffres  7766  caucvgsr  7768  suplocsrlempr  7773  pitonnlem2  7813  peano1nnnn  7818  peano2nnnn  7819  ax1cn  7827  ax1re  7828  axicn  7829  axi2m1  7841  ax1rid  7843  axprecex  7846  axcnre  7847