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