Theorem nnge1 10557

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 4443	. 2 |- ( x = 1 -> ( 1 <_ x <-> 1 <_ 1 ) )
2		breq2 4443	. 2 |- ( x = y -> ( 1 <_ x <-> 1 <_ y ) )
3		breq2 4443	. 2 |- ( x = ( y + 1 ) -> ( 1 <_ x <-> 1 <_ ( y + 1 ) ) )
4		breq2 4443	. 2 |- ( x = A -> ( 1 <_ x <-> 1 <_ A ) )
5		1le1 10173	. 2 |- 1 <_ 1
6		nnre 10538	. . 3 |- ( y e. NN -> y e. RR )
7		recn 9571	. . . . . 6 |- ( y e. RR -> y e. CC )
8	7	addid1d 9769	. . . . 5 |- ( y e. RR -> ( y + 0 ) = y )
9	8	breq2d 4451	. . . 4 |- ( y e. RR -> ( 1 <_ ( y + 0 ) <-> 1 <_ y ) )
10		0lt1 10071	. . . . . . . 8 |- 0 < 1
11		0re 9585	. . . . . . . . 9 |- 0 e. RR
12		1re 9584	. . . . . . . . 9 |- 1 e. RR
13		axltadd 9647	. . . . . . . . 9 |- ( ( 0 e. RR /\ 1 e. RR /\ y e. RR ) -> ( 0 < 1 -> ( y + 0 ) < ( y + 1 ) ) )
14	11, 12, 13	mp3an12 1312	. . . . . . . 8 |- ( y e. RR -> ( 0 < 1 -> ( y + 0 ) < ( y + 1 ) ) )
15	10, 14	mpi 17	. . . . . . 7 |- ( y e. RR -> ( y + 0 ) < ( y + 1 ) )
16		readdcl 9564	. . . . . . . . 9 |- ( ( y e. RR /\ 0 e. RR ) -> ( y + 0 ) e. RR )
17	11, 16	mpan2 669	. . . . . . . 8 |- ( y e. RR -> ( y + 0 ) e. RR )
18		peano2re 9742	. . . . . . . 8 |- ( y e. RR -> ( y + 1 ) e. RR )
19		lttr 9650	. . . . . . . . 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 1311	. . . . . . . 8 |- ( ( ( y + 0 ) e. RR /\ ( y + 1 ) e. RR ) -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
21	17, 18, 20	syl2anc 659	. . . . . . 7 |- ( y e. RR -> ( ( ( y + 0 ) < ( y + 1 ) /\ ( y + 1 ) < 1 ) -> ( y + 0 ) < 1 ) )
22	15, 21	mpand 673	. . . . . 6 |- ( y e. RR -> ( ( y + 1 ) < 1 -> ( y + 0 ) < 1 ) )
23	22	con3d 133	. . . . 5 |- ( y e. RR -> ( -. ( y + 0 ) < 1 -> -. ( y + 1 ) < 1 ) )
24		lenlt 9652	. . . . . 6 |- ( ( 1 e. RR /\ ( y + 0 ) e. RR ) -> ( 1 <_ ( y + 0 ) <-> -. ( y + 0 ) < 1 ) )
25	12, 17, 24	sylancr 661	. . . . 5 |- ( y e. RR -> ( 1 <_ ( y + 0 ) <-> -. ( y + 0 ) < 1 ) )
26		lenlt 9652	. . . . . 6 |- ( ( 1 e. RR /\ ( y + 1 ) e. RR ) -> ( 1 <_ ( y + 1 ) <-> -. ( y + 1 ) < 1 ) )
27	12, 18, 26	sylancr 661	. . . . 5 |- ( y e. RR -> ( 1 <_ ( y + 1 ) <-> -. ( y + 1 ) < 1 ) )
28	23, 25, 27	3imtr4d 268	. . . 4 |- ( y e. RR -> ( 1 <_ ( y + 0 ) -> 1 <_ ( y + 1 ) ) )
29	9, 28	sylbird 235	. . 3 |- ( y e. RR -> ( 1 <_ y -> 1 <_ ( y + 1 ) ) )
30	6, 29	syl 16	. 2 |- ( y e. NN -> ( 1 <_ y -> 1 <_ ( y + 1 ) ) )
31	1, 2, 3, 4, 5, 30	nnind 10549	1 |- ( A e. NN -> 1 <_ A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   e. wcel 1823   class class class wbr 4439  (class class class)co 6270   RRcr 9480   0cc0 9481   1c1 9482   + caddc 9484   < clt 9617   <_ cle 9618   NNcn 10531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-recs 7034  df-rdg 7068  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-nn 10532

This theorem is referenced by:  nngt1ne1  10558  nnle1eq1  10559  nngt0  10560  nnnlt1  10561  nnrecgt0  10569  nnge1d  10574  elnnnn0c  10837  elnnz1  10886  zltp1le  10909  elfz1b  11752  fzo1fzo0n0  11841  elfzom1elp1fzo  11864  fzo0sn0fzo1  11883  nnlesq  12253  digit1  12282  faclbnd  12350  faclbnd3  12352  faclbnd4lem1  12353  faclbnd4lem4  12356  fstwrdne0  12569  swrdtrcfv  12657  swrdccatwrd  12684  divalglem1  14136  isprm3  14310  pockthg  14508  infpn2  14515  chfacfpmmulgsum2  19533  dscmet  21259  ovolunlem1a  22073  vitali  22188  plyeq0lem  22773  logtayllem  23208  leibpi  23470  vmalelog  23678  chtublem  23684  logfaclbnd  23695  bposlem1  23757  dchrisum0lem1  23899  logdivbnd  23939  pntlemn  23983  ostth2lem3  24018  clwwisshclwwlem  25008  clwlkfclwwlk  25046  eulerpartlems  28563  eulerpartlemb  28571  ballotlem2  28691  fz0n  29351  nndivlub  30151  fzsplit1nn0  30926  pell1qrgaplem  31048  pellqrex  31054  monotoddzzfi  31117  jm2.23  31177  sumnnodd  31875  dvnmul  31979  wallispilem4  32089  wallispilem5  32090  wallispi  32091  wallispi2lem1  32092  stirlinglem5  32099  stirlinglem13  32107  dirkertrigeqlem1  32119  fouriersw  32253  etransclem24  32280  logbpw2m1  33442  blennnelnn  33451  blenpw2m1  33454  dignnld  33478