Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mappsrpr Structured version   Visualization version   GIF version

Theorem mappsrpr 9967
 Description: Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
Hypothesis
Ref Expression
mappsrpr.2 𝐶R
Assertion
Ref Expression
mappsrpr ((𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ) ↔ 𝐴P)

Proof of Theorem mappsrpr
StepHypRef Expression
1 df-m1r 9922 . . . 4 -1R = [⟨1P, (1P +P 1P)⟩] ~R
21breq1i 4692 . . 3 (-1R <R [⟨𝐴, 1P⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝐴, 1P⟩] ~R )
3 ltsrpr 9936 . . 3 ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
42, 3bitri 264 . 2 (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
5 mappsrpr.2 . . 3 𝐶R
6 ltasr 9959 . . 3 (𝐶R → (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R )))
75, 6ax-mp 5 . 2 (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ))
8 ltrelpr 9858 . . . . . 6 <P ⊆ (P × P)
98brel 5202 . . . . 5 ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) → ((1P +P 1P) ∈ P ∧ ((1P +P 1P) +P 𝐴) ∈ P))
109simprd 478 . . . 4 ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) → ((1P +P 1P) +P 𝐴) ∈ P)
11 dmplp 9872 . . . . . 6 dom +P = (P × P)
12 0npr 9852 . . . . . 6 ¬ ∅ ∈ P
1311, 12ndmovrcl 6862 . . . . 5 (((1P +P 1P) +P 𝐴) ∈ P → ((1P +P 1P) ∈ P𝐴P))
1413simprd 478 . . . 4 (((1P +P 1P) +P 𝐴) ∈ P𝐴P)
1510, 14syl 17 . . 3 ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) → 𝐴P)
16 1pr 9875 . . . . 5 1PP
17 addclpr 9878 . . . . 5 ((1PP ∧ 1PP) → (1P +P 1P) ∈ P)
1816, 16, 17mp2an 708 . . . 4 (1P +P 1P) ∈ P
19 ltaddpr 9894 . . . 4 (((1P +P 1P) ∈ P𝐴P) → (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
2018, 19mpan 706 . . 3 (𝐴P → (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
2115, 20impbii 199 . 2 ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) ↔ 𝐴P)
224, 7, 213bitr3i 290 1 ((𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ) ↔ 𝐴P)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∈ wcel 2030  ⟨cop 4216   class class class wbr 4685  (class class class)co 6690  [cec 7785  Pcnp 9719  1Pc1p 9720   +P cpp 9721
 Copyright terms: Public domain W3C validator