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

Theorem mulclprlem 9429
 Description: Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 14-Mar-1996.) (New usage is discouraged.)
Assertion
Ref Expression
mulclprlem
Distinct variable groups:   ,,   ,   ,
Allowed substitution hints:   (,)   (,)

Proof of Theorem mulclprlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elprnq 9401 . . . . . 6
2 elprnq 9401 . . . . . 6
3 recclnq 9376 . . . . . . . . 9
43adantl 466 . . . . . . . 8
5 vex 3064 . . . . . . . . 9
6 ovex 6308 . . . . . . . . 9
7 ltmnq 9382 . . . . . . . . 9
8 fvex 5861 . . . . . . . . 9
9 mulcomnq 9363 . . . . . . . . 9
105, 6, 7, 8, 9caovord2 6470 . . . . . . . 8
114, 10syl 17 . . . . . . 7
12 mulassnq 9369 . . . . . . . . . 10
13 recidnq 9375 . . . . . . . . . . 11
1413oveq2d 6296 . . . . . . . . . 10
1512, 14syl5eq 2457 . . . . . . . . 9
16 mulidnq 9373 . . . . . . . . 9
1715, 16sylan9eqr 2467 . . . . . . . 8
1817breq2d 4409 . . . . . . 7
1911, 18bitrd 255 . . . . . 6
201, 2, 19syl2an 477 . . . . 5
21 prcdnq 9403 . . . . . 6
2221adantr 465 . . . . 5
2320, 22sylbid 217 . . . 4
24 df-mp 9394 . . . . . . . . 9
25 mulclnq 9357 . . . . . . . . 9
2624, 25genpprecl 9411 . . . . . . . 8
2726exp4b 607 . . . . . . 7
2827com34 85 . . . . . 6
2928imp32 433 . . . . 5
3029adantlr 715 . . . 4
3123, 30syld 44 . . 3