Theorem eldmgm

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

	Ref	Expression
Assertion	eldmgm	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ - 𝐴 ∈ ℕ0 ) )

Proof

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