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	$$⊢C\in 𝑷\to \left(A{<}_{𝑷}B\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	$$⊢{<}_{𝑷}\subseteq 𝑷\times 𝑷$$
2	1	brel	$$⊢A{<}_{𝑷}B\to \left(A\in 𝑷\wedge B\in 𝑷\right)$$
3	2	simpld	$$⊢A{<}_{𝑷}B\to A\in 𝑷$$
4		ltexpri	$$⊢A{<}_{𝑷}B\to \exists x\in 𝑷A{+}_{𝑷}x=B$$
5		addclpr	$$⊢\left(C\in 𝑷\wedge A\in 𝑷\right)\to C{+}_{𝑷}A\in 𝑷$$
6		ltaddpr	$$⊢\left(C{+}_{𝑷}A\in 𝑷\wedge x\in 𝑷\right)\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(\left(C{+}_{𝑷}A\right){+}_{𝑷}x\right)$$
7		addasspr	$$⊢\left(C{+}_{𝑷}A\right){+}_{𝑷}x=C{+}_{𝑷}\left(A{+}_{𝑷}x\right)$$
8		oveq2	$$⊢A{+}_{𝑷}x=B\to C{+}_{𝑷}\left(A{+}_{𝑷}x\right)=C{+}_{𝑷}B$$
9	7 8	syl5eq	$$⊢A{+}_{𝑷}x=B\to \left(C{+}_{𝑷}A\right){+}_{𝑷}x=C{+}_{𝑷}B$$
10	9	breq2d	$$⊢A{+}_{𝑷}x=B\to \left(\left(C{+}_{𝑷}A\right){<}_{𝑷}\left(\left(C{+}_{𝑷}A\right){+}_{𝑷}x\right)\leftrightarrow \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)$$
11	6 10	syl5ib	$$⊢A{+}_{𝑷}x=B\to \left(\left(C{+}_{𝑷}A\in 𝑷\wedge x\in 𝑷\right)\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)$$
12	11	expd	$$⊢A{+}_{𝑷}x=B\to \left(C{+}_{𝑷}A\in 𝑷\to \left(x\in 𝑷\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)\right)$$
13	5 12	syl5	$$⊢A{+}_{𝑷}x=B\to \left(\left(C\in 𝑷\wedge A\in 𝑷\right)\to \left(x\in 𝑷\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)\right)$$
14	13	com3r	$$⊢x\in 𝑷\to \left(A{+}_{𝑷}x=B\to \left(\left(C\in 𝑷\wedge A\in 𝑷\right)\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)\right)$$
15	14	rexlimiv	$$⊢\exists x\in 𝑷A{+}_{𝑷}x=B\to \left(\left(C\in 𝑷\wedge A\in 𝑷\right)\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)$$
16	4 15	syl	$$⊢A{<}_{𝑷}B\to \left(\left(C\in 𝑷\wedge A\in 𝑷\right)\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)$$
17	3 16	sylan2i	$$⊢A{<}_{𝑷}B\to \left(\left(C\in 𝑷\wedge A{<}_{𝑷}B\right)\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)$$
18	17	expd	$$⊢A{<}_{𝑷}B\to \left(C\in 𝑷\to \left(A{<}_{𝑷}B\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)\right)$$
19	18	pm2.43b	$$⊢C\in 𝑷\to \left(A{<}_{𝑷}B\to \left(C{+}_{𝑷}A\right){<}_{𝑷}\left(C{+}_{𝑷}B\right)\right)$$