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

Theorem mappsrprg 7619
 Description: Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
Assertion
Ref Expression
mappsrprg ((𝐴P𝐶R) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ))

Proof of Theorem mappsrprg
StepHypRef Expression
1 1pr 7369 . . . . 5 1PP
2 addclpr 7352 . . . . 5 ((1PP ∧ 1PP) → (1P +P 1P) ∈ P)
31, 1, 2mp2an 422 . . . 4 (1P +P 1P) ∈ P
4 ltaddpr 7412 . . . 4 (((1P +P 1P) ∈ P𝐴P) → (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
53, 4mpan 420 . . 3 (𝐴P → (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
65adantr 274 . 2 ((𝐴P𝐶R) → (1P +P 1P)<P ((1P +P 1P) +P 𝐴))
7 df-m1r 7548 . . . . . 6 -1R = [⟨1P, (1P +P 1P)⟩] ~R
87breq1i 3936 . . . . 5 (-1R <R [⟨𝐴, 1P⟩] ~R ↔ [⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝐴, 1P⟩] ~R )
91a1i 9 . . . . . 6 (𝐴P → 1PP)
103a1i 9 . . . . . 6 (𝐴P → (1P +P 1P) ∈ P)
11 id 19 . . . . . 6 (𝐴P𝐴P)
12 ltsrprg 7562 . . . . . 6 (((1PP ∧ (1P +P 1P) ∈ P) ∧ (𝐴P ∧ 1PP)) → ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴)))
139, 10, 11, 9, 12syl22anc 1217 . . . . 5 (𝐴P → ([⟨1P, (1P +P 1P)⟩] ~R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴)))
148, 13syl5bb 191 . . . 4 (𝐴P → (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴)))
1514adantr 274 . . 3 ((𝐴P𝐶R) → (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (1P +P 1P)<P ((1P +P 1P) +P 𝐴)))
16 m1r 7567 . . . 4 -1RR
17 opelxpi 4571 . . . . . . 7 ((𝐴P ∧ 1PP) → ⟨𝐴, 1P⟩ ∈ (P × P))
18 enrex 7552 . . . . . . . 8 ~R ∈ V
1918ecelqsi 6483 . . . . . . 7 (⟨𝐴, 1P⟩ ∈ (P × P) → [⟨𝐴, 1P⟩] ~R ∈ ((P × P) / ~R ))
2017, 19syl 14 . . . . . 6 ((𝐴P ∧ 1PP) → [⟨𝐴, 1P⟩] ~R ∈ ((P × P) / ~R ))
211, 20mpan2 421 . . . . 5 (𝐴P → [⟨𝐴, 1P⟩] ~R ∈ ((P × P) / ~R ))
22 df-nr 7542 . . . . 5 R = ((P × P) / ~R )
2321, 22eleqtrrdi 2233 . . . 4 (𝐴P → [⟨𝐴, 1P⟩] ~RR)
24 simpr 109 . . . 4 ((𝐴P𝐶R) → 𝐶R)
25 ltasrg 7585 . . . 4 ((-1RR ∧ [⟨𝐴, 1P⟩] ~RR𝐶R) → (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R )))
2616, 23, 24, 25mp3an2ani 1322 . . 3 ((𝐴P𝐶R) → (-1R <R [⟨𝐴, 1P⟩] ~R ↔ (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R )))
2715, 26bitr3d 189 . 2 ((𝐴P𝐶R) → ((1P +P 1P)<P ((1P +P 1P) +P 𝐴) ↔ (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R )))
286, 27mpbid 146 1 ((𝐴P𝐶R) → (𝐶 +R -1R) <R (𝐶 +R [⟨𝐴, 1P⟩] ~R ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∈ wcel 1480  ⟨cop 3530   class class class wbr 3929   × cxp 4537  (class class class)co 5774  [cec 6427   / cqs 6428  Pcnp 7106  1Pc1p 7107   +P cpp 7108
 Copyright terms: Public domain W3C validator