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

Theorem mulclprlem 8523
 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
StepHypRef Expression
1 elprnq 8495 . . . . . 6
2 elprnq 8495 . . . . . 6
3 recclnq 8470 . . . . . . . . 9
43adantl 454 . . . . . . . 8
5 vex 2730 . . . . . . . . 9
6 ovex 5735 . . . . . . . . 9
7 ltmnq 8476 . . . . . . . . 9
8 fvex 5391 . . . . . . . . 9
9 mulcomnq 8457 . . . . . . . . 9
105, 6, 7, 8, 9caovord2 5884 . . . . . . . 8
114, 10syl 17 . . . . . . 7
12 mulassnq 8463 . . . . . . . . . 10
13 recidnq 8469 . . . . . . . . . . 11
1413oveq2d 5726 . . . . . . . . . 10
1512, 14syl5eq 2297 . . . . . . . . 9
16 mulidnq 8467 . . . . . . . . 9
1715, 16sylan9eqr 2307 . . . . . . . 8
1817breq2d 3932 . . . . . . 7
1911, 18bitrd 246 . . . . . 6
201, 2, 19syl2an 465 . . . . 5
21 prcdnq 8497 . . . . . 6
2221adantr 453 . . . . 5
2320, 22sylbid 208 . . . 4
24 df-mp 8488 . . . . . . . . 9
25 mulclnq 8451 . . . . . . . . 9
2624, 25genpprecl 8505 . . . . . . . 8
2726exp4b 593 . . . . . . 7
2827com34 79 . . . . . 6
2928imp32 424 . . . . 5
3029adantlr 698 . . . 4
3123, 30syld 42 . . 3