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

Theorem ltm1sr 7597
 Description: Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.)
Assertion
Ref Expression
ltm1sr (𝐴R → (𝐴 +R -1R) <R 𝐴)

Proof of Theorem ltm1sr
StepHypRef Expression
1 m1r 7572 . . . . . 6 -1RR
2 addclsr 7573 . . . . . 6 ((𝐴R ∧ -1RR) → (𝐴 +R -1R) ∈ R)
31, 2mpan2 421 . . . . 5 (𝐴R → (𝐴 +R -1R) ∈ R)
4 ltadd1sr 7596 . . . . 5 ((𝐴 +R -1R) ∈ R → (𝐴 +R -1R) <R ((𝐴 +R -1R) +R 1R))
53, 4syl 14 . . . 4 (𝐴R → (𝐴 +R -1R) <R ((𝐴 +R -1R) +R 1R))
6 1sr 7571 . . . . 5 1RR
7 addasssrg 7576 . . . . 5 ((𝐴R ∧ -1RR ∧ 1RR) → ((𝐴 +R -1R) +R 1R) = (𝐴 +R (-1R +R 1R)))
81, 6, 7mp3an23 1307 . . . 4 (𝐴R → ((𝐴 +R -1R) +R 1R) = (𝐴 +R (-1R +R 1R)))
95, 8breqtrd 3954 . . 3 (𝐴R → (𝐴 +R -1R) <R (𝐴 +R (-1R +R 1R)))
10 m1p1sr 7580 . . . 4 (-1R +R 1R) = 0R
1110oveq2i 5785 . . 3 (𝐴 +R (-1R +R 1R)) = (𝐴 +R 0R)
129, 11breqtrdi 3969 . 2 (𝐴R → (𝐴 +R -1R) <R (𝐴 +R 0R))
13 0idsr 7587 . 2 (𝐴R → (𝐴 +R 0R) = 𝐴)
1412, 13breqtrd 3954 1 (𝐴R → (𝐴 +R -1R) <R 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480   class class class wbr 3929  (class class class)co 5774  Rcnr 7117  0Rc0r 7118  1Rc1r 7119  -1Rcm1r 7120   +R cplr 7121
 Copyright terms: Public domain W3C validator