Metamath Proof Explorer


Theorem addclprlem2

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 addclprlem2 A 𝑷 g A B 𝑷 h B x 𝑸 x < 𝑸 g + 𝑸 h x A + 𝑷 B

Proof

Step Hyp Ref Expression
1 addclprlem1 A 𝑷 g A x 𝑸 x < 𝑸 g + 𝑸 h x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g A
2 1 adantlr A 𝑷 g A B 𝑷 h B x 𝑸 x < 𝑸 g + 𝑸 h x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g A
3 addclprlem1 B 𝑷 h B x 𝑸 x < 𝑸 h + 𝑸 g x 𝑸 * 𝑸 h + 𝑸 g 𝑸 h B
4 addcomnq g + 𝑸 h = h + 𝑸 g
5 4 breq2i x < 𝑸 g + 𝑸 h x < 𝑸 h + 𝑸 g
6 4 fveq2i * 𝑸 g + 𝑸 h = * 𝑸 h + 𝑸 g
7 6 oveq2i x 𝑸 * 𝑸 g + 𝑸 h = x 𝑸 * 𝑸 h + 𝑸 g
8 7 oveq1i x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h = x 𝑸 * 𝑸 h + 𝑸 g 𝑸 h
9 8 eleq1i x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h B x 𝑸 * 𝑸 h + 𝑸 g 𝑸 h B
10 3 5 9 3imtr4g B 𝑷 h B x 𝑸 x < 𝑸 g + 𝑸 h x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h B
11 10 adantll A 𝑷 g A B 𝑷 h B x 𝑸 x < 𝑸 g + 𝑸 h x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h B
12 2 11 jcad A 𝑷 g A B 𝑷 h B x 𝑸 x < 𝑸 g + 𝑸 h x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g A x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h B
13 simpl A 𝑷 g A B 𝑷 h B x 𝑸 A 𝑷 g A B 𝑷 h B
14 simpl A 𝑷 g A A 𝑷
15 simpl B 𝑷 h B B 𝑷
16 14 15 anim12i A 𝑷 g A B 𝑷 h B A 𝑷 B 𝑷
17 df-plp + 𝑷 = w 𝑷 , v 𝑷 x | y w z v x = y + 𝑸 z
18 addclnq y 𝑸 z 𝑸 y + 𝑸 z 𝑸
19 17 18 genpprecl A 𝑷 B 𝑷 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g A x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h B x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h A + 𝑷 B
20 13 16 19 3syl A 𝑷 g A B 𝑷 h B x 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g A x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h B x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h A + 𝑷 B
21 12 20 syld A 𝑷 g A B 𝑷 h B x 𝑸 x < 𝑸 g + 𝑸 h x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h A + 𝑷 B
22 distrnq x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h = x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h
23 mulassnq x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h = x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h
24 22 23 eqtr3i x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h = x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h
25 mulcomnq * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h = g + 𝑸 h 𝑸 * 𝑸 g + 𝑸 h
26 elprnq A 𝑷 g A g 𝑸
27 elprnq B 𝑷 h B h 𝑸
28 26 27 anim12i A 𝑷 g A B 𝑷 h B g 𝑸 h 𝑸
29 addclnq g 𝑸 h 𝑸 g + 𝑸 h 𝑸
30 recidnq g + 𝑸 h 𝑸 g + 𝑸 h 𝑸 * 𝑸 g + 𝑸 h = 1 𝑸
31 28 29 30 3syl A 𝑷 g A B 𝑷 h B g + 𝑸 h 𝑸 * 𝑸 g + 𝑸 h = 1 𝑸
32 25 31 eqtrid A 𝑷 g A B 𝑷 h B * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h = 1 𝑸
33 32 oveq2d A 𝑷 g A B 𝑷 h B x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h = x 𝑸 1 𝑸
34 mulidnq x 𝑸 x 𝑸 1 𝑸 = x
35 33 34 sylan9eq A 𝑷 g A B 𝑷 h B x 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 h = x
36 24 35 eqtrid A 𝑷 g A B 𝑷 h B x 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h = x
37 36 eleq1d A 𝑷 g A B 𝑷 h B x 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 g + 𝑸 x 𝑸 * 𝑸 g + 𝑸 h 𝑸 h A + 𝑷 B x A + 𝑷 B
38 21 37 sylibd A 𝑷 g A B 𝑷 h B x 𝑸 x < 𝑸 g + 𝑸 h x A + 𝑷 B