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

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