This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltaprlem

Description: Lemma for Proposition 9-3.5(v) of Gleason p. 123. (Contributed by NM, 8-Apr-1996) (New usage is discouraged.)

Ref Expression
Assertion ltaprlem ( 𝐶 ∈ P → ( 𝐴 <P 𝐵 → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ltrelpr ⊢ <P ⊆ ( P × P )
2 1 brel ⊢ ( 𝐴 <P 𝐵 → ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) )
3 2 simpld ⊢ ( 𝐴 <P 𝐵 → 𝐴 ∈ P )
4 ltexpri ⊢ ( 𝐴 <P 𝐵 → ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 )
5 addclpr ⊢ ( ( 𝐶 ∈ P ∧ 𝐴 ∈ P ) → ( 𝐶 +P 𝐴 ) ∈ P )
6 ltaddpr ⊢ ( ( ( 𝐶 +P 𝐴 ) ∈ P ∧ 𝑥 ∈ P ) → ( 𝐶 +P 𝐴 ) <P ( ( 𝐶 +P 𝐴 ) +P 𝑥 ) )
7 addasspr ⊢ ( ( 𝐶 +P 𝐴 ) +P 𝑥 ) = ( 𝐶 +P ( 𝐴 +P 𝑥 ) )
8 oveq2 ⊢ ( ( 𝐴 +P 𝑥 ) = 𝐵 → ( 𝐶 +P ( 𝐴 +P 𝑥 ) ) = ( 𝐶 +P 𝐵 ) )
9 7 8 eqtrid ⊢ ( ( 𝐴 +P 𝑥 ) = 𝐵 → ( ( 𝐶 +P 𝐴 ) +P 𝑥 ) = ( 𝐶 +P 𝐵 ) )
10 9 breq2d ⊢ ( ( 𝐴 +P 𝑥 ) = 𝐵 → ( ( 𝐶 +P 𝐴 ) <P ( ( 𝐶 +P 𝐴 ) +P 𝑥 ) ↔ ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )
11 6 10 imbitrid ⊢ ( ( 𝐴 +P 𝑥 ) = 𝐵 → ( ( ( 𝐶 +P 𝐴 ) ∈ P ∧ 𝑥 ∈ P ) → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )
12 11 expd ⊢ ( ( 𝐴 +P 𝑥 ) = 𝐵 → ( ( 𝐶 +P 𝐴 ) ∈ P → ( 𝑥 ∈ P → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) ) )
13 5 12 syl5 ⊢ ( ( 𝐴 +P 𝑥 ) = 𝐵 → ( ( 𝐶 ∈ P ∧ 𝐴 ∈ P ) → ( 𝑥 ∈ P → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) ) )
14 13 com3r ⊢ ( 𝑥 ∈ P → ( ( 𝐴 +P 𝑥 ) = 𝐵 → ( ( 𝐶 ∈ P ∧ 𝐴 ∈ P ) → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) ) )
15 14 rexlimiv ⊢ ( ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 → ( ( 𝐶 ∈ P ∧ 𝐴 ∈ P ) → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )
16 4 15 syl ⊢ ( 𝐴 <P 𝐵 → ( ( 𝐶 ∈ P ∧ 𝐴 ∈ P ) → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )
17 3 16 sylan2i ⊢ ( 𝐴 <P 𝐵 → ( ( 𝐶 ∈ P ∧ 𝐴 <P 𝐵 ) → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )
18 17 expd ⊢ ( 𝐴 <P 𝐵 → ( 𝐶 ∈ P → ( 𝐴 <P 𝐵 → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) ) )
19 18 pm2.43b ⊢ ( 𝐶 ∈ P → ( 𝐴 <P 𝐵 → ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )