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

Theorem elni2 7166
 Description: Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)
Assertion
Ref Expression
elni2

Proof of Theorem elni2
StepHypRef Expression
1 pinn 7161 . . 3
2 0npi 7165 . . . . . 6
3 eleq1 2203 . . . . . 6
42, 3mtbiri 665 . . . . 5
54con2i 617 . . . 4
6 0elnn 4541 . . . . . 6
71, 6syl 14 . . . . 5
87ord 714 . . . 4
95, 8mpd 13 . . 3
101, 9jca 304 . 2
11 nndceq0 4540 . . . . . 6 DECID
12 df-dc 821 . . . . . 6 DECID
1311, 12sylib 121 . . . . 5
1413anim1i 338 . . . 4
15 ancom 264 . . . . 5
16 andi 808 . . . . 5
1715, 16bitr3i 185 . . . 4
1814, 17sylib 121 . . 3
19 noel 3373 . . . . . . . . 9
20 eleq2 2204 . . . . . . . . 9
2119, 20mtbiri 665 . . . . . . . 8
2221pm2.21d 609 . . . . . . 7
2322impcom 124 . . . . . 6
2423a1i 9 . . . . 5
25 df-ne 2310 . . . . . . 7
26 elni 7160 . . . . . . . 8
2726simplbi2 383 . . . . . . 7
2825, 27syl5bir 152 . . . . . 6
2928adantld 276 . . . . 5
3024, 29jaod 707 . . . 4