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

Theorem ltexpi 7086
 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 7058 . . 3 (𝐴N𝐴 ∈ ω)
2 pinn 7058 . . 3 (𝐵N𝐵 ∈ ω)
3 nnaordex 6374 . . 3 ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))
41, 2, 3syl2an 285 . 2 ((𝐴N𝐵N) → (𝐴𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))
5 ltpiord 7068 . 2 ((𝐴N𝐵N) → (𝐴 <N 𝐵𝐴𝐵))
6 addpiord 7065 . . . . . . 7 ((𝐴N𝑥N) → (𝐴 +N 𝑥) = (𝐴 +o 𝑥))
76eqeq1d 2121 . . . . . 6 ((𝐴N𝑥N) → ((𝐴 +N 𝑥) = 𝐵 ↔ (𝐴 +o 𝑥) = 𝐵))
87pm5.32da 445 . . . . 5 (𝐴N → ((𝑥N ∧ (𝐴 +N 𝑥) = 𝐵) ↔ (𝑥N ∧ (𝐴 +o 𝑥) = 𝐵)))
9 elni2 7063 . . . . . . 7 (𝑥N ↔ (𝑥 ∈ ω ∧ ∅ ∈ 𝑥))
109anbi1i 451 . . . . . 6 ((𝑥N ∧ (𝐴 +o 𝑥) = 𝐵) ↔ ((𝑥 ∈ ω ∧ ∅ ∈ 𝑥) ∧ (𝐴 +o 𝑥) = 𝐵))
11 anass 396 . . . . . 6 (((𝑥 ∈ ω ∧ ∅ ∈ 𝑥) ∧ (𝐴 +o 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))
1210, 11bitri 183 . . . . 5 ((𝑥N ∧ (𝐴 +o 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))
138, 12syl6bb 195 . . . 4 (𝐴N → ((𝑥N ∧ (𝐴 +N 𝑥) = 𝐵) ↔ (𝑥 ∈ ω ∧ (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))))
1413rexbidv2 2412 . . 3 (𝐴N → (∃𝑥N (𝐴 +N 𝑥) = 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))
1514adantr 272 . 2 ((𝐴N𝐵N) → (∃𝑥N (𝐴 +N 𝑥) = 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵)))
164, 5, 153bitr4d 219 1 ((𝐴N𝐵N) → (𝐴 <N 𝐵 ↔ ∃𝑥N (𝐴 +N 𝑥) = 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1312   ∈ wcel 1461  ∃wrex 2389  ∅c0 3327   class class class wbr 3893  ωcom 4462  (class class class)co 5726   +o coa 6261  Ncnpi 7021   +N cpli 7022
 Copyright terms: Public domain W3C validator