Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltexpi Structured version   Visualization version   GIF version

Theorem ltexpi 9668
 Description: Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ltexpi ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ ∃𝑥N (𝐴 +N 𝑥) = 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ltexpi
StepHypRef Expression
1 pinn 9644 . . 3 (𝐴N𝐴 ∈ ω)
2 pinn 9644 . . 3 (𝐵N𝐵 ∈ ω)
3 nnaordex 7663 . . 3 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
41, 2, 3syl2an 494 . 2 ((𝐴N𝐵N) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
5 ltpiord 9653 . 2 ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))
6 addpiord 9650 . . . . . . 7 ((𝐴N𝑥N) → (𝐴 +N 𝑥) = (𝐴 +𝑜 𝑥))
76eqeq1d 2623 . . . . . 6 ((𝐴N𝑥N) → ((𝐴 +N 𝑥) = 𝐵 ↔ (𝐴 +𝑜 𝑥) = 𝐵))
87pm5.32da 672 . . . . 5 (𝐴N → ((𝑥N ∧ (𝐴 +N 𝑥) = 𝐵) ↔ (𝑥N ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
9 elni2 9643 . . . . . . 7 (𝑥N ↔ (𝑥 ∈ ω ∧ ∅ ∈ 𝑥))
109anbi1i 730 . . . . . 6 ((𝑥N ∧ (𝐴 +𝑜 𝑥) = 𝐵) ↔ ((𝑥 ∈ ω ∧ ∅ ∈ 𝑥) ∧ (𝐴 +𝑜 𝑥) = 𝐵))
11 anass 680 . . . . . 6 (((𝑥 ∈ ω ∧ ∅ ∈ 𝑥) ∧ (𝐴 +𝑜 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
1210, 11bitri 264 . . . . 5 ((𝑥N ∧ (𝐴 +𝑜 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
138, 12syl6bb 276 . . . 4 (𝐴N → ((𝑥N ∧ (𝐴 +N 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵))))
1413rexbidv2 3041 . . 3 (𝐴N → (∃𝑥N (𝐴 +N 𝑥) = 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
1514adantr 481 . 2 ((𝐴N𝐵N) → (∃𝑥N (𝐴 +N 𝑥) = 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
164, 5, 153bitr4d 300 1 ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ ∃𝑥N (𝐴 +N 𝑥) = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∃wrex 2908  ∅c0 3891   class class class wbr 4613  (class class class)co 6604  ωcom 7012   +𝑜 coa 7502  Ncnpi 9610   +N cpli 9611
 Copyright terms: Public domain W3C validator