Theorem nnge1 10581

Description: A positive integer is one or greater. (Contributed by NM, 25-Aug-1999.)

Assertion

Ref	Expression
nnge1	|- ( A e. NN -> 1 <_ A )

Proof of Theorem nnge1

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4365	. 2 |- ( x = 1 -> ( 1 <_ x <-> 1 <_ 1 ) )
2		breq2 4365	. 2 |- ( x = y -> ( 1 <_ x <-> 1 <_ y ) )
3		breq2 4365	. 2 |- ( x = ( y + 1 ) -> ( 1 <_ x <-> 1 <_ ( y + 1 ) ) )
4		breq2 4365	. 2 |- ( x = A -> ( 1 <_ x <-> 1 <_ A ) )
5		1le1 10186	. 2 |- 1 <_ 1
6		nnre 10562	. . 3 |- ( y e. NN -> y e. RR )
7		recn 9575	. . . . . 6 |- ( y e. RR -> y e. CC )
8	7	addid1d 9779	. . . . 5 |- ( y e. RR -> ( y + 0 ) = y )
9	8	breq2d 4373	. . . 4 |- ( y e. RR -> ( 1 <_ ( y + 0 ) <-> 1 <_ y ) )
10		0lt1 10082	. . . . . . . 8 |- 0 < 1
11		0re 9589	. . . . . . . . 9 |- 0 e. RR
12		1re 9588	. . . . . . . . 9 |- 1 e. RR
13		axltadd 9653	. . . . . . . . 9 |- ( ( 0 e. RR /\ 1 e. RR /\ y e. RR ) -> ( 0 < 1 -> ( y + 0 ) < ( y + 1 ) ) )
14	11, 12, 13	mp3an12 1350	. . . . . . . 8 |- ( y e. RR -> ( 0 < 1 -> ( y + 0 ) < ( y + 1 ) ) )
15	10, 14	mpi 20	. . . . . . 7 |- ( y e. RR -> ( y + 0 ) < ( y + 1 ) )
16		readdcl 9568	. . . . . . . . 9 |- ( ( y e. RR /\ 0 e. RR ) -> ( y + 0 ) e. RR )
17	11, 16	mpan2 675	. . . . . . . 8 |- ( y e. RR -> ( y + 0 ) e. RR )
18		peano2re 9752	. . . . . . . 8 |- ( y e. RR -> ( y + 1 ) e. RR )
19		lttr 9656	. . . . . . . . 9 |- ( ( ( y + 0 ) e. RR /\ ( y + 1 ) e. RR /\ 1 e. RR ) -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
20	12, 19	mp3an3 1349	. . . . . . . 8 |- ( ( ( y + 0 ) e. RR /\ ( y + 1 ) e. RR ) -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
21	17, 18, 20	syl2anc 665	. . . . . . 7 |- ( y e. RR -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
22	15, 21	mpand 679	. . . . . 6 |- ( y e. RR -> ( ( y + 1 ) < 1 -> ( y + 0 ) < 1 ) )
23	22	con3d 138	. . . . 5 |- ( y e. RR -> ( -. ( y + 0 ) < 1 -> -. ( y + 1 ) < 1 ) )
24		lenlt 9658	. . . . . 6 |- ( ( 1 e. RR /\ ( y + 0 ) e. RR ) -> ( 1 <_ ( y + 0 ) <-> -. ( y + 0 ) < 1 ) )
25	12, 17, 24	sylancr 667	. . . . 5 |- ( y e. RR -> ( 1 <_ ( y + 0 ) <-> -. ( y + 0 ) < 1 ) )
26		lenlt 9658	. . . . . 6 |- ( ( 1 e. RR /\ ( y + 1 ) e. RR ) -> ( 1 <_ ( y + 1 ) <-> -. ( y + 1 ) < 1 ) )
27	12, 18, 26	sylancr 667	. . . . 5 |- ( y e. RR -> ( 1 <_ ( y + 1 ) <-> -. ( y + 1 ) < 1 ) )
28	23, 25, 27	3imtr4d 271	. . . 4 |- ( y e. RR -> ( 1 <_ ( y + 0 ) -> 1 <_ ( y + 1 ) ) )
29	9, 28	sylbird 238	. . 3 |- ( y e. RR -> ( 1 <_ y -> 1 <_ ( y + 1 ) ) )
30	6, 29	syl 17	. 2 |- ( y e. NN -> ( 1 <_ y -> 1 <_ ( y + 1 ) ) )
31	1, 2, 3, 4, 5, 30	nnind 10573	1 |- ( A e. NN -> 1 <_ A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   e. wcel 1872   class class class wbr 4361  (class class class)co 6244   RRcr 9484   0cc0 9485   1c1 9486   + caddc 9488   < clt 9621   <_ cle 9622   NNcn 10555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-nn 10556

This theorem is referenced by:  nngt1ne1  10582  nnle1eq1  10583  nngt0  10584  nnnlt1  10585  nnrecgt0  10593  nnge1d  10598  elnnnn0c  10861  elnnz1  10909  zltp1le  10932  elfz1b  11810  fzo1fzo0n0  11903  elfzom1elp1fzo  11926  fzo0sn0fzo1  11946  nnlesq  12323  digit1  12351  faclbnd  12420  faclbnd3  12422  faclbnd4lem1  12423  faclbnd4lem4  12426  fstwrdne0  12650  swrdtrcfv  12738  swrdccatwrd  12765  divalglem1  14310  isprm3  14571  coprmgcdb  14592  pockthg  14788  infpn2  14795  chfacfpmmulgsum2  19826  dscmet  21524  ovolunlem1a  22386  vitali  22508  plyeq0lem  23101  logtayllem  23541  leibpi  23805  vmalelog  24070  chtublem  24076  logfaclbnd  24087  bposlem1  24149  dchrisum0lem1  24291  logdivbnd  24331  pntlemn  24375  ostth2lem3  24410  clwwisshclwwlem  25471  clwlkfclwwlk  25509  lmatfvlem  28588  eulerpartlems  29140  eulerpartlemb  29148  ballotlem2  29268  fz0n  30310  nndivlub  31062  fzsplit1nn0  35508  pell1qrgaplem  35632  pellqrex  35639  monotoddzzfi  35703  jm2.23  35764  sumnnodd  37593  dvnmul  37701  wallispilem4  37813  wallispilem5  37814  wallispi  37815  wallispi2lem1  37816  stirlinglem5  37823  stirlinglem13  37831  dirkertrigeqlem1  37843  fouriersw  37978  etransclem24  38006  iccpartigtl  38550  logbpw2m1  39971  blennnelnn  39980  blenpw2m1  39983  dignnld  40007