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 syl5bb 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