Metamath Proof Explorer

Theorem ltexpi

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.)

Ref Expression
Assertion ltexpi ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A < 𝑵 B ↔ ∃ x ∈ 𝑵 A + 𝑵 x = B

Proof

Step Hyp Ref Expression
1 pinn ⊢ A ∈ 𝑵 → A ∈ ω
2 pinn ⊢ B ∈ 𝑵 → B ∈ ω
3 nnaordex ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B ↔ ∃ x ∈ ω ∅ ∈ x ∧ A + 𝑜 x = B
4 1 2 3 syl2an ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A ∈ B ↔ ∃ x ∈ ω ∅ ∈ x ∧ A + 𝑜 x = B
5 ltpiord ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A < 𝑵 B ↔ A ∈ B
6 addpiord ⊢ A ∈ 𝑵 ∧ x ∈ 𝑵 → A + 𝑵 x = A + 𝑜 x
7 6 eqeq1d ⊢ A ∈ 𝑵 ∧ x ∈ 𝑵 → A + 𝑵 x = B ↔ A + 𝑜 x = B
8 7 pm5.32da ⊢ A ∈ 𝑵 → x ∈ 𝑵 ∧ A + 𝑵 x = B ↔ x ∈ 𝑵 ∧ A + 𝑜 x = B
9 elni2 ⊢ x ∈ 𝑵 ↔ x ∈ ω ∧ ∅ ∈ x
10 9 anbi1i ⊢ x ∈ 𝑵 ∧ A + 𝑜 x = B ↔ x ∈ ω ∧ ∅ ∈ x ∧ A + 𝑜 x = B
11 anass ⊢ x ∈ ω ∧ ∅ ∈ x ∧ A + 𝑜 x = B ↔ x ∈ ω ∧ ∅ ∈ x ∧ A + 𝑜 x = B
12 10 11 bitri ⊢ x ∈ 𝑵 ∧ A + 𝑜 x = B ↔ x ∈ ω ∧ ∅ ∈ x ∧ A + 𝑜 x = B
13 8 12 syl6bb ⊢ A ∈ 𝑵 → x ∈ 𝑵 ∧ A + 𝑵 x = B ↔ x ∈ ω ∧ ∅ ∈ x ∧ A + 𝑜 x = B
14 13 rexbidv2 ⊢ A ∈ 𝑵 → ∃ x ∈ 𝑵 A + 𝑵 x = B ↔ ∃ x ∈ ω ∅ ∈ x ∧ A + 𝑜 x = B
15 14 adantr ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → ∃ x ∈ 𝑵 A + 𝑵 x = B ↔ ∃ x ∈ ω ∅ ∈ x ∧ A + 𝑜 x = B
16 4 5 15 3bitr4d ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 → A < 𝑵 B ↔ ∃ x ∈ 𝑵 A + 𝑵 x = B