Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  0idsr GIF version

Theorem 0idsr 7666
 Description: The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.)
Assertion
Ref Expression
0idsr (𝐴R → (𝐴 +R 0R) = 𝐴)

Proof of Theorem 0idsr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nr 7626 . 2 R = ((P × P) / ~R )
2 oveq1 5821 . . 3 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → ([⟨𝑥, 𝑦⟩] ~R +R 0R) = (𝐴 +R 0R))
3 id 19 . . 3 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → [⟨𝑥, 𝑦⟩] ~R = 𝐴)
42, 3eqeq12d 2169 . 2 ([⟨𝑥, 𝑦⟩] ~R = 𝐴 → (([⟨𝑥, 𝑦⟩] ~R +R 0R) = [⟨𝑥, 𝑦⟩] ~R ↔ (𝐴 +R 0R) = 𝐴))
5 df-0r 7630 . . . 4 0R = [⟨1P, 1P⟩] ~R
65oveq2i 5825 . . 3 ([⟨𝑥, 𝑦⟩] ~R +R 0R) = ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R )
7 1pr 7453 . . . . 5 1PP
8 addsrpr 7644 . . . . 5 (((𝑥P𝑦P) ∧ (1PP ∧ 1PP)) → ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R ) = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R )
97, 7, 8mpanr12 436 . . . 4 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R ) = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R )
10 simpl 108 . . . . . 6 ((𝑥P𝑦P) → 𝑥P)
11 simpr 109 . . . . . 6 ((𝑥P𝑦P) → 𝑦P)
127a1i 9 . . . . . 6 ((𝑥P𝑦P) → 1PP)
13 addcomprg 7477 . . . . . . 7 ((𝑧P𝑤P) → (𝑧 +P 𝑤) = (𝑤 +P 𝑧))
1413adantl 275 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P)) → (𝑧 +P 𝑤) = (𝑤 +P 𝑧))
15 addassprg 7478 . . . . . . 7 ((𝑧P𝑤P𝑣P) → ((𝑧 +P 𝑤) +P 𝑣) = (𝑧 +P (𝑤 +P 𝑣)))
1615adantl 275 . . . . . 6 (((𝑥P𝑦P) ∧ (𝑧P𝑤P𝑣P)) → ((𝑧 +P 𝑤) +P 𝑣) = (𝑧 +P (𝑤 +P 𝑣)))
1710, 11, 12, 14, 16caov12d 5992 . . . . 5 ((𝑥P𝑦P) → (𝑥 +P (𝑦 +P 1P)) = (𝑦 +P (𝑥 +P 1P)))
18 addclpr 7436 . . . . . . . 8 ((𝑥P ∧ 1PP) → (𝑥 +P 1P) ∈ P)
197, 18mpan2 422 . . . . . . 7 (𝑥P → (𝑥 +P 1P) ∈ P)
20 addclpr 7436 . . . . . . . 8 ((𝑦P ∧ 1PP) → (𝑦 +P 1P) ∈ P)
217, 20mpan2 422 . . . . . . 7 (𝑦P → (𝑦 +P 1P) ∈ P)
2219, 21anim12i 336 . . . . . 6 ((𝑥P𝑦P) → ((𝑥 +P 1P) ∈ P ∧ (𝑦 +P 1P) ∈ P))
23 enreceq 7635 . . . . . 6 (((𝑥P𝑦P) ∧ ((𝑥 +P 1P) ∈ P ∧ (𝑦 +P 1P) ∈ P)) → ([⟨𝑥, 𝑦⟩] ~R = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R ↔ (𝑥 +P (𝑦 +P 1P)) = (𝑦 +P (𝑥 +P 1P))))
2422, 23mpdan 418 . . . . 5 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R ↔ (𝑥 +P (𝑦 +P 1P)) = (𝑦 +P (𝑥 +P 1P))))
2517, 24mpbird 166 . . . 4 ((𝑥P𝑦P) → [⟨𝑥, 𝑦⟩] ~R = [⟨(𝑥 +P 1P), (𝑦 +P 1P)⟩] ~R )
269, 25eqtr4d 2190 . . 3 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R +R [⟨1P, 1P⟩] ~R ) = [⟨𝑥, 𝑦⟩] ~R )
276, 26syl5eq 2199 . 2 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R +R 0R) = [⟨𝑥, 𝑦⟩] ~R )
281, 4, 27ecoptocl 6556 1 (𝐴R → (𝐴 +R 0R) = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1332   ∈ wcel 2125  ⟨cop 3559  (class class class)co 5814  [cec 6467  Pcnp 7190  1Pc1p 7191   +P cpp 7192   ~R cer 7195  Rcnr 7196  0Rc0r 7197   +R cplr 7200 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 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-iinf 4541 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 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-ral 2437  df-rex 2438  df-reu 2439  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-eprel 4244  df-id 4248  df-po 4251  df-iso 4252  df-iord 4321  df-on 4323  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-ov 5817  df-oprab 5818  df-mpo 5819  df-1st 6078  df-2nd 6079  df-recs 6242  df-irdg 6307  df-1o 6353  df-2o 6354  df-oadd 6357  df-omul 6358  df-er 6469  df-ec 6471  df-qs 6475  df-ni 7203  df-pli 7204  df-mi 7205  df-lti 7206  df-plpq 7243  df-mpq 7244  df-enq 7246  df-nqqs 7247  df-plqqs 7248  df-mqqs 7249  df-1nqqs 7250  df-rq 7251  df-ltnqqs 7252  df-enq0 7323  df-nq0 7324  df-0nq0 7325  df-plq0 7326  df-mq0 7327  df-inp 7365  df-i1p 7366  df-iplp 7367  df-enr 7625  df-nr 7626  df-plr 7627  df-0r 7630 This theorem is referenced by:  addgt0sr  7674  ltadd1sr  7675  ltm1sr  7676  caucvgsrlemoffval  7695  caucvgsrlemoffres  7699  caucvgsr  7701  map2psrprg  7704  suplocsrlempr  7706  addresr  7736  mulresr  7737  axi2m1  7774  ax0id  7777  axcnre  7780
 Copyright terms: Public domain W3C validator