Metamath Proof Explorer

Theorem eldmgm

Description: Elementhood in the set of non-nonpositive integers. (Contributed by Mario Carneiro, 12-Jul-2014)

Ref Expression
Assertion eldmgm ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ ↔ A ∈ ℂ ∧ ¬ − A ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 eldif ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ ↔ A ∈ ℂ ∧ ¬ A ∈ ℤ ∖ ℕ
2 eldif ⊢ A ∈ ℤ ∖ ℕ ↔ A ∈ ℤ ∧ ¬ A ∈ ℕ
3 elznn ⊢ A ∈ ℤ ↔ A ∈ ℝ ∧ A ∈ ℕ ∨ − A ∈ ℕ 0
4 3 simprbi ⊢ A ∈ ℤ → A ∈ ℕ ∨ − A ∈ ℕ 0
5 4 orcanai ⊢ A ∈ ℤ ∧ ¬ A ∈ ℕ → − A ∈ ℕ 0
6 negneg ⊢ A ∈ ℂ → − − A = A
7 6 adantr ⊢ A ∈ ℂ ∧ − A ∈ ℕ 0 → − − A = A
8 nn0negz ⊢ − A ∈ ℕ 0 → − − A ∈ ℤ
9 8 adantl ⊢ A ∈ ℂ ∧ − A ∈ ℕ 0 → − − A ∈ ℤ
10 7 9 eqeltrrd ⊢ A ∈ ℂ ∧ − A ∈ ℕ 0 → A ∈ ℤ
11 10 ex ⊢ A ∈ ℂ → − A ∈ ℕ 0 → A ∈ ℤ
12 nngt0 ⊢ A ∈ ℕ → 0 < A
13 nnre ⊢ A ∈ ℕ → A ∈ ℝ
14 13 lt0neg2d ⊢ A ∈ ℕ → 0 < A ↔ − A < 0
15 12 14 mpbid ⊢ A ∈ ℕ → − A < 0
16 13 renegcld ⊢ A ∈ ℕ → − A ∈ ℝ
17 0re ⊢ 0 ∈ ℝ
18 ltnle ⊢ − A ∈ ℝ ∧ 0 ∈ ℝ → − A < 0 ↔ ¬ 0 ≤ − A
19 16 17 18 sylancl ⊢ A ∈ ℕ → − A < 0 ↔ ¬ 0 ≤ − A
20 15 19 mpbid ⊢ A ∈ ℕ → ¬ 0 ≤ − A
21 nn0ge0 ⊢ − A ∈ ℕ 0 → 0 ≤ − A
22 20 21 nsyl3 ⊢ − A ∈ ℕ 0 → ¬ A ∈ ℕ
23 11 22 jca2 ⊢ A ∈ ℂ → − A ∈ ℕ 0 → A ∈ ℤ ∧ ¬ A ∈ ℕ
24 5 23 impbid2 ⊢ A ∈ ℂ → A ∈ ℤ ∧ ¬ A ∈ ℕ ↔ − A ∈ ℕ 0
25 2 24 syl5bb ⊢ A ∈ ℂ → A ∈ ℤ ∖ ℕ ↔ − A ∈ ℕ 0
26 25 notbid ⊢ A ∈ ℂ → ¬ A ∈ ℤ ∖ ℕ ↔ ¬ − A ∈ ℕ 0
27 26 pm5.32i ⊢ A ∈ ℂ ∧ ¬ A ∈ ℤ ∖ ℕ ↔ A ∈ ℂ ∧ ¬ − A ∈ ℕ 0
28 1 27 bitri ⊢ A ∈ ℂ ∖ ℤ ∖ ℕ ↔ A ∈ ℂ ∧ ¬ − A ∈ ℕ 0