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

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

Proof of Theorem ltexpi
StepHypRef Expression
1 pinn 6407 . . 3 (𝐴N𝐴 ∈ ω)
2 pinn 6407 . . 3 (𝐵N𝐵 ∈ ω)
3 nnaordex 6100 . . 3 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
41, 2, 3syl2an 273 . 2 ((𝐴N𝐵N) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
5 ltpiord 6417 . 2 ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))
6 addpiord 6414 . . . . . . 7 ((𝐴N𝑥N) → (𝐴 +N 𝑥) = (𝐴 +𝑜 𝑥))
76eqeq1d 2048 . . . . . 6 ((𝐴N𝑥N) → ((𝐴 +N 𝑥) = 𝐵 ↔ (𝐴 +𝑜 𝑥) = 𝐵))
87pm5.32da 425 . . . . 5 (𝐴N → ((𝑥N ∧ (𝐴 +N 𝑥) = 𝐵) ↔ (𝑥N ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
9 elni2 6412 . . . . . . 7 (𝑥N ↔ (𝑥 ∈ ω ∧ ∅ ∈ 𝑥))
109anbi1i 431 . . . . . 6 ((𝑥N ∧ (𝐴 +𝑜 𝑥) = 𝐵) ↔ ((𝑥 ∈ ω ∧ ∅ ∈ 𝑥) ∧ (𝐴 +𝑜 𝑥) = 𝐵))
11 anass 381 . . . . . 6 (((𝑥 ∈ ω ∧ ∅ ∈ 𝑥) ∧ (𝐴 +𝑜 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
1210, 11bitri 173 . . . . 5 ((𝑥N ∧ (𝐴 +𝑜 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
138, 12syl6bb 185 . . . 4 (𝐴N → ((𝑥N ∧ (𝐴 +N 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵))))
1413rexbidv2 2329 . . 3 (𝐴N → (∃𝑥N (𝐴 +N 𝑥) = 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
1514adantr 261 . 2 ((𝐴N𝐵N) → (∃𝑥N (𝐴 +N 𝑥) = 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +𝑜 𝑥) = 𝐵)))
164, 5, 153bitr4d 209 1 ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ ∃𝑥N (𝐴 +N 𝑥) = 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  ∃wrex 2307  ∅c0 3224   class class class wbr 3764  ωcom 4313  (class class class)co 5512   +𝑜 coa 5998  Ncnpi 6370   +N cpli 6371
 Copyright terms: Public domain W3C validator