Metamath Proof Explorer


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 syl6ib
 |-  ( ( 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 )