Metamath Proof Explorer

Theorem addclprlem1

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.)

Ref Expression
Assertion addclprlem1 ⊢A∈𝑷∧g∈A∧x∈𝑸→x<𝑸g+𝑸h→x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g∈A

Proof

Step Hyp Ref Expression
1 elprnq ⊢A∈𝑷∧g∈A→g∈𝑸
2 ltrnq ⊢x<𝑸g+𝑸h↔*𝑸⁡g+𝑸h<𝑸*𝑸⁡x
3 ltmnq ⊢x∈𝑸→*𝑸⁡g+𝑸h<𝑸*𝑸⁡x↔x⋅𝑸*𝑸⁡g+𝑸h<𝑸x⋅𝑸*𝑸⁡x
4 ovex ⊢x⋅𝑸*𝑸⁡g+𝑸h∈V
5 ovex ⊢x⋅𝑸*𝑸⁡x∈V
6 ltmnq ⊢w∈𝑸→y<𝑸z↔w⋅𝑸y<𝑸w⋅𝑸z
7 vex ⊢g∈V
8 mulcomnq ⊢y⋅𝑸z=z⋅𝑸y
9 4 5 6 7 8 caovord2 ⊢g∈𝑸→x⋅𝑸*𝑸⁡g+𝑸h<𝑸x⋅𝑸*𝑸⁡x↔x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸x⋅𝑸*𝑸⁡x⋅𝑸g
10 3 9 sylan9bbr ⊢g∈𝑸∧x∈𝑸→*𝑸⁡g+𝑸h<𝑸*𝑸⁡x↔x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸x⋅𝑸*𝑸⁡x⋅𝑸g
11 2 10 bitrid ⊢g∈𝑸∧x∈𝑸→x<𝑸g+𝑸h↔x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸x⋅𝑸*𝑸⁡x⋅𝑸g
12 recidnq ⊢x∈𝑸→x⋅𝑸*𝑸⁡x=1𝑸
13 12 oveq1d ⊢x∈𝑸→x⋅𝑸*𝑸⁡x⋅𝑸g=1𝑸⋅𝑸g
14 mulcomnq ⊢1𝑸⋅𝑸g=g⋅𝑸1𝑸
15 mulidnq ⊢g∈𝑸→g⋅𝑸1𝑸=g
16 14 15 eqtrid ⊢g∈𝑸→1𝑸⋅𝑸g=g
17 13 16 sylan9eqr ⊢g∈𝑸∧x∈𝑸→x⋅𝑸*𝑸⁡x⋅𝑸g=g
18 17 breq2d ⊢g∈𝑸∧x∈𝑸→x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸x⋅𝑸*𝑸⁡x⋅𝑸g↔x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸g
19 11 18 bitrd ⊢g∈𝑸∧x∈𝑸→x<𝑸g+𝑸h↔x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸g
20 1 19 sylan ⊢A∈𝑷∧g∈A∧x∈𝑸→x<𝑸g+𝑸h↔x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸g
21 prcdnq ⊢A∈𝑷∧g∈A→x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸g→x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g∈A
22 21 adantr ⊢A∈𝑷∧g∈A∧x∈𝑸→x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g<𝑸g→x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g∈A
23 20 22 sylbid ⊢A∈𝑷∧g∈A∧x∈𝑸→x<𝑸g+𝑸h→x⋅𝑸*𝑸⁡g+𝑸h⋅𝑸g∈A