Theorem lt01 5604

Description: 0 is less than 1. Theorem I.21 of [Apostol] p. 20.

Assertion

Ref	Expression
lt01	|- 0 < 1

Proof of Theorem lt01

Step	Hyp	Ref	Expression
1		ax1ne0 5203	. . 3 |- 1 =/= 0
2		1re 5358	. . . 4 |- 1 e. RR
3	2	msqgt0 5538	. . 3 |- (1 =/= 0 -> 0 < (1 x. 1))
4	1, 3	ax-mp 7	. 2 |- 0 < (1 x. 1)
5		ax1cn 5192	. . 3 |- 1 e. CC
6	5	mulid1 5255	. 2 |- (1 x. 1) = 1
7	4, 6	breqtr 2606	1 |- 0 < 1

Syntax hints:   =/= wne 1561   class class class wbr 2587  (class class class)co 3902  0cc0 5157  1c1 5158   x. cmul 5162   < clt 5409

This theorem is referenced by:  eqneg 5711  elimgt0 5716  ltp1t 5718  recgt0i 5721  ltm1t 5722  mulgt1t 5752  lemulge11t 5755  recgt0t 5766  reclt1t 5797  recgt1t 5798  recgt1it 5799  recp1lt1 5800  recrecltt 5801  halfpos 5803  posex 5807  nnge1t 5842  nngt0t 5845  0nnn 5847  nnrecgt0t 5851  nnleltp1t 5852  2pos 5887  3pos 5889  4pos 5890  5pos 5891  6pos 5892  7pos 5893  8pos 5894  9pos 5895  10pos 5896  halflt1 5928  lt0nnn0 6014  elnnz1 6053  zltp1let 6079  recnzt 6089  rpexpclt 6465  expgt0t 6471  expge0t 6473  expordit 6482  exple1t 6489  expnbndt 6536  nnesq 6543  sqrlem1 6554  sqrlem2 6555  sqrlem3 6556  sqrlem6 6559  sqrlem8 6561  sqrlem9 6562  sqrlem10 6563  sqrlem11 6564  sqrlem16 6569  sqrlem19 6572  sqrlem20 6573  sqrlem21 6574  sqrlem22 6575  sqr1 6597  sqr2gt1lt2 6600  inelr 6616  nthruz 6628  absexpt 6754  abs1m 6792  caubnd 6814  faclbnd3 6835  faclbnd4lem1 6836  bcpasc 6858  climmullem1 7007  climmullem2 7008  climmullem3 7009  climmullem4 7010  fnsmnt 7112  expcnvlem2 7114  expcnvlem5 7117  geolim 7123  geolim1 7125  georeclim 7126  geoisumr 7129  mulc1cncf 7165  efcltlem1 7197  ef01tlub 7278  absef01tlub 7280  eirrlem4 7284  efgt0 7296  eflegeolem2 7305  eflegeot 7307  efm1legeot 7309  efcnlem4 7313  reeff1olem1 7315  reeff1olem1OLD 7317  sinbndt 7358  cosbndt 7359  cos1bnd 7367  sin01gt0 7369  sincos1sgn 7372  blex 7737  opnm 7748  tgioolem 7801  dscmet 7804  caun0 7828  nvm1 8168  nvmtri 8175  nv1 8180  sm1cnilem 8216  nmosetn0 8295  nmo0 8318  blocnilem 8330  minveclem25 8435  sinhalfpilem 8511  efifolem1 8550  efifolem5 8554  efifolem7 8556  circgrpOLD 8571  log1 8601  log1OLD 8620  iintlem2 8827  normlem7tALT 9134  norm-ii 9153  normsub 9157  norm1t 9272  projlem2 9317  projlem6 9321  projlem28 9343  nmopsetn0 9923  nmfnsetn0 9936  nmopge0t 9965  nmfnge0t 9981  0cnop 10033  0cnfn 10034  nmop0 10040  nmfn0 10041  nmcopexlem2 10081  nmcopexlem5 10084  nmcfnexlem2 10110  nmcfnexlem5 10113  hstle1t 10277  strlem1 10301  strlem3a 10303  strlem5 10306  jplem1 10319

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-nel 1564  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-f1 3158  df-fo 3159  df-f1o 3160  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-en 4305  df-dom 4306  df-sdom 4307  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-1p 5010  df-plp 5011  df-mp 5012  df-ltp 5013  df-plpr 5087  df-mpr 5088  df-enr 5089  df-nr 5090  df-plr 5091  df-mr 5092  df-ltr 5093  df-0r 5094  df-1r 5095  df-m1r 5096  df-c 5163  df-0 5164  df-1 5165  df-i 5166  df-r 5167  df-plus 5168  df-mul 5169  df-lt 5170  df-sub 5279  df-neg 5281  df-pnf 5410  df-mnf 5411  df-xr 5412  df-ltxr 5413  df-le 5414

Copyright terms: Public domain