Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addclprlem1 Structured version   Unicode version

 Description: Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
Assertion
Ref Expression

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elprnq 8870 . . 3
2 ltrnq 8858 . . . . 5
3 ltmnq 8851 . . . . . 6
4 ovex 6108 . . . . . . 7
5 ovex 6108 . . . . . . 7
6 ltmnq 8851 . . . . . . 7
7 vex 2961 . . . . . . 7
8 mulcomnq 8832 . . . . . . 7
94, 5, 6, 7, 8caovord2 6261 . . . . . 6
103, 9sylan9bbr 683 . . . . 5
112, 10syl5bb 250 . . . 4
12 recidnq 8844 . . . . . . 7
1312oveq1d 6098 . . . . . 6
14 mulcomnq 8832 . . . . . . 7
15 mulidnq 8842 . . . . . . 7
1614, 15syl5eq 2482 . . . . . 6
1713, 16sylan9eqr 2492 . . . . 5
1817breq2d 4226 . . . 4
1911, 18bitrd 246 . . 3
201, 19sylan 459 . 2
21 prcdnq 8872 . . 3