Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltapig GIF version

Theorem ltapig 6393
 Description: Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
Assertion
Ref Expression
ltapig ((𝐴N𝐵N𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))

Proof of Theorem ltapig
StepHypRef Expression
1 pinn 6364 . . . . 5 (𝐴N𝐴 ∈ ω)
2 pinn 6364 . . . . 5 (𝐵N𝐵 ∈ ω)
3 pinn 6364 . . . . 5 (𝐶N𝐶 ∈ ω)
4 nnaord 6045 . . . . 5 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴𝐵 ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
51, 2, 3, 4syl3an 1177 . . . 4 ((𝐴N𝐵N𝐶N) → (𝐴𝐵 ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
653expa 1104 . . 3 (((𝐴N𝐵N) ∧ 𝐶N) → (𝐴𝐵 ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
7 ltpiord 6374 . . . 4 ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))
87adantr 261 . . 3 (((𝐴N𝐵N) ∧ 𝐶N) → (𝐴 <N 𝐵𝐴𝐵))
9 addclpi 6382 . . . . . . 7 ((𝐶N𝐴N) → (𝐶 +N 𝐴) ∈ N)
10 addclpi 6382 . . . . . . 7 ((𝐶N𝐵N) → (𝐶 +N 𝐵) ∈ N)
11 ltpiord 6374 . . . . . . 7 (((𝐶 +N 𝐴) ∈ N ∧ (𝐶 +N 𝐵) ∈ N) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +N 𝐴) ∈ (𝐶 +N 𝐵)))
129, 10, 11syl2an 273 . . . . . 6 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +N 𝐴) ∈ (𝐶 +N 𝐵)))
13 addpiord 6371 . . . . . . . 8 ((𝐶N𝐴N) → (𝐶 +N 𝐴) = (𝐶 +𝑜 𝐴))
1413adantr 261 . . . . . . 7 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → (𝐶 +N 𝐴) = (𝐶 +𝑜 𝐴))
15 addpiord 6371 . . . . . . . 8 ((𝐶N𝐵N) → (𝐶 +N 𝐵) = (𝐶 +𝑜 𝐵))
1615adantl 262 . . . . . . 7 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → (𝐶 +N 𝐵) = (𝐶 +𝑜 𝐵))
1714, 16eleq12d 2108 . . . . . 6 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → ((𝐶 +N 𝐴) ∈ (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
1812, 17bitrd 177 . . . . 5 (((𝐶N𝐴N) ∧ (𝐶N𝐵N)) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
1918anandis 526 . . . 4 ((𝐶N ∧ (𝐴N𝐵N)) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
2019ancoms 255 . . 3 (((𝐴N𝐵N) ∧ 𝐶N) → ((𝐶 +N 𝐴) <N (𝐶 +N 𝐵) ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵)))
216, 8, 203bitr4d 209 . 2 (((𝐴N𝐵N) ∧ 𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
22213impa 1099 1 ((𝐴N𝐵N𝐶N) → (𝐴 <N 𝐵 ↔ (𝐶 +N 𝐴) <N (𝐶 +N 𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885   = wceq 1243   ∈ wcel 1393   class class class wbr 3761  ωcom 4276  (class class class)co 5475   +𝑜 coa 5961  Ncnpi 6327   +N cpli 6328
 Copyright terms: Public domain W3C validator