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 𝐵 ) ) )