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

Theorem mappsrpr 10522
 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 10476 . . . 4 -1R = [⟨1P, (1P +P 1P)⟩] ~R
21breq1i 5038 . . 3 (-1R <R [⟨𝐴, 1P⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝐴, 1P⟩] ~R )
3 ltsrpr 10491 . . 3 ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
42, 3bitri 278 . 2 (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
5 mappsrpr.2 . . 3 𝐶R
6 ltasr 10514 . . 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 10412 . . . . 5 <P ⊆ (P × P)
98brel 5582 . . . 4 ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) → ((1P +P 1P) ∈ P ∧ ((1P +P 1P) +P 𝐴) ∈ P))
10 dmplp 10426 . . . . . 6 dom +P = (P × P)
11 0npr 10406 . . . . . 6 ¬ ∅ ∈ P
1210, 11ndmovrcl 7316 . . . . 5 (((1P +P 1P) +P 𝐴) ∈ P → ((1P +P 1P) ∈ P𝐴P))
1312simprd 499 . . . 4 (((1P +P 1P) +P 𝐴) ∈ P𝐴P)
149, 13simpl2im 507 . . 3 ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) → 𝐴P)
15 1pr 10429 . . . . 5 1PP
16 addclpr 10432 . . . . 5 ((1PP ∧ 1PP) → (1P +P 1P) ∈ P)
1715, 15, 16mp2an 691 . . . 4 (1P +P 1P) ∈ P
18 ltaddpr 10448 . . . 4 (((1P +P 1P) ∈ P𝐴P) → (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
1917, 18mpan 689 . . 3 (𝐴P → (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
2014, 19impbii 212 . 2 ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) ↔ 𝐴P)
214, 7, 203bitr3i 304 1 ((𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ) ↔ 𝐴P)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∈ wcel 2111  ⟨cop 4531   class class class wbr 5031  (class class class)co 7136  [cec 8273  Pcnp 10273  1Pc1p 10274   +P cpp 10275
 Copyright terms: Public domain W3C validator