Theorem 1re 5500

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 5334, 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 5335	. . . 4 |- i e. CC
2		axcnre 5351	. . . 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 1637	. . . . . . . . 9 |- (z = x -> (z =/= 0 <-> x =/= 0))
5	4	rcla4ev 1924	. . . . . . . 8 |- ((x e. RR /\ x =/= 0) -> E.z e. RR z =/= 0)
6	5	adantlr 402	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ x =/= 0) -> E.z e. RR z =/= 0)
7		neeq1 1637	. . . . . . . . 9 |- (z = y -> (z =/= 0 <-> y =/= 0))
8	7	rcla4ev 1924	. . . . . . . 8 |- ((y e. RR /\ y =/= 0) -> E.z e. RR z =/= 0)
9	8	adantll 401	. . . . . . 7 |- (((x e. RR /\ y e. RR) /\ y =/= 0) -> E.z e. RR z =/= 0)
10	6, 9	jaodan 435	. . . . . 6 |- (((x e. RR /\ y e. RR) /\ (x =/= 0 \/ y =/= 0)) -> E.z e. RR z =/= 0)
11	10	ex 380	. . . . 5 |- ((x e. RR /\ y e. RR) -> ((x =/= 0 \/ y =/= 0) -> E.z e. RR z =/= 0))
12		ine0 5499	. . . . . . 7 |- i =/= 0
13		neeq1 1637	. . . . . . 7 |- (i = (x + (i x. y)) -> (i =/= 0 <-> (x + (i x. y)) =/= 0))
14	12, 13	mpbii 200	. . . . . 6 |- (i = (x + (i x. y)) -> (x + (i x. y)) =/= 0)
15		ioran 313	. . . . . . . . 9 |- (-. (x =/= 0 \/ y =/= 0) <-> (-. x =/= 0 /\ -. y =/= 0))
16		nne 1636	. . . . . . . . . 10 |- (-. x =/= 0 <-> x = 0)
17		nne 1636	. . . . . . . . . 10 |- (-. y =/= 0 <-> y = 0)
18	16, 17	anbi12i 493	. . . . . . . . 9 |- ((-. x =/= 0 /\ -. y =/= 0) <-> (x = 0 /\ y = 0))
19	15, 18	bitri 180	. . . . . . . 8 |- (-. (x =/= 0 \/ y =/= 0) <-> (x = 0 /\ y = 0))
20		opreq12 4028	. . . . . . . . . 10 |- ((x = 0 /\ (i x. y) = 0) -> (x + (i x. y)) = (0 + 0))
21		opreq2 4027	. . . . . . . . . . 11 |- (y = 0 -> (i x. y) = (i x. 0))
22	1	mul01i 5496	. . . . . . . . . . 11 |- (i x. 0) = 0
23	21, 22	syl6eq 1570	. . . . . . . . . 10 |- (y = 0 -> (i x. y) = 0)
24	20, 23	sylan2 462	. . . . . . . . 9 |- ((x = 0 /\ y = 0) -> (x + (i x. y)) = (0 + 0))
25		0cn 5393	. . . . . . . . . 10 |- 0 e. CC
26	25	addid1i 5395	. . . . . . . . 9 |- (0 + 0) = 0
27	24, 26	syl6eq 1570	. . . . . . . 8 |- ((x = 0 /\ y = 0) -> (x + (i x. y)) = 0)
28	19, 27	sylbi 206	. . . . . . 7 |- (-. (x =/= 0 \/ y =/= 0) -> (x + (i x. y)) = 0)
29	28	necon1ai 1655	. . . . . 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 1795	. . 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 5349	. . . 4 |- ((z e. RR /\ z =/= 0) -> E.x e. RR (z x. x) = 1)
35		eleq1 1581	. . . . . . 7 |- ((z x. x) = 1 -> ((z x. x) e. RR <-> 1 e. RR))
36		remulcl 5369	. . . . . . 7 |- ((z e. RR /\ x e. RR) -> (z x. x) e. RR)
37	35, 36	syl5cbi 216	. . . . . 6 |- ((z e. RR /\ x e. RR) -> ((z x. x) = 1 -> 1 e. RR))
38	37	r19.23adva 1794	. . . . 5 |- (z e. RR -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
39	38	adantr 398	. . . 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 1791	. 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 229   /\ wa 230   = wceq 997   e. wcel 999   =/= wne 1632  E.wrex 1693  (class class class)co 4021  CCcc 5297  RRcr 5298  0cc0 5299  1c1 5300  ici 5301   + caddc 5302   x. cmul 5304

This theorem is referenced by:  peano2re 5501  renegcl 5502  0reALT 5506  peano2rem 5507  lt01 5745  redivclzi 5857  rereccli 5859  rerecclzi 5860  rereccl 5861  eqnegi 5862  ltp1 5869  recgt0ii 5872  ltm1 5873  prodgt0i 5877  ltmul1i 5880  ltdiv1i 5882  mulgt1 5903  ltmulgt11 5904  lemulge11 5906  recgt0 5919  ltreci 5939  reclt1 5958  recgt1 5959  recgt1i 5960  recp1lt1 5961  recreclt 5962  halfposi 5964  ledivp1i 5966  ltdivp1i 5967  posexi 5968  nnssre 5987  nnge1 6003  nngt1ne1 6004  nnle1eq1 6005  nngt0 6006  lt1nnn 6007  nnrecre 6013  nnrecgt0 6014  nnleltp1 6015  nnltp1le 6016  nnsubi 6017  nnaddm1cl 6019  2re 6040  3re 6042  4re 6043  5re 6044  6re 6045  7re 6046  8re 6047  9re 6048  10re 6049  2pos 6050  3pos 6052  4pos 6053  5pos 6054  6pos 6055  7pos 6056  8pos 6057  9pos 6058  10pos 6059  1lt2 6089  halflt1 6091  1rp 6109  nnunb 6152  nnrecl 6154  xrub 6162  lt0nnn0 6198  nn0ltp1le 6209  nn0leltp1 6210  nn0ltlem1 6211  elnnz1 6237  znnnlt1 6238  elnn0nn 6253  zltp1le 6263  zleltp1 6264  recnz 6276  gtndiv 6278  nneoi 6282  dfuzi 6287  uzindOLD 6293  nn0ind-raph 6299  zbtwnre 6306  rebtwnz 6307  qbtwnre 6331  qbtwnxr 6332  fraclt1 6342  flbi2 6353  fldiv 6368  flmodOLD 6375  monoord 6381  eluzp1m1 6459  eluzp1p1 6461  seq1lem2 6569  reexpcl 6669  expge0 6680  expge1 6682  expordi 6689  expwordi 6692  expword2i 6694  expmwordi 6695  exple1 6696  bernneq 6741  bernneq2 6742  expnbnd 6743  expnlbnd 6744  expnlbnd2 6745  discrlem2 6747  discrlem3 6748  nnlesqi 6751  nnesqi 6752  sqrlem1 6763  sqrlem2 6764  sqrlem3 6765  sqrlem6 6768  sqrlem8 6770  sqrlem9 6771  sqrlem10 6772  sqrlem11 6773  sqrlem16 6778  sqrlem19 6781  sqrlem20 6782  sqrlem21 6783  sqrlem22 6784  sqrthi 6789  sqrcli 6790  sqrgt0i 6791  sqr1 6806  sqr2gt1lt2 6809  sqr2irrlem1 6814  inelr 6825  nthruz 6836  cjexp 6907  re1 6912  im1 6913  rei 6914  imi 6915  absexp 6958  abs1mi 6994  seq1bndi 7000  caubndi 7016  facwordi 7034  faclbnd3 7037  faclbnd4lem1 7038  faclbnd4lem4 7041  facavg 7045  bcnp11 7055  bcnp1n 7056  bcpasc2i 7057  bcpasc2 7058  bcpasci 7059  bccl2 7061  climmullem1 7210  climmullem2 7211  climmullem3 7212  climmullem4 7213  climmullem5 7214  serzf0i 7259  ser1f0i 7260  arisumi 7316  expcnvlem1 7317  expcnvlem2 7318  expcnvlem4 7320  expcnvlem5 7321  geolimilem 7325  geolim1i 7328  georeclim 7330  geoisumr 7333  geoisum1c 7335  0.999... 7336  efcltlem1 7394  erelem7 7415  ele3lem 7416  ege2lem2 7418  ege2le3lem2 7419  ere 7420  efaddlem1 7428  efaddlem2 7429  efaddlem7 7434  efaddlem8 7435  efaddlem10 7437  efaddlem12 7439  efaddlem13 7440  efaddlem15 7442  efaddlem20 7447  ef01tllem2 7474  ef01tllem2OLD 7475  ef01tlubi 7476  absef01tlubi 7478  eirrlem1 7479  eirrlem3 7481  eirrlem4 7482  abspef01tlubi 7486  efgt1i 7494  efgt0i 7495  eflti 7497  eflegeolem2 7505  efm1legeoi 7508  efcnlem1 7510  efcnlem2 7511  efcnlem4 7513  reeff1olem1 7515  reeff1o 7517  resin4p 7527  recos4p 7528  sinbnd 7557  cosbnd 7558  sin01bndlem2 7560  sin01bndlem3 7561  cos01bndlem2 7562  cos01bndlem3 7563  cos1bnd 7566  cos2bnd 7567  sin01gt0 7568  cos01gt0 7569  sin02gt0 7570  sincos1sgn 7571  infpn2 7601  ruclem8 7609  ruclem13 7614  ruclem25 7626  blex 7934  opnm 7945  tgioolem 7999  dscmet 8003  lmnn 8020  caun0 8030  bcthlem16 8099  bcthlem18 8101  nvm1 8376  nvmtri 8383  nv1 8388  sm1cnilem 8431  ipid 8447  nmosetn0 8512  nmoub3i 8520  nmo0 8535  nmlno0lem 8537  blocnilem 8548  ipasslem10 8583  minveclem25 8653  htthlem6 8709  sinhalfpilem 8762  sinperlem1 8769  sincos4thpi 8793  sincos6thpi 8794  sineq0 8796  efifolem1 8805  efifolem3 8807  efifolem4 8808  efifolem5 8809  efifolem6 8810  efifolem7 8811  loge 8850  hisubcomi 9053  normlem9 9067  normlem7tALT 9068  norm-ii.i 9087  normsubi 9091  bcs2 9132  norm1 9204  projlem1 9269  projlem2 9270  projlem4 9272  projlem6 9274  projlem28 9296  projlem29 9297  nmopsetn0 9875  nmfnsetn0 9888  nmopub2tALT 9916  nmopge0 9918  nmfnleub2 9933  nmfnge0 9934  0cnop 9986  0cnfn 9987  nmop0 9993  nmfn0 9994  nmlnop0iALT 10003  nmopun 10022  unopbd 10023  hmopd 10030  nmcopexlem2 10035  nmcopexlem5 10038  nmcfnexlem2 10064  nmcfnexlem5 10067  nmopadjlem 10105  nmopcoi 10111  nmopcoadji 10117  branmfn 10121  pjnmopi 10158  pjbdlni 10159  hstle1 10237  hstle 10241  hstles 10242  stge1i 10249  stlesi 10252  staddi 10257  stadd3i 10259  strlem1 10261  strlem3a 10263  strlem5 10266  strlem6 10267  hstrlem6 10275  jplem1 10279  cdj1i 10444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-1p 5152  df-plp 5153  df-mp 5154  df-ltp 5155  df-plpr 5229  df-mpr 5230  df-enr 5231  df-nr 5232  df-plr 5233  df-mr 5234  df-ltr 5235  df-0r 5236  df-1r 5237  df-m1r 5238  df-c 5305  df-0 5306  df-1 5307  df-i 5308  df-r 5309  df-plus 5310  df-mul 5311  df-sub 5421  df-neg 5423

Copyright terms: Public domain