Theorem 1re 5587

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 5421, 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 5422	. . . 4 |- i e. CC
2		axcnre 5438	. . . 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 1632	. . . . . . . . 9 |- (z = x -> (z =/= 0 <-> x =/= 0))
5	4	rcla4ev 1922	. . . . . . . 8 |- ((x e. RR /\ x =/= 0) -> E.z e. RR z =/= 0)
6	5	adantlr 393	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ x =/= 0) -> E.z e. RR z =/= 0)
7		neeq1 1632	. . . . . . . . 9 |- (z = y -> (z =/= 0 <-> y =/= 0))
8	7	rcla4ev 1922	. . . . . . . 8 |- ((y e. RR /\ y =/= 0) -> E.z e. RR z =/= 0)
9	8	adantll 392	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ y =/= 0) -> E.z e. RR z =/= 0)
10	6, 9	jaodan 426	. . . . . 6 |- (((x e. RR /\ y e. RR) /\ (x =/= 0 \/ y =/= 0)) -> E.z e. RR z =/= 0)
11	10	ex 371	. . . . 5 |- ((x e. RR /\ y e. RR) -> ((x =/= 0 \/ y =/= 0) -> E.z e. RR z =/= 0))
12		ine0 5586	. . . . . . 7 |- i =/= 0
13		neeq1 1632	. . . . . . 7 |- (i = (x + (i x. y)) -> (i =/= 0 <-> (x + (i x. y)) =/= 0))
14	12, 13	mpbii 191	. . . . . 6 |- (i = (x + (i x. y)) -> (x + (i x. y)) =/= 0)
15		ioran 304	. . . . . . . . 9 |- (-. (x =/= 0 \/ y =/= 0) <-> (-. x =/= 0 /\ -. y =/= 0))
16		nne 1631	. . . . . . . . . 10 |- (-. x =/= 0 <-> x = 0)
17		nne 1631	. . . . . . . . . 10 |- (-. y =/= 0 <-> y = 0)
18	16, 17	anbi12i 484	. . . . . . . . 9 |- ((-. x =/= 0 /\ -. y =/= 0) <-> (x = 0 /\ y = 0))
19	15, 18	bitri 171	. . . . . . . 8 |- (-. (x =/= 0 \/ y =/= 0) <-> (x = 0 /\ y = 0))
20		opreq12 4026	. . . . . . . . . 10 |- ((x = 0 /\ (i x. y) = 0) -> (x + (i x. y)) = (0 + 0))
21		opreq2 4025	. . . . . . . . . . 11 |- (y = 0 -> (i x. y) = (i x. 0))
22	1	mul01i 5583	. . . . . . . . . . 11 |- (i x. 0) = 0
23	21, 22	syl6eq 1565	. . . . . . . . . 10 |- (y = 0 -> (i x. y) = 0)
24	20, 23	sylan2 453	. . . . . . . . 9 |- ((x = 0 /\ y = 0) -> (x + (i x. y)) = (0 + 0))
25		0cn 5480	. . . . . . . . . 10 |- 0 e. CC
26	25	addid1i 5482	. . . . . . . . 9 |- (0 + 0) = 0
27	24, 26	syl6eq 1565	. . . . . . . 8 |- ((x = 0 /\ y = 0) -> (x + (i x. y)) = 0)
28	19, 27	sylbi 197	. . . . . . 7 |- (-. (x =/= 0 \/ y =/= 0) -> (x + (i x. y)) = 0)
29	28	necon1ai 1650	. . . . . 6 |- ((x + (i x. y)) =/= 0 -> (x =/= 0 \/ y =/= 0))
30	14, 29	syl 10	. . . . 5 |- (i = (x + (i x. y)) -> (x =/= 0 \/ y =/= 0))
31	11, 30	syl5 21	. . . 4 |- ((x e. RR /\ y e. RR) -> (i = (x + (i x. y)) -> E.z e. RR z =/= 0))
32	31	r19.23aivv 1793	. . 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 5436	. . . 4 |- ((z e. RR /\ z =/= 0) -> E.x e. RR (z x. x) = 1)
35		eleq1 1576	. . . . . . 7 |- ((z x. x) = 1 -> ((z x. x) e. RR <-> 1 e. RR))
36		remulcl 5456	. . . . . . 7 |- ((z e. RR /\ x e. RR) -> (z x. x) e. RR)
37	35, 36	syl5cbi 207	. . . . . 6 |- ((z e. RR /\ x e. RR) -> ((z x. x) = 1 -> 1 e. RR))
38	37	r19.23adva 1792	. . . . 5 |- (z e. RR -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
39	38	adantr 389	. . . 4 |- ((z e. RR /\ z =/= 0) -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
40	34, 39	mpd 26	. . 3 |- ((z e. RR /\ z =/= 0) -> 1 e. RR)
41	40	r19.23aiva 1789	. 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 220   /\ wa 221   = wceq 991   e. wcel 993   =/= wne 1627  E.wrex 1691  (class class class)co 4019  CCcc 5384  RRcr 5385  0cc0 5386  1c1 5387  ici 5388   + caddc 5389   x. cmul 5391

This theorem is referenced by:  peano2re 5588  renegcl 5589  0reALT 5593  peano2rem 5594  lt01 5834  redivclzi 5937  rereccli 5939  rerecclzi 5940  rereccl 5941  eqnegi 5942  ltp1 5949  recgt0ii 5952  ltm1 5953  prodgt0i 5957  ltmul1i 5960  ltdiv1i 5962  mulgt1 5987  ltmulgt11 5988  lemulge11 5990  recgt0 6003  ltreci 6022  reclt1 6041  recgt1 6042  recgt1i 6043  recp1lt1 6044  recreclt 6045  halfposi 6047  ledivp1i 6049  ltdivp1i 6050  posexi 6051  nnssre 6070  nnge1 6086  nngt1ne1 6087  nnle1eq1 6088  nngt0 6089  lt1nnn 6090  nnrecre 6096  nnrecgt0 6097  nnleltp1 6098  nnltp1le 6099  nnsubi 6100  nnaddm1cl 6102  2re 6123  3re 6125  4re 6126  5re 6127  6re 6128  7re 6129  8re 6130  9re 6131  10re 6132  2pos 6133  3pos 6135  4pos 6136  5pos 6137  6pos 6138  7pos 6139  8pos 6140  9pos 6141  10pos 6142  1lt2 6172  halflt1 6174  1rp 6192  nnunb 6236  nnrecl 6238  xrub 6246  lt0nnn0 6282  nn0ltp1le 6293  nn0leltp1 6294  nn0ltlem1 6295  elnnz1 6321  znnnlt1 6322  elnn0nn 6337  zltp1le 6347  zleltp1 6348  recnz 6360  gtndiv 6362  nneoi 6366  dfuzi 6371  uzindOLD 6377  nn0ind-raph 6383  zbtwnre 6391  rebtwnz 6392  qbtwnre 6416  qbtwnxr 6417  fraclt1 6427  flbi2 6438  fldiv 6454  modid 6469  monoord 6480  eluzp1m1 6558  eluzp1p1 6560  cardfz 6669  seq1lem2 6673  reexpcl 6773  expge0 6783  expge1 6785  expordi 6795  expwordi 6798  expword2i 6800  expmwordi 6801  exple1 6802  bernneq 6847  bernneqOLD 6848  bernneq2 6849  expnbnd 6850  expnlbnd 6851  expnlbnd2 6852  discrlem2 6856  discrlem3 6857  nnlesqi 6860  nnesqi 6861  sqrlem1 6872  sqrlem2 6873  sqrlem3 6874  sqrlem6 6877  sqrlem8 6879  sqrlem9 6880  sqrlem10 6881  sqrlem11 6882  sqrlem16 6887  sqrlem19 6890  sqrlem20 6891  sqrlem21 6892  sqrlem22 6893  sqrthi 6898  sqrcli 6899  sqrgt0i 6900  sqr1 6915  sqr2gt1lt2 6918  sqr2irrlem1 6923  inelr 6934  nthruz 6945  cjexp 7016  re1 7021  im1 7022  rei 7023  imi 7024  absexp 7068  abs1mi 7105  seq1bndi 7111  caubndi 7127  facwordi 7145  faclbnd3 7148  faclbnd4lem1 7149  faclbnd4lem4 7152  facavg 7156  bcnp11 7166  bcnp1n 7167  bcpasc2i 7168  bcpasc2 7169  bcpasci 7170  bccl2 7172  climmullem1 7321  climmullem2 7322  climmullem3 7323  climmullem4 7324  climmullem5 7325  serzf0i 7370  arisumi 7428  expcnvlem1 7429  expcnvlem2 7430  expcnvlem4 7432  expcnvlem5 7433  geolimilem 7438  geolim1i 7441  georeclim 7443  geoisumr 7446  geoisum1c 7448  0.999... 7449  efcltlem1 7507  erelem7 7528  ele3lem 7529  ege2lem2 7531  ege2le3lem2 7532  ere 7533  efaddlem1 7541  efaddlem2 7542  efaddlem7 7547  efaddlem8 7548  efaddlem10 7550  efaddlem12 7552  efaddlem13 7553  efaddlem15 7555  efaddlem20 7560  ef01tllem2 7587  ef01tllem2OLD 7588  ef01tlubi 7589  absef01tlubi 7591  eirrlem1 7592  eirrlem3 7594  eirrlem4 7595  abspef01tlubi 7601  efgt1i 7609  efgt0i 7610  eflti 7612  eflegeolem2 7620  efm1legeoi 7623  efcnlem1 7625  efcnlem2 7626  efcnlem4 7628  reeff1olem1 7630  reeff1o 7632  resin4p 7642  recos4p 7643  sinbnd 7672  cosbnd 7673  sin01bndlem2 7675  sin01bndlem3 7676  cos01bndlem2 7677  cos01bndlem3 7678  cos1bnd 7681  cos2bnd 7682  sin01gt0 7683  cos01gt0 7684  sin02gt0 7685  sincos1sgn 7686  efieq1re 7692  infpn2 7719  ruclem8 7727  ruclem13 7732  ruclem25 7744  blex 8057  opnm 8068  tgioolem 8123  dscmet 8127  lmnn 8144  caun0 8154  bcthlem16 8223  bcthlem18 8225  nvm1 8533  nvmtri 8540  nv1 8545  sm1cnilem 8595  ipid 8611  nmosetn0 8676  nmoub3i 8684  nmo0 8700  nmlno0lem 8702  blocnilem 8713  ipasslem10 8749  minveclem25 8823  htthlem6 8881  sinhalfpilem 8940  sinperlem1 8947  sincos4thpi 8972  sincos6thpi 8973  coskpi 8976  sineq0 8977  sineq0OLD 8978  sineq0re 8979  efifolem1 8988  efifolem3 8990  efifolem4 8991  efifolem5 8992  efifolem6 8993  efifolem7 8994  loge 9033  hisubcomi 9240  normlem9 9254  normlem7tALT 9255  norm-ii.i 9274  normsubi 9278  bcs2 9319  norm1 9391  projlem1 9456  projlem2 9457  projlem4 9459  projlem6 9461  projlem28 9483  projlem29 9484  nmopsetn0 10066  nmfnsetn0 10079  nmopub2tALT 10107  nmopge0 10109  nmfnleub2 10124  nmfnge0 10125  0cnop 10176  0cnfn 10177  nmop0 10183  nmfn0 10184  nmlnop0iALT 10193  nmopun 10212  unopbd 10213  hmopd 10220  nmcopexlem2 10225  nmcopexlem5 10228  nmcfnexlem2 10254  nmcfnexlem5 10257  nmopadjlem 10295  nmopcoi 10301  nmopcoadji 10307  branmfn 10311  branmfnOLD 10312  pjnmopi 10349  pjbdlni 10350  hstle1 10428  hstle 10432  hstles 10433  stge1i 10440  stlesi 10443  staddi 10448  stadd3i 10450  strlem1 10452  strlem3a 10454  strlem5 10457  strlem6 10458  hstrlem6 10466  jplem1 10470  cdj1i 10636  altretop 11110  rddif 11762  absrdbnd 11763  incsequz 11772  fsumltisumi 11779  mettrifi 11805  geomcau 11807  iiuni 11826  dfii2 11827  iirev 11828  iihalf1 11829  iihalf2 11830  iimulcl 11831  lincmb01cmp 11835  lincmb01icc 11836  totbndbnd 11893  heiborlem30 11933  heiborlem31 11934  heiborlem32 11935  heiborlem33 11936  heiborlem35 11938  bfplem9 11955  rrntotbndlem1 11969  rrntotbndlem2 11970  rrntotbnd 11971  iccbnd 11975  iicmp 11977  phtpyid 11984  phtpycom 11985  phtpycolem1 11986  phtpycolem2 11987  phtpycolem3 11988  phtpycolem4 11989  phtpycolem5 11990  phtpyco 11991

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 997  ax-gen 998  ax-8 999  ax-9 1000  ax-10 1001  ax-11 1002  ax-12 1003  ax-13 1004  ax-14 1005  ax-17 1006  ax-4 1008  ax-5o 1010  ax-6o 1013  ax-9o 1158  ax-10o 1176  ax-16 1246  ax-11o 1254  ax-ext 1499  ax-rep 2766  ax-sep 2776  ax-nul 2783  ax-pow 2817  ax-pr 2854  ax-un 3088  ax-inf2 4768

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 781  df-3an 782  df-ex 1016  df-sb 1208  df-eu 1420  df-mo 1421  df-clab 1505  df-cleq 1510  df-clel 1513  df-ne 1629  df-ral 1694  df-rex 1695  df-reu 1696  df-rab 1697  df-v 1857  df-sbc 1986  df-csb 2051  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2415  df-pw 2458  df-sn 2469  df-pr 2470  df-tp 2472  df-op 2473  df-uni 2569  df-int 2600  df-iun 2634  df-br 2692  df-opab 2740  df-tr 2754  df-eprel 2909  df-id 2912  df-po 2917  df-so 2928  df-fr 2946  df-we 2961  df-ord 2977  df-on 2978  df-lim 2979  df-suc 2980  df-om 3218  df-xp 3264  df-rel 3265  df-cnv 3266  df-co 3267  df-dm 3268  df-rn 3269  df-res 3270  df-ima 3271  df-fun 3272  df-fn 3273  df-f 3274  df-fv 3278  df-opr 4021  df-oprab 4022  df-1st 4138  df-2nd 4139  df-rdg 4231  df-1o 4267  df-oadd 4269  df-omul 4270  df-er 4399  df-ec 4401  df-qs 4404  df-ni 5152  df-pli 5153  df-mi 5154  df-lti 5155  df-plpq 5187  df-mpq 5188  df-enq 5189  df-nq 5190  df-plq 5191  df-mq 5192  df-rq 5193  df-ltq 5194  df-1q 5195  df-np 5238  df-1p 5239  df-plp 5240  df-mp 5241  df-ltp 5242  df-plpr 5316  df-mpr 5317  df-enr 5318  df-nr 5319  df-plr 5320  df-mr 5321  df-ltr 5322  df-0r 5323  df-1r 5324  df-m1r 5325  df-c 5392  df-0 5393  df-1 5394  df-i 5395  df-r 5396  df-plus 5397  df-mul 5398  df-sub 5508  df-neg 5510

Copyright terms: Public domain