Theorem 0r 5202

Description: The constant 0_R is a signed real.

Assertion

Ref	Expression
0r	⊢ 0R ∈ R

Proof of Theorem 0r

Step	Hyp	Ref	Expression
1		1pr 5130	. . . 4 ⊢ 1P ∈ P
2		opelxpi 3231	. . . 4 ⊢ ((1P ∈ P ⋀ 1P ∈ P) → ⟨1P, 1P⟩ ∈ (P × P))
3	1, 1, 2	mp2an 701	. . 3 ⊢ ⟨1P, 1P⟩ ∈ (P × P)
4		enrex 5191	. . . 4 ⊢ ~R ∈ V
5	4	ecelqsi 4306	. . 3 ⊢ (⟨1P, 1P⟩ ∈ (P × P) → [⟨1P, 1P⟩] ~R ∈ ((P × P) / ~R ))
6	3, 5	ax-mp 7	. 2 ⊢ [⟨1P, 1P⟩] ~R ∈ ((P × P) / ~R )
7		df-0r 5184	. . 3 ⊢ 0R = [⟨1P, 1P⟩] ~R
8		df-nr 5180	. . 3 ⊢ R = ((P × P) / ~R )
9	7, 8	eleq12i 1546	. 2 ⊢ (0R ∈ R ↔ [⟨1P, 1P⟩] ~R ∈ ((P × P) / ~R ))
10	6, 9	mpbir 190	1 ⊢ 0R ∈ R

Syntax hints:   ∈ wcel 962  ⟨cop 2421   × cxp 3182  [cec 4273   / cqs 4274  Pcnp 4998  1_Pc1p 4999   ~_R cer 5005  Rcnr 5006  0_Rc0r 5007

This theorem is referenced by:  addgt0sr 5226  sqgt0sr 5228  ssgt0sr 5230  suppsr2 5236  suppsr3 5237  supsrlem2 5239  supsr 5244  opelreal 5262  elreal 5263  eqresr 5268  addresr 5269  mulresr 5270  axresscn 5281  axicn 5283  ax0id 5294  ax1id 5295  axi2m1 5298  axcnre 5299  pre-axmulgt0 5303

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-rep 2706  ax-sep 2716  ax-nul 2723  ax-pow 2756  ax-pr 2793  ax-un 2880  ax-inf2 4637

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2010  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-pss 2064  df-nul 2290  df-if 2372  df-pw 2412  df-sn 2422  df-pr 2423  df-tp 2425  df-op 2426  df-uni 2516  df-int 2546  df-iun 2580  df-br 2633  df-opab 2680  df-tr 2694  df-eprel 2846  df-id 2849  df-po 2854  df-so 2864  df-fr 2931  df-we 2948  df-ord 2965  df-on 2966  df-lim 2967  df-suc 2968  df-om 3146  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-fv 3212  df-rdg 3946  df-opr 3979  df-oprab 3980  df-1st 4093  df-2nd 4094  df-1o 4147  df-oadd 4149  df-omul 4150  df-er 4275  df-ec 4277  df-qs 4280  df-ni 5013  df-pli 5014  df-mi 5015  df-lti 5016  df-plpq 5048  df-mpq 5049  df-enq 5050  df-nq 5051  df-plq 5052  df-mq 5053  df-rq 5054  df-ltq 5055  df-1q 5056  df-np 5099  df-1p 5100  df-enr 5179  df-nr 5180  df-0r 5184

Copyright terms: Public domain