Theorem 1re 6394

Description: 1 is a real number. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax1cn 6218, by exploiting properties of the imaginary unit _i. (Contributed by Eric Schmidt, 11-Apr-2007.)

Assertion

Ref	Expression
1re	|- 1 e. RR

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		axicn 6219	. . . 4 |- _i e. CC
2		axcnre 6235	. . . 4 |- (_i e. CC -> E.x e. RR E.y e. RR _i = (x + (_i x. y)))
3	1, 2	ax-mp 7	. . 3 |- E.x e. RR E.y e. RR _i = (x + (_i x. y))
4		neeq1 1859	. . . . . . . . 9 |- (z = x -> (z =/= 0 <-> x =/= 0))
5	4	rcla4ev 2214	. . . . . . . 8 |- ((x e. RR /\ x =/= 0) -> E.z e. RR z =/= 0)
6	5	adantlr 427	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ x =/= 0) -> E.z e. RR z =/= 0)
7		neeq1 1859	. . . . . . . . 9 |- (z = y -> (z =/= 0 <-> y =/= 0))
8	7	rcla4ev 2214	. . . . . . . 8 |- ((y e. RR /\ y =/= 0) -> E.z e. RR z =/= 0)
9	8	adantll 426	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ y =/= 0) -> E.z e. RR z =/= 0)
10	6, 9	jaodan 469	. . . . . 6 |- (((x e. RR /\ y e. RR) /\ (x =/= 0 \/ y =/= 0)) -> E.z e. RR z =/= 0)
11	10	ex 400	. . . . 5 |- ((x e. RR /\ y e. RR) -> ((x =/= 0 \/ y =/= 0) -> E.z e. RR z =/= 0))
12		ine0 6393	. . . . . . 7 |- _i =/= 0
13		neeq1 1859	. . . . . . 7 |- (_i = (x + (_i x. y)) -> (_i =/= 0 <-> (x + (_i x. y)) =/= 0))
14	12, 13	mpbii 209	. . . . . 6 |- (_i = (x + (_i x. y)) -> (x + (_i x. y)) =/= 0)
15		ioran 329	. . . . . . . . 9 |- (-. (x =/= 0 \/ y =/= 0) <-> (-. x =/= 0 /\ -. y =/= 0))
16		nne 1858	. . . . . . . . . 10 |- (-. x =/= 0 <-> x = 0)
17		nne 1858	. . . . . . . . . 10 |- (-. y =/= 0 <-> y = 0)
18	16, 17	anbi12i 537	. . . . . . . . 9 |- ((-. x =/= 0 /\ -. y =/= 0) <-> (x = 0 /\ y = 0))
19	15, 18	bitri 189	. . . . . . . 8 |- (-. (x =/= 0 \/ y =/= 0) <-> (x = 0 /\ y = 0))
20		opreq12 4702	. . . . . . . . . 10 |- ((x = 0 /\ (_i x. y) = 0) -> (x + (_i x. y)) = (0 + 0))
21		opreq2 4701	. . . . . . . . . . 11 |- (y = 0 -> (_i x. y) = (_i x. 0))
22	1	mul01i 6390	. . . . . . . . . . 11 |- (_i x. 0) = 0
23	21, 22	syl6eq 1781	. . . . . . . . . 10 |- (y = 0 -> (_i x. y) = 0)
24	20, 23	sylan2 498	. . . . . . . . 9 |- ((x = 0 /\ y = 0) -> (x + (_i x. y)) = (0 + 0))
25		0cn 6277	. . . . . . . . . 10 |- 0 e. CC
26	25	addid1i 6279	. . . . . . . . 9 |- (0 + 0) = 0
27	24, 26	syl6eq 1781	. . . . . . . 8 |- ((x = 0 /\ y = 0) -> (x + (_i x. y)) = 0)
28	19, 27	sylbi 215	. . . . . . 7 |- (-. (x =/= 0 \/ y =/= 0) -> (x + (_i x. y)) = 0)
29	28	necon1ai 1882	. . . . . 6 |- ((x + (_i x. y)) =/= 0 -> (x =/= 0 \/ y =/= 0))
30	14, 29	syl 12	. . . . 5 |- (_i = (x + (_i x. y)) -> (x =/= 0 \/ y =/= 0))
31	11, 30	syl5 20	. . . 4 |- ((x e. RR /\ y e. RR) -> (_i = (x + (_i x. y)) -> E.z e. RR z =/= 0))
32	31	r19.23aivv 2051	. . 3 |- (E.x e. RR E.y e. RR _i = (x + (_i x. y)) -> E.z e. RR z =/= 0)
33	3, 32	ax-mp 7	. 2 |- E.z e. RR z =/= 0
34		axrrecex 6233	. . . 4 |- ((z e. RR /\ z =/= 0) -> E.x e. RR (z x. x) = 1)
35		eleq1 1794	. . . . . . 7 |- ((z x. x) = 1 -> ((z x. x) e. RR <-> 1 e. RR))
36		remulcl 6253	. . . . . . 7 |- ((z e. RR /\ x e. RR) -> (z x. x) e. RR)
37	35, 36	syl5cbi 225	. . . . . 6 |- ((z e. RR /\ x e. RR) -> ((z x. x) = 1 -> 1 e. RR))
38	37	r19.23adva 2050	. . . . 5 |- (z e. RR -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
39	38	adantr 423	. . . 4 |- ((z e. RR /\ z =/= 0) -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
40	34, 39	mpd 29	. . 3 |- ((z e. RR /\ z =/= 0) -> 1 e. RR)
41	40	r19.23aiva 2046	. 2 |- (E.z e. RR z =/= 0 -> 1 e. RR)
42	33, 41	ax-mp 7	1 |- 1 e. RR

Syntax hints:  -. wn 2   -> wi 3   \/ wo 238   /\ wa 239   = wceq 1136   e. wcel 1138   =/= wne 1854  E.wrex 1940  (class class class)co 4695  CCcc 6180  RRcr 6181  0cc0 6182  1c1 6183  _ici 6184   + caddc 6185   x. cmul 6187

This theorem is referenced by:  peano2re 6395  renegcl 6396  0reALT 6400  peano2rem 6401  lt01 6667  redivclzi 6772  rereccli 6774  rerecclzi 6775  rereccl 6776  eqnegi 6777  ltp1 6784  recgt0ii 6787  ltm1 6788  prodgt0i 6792  ltmul1i 6795  ltdiv1i 6797  mulgt1 6822  ltmulgt11 6823  lemulge11 6825  recgt0 6838  ltreci 6857  reclt1 6876  recgt1 6877  recgt1i 6878  recp1lt1 6879  recreclt 6880  halfposi 6882  ledivp1i 6884  ltdivp1i 6885  posexi 6886  nnssre 6905  nnge1 6921  nngt1ne1 6922  nnle1eq1 6923  nngt0 6924  lt1nnn 6925  nnrecre 6931  nnrecgt0 6932  nnleltp1 6933  nnltp1le 6934  nnsubi 6935  nnaddm1cl 6937  2re 6958  3re 6960  4re 6961  5re 6962  6re 6963  7re 6964  8re 6965  9re 6966  10re 6967  2pos 6968  3pos 6970  4pos 6971  5pos 6972  6pos 6973  7pos 6974  8pos 6975  9pos 6976  10pos 6977  1lt2 7007  1lt3 7009  halflt1 7011  addltmul 7024  1rp 7030  nnunb 7074  nnrecl 7076  xrub 7084  lt0nnn0 7120  nn0ltp1le 7131  nn0leltp1 7132  nn0ltlem1 7133  elnnz1 7159  znnnlt1 7160  elnn0nn 7175  zltp1le 7185  zleltp1 7186  recnz 7198  gtndiv 7200  nneoi 7204  dfuzi 7209  uzindOLD 7215  nn0ind-raph 7221  zbtwnre 7229  rebtwnz 7230  qbtwnre 7254  qbtwnxr 7255  fraclt1 7265  flbi2 7276  fldiv 7292  modid 7307  monoord 7318  eluzp1m1 7397  eluzp1p1 7399  fzprval 7482  fztpval 7483  cardfz 7514  seq1lem2 7518  reexpcl 7618  expge0 7628  expge1 7630  expordi 7640  expwordi 7643  expword2i 7645  expmwordi 7646  exple1 7647  bernneq 7693  bernneqOLD 7694  bernneq2 7695  expnbnd 7696  expnlbnd 7697  expnlbnd2 7698  discrlem2 7702  discrlem3 7703  nnlesqi 7706  nnesqi 7707  sqrlem1 7718  sqrlem2 7719  sqrlem3 7720  sqrlem6 7723  sqrlem8 7725  sqrlem9 7726  sqrlem10 7727  sqrlem11 7728  sqrlem16 7733  sqrlem19 7736  sqrlem20 7737  sqrlem21 7738  sqrlem22 7739  sqrthi 7744  sqrcli 7745  sqrgt0i 7746  sqr1 7761  sqr2gt1lt2 7764  sqr2irrlem1 7769  inelr 7780  nthruz 7791  cjexp 7862  re1 7867  im1 7868  rei 7869  imi 7870  absexp 7914  abs1mi 7951  seq1bndi 7957  caubndi 7973  facwordi 7991  faclbnd3 7994  faclbnd4lem1 7995  faclbnd4lem4 7998  facavg 8002  bcnp11 8012  bcnp1n 8013  bcpasc2i 8014  bcpasc2 8015  bcpasci 8016  bccl2 8018  climmullem1 8175  climmullem2 8176  climmullem3 8177  climmullem4 8178  climmullem5 8179  serzf0i 8224  arisumi 8282  expcnvlem1 8283  expcnvlem2 8284  expcnvlem4 8286  expcnvlem5 8287  geolimilem 8292  geolim1i 8295  georeclim 8297  geoisumr 8300  geoisum1c 8302  0.999... 8303  efcltlem1 8361  erelem7 8382  ele3lem 8383  ege2lem2 8385  ege2le3lem2 8386  ere 8387  efaddlem1 8395  efaddlem2 8396  efaddlem7 8401  efaddlem8 8402  efaddlem10 8404  efaddlem12 8406  efaddlem13 8407  efaddlem15 8409  efaddlem20 8414  ef01tllem2 8441  ef01tllem2OLD 8442  ef01tlubi 8443  absef01tlubi 8445  eirrlem1 8446  eirrlem3 8448  eirrlem4 8449  abspef01tlubi 8455  efgt1i 8463  efgt0i 8464  eflti 8466  eflegeolem2 8474  efm1legeoi 8477  efcnlem1 8479  efcnlem2 8480  efcnlem4 8482  reeff1olem1 8484  reeff1o 8486  resin4p 8496  recos4p 8497  sinbnd 8526  cosbnd 8527  sin01bndlem2 8529  sin01bndlem3 8530  cos01bndlem2 8531  cos01bndlem3 8532  cos1bnd 8535  cos2bnd 8536  sin01gt0 8537  cos01gt0 8538  sin02gt0 8539  sincos1sgn 8540  efieq1re 8546  infpn2 8573  ruclem8 8581  ruclem13 8586  ruclem25 8598  blex 8921  opnm 8932  tgioolem 8987  dscmet 8991  lmnn 9008  caun0 9018  bcthlem16 9087  bcthlem18 9089  nvm1 9419  nvmtri 9426  nv1 9431  sm1cnilem 9481  ipid 9497  nmosetn0 9562  nmoub3i 9570  nmo0 9586  nmlno0lem 9588  blocnilem 9599  ipasslem10 9635  minveclem25 9709  htthlem6 9767  sinhalfpilem 9823  sinperlem1 9830  sincos4thpi 9855  sincos6thpi 9856  coskpi 9859  sineq0 9860  sineq0OLD 9861  sineq0re 9862  efifolem1 9871  efifolem3 9873  efifolem4 9874  efifolem5 9875  efifolem6 9876  efifolem7 9877  loge 9916  hisubcomi 10395  normlem9 10409  normlem7tALT 10410  norm-ii.i 10429  normsubi 10433  bcs2 10474  norm1 10546  projlem1 10611  projlem2 10612  projlem4 10614  projlem6 10616  projlem28 10638  projlem29 10639  nmopsetn0 11221  nmfnsetn0 11234  nmopub2tALT 11262  nmopge0 11264  nmfnleub2 11279  nmfnge0 11280  0cnop 11332  0cnfn 11333  nmop0 11339  nmfn0 11340  nmlnop0iALT 11349  nmopun 11368  unopbd 11369  hmopd 11376  nmcopexlem2 11381  nmcopexlem5 11384  nmcfnexlem2 11410  nmcfnexlem5 11413  nmopadjlem 11451  nmopcoi 11457  nmopcoadji 11463  branmfn 11467  branmfnOLD 11468  pjnmopi 11511  pjbdlni 11512  hstle1 11590  hstle 11594  hstles 11595  stge1i 11602  stlesi 11605  staddi 11610  stadd3i 11612  strlem1 11614  strlem3a 11616  strlem5 11619  strlem6 11620  hstrlem6 11628  jplem1 11632  cdj1i 11797  addltmulALT 11810  fseq1cl 13411  mulgcdlem3 13550  1nprm 13561  zgt1b1 13563  isprm3 13568  coprm 13574  seqzp2 14439  altretop 14707  cntrsetlem 14709  fz10 15470  rddif 15480  absrdbnd 15481  fdc 15494  incsequz 15497  fsumltisumi 15505  mettrifi 15529  geomcau 15531  iiuni 15550  dfii2 15551  dfii3 15552  iirev 15553  iihalf1 15554  iihalf2 15555  iimulcl 15556  lincmb01cmp 15560  lincmb01icc 15561  totbndbnd 15626  heiborlem30 15666  heiborlem31 15667  heiborlem32 15668  heiborlem33 15669  heiborlem35 15671  bfplem9 15688  rrntotbndlem1 15702  rrntotbndlem2 15703  rrntotbnd 15704  iccbnd 15708  iicmp 15710  phtpyid 15731  phtpycom 15732  phtpycolem1 15733  phtpycolem2 15734  phtpycolem3 15735  phtpycolem4 15736  phtpycolem5 15737  phtpyco 15738  reparphtlem2 15746  reparpht 15747  pcoval1 15756  pcoval2 15757  pcocn 15758  pco1 15760  pcohtpylem1 15762  pcohtpylem2 15763  pcohtpylem3 15764  pcohtpy 15765  pcopt 15766  pcoass 15767  pcorevlem 15768  pcorev 15769  pi1gp 15777  stb2val1 16494  stb2val2 16495  stb3val1 16498  stb3val2 16499  stb3val3 16500  stb2xpl 16501  stb3xpl 16502  divrngmclNEW 16893  invrcl 16900

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-rep 3243  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601  ax-inf2 5540

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3or 856  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-sbc 2287  df-csb 2374  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-int 3037  df-iun 3079  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-opr 4697  df-oprab 4698  df-mpt 4817  df-1st 4831  df-2nd 4832  df-iota 4900  df-rdg 4951  df-1o 4988  df-oadd 4990  df-omul 4991  df-er 5129  df-ec 5131  df-qs 5134  df-en 5238  df-dom 5239  df-sdom 5240  df-undef 5367  df-riota 5371  df-ni 5948  df-pli 5949  df-mi 5950  df-lti 5951  df-plpq 5983  df-mpq 5984  df-enq 5985  df-nq 5986  df-plq 5987  df-mq 5988  df-rq 5989  df-ltq 5990  df-1q 5991  df-np 6034  df-1p 6035  df-plp 6036  df-mp 6037  df-ltp 6038  df-plpr 6112  df-mpr 6113  df-enr 6114  df-nr 6115  df-plr 6116  df-mr 6117  df-ltr 6118  df-0r 6119  df-1r 6120  df-m1r 6121  df-c 6188  df-0 6189  df-1 6190  df-i 6191  df-r 6192  df-plus 6193  df-mul 6194  df-sub 6307  df-neg 6309

Copyright terms: Public domain