Metamath Proof Explorer

Theorem gt0srpr

Description: Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996) (New usage is discouraged.)

Ref Expression
Assertion gt0srpr ⊢ 0 𝑹 < 𝑹 A B ~ 𝑹 ↔ B < 𝑷 A

Proof

Step Hyp Ref Expression
1 ltsrpr ⊢ 1 𝑷 1 𝑷 ~ 𝑹 < 𝑹 A B ~ 𝑹 ↔ 1 𝑷 + 𝑷 B < 𝑷 1 𝑷 + 𝑷 A
2 df-0r ⊢ 0 𝑹 = 1 𝑷 1 𝑷 ~ 𝑹
3 2 breq1i ⊢ 0 𝑹 < 𝑹 A B ~ 𝑹 ↔ 1 𝑷 1 𝑷 ~ 𝑹 < 𝑹 A B ~ 𝑹
4 1pr ⊢ 1 𝑷 ∈ 𝑷
5 ltapr ⊢ 1 𝑷 ∈ 𝑷 → B < 𝑷 A ↔ 1 𝑷 + 𝑷 B < 𝑷 1 𝑷 + 𝑷 A
6 4 5 ax-mp ⊢ B < 𝑷 A ↔ 1 𝑷 + 𝑷 B < 𝑷 1 𝑷 + 𝑷 A
7 1 3 6 3bitr4i ⊢ 0 𝑹 < 𝑹 A B ~ 𝑹 ↔ B < 𝑷 A