Theorem m1r 6709

Description: The constant -1R is a signed real.

Assertion

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

Proof of Theorem m1r

Step	Hyp	Ref	Expression
1		1pr 6635	. . . 4 |- 1P e. P.
2		addclpr 6638	. . . . 5 |- ((1P e. P. /\ 1P e. P.) -> (1P +P. 1P) e. P.)
3	1, 1, 2	mp2an 681	. . . 4 |- (1P +P. 1P) e. P.
4		opelxpi 4173	. . . 4 |- ((1P e. P. /\ (1P +P. 1P) e. P.) -> <.1P, (1P +P. 1P)>. e. (P. X. P.))
5	1, 3, 4	mp2an 681	. . 3 |- <.1P, (1P +P. 1P)>. e. (P. X. P.)
6		enrex 6696	. . . 4 |- ~R e. _V
7	6	ecelqsi 5511	. . 3 |- (<.1P, (1P +P. 1P)>. e. (P. X. P.) -> [<.1P, (1P +P. 1P)>.] ~R e. ((P. X. P.)/. ~R ))
8	5, 7	ax-mp 7	. 2 |- [<.1P, (1P +P. 1P)>.] ~R e. ((P. X. P.)/. ~R )
9		df-m1r 6691	. . 3 |- -1R = [<.1P, (1P +P. 1P)>.] ~R
10		df-nr 6685	. . 3 |- R. = ((P. X. P.)/. ~R )
11	9, 10	eleq12i 2209	. 2 |- (-1R e. R. <-> [<.1P, (1P +P. 1P)>.] ~R e. ((P. X. P.)/. ~R ))
12	8, 11	mpbir 273	1 |- -1R e. R.

Syntax hints:   e. wcel 1588  <.cop 3240   X. cxp 4117  (class class class)co 4981  [cec 5477  /.cqs 5478  P.cnp 6503  1Pc1p 6504   +P. cpp 6505   ~R cer 6510  R.cnr 6511  -1Rcm1r 6514

This theorem is referenced by:  pn0sr 6728  negexsr 6729  sqgt0sr 6733  supsrlem1 6743  supsrlem2 6744  supsrlem3 6745  supsrlem5 6747  mulresr 6775  axmulopr 6784  axmulass 6795  axdistr 6796  axi2m1 6801  axcnre 6802

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-enr 6684  df-nr 6685  df-m1r 6691

Copyright terms: Public domain