Metamath Proof Explorer

Theorem ltapi

Description: Ordering property of addition for positive integers. (Contributed by NM, 7-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion ltapi ( 𝐶 ∈ N → ( 𝐴 <N 𝐵 ↔ ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dmaddpi ⊢ dom +N = ( N × N )
2 ltrelpi ⊢ <N ⊆ ( N × N )
3 0npi ⊢ ¬ ∅ ∈ N
4 pinn ⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
5 pinn ⊢ ( 𝐵 ∈ N → 𝐵 ∈ ω )
6 pinn ⊢ ( 𝐶 ∈ N → 𝐶 ∈ ω )
7 nnaord ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
8 4 5 6 7 syl3an ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
9 8 3expa ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
10 ltpiord ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 <N 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
12 addclpi ⊢ ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) → ( 𝐶 +N 𝐴 ) ∈ N )
13 addclpi ⊢ ( ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐶 +N 𝐵 ) ∈ N )
14 ltpiord ⊢ ( ( ( 𝐶 +N 𝐴 ) ∈ N ∧ ( 𝐶 +N 𝐵 ) ∈ N ) → ( ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ↔ ( 𝐶 +N 𝐴 ) ∈ ( 𝐶 +N 𝐵 ) ) )
15 12 13 14 syl2an ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ↔ ( 𝐶 +N 𝐴 ) ∈ ( 𝐶 +N 𝐵 ) ) )
16 addpiord ⊢ ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) → ( 𝐶 +N 𝐴 ) = ( 𝐶 +o 𝐴 ) )
17 16 adantr ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( 𝐶 +N 𝐴 ) = ( 𝐶 +o 𝐴 ) )
18 addpiord ⊢ ( ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) → ( 𝐶 +N 𝐵 ) = ( 𝐶 +o 𝐵 ) )
19 18 adantl ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( 𝐶 +N 𝐵 ) = ( 𝐶 +o 𝐵 ) )
20 17 19 eleq12d ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 +N 𝐴 ) ∈ ( 𝐶 +N 𝐵 ) ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
21 15 20 bitrd ⊢ ( ( ( 𝐶 ∈ N ∧ 𝐴 ∈ N ) ∧ ( 𝐶 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
22 21 anandis ⊢ ( ( 𝐶 ∈ N ∧ ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ) → ( ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
23 22 ancoms ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ↔ ( 𝐶 +o 𝐴 ) ∈ ( 𝐶 +o 𝐵 ) ) )
24 9 11 23 3bitr4d ⊢ ( ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ) ∧ 𝐶 ∈ N ) → ( 𝐴 <N 𝐵 ↔ ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ) )
25 24 3impa ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 <N 𝐵 ↔ ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ) )
26 1 2 3 25 ndmovord ⊢ ( 𝐶 ∈ N → ( 𝐴 <N 𝐵 ↔ ( 𝐶 +N 𝐴 ) <N ( 𝐶 +N 𝐵 ) ) )