Theorem 1re 6839

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 6787, by exploiting properties of the imaginary unit _i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
1re	|- 1 e. RR

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		ax1ne0 6797	. . . 4 |- 1 =/= 0
2		ax1cn 6787	. . . . . . 7 |- 1 e. CC
3	2	cnrei 6838	. . . . . 6 |- E.a e. RR E.b e. RR 1 = (a + (_i x. b))
4		neeq1 2273	. . . . . . . . . 10 |- (1 = (a + (_i x. b)) -> (1 =/= 0 <-> (a + (_i x. b)) =/= 0))
5	4	biimpcd 233	. . . . . . . . 9 |- (1 =/= 0 -> (1 = (a + (_i x. b)) -> (a + (_i x. b)) =/= 0))
6		0cn 6831	. . . . . . . . . 10 |- 0 e. CC
7	6	cnrei 6838	. . . . . . . . 9 |- E.c e. RR E.d e. RR 0 = (c + (_i x. d))
8		neeq2 2274	. . . . . . . . . . . 12 |- (0 = (c + (_i x. d)) -> ((a + (_i x. b)) =/= 0 <-> (a + (_i x. b)) =/= (c + (_i x. d))))
9	8	biimpcd 233	. . . . . . . . . . 11 |- ((a + (_i x. b)) =/= 0 -> (0 = (c + (_i x. d)) -> (a + (_i x. b)) =/= (c + (_i x. d))))
10	9	reximdv 2452	. . . . . . . . . 10 |- ((a + (_i x. b)) =/= 0 -> (E.d e. RR 0 = (c + (_i x. d)) -> E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d))))
11	10	reximdv 2452	. . . . . . . . 9 |- ((a + (_i x. b)) =/= 0 -> (E.c e. RR E.d e. RR 0 = (c + (_i x. d)) -> E.c e. RR E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d))))
12	5, 7, 11	syl6mpi 104	. . . . . . . 8 |- (1 =/= 0 -> (1 = (a + (_i x. b)) -> E.c e. RR E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d))))
13	12	reximdv 2452	. . . . . . 7 |- (1 =/= 0 -> (E.b e. RR 1 = (a + (_i x. b)) -> E.b e. RR E.c e. RR E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d))))
14	13	reximdv 2452	. . . . . 6 |- (1 =/= 0 -> (E.a e. RR E.b e. RR 1 = (a + (_i x. b)) -> E.a e. RR E.b e. RR E.c e. RR E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d))))
15	3, 14	mpi 97	. . . . 5 |- (1 =/= 0 -> E.a e. RR E.b e. RR E.c e. RR E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d)))
16		ioran 424	. . . . . . . . . . . 12 |- (-. (a =/= c \/ b =/= d) <-> (-. a =/= c /\ -. b =/= d))
17		df-ne 2268	. . . . . . . . . . . . . 14 |- (a =/= c <-> -. a = c)
18	17	con2bii 335	. . . . . . . . . . . . 13 |- (a = c <-> -. a =/= c)
19		df-ne 2268	. . . . . . . . . . . . . 14 |- (b =/= d <-> -. b = d)
20	19	con2bii 335	. . . . . . . . . . . . 13 |- (b = d <-> -. b =/= d)
21	18, 20	anbi12i 710	. . . . . . . . . . . 12 |- ((a = c /\ b = d) <-> (-. a =/= c /\ -. b =/= d))
22	16, 21	bitr4i 283	. . . . . . . . . . 11 |- (-. (a =/= c \/ b =/= d) <-> (a = c /\ b = d))
23		id 15	. . . . . . . . . . . 12 |- (a = c -> a = c)
24		opreq2 4987	. . . . . . . . . . . 12 |- (b = d -> (_i x. b) = (_i x. d))
25	23, 24	opreqan12d 4997	. . . . . . . . . . 11 |- ((a = c /\ b = d) -> (a + (_i x. b)) = (c + (_i x. d)))
26	22, 25	sylbi 225	. . . . . . . . . 10 |- (-. (a =/= c \/ b =/= d) -> (a + (_i x. b)) = (c + (_i x. d)))
27	26	necon1ai 2307	. . . . . . . . 9 |- ((a + (_i x. b)) =/= (c + (_i x. d)) -> (a =/= c \/ b =/= d))
28		neeq1 2273	. . . . . . . . . . . . 13 |- (x = a -> (x =/= y <-> a =/= y))
29		neeq2 2274	. . . . . . . . . . . . 13 |- (y = c -> (a =/= y <-> a =/= c))
30	28, 29	rcla42ev 2625	. . . . . . . . . . . 12 |- ((a e. RR /\ c e. RR /\ a =/= c) -> E.x e. RR E.y e. RR x =/= y)
31	30	3expia 1319	. . . . . . . . . . 11 |- ((a e. RR /\ c e. RR) -> (a =/= c -> E.x e. RR E.y e. RR x =/= y))
32	31	ad2ant2r 807	. . . . . . . . . 10 |- (((a e. RR /\ b e. RR) /\ (c e. RR /\ d e. RR)) -> (a =/= c -> E.x e. RR E.y e. RR x =/= y))
33		neeq1 2273	. . . . . . . . . . . . 13 |- (x = b -> (x =/= y <-> b =/= y))
34		neeq2 2274	. . . . . . . . . . . . 13 |- (y = d -> (b =/= y <-> b =/= d))
35	33, 34	rcla42ev 2625	. . . . . . . . . . . 12 |- ((b e. RR /\ d e. RR /\ b =/= d) -> E.x e. RR E.y e. RR x =/= y)
36	35	3expia 1319	. . . . . . . . . . 11 |- ((b e. RR /\ d e. RR) -> (b =/= d -> E.x e. RR E.y e. RR x =/= y))
37	36	ad2ant2l 806	. . . . . . . . . 10 |- (((a e. RR /\ b e. RR) /\ (c e. RR /\ d e. RR)) -> (b =/= d -> E.x e. RR E.y e. RR x =/= y))
38	32, 37	jaod 454	. . . . . . . . 9 |- (((a e. RR /\ b e. RR) /\ (c e. RR /\ d e. RR)) -> ((a =/= c \/ b =/= d) -> E.x e. RR E.y e. RR x =/= y))
39	27, 38	syl5 35	. . . . . . . 8 |- (((a e. RR /\ b e. RR) /\ (c e. RR /\ d e. RR)) -> ((a + (_i x. b)) =/= (c + (_i x. d)) -> E.x e. RR E.y e. RR x =/= y))
40	39	ex 398	. . . . . . 7 |- ((a e. RR /\ b e. RR) -> ((c e. RR /\ d e. RR) -> ((a + (_i x. b)) =/= (c + (_i x. d)) -> E.x e. RR E.y e. RR x =/= y)))
41	40	r19.23advv 2466	. . . . . 6 |- ((a e. RR /\ b e. RR) -> (E.c e. RR E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d)) -> E.x e. RR E.y e. RR x =/= y))
42	41	r19.23aivv 2465	. . . . 5 |- (E.a e. RR E.b e. RR E.c e. RR E.d e. RR (a + (_i x. b)) =/= (c + (_i x. d)) -> E.x e. RR E.y e. RR x =/= y)
43	15, 42	syl 13	. . . 4 |- (1 =/= 0 -> E.x e. RR E.y e. RR x =/= y)
44	1, 43	ax-mp 7	. . 3 |- E.x e. RR E.y e. RR x =/= y
45		eqtr3 2160	. . . . . . . . . 10 |- ((x = 0 /\ y = 0) -> x = y)
46	45	ex 398	. . . . . . . . 9 |- (x = 0 -> (y = 0 -> x = y))
47	46	necon3d 2303	. . . . . . . 8 |- (x = 0 -> (x =/= y -> y =/= 0))
48		neeq1 2273	. . . . . . . . . 10 |- (z = y -> (z =/= 0 <-> y =/= 0))
49	48	rcla4ev 2620	. . . . . . . . 9 |- ((y e. RR /\ y =/= 0) -> E.z e. RR z =/= 0)
50	49	expcom 399	. . . . . . . 8 |- (y =/= 0 -> (y e. RR -> E.z e. RR z =/= 0))
51	47, 50	syl6 42	. . . . . . 7 |- (x = 0 -> (x =/= y -> (y e. RR -> E.z e. RR z =/= 0)))
52	51	com23 65	. . . . . 6 |- (x = 0 -> (y e. RR -> (x =/= y -> E.z e. RR z =/= 0)))
53	52	adantld 450	. . . . 5 |- (x = 0 -> ((x e. RR /\ y e. RR) -> (x =/= y -> E.z e. RR z =/= 0)))
54		neeq1 2273	. . . . . . . . 9 |- (z = x -> (z =/= 0 <-> x =/= 0))
55	54	rcla4ev 2620	. . . . . . . 8 |- ((x e. RR /\ x =/= 0) -> E.z e. RR z =/= 0)
56	55	expcom 399	. . . . . . 7 |- (x =/= 0 -> (x e. RR -> E.z e. RR z =/= 0))
57	56	adantrd 452	. . . . . 6 |- (x =/= 0 -> ((x e. RR /\ y e. RR) -> E.z e. RR z =/= 0))
58	57	a1dd 94	. . . . 5 |- (x =/= 0 -> ((x e. RR /\ y e. RR) -> (x =/= y -> E.z e. RR z =/= 0)))
59	53, 58	pm2.61ine 2339	. . . 4 |- ((x e. RR /\ y e. RR) -> (x =/= y -> E.z e. RR z =/= 0))
60	59	r19.23aivv 2465	. . 3 |- (E.x e. RR E.y e. RR x =/= y -> E.z e. RR z =/= 0)
61	44, 60	ax-mp 7	. 2 |- E.z e. RR z =/= 0
62		axrrecex 6800	. . . 4 |- ((z e. RR /\ z =/= 0) -> E.x e. RR (z x. x) = 1)
63		remulcl 6811	. . . . . . 7 |- ((z e. RR /\ x e. RR) -> (z x. x) e. RR)
64	63	adantlr 777	. . . . . 6 |- (((z e. RR /\ z =/= 0) /\ x e. RR) -> (z x. x) e. RR)
65		eleq1 2204	. . . . . 6 |- ((z x. x) = 1 -> ((z x. x) e. RR <-> 1 e. RR))
66	64, 65	syl5ibcom 254	. . . . 5 |- (((z e. RR /\ z =/= 0) /\ x e. RR) -> ((z x. x) = 1 -> 1 e. RR))
67	66	r19.23adva 2464	. . . 4 |- ((z e. RR /\ z =/= 0) -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
68	62, 67	mpd 11	. . 3 |- ((z e. RR /\ z =/= 0) -> 1 e. RR)
69	68	r19.23aiva 2460	. 2 |- (E.z e. RR z =/= 0 -> 1 e. RR)
70	61, 69	ax-mp 7	1 |- 1 e. RR

Syntax hints:  -. wn 2   -> wi 3   \/ wo 336   /\ wa 337   = wceq 1586   e. wcel 1588   =/= wne 2266  E.wrex 2356  (class class class)co 4981  RRcr 6751  0cc0 6752  1c1 6753  _ici 6754   + caddc 6755   x. cmul 6757

This theorem is referenced by:  0re 6840  peano2re 6967  readdcan 6969  mul02lem2 6972  addid1 6977  renegcl 7077  0reALT 7080  peano2rem 7081  lt01 7204  redivclzi 7308  rereccli 7310  rerecclzi 7311  rereccl 7312  eqnegi 7313  ltp1 7320  recgt0ii 7323  ltm1 7324  prodgt0i 7328  ltmul1i 7331  ltdiv1i 7333  mulgt1 7359  ltmulgt11 7360  lemulge11 7362  recgt0 7376  ltreci 7395  reclt1 7414  recgt1 7415  recgt1i 7416  recp1lt1 7417  recreclt 7418  halfposi 7420  ledivp1i 7422  ltdivp1i 7423  posexi 7424  nnssre 7443  nnge1 7459  nngt1ne1 7460  nnle1eq1 7461  nngt0 7462  lt1nnn 7463  nnrecre 7469  nnrecgt0 7470  nnleltp1 7471  nnltp1le 7472  nnsubi 7473  nnaddm1cl 7475  2re 7496  3re 7498  4re 7499  5re 7500  6re 7501  7re 7502  8re 7503  9re 7504  10re 7505  2pos 7506  3pos 7508  4pos 7509  5pos 7510  6pos 7511  7pos 7512  8pos 7513  9pos 7514  10pos 7515  1lt2 7547  1ne2 7548  1lt3 7550  1lt6 7551  1lt9 7552  1ne9 7553  1lt10 7554  halflt1 7556  addltmul 7569  1rp 7575  nnunb 7619  nnrecl 7621  xrub 7629  lt0nnn0 7666  nn0ltp1le 7677  nn0leltp1 7678  nn0ltlem1 7679  elnnz1 7705  znnnlt1 7706  elnn0nn 7721  zltp1le 7732  zleltp1 7733  recnz 7746  gtndiv 7748  nneoi 7752  dfuzi 7757  uzindOLD 7763  nn0ind-raph 7771  zbtwnre 7779  rebtwnz 7780  qbtwnre 7805  qbtwnxr 7806  fraclt1 7816  flbi2 7827  fldiv 7843  modid 7858  monoord 7869  eluzp1m1 7949  eluzp1p1 7951  eluz2b2 7980  eluz2b3 7981  indstr2 7985  fzprval 8050  fztpval 8051  fzennn 8090  cardfzOLD 8092  seq1lem2 8096  reexpcl 8207  expge0 8217  expge1 8219  expordi 8229  expwordi 8232  expword2i 8234  expmwordi 8235  exple1 8236  bernneq 8282  bernneqOLD 8283  bernneq2 8284  expnbnd 8285  expnlbnd 8286  expnlbnd2 8287  discrlem2 8291  discrlem3 8292  nnlesqi 8295  nnesqi 8296  sqrlem1 8307  sqrlem2 8308  sqrlem3 8309  sqrlem6 8312  sqrlem8 8314  sqrlem9 8315  sqrlem10 8316  sqrlem11 8317  sqrlem16 8322  sqrlem19 8325  sqrlem20 8326  sqrlem21 8327  sqrlem22 8328  sqrthi 8333  sqrcli 8334  sqrgt0i 8335  sqr1 8350  sqr2gt1lt2 8353  sqr2irrlem1 8358  inelr 8369  nthruz 8380  cjexp 8451  re1 8456  im1 8457  rei 8458  imi 8459  absexp 8503  abs1mi 8541  seq1bndi 8547  caubndi 8563  facwordi 8581  faclbnd3 8584  faclbnd4lem1 8585  faclbnd4lem4 8588  faclbnd6 8591  facavg 8592  bcnp11 8602  bcnp1n 8603  bcpasc2i 8604  bcpasc2 8605  bcpasci 8606  bccl2 8608  climmullem1 8776  climmullem2 8777  climmullem3 8778  climmullem4 8779  climmullem5 8780  serzf0i 8825  arisumi 8885  expcnvlem1 8886  expcnvlem2 8887  expcnvlem4 8889  expcnvlem5 8890  geolimilem 8895  geolim1i 8898  georeclim 8900  geoisumr 8903  geoisum1c 8905  0.999... 8906  efcltlem1 8964  erelem7 8985  ele3lem 8986  ege2lem2 8988  ege2le3lem2 8989  ere 8990  efaddlem1 8998  efaddlem2 8999  efaddlem7 9004  efaddlem8 9005  efaddlem10 9007  efaddlem12 9009  efaddlem13 9010  efaddlem15 9012  efaddlem20 9017  ef01tllem2 9044  ef01tllem2OLD 9045  ef01tlubi 9046  absef01tlubi 9048  eirrlem1 9049  eirrlem3 9051  eirrlem4 9052  abspef01tlubi 9058  efgt1i 9066  efgt0i 9067  eflti 9069  eflegeolem2 9077  efm1legeoi 9080  efcnlem1 9082  efcnlem2 9083  efcnlem4 9085  reeff1olem1 9087  reeff1o 9089  resin4p 9099  recos4p 9100  sinbnd 9129  cosbnd 9130  sin01bndlem2 9132  sin01bndlem3 9133  cos01bndlem2 9134  cos01bndlem3 9135  cos1bnd 9138  cos2bnd 9139  sin01gt0 9140  cos01gt0 9141  sin02gt0 9142  sincos1sgn 9143  efieq1re 9149  ruclem8 9180  ruclem13 9185  ruclem25 9197  mulgcdlem3 9353  1nprm 9366  isprm3 9370  coprm 9377  nprmdvds1 9382  infpn2 9391  divrngmcl 9529  invrcl 9536  poshyp 9546  indistpsx 9776  blex 9992  opnm 10003  tgioolem 10058  dscmet 10062  lmnn 10079  caun0 10089  bcthlem16 10158  bcthlem18 10160  nvm1 10493  nvmtri 10500  nv1 10505  sm1cnilem 10555  ipid 10571  nmosetn0 10636  nmoub3i 10644  nmo0 10660  nmlno0lem 10662  blocnilem 10673  ipasslem10 10709  minveclem25 10784  htthlem6 10843  sinhalfpilem 10899  sinperlem1 10906  sincos4thpi 10931  sincos6thpi 10932  coskpi 10935  sineq0 10936  sineq0OLD 10937  sineq0re 10938  efifolem1 10947  efifolem3 10949  efifolem4 10950  efifolem5 10951  efifolem6 10952  efifolem7 10953  loge 10992  hisubcomi 11440  normlem9 11454  normlem7tALT 11455  norm-ii.i 11473  normsubi 11477  bcs2 11518  norm1 11588  projlem1 11653  projlem2 11654  projlem4 11656  projlem6 11658  projlem28 11680  projlem29 11681  nmopsetn0 12261  nmfnsetn0 12274  nmopub2tALT 12302  nmopge0 12304  nmfnleub2 12319  nmfnge0 12320  0cnop 12372  0cnfn 12373  nmop0 12379  nmfn0 12380  nmlnop0iALT 12389  nmopun 12408  unopbd 12409  hmopd 12416  nmcopexlem2 12421  nmcopexlem5 12424  nmcfnexlem2 12450  nmcfnexlem5 12453  nmopadjlem 12491  nmopcoi 12497  nmopcoadji 12503  branmfn 12507  pjnmopi 12550  pjbdlni 12551  hstle1 12629  hstle 12633  hstles 12634  stge1i 12641  stlesi 12644  staddi 12649  stadd3i 12651  strlem1 12653  strlem3a 12655  strlem5 12658  strlem6 12659  hstrlem6 12667  jplem1 12671  cdj1i 12836  addltmulALT 12849  sindivcvglem1 14386  sindivcvglem2 14387  sindivcvglem3 14388  sindivcvglem5 14390  sindivcvglem8 14393  elfzm12 14401  fseq1cl 14409  seqzp2 15451  altretop 15788  cntrsetlem 15791  fz10 16612  rddif 16622  absrdbnd 16623  fdc 16636  incsequz 16639  fsumltisumi 16647  mettrifi 16671  geomcau 16673  iiuni 16692  dfii2 16693  dfii3 16694  iirev 16695  iihalf1 16696  iihalf2 16697  iimulcl 16698  lincmb01cmp 16702  lincmb01icc 16703  totbndbnd 16768  heiborlem30 16808  heiborlem31 16809  heiborlem32 16810  heiborlem33 16811  heiborlem35 16813  bfplem9 16830  rrntotbndlem1 16844  rrntotbndlem2 16845  rrntotbnd 16846  iccbnd 16850  iicmp 16852  phtpyid 16873  phtpycom 16874  phtpycolem1 16875  phtpycolem2 16876  phtpycolem3 16877  phtpycolem4 16878  phtpycolem5 16879  phtpyco 16880  reparphtlem2 16888  reparpht 16889  pcoval1 16898  pcoval2 16899  pcocn 16900  pco1 16902  pcohtpylem1 16904  pcohtpylem2 16905  pcohtpylem3 16906  pcohtpy 16907  pcopt 16908  pcoass 16909  pcorevlem 16910  pcorev 16911  pi1gp 16919

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764

Copyright terms: Public domain