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∈𝑷→A<𝑷B↔C+𝑷A<𝑷C+𝑷B

Proof

Step Hyp Ref Expression
1 dmplp ⊢dom⁡+𝑷=𝑷×𝑷
2 ltrelpr ⊢<𝑷⊆𝑷×𝑷
3 0npr ⊢¬∅∈𝑷
4 ltaprlem ⊢C∈𝑷→A<𝑷B→C+𝑷A<𝑷C+𝑷B
5 4 adantr ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→A<𝑷B→C+𝑷A<𝑷C+𝑷B
6 olc ⊢C+𝑷A<𝑷C+𝑷B→C+𝑷B=C+𝑷A∨C+𝑷A<𝑷C+𝑷B
7 ltaprlem ⊢C∈𝑷→B<𝑷A→C+𝑷B<𝑷C+𝑷A
8 7 adantr ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→B<𝑷A→C+𝑷B<𝑷C+𝑷A
9 ltsopr ⊢<𝑷Or𝑷
10 sotric ⊢<𝑷Or𝑷∧B∈𝑷∧A∈𝑷→B<𝑷A↔¬B=A∨A<𝑷B
11 9 10 mpan ⊢B∈𝑷∧A∈𝑷→B<𝑷A↔¬B=A∨A<𝑷B
12 11 adantl ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→B<𝑷A↔¬B=A∨A<𝑷B
13 addclpr ⊢C∈𝑷∧B∈𝑷→C+𝑷B∈𝑷
14 addclpr ⊢C∈𝑷∧A∈𝑷→C+𝑷A∈𝑷
15 13 14 anim12dan ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→C+𝑷B∈𝑷∧C+𝑷A∈𝑷
16 sotric ⊢<𝑷Or𝑷∧C+𝑷B∈𝑷∧C+𝑷A∈𝑷→C+𝑷B<𝑷C+𝑷A↔¬C+𝑷B=C+𝑷A∨C+𝑷A<𝑷C+𝑷B
17 9 15 16 sylancr ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→C+𝑷B<𝑷C+𝑷A↔¬C+𝑷B=C+𝑷A∨C+𝑷A<𝑷C+𝑷B
18 8 12 17 3imtr3d ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→¬B=A∨A<𝑷B→¬C+𝑷B=C+𝑷A∨C+𝑷A<𝑷C+𝑷B
19 18 con4d ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→C+𝑷B=C+𝑷A∨C+𝑷A<𝑷C+𝑷B→B=A∨A<𝑷B
20 6 19 syl5 ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→C+𝑷A<𝑷C+𝑷B→B=A∨A<𝑷B
21 df-or ⊢B=A∨A<𝑷B↔¬B=A→A<𝑷B
22 20 21 imbitrdi ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→C+𝑷A<𝑷C+𝑷B→¬B=A→A<𝑷B
23 22 com23 ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→¬B=A→C+𝑷A<𝑷C+𝑷B→A<𝑷B
24 9 2 soirri ⊢¬C+𝑷A<𝑷C+𝑷A
25 oveq2 ⊢B=A→C+𝑷B=C+𝑷A
26 25 breq2d ⊢B=A→C+𝑷A<𝑷C+𝑷B↔C+𝑷A<𝑷C+𝑷A
27 24 26 mtbiri ⊢B=A→¬C+𝑷A<𝑷C+𝑷B
28 27 pm2.21d ⊢B=A→C+𝑷A<𝑷C+𝑷B→A<𝑷B
29 23 28 pm2.61d2 ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→C+𝑷A<𝑷C+𝑷B→A<𝑷B
30 5 29 impbid ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→A<𝑷B↔C+𝑷A<𝑷C+𝑷B
31 30 3impb ⊢C∈𝑷∧B∈𝑷∧A∈𝑷→A<𝑷B↔C+𝑷A<𝑷C+𝑷B
32 31 3com13 ⊢A∈𝑷∧B∈𝑷∧C∈𝑷→A<𝑷B↔C+𝑷A<𝑷C+𝑷B
33 1 2 3 32 ndmovord ⊢C∈𝑷→A<𝑷B↔C+𝑷A<𝑷C+𝑷B