Theorem ltapr

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

	Ref	Expression
Assertion	ltapr	|- ( C e. P. -> ( A ( C +P. A )

Proof

Step	Hyp	Ref	Expression
1		dmplp	|- dom +P. = ( P. X. P. )
2		ltrelpr	|-
3		0npr	|- -. (/) e. P.
4		ltaprlem	|- ( C e. P. -> ( A ( C +P. A )
5	4	adantr	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( A ( C +P. A )
6		olc	|- ( ( C +P. A ) ( ( C +P. B ) = ( C +P. A ) \/ ( C +P. A )
7		ltaprlem	|- ( C e. P. -> ( B ( C +P. B )
8	7	adantr	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( B ( C +P. B )
9		ltsopr	|-
10		sotric	|- ( ( ( B -. ( B = A \/ A
11	9 10	mpan	|- ( ( B e. P. /\ A e. P. ) -> ( B -. ( B = A \/ A
12	11	adantl	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( B -. ( B = A \/ A
13		addclpr	|- ( ( C e. P. /\ B e. P. ) -> ( C +P. B ) e. P. )
14		addclpr	|- ( ( C e. P. /\ A e. P. ) -> ( C +P. A ) e. P. )
15	13 14	anim12dan	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( ( C +P. B ) e. P. /\ ( C +P. A ) e. P. ) )
16		sotric	|- ( ( ( ( C +P. B ) -. ( ( C +P. B ) = ( C +P. A ) \/ ( C +P. A )
17	9 15 16	sylancr	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( ( C +P. B ) -. ( ( C +P. B ) = ( C +P. A ) \/ ( C +P. A )
18	8 12 17	3imtr3d	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( -. ( B = A \/ A -. ( ( C +P. B ) = ( C +P. A ) \/ ( C +P. A )
19	18	con4d	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( ( ( C +P. B ) = ( C +P. A ) \/ ( C +P. A ) ( B = A \/ A
20	6 19	syl5	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( ( C +P. A ) ( B = A \/ A
21		df-or	|- ( ( B = A \/ A ( -. B = A -> A
22	20 21	imbitrdi	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( ( C +P. A ) ( -. B = A -> A
23	22	com23	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( -. B = A -> ( ( C +P. A ) A
24	9 2	soirri	|- -. ( C +P. A )
25		oveq2	|- ( B = A -> ( C +P. B ) = ( C +P. A ) )
26	25	breq2d	|- ( B = A -> ( ( C +P. A ) ( C +P. A )
27	24 26	mtbiri	|- ( B = A -> -. ( C +P. A )
28	27	pm2.21d	|- ( B = A -> ( ( C +P. A ) A
29	23 28	pm2.61d2	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( ( C +P. A ) A
30	5 29	impbid	|- ( ( C e. P. /\ ( B e. P. /\ A e. P. ) ) -> ( A ( C +P. A )
31	30	3impb	|- ( ( C e. P. /\ B e. P. /\ A e. P. ) -> ( A ( C +P. A )
32	31	3com13	|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A ( C +P. A )
33	1 2 3 32	ndmovord	|- ( C e. P. -> ( A ( C +P. A )