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 ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 +Q ℎ ) → ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elprnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) → 𝑔 ∈ Q )
2 ltrnq ⊢ ( 𝑥 <Q ( 𝑔 +Q ℎ ) ↔ ( *Q ‘ ( 𝑔 +Q ℎ ) ) <Q ( *Q ‘ 𝑥 ) )
3 ltmnq ⊢ ( 𝑥 ∈ Q → ( ( *Q ‘ ( 𝑔 +Q ℎ ) ) <Q ( *Q ‘ 𝑥 ) ↔ ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) <Q ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ) )
4 ovex ⊢ ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ∈ V
5 ovex ⊢ ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ∈ V
6 ltmnq ⊢ ( 𝑤 ∈ Q → ( 𝑦 <Q 𝑧 ↔ ( 𝑤 ·Q 𝑦 ) <Q ( 𝑤 ·Q 𝑧 ) ) )
7 vex ⊢ 𝑔 ∈ V
8 mulcomnq ⊢ ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 )
9 4 5 6 7 8 caovord2 ⊢ ( 𝑔 ∈ Q → ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) <Q ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ↔ ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q ( ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ·Q 𝑔 ) ) )
10 3 9 sylan9bbr ⊢ ( ( 𝑔 ∈ Q ∧ 𝑥 ∈ Q ) → ( ( *Q ‘ ( 𝑔 +Q ℎ ) ) <Q ( *Q ‘ 𝑥 ) ↔ ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q ( ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ·Q 𝑔 ) ) )
11 2 10 syl5bb ⊢ ( ( 𝑔 ∈ Q ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 +Q ℎ ) ↔ ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q ( ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ·Q 𝑔 ) ) )
12 recidnq ⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) = 1Q )
13 12 oveq1d ⊢ ( 𝑥 ∈ Q → ( ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ·Q 𝑔 ) = ( 1Q ·Q 𝑔 ) )
14 mulcomnq ⊢ ( 1Q ·Q 𝑔 ) = ( 𝑔 ·Q 1Q )
15 mulidnq ⊢ ( 𝑔 ∈ Q → ( 𝑔 ·Q 1Q ) = 𝑔 )
16 14 15 syl5eq ⊢ ( 𝑔 ∈ Q → ( 1Q ·Q 𝑔 ) = 𝑔 )
17 13 16 sylan9eqr ⊢ ( ( 𝑔 ∈ Q ∧ 𝑥 ∈ Q ) → ( ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ·Q 𝑔 ) = 𝑔 )
18 17 breq2d ⊢ ( ( 𝑔 ∈ Q ∧ 𝑥 ∈ Q ) → ( ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q ( ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) ·Q 𝑔 ) ↔ ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q 𝑔 ) )
19 11 18 bitrd ⊢ ( ( 𝑔 ∈ Q ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 +Q ℎ ) ↔ ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q 𝑔 ) )
20 1 19 sylan ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 +Q ℎ ) ↔ ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q 𝑔 ) )
21 prcdnq ⊢ ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) → ( ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q 𝑔 → ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) ∈ 𝐴 ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑥 ∈ Q ) → ( ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) <Q 𝑔 → ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) ∈ 𝐴 ) )
23 20 22 sylbid ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑔 ∈ 𝐴 ) ∧ 𝑥 ∈ Q ) → ( 𝑥 <Q ( 𝑔 +Q ℎ ) → ( ( 𝑥 ·Q ( *Q ‘ ( 𝑔 +Q ℎ ) ) ) ·Q 𝑔 ) ∈ 𝐴 ) )