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 ( 𝐶 ∈ P → ( 𝐴 <P 𝐵 ↔ ( 𝐶 +P 𝐴 ) <P ( 𝐶 +P 𝐵 ) ) )

Proof

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