HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 1re 5415
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 5249, 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
StepHypRef Expression
1 axicn 5250 . . . 4 |- i e. CC
2 axcnre 5266 . . . 4 |- (i e. CC -> E.x e. RR E.y e. RR i = (x + (i x. y)))
31, 2ax-mp 7 . . 3 |- E.x e. RR E.y e. RR i = (x + (i x. y))
4 neeq1 1587 . . . . . . . . 9 |- (z = x -> (z =/= 0 <-> x =/= 0))
54rcla4ev 1873 . . . . . . . 8 |- ((x e. RR /\ x =/= 0) -> E.z e. RR z =/= 0)
65adantlr 393 . . . . . . 7 |- (((x e. RR /\ y e. RR) /\ x =/= 0) -> E.z e. RR z =/= 0)
7 neeq1 1587 . . . . . . . . 9 |- (z = y -> (z =/= 0 <-> y =/= 0))
87rcla4ev 1873 . . . . . . . 8 |- ((y e. RR /\ y =/= 0) -> E.z e. RR z =/= 0)
98adantll 392 . . . . . . 7 |- (((x e. RR /\ y e. RR) /\ y =/= 0) -> E.z e. RR z =/= 0)
106, 9jaodan 426 . . . . . 6 |- (((x e. RR /\ y e. RR) /\ (x =/= 0 \/ y =/= 0)) -> E.z e. RR z =/= 0)
1110ex 373 . . . . 5 |- ((x e. RR /\ y e. RR) -> ((x =/= 0 \/ y =/= 0) -> E.z e. RR z =/= 0))
12 ine0 5414 . . . . . . 7 |- i =/= 0
13 neeq1 1587 . . . . . . 7 |- (i = (x + (i x. y)) -> (i =/= 0 <-> (x + (i x. y)) =/= 0))
1412, 13mpbii 193 . . . . . 6 |- (i = (x + (i x. y)) -> (x + (i x. y)) =/= 0)
15 ioran 306 . . . . . . . . 9 |- (-. (x =/= 0 \/ y =/= 0) <-> (-. x =/= 0 /\ -. y =/= 0))
16 nne 1586 . . . . . . . . . 10 |- (-. x =/= 0 <-> x = 0)
17 nne 1586 . . . . . . . . . 10 |- (-. y =/= 0 <-> y = 0)
1816, 17anbi12i 482 . . . . . . . . 9 |- ((-. x =/= 0 /\ -. y =/= 0) <-> (x = 0 /\ y = 0))
1915, 18bitr 173 . . . . . . . 8 |- (-. (x =/= 0 \/ y =/= 0) <-> (x = 0 /\ y = 0))
20 opreq12 3961 . . . . . . . . . 10 |- ((x = 0 /\ (i x. y) = 0) -> (x + (i x. y)) = (0 + 0))
21 opreq2 3960 . . . . . . . . . . 11 |- (y = 0 -> (i x. y) = (i x. 0))
221mul01 5411 . . . . . . . . . . 11 |- (i x. 0) = 0
2321, 22syl6eq 1520 . . . . . . . . . 10 |- (y = 0 -> (i x. y) = 0)
2420, 23sylan2 451 . . . . . . . . 9 |- ((x = 0 /\ y = 0) -> (x + (i x. y)) = (0 + 0))
25 0cn 5308 . . . . . . . . . 10 |- 0 e. CC
2625addid1 5310 . . . . . . . . 9 |- (0 + 0) = 0
2724, 26syl6eq 1520 . . . . . . . 8 |- ((x = 0 /\ y = 0) -> (x + (i x. y)) = 0)
2819, 27sylbi 199 . . . . . . 7 |- (-. (x =/= 0 \/ y =/= 0) -> (x + (i x. y)) = 0)
2928necon1ai 1605 . . . . . 6 |- ((x + (i x. y)) =/= 0 -> (x =/= 0 \/ y =/= 0))
3014, 29syl 10 . . . . 5 |- (i = (x + (i x. y)) -> (x =/= 0 \/ y =/= 0))
3111, 30syl5 21 . . . 4 |- ((x e. RR /\ y e. RR) -> (i = (x + (i x. y)) -> E.z e. RR z =/= 0))
3231r19.23aivv 1745 . . 3 |- (E.x e. RR E.y e. RR i = (x + (i x. y)) -> E.z e. RR z =/= 0)
333, 32ax-mp 7 . 2 |- E.z e. RR z =/= 0
34 axrrecex 5264 . . . 4 |- ((z e. RR /\ z =/= 0) -> E.x e. RR (z x. x) = 1)
35 eleq1 1531 . . . . . . 7 |- ((z x. x) = 1 -> ((z x. x) e. RR <-> 1 e. RR))
36 axmulrcl 5254 . . . . . . 7 |- ((z e. RR /\ x e. RR) -> (z x. x) e. RR)
3735, 36syl5cbi 209 . . . . . 6 |- ((z e. RR /\ x e. RR) -> ((z x. x) = 1 -> 1 e. RR))
3837r19.23adva 1744 . . . . 5 |- (z e. RR -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
3938adantr 389 . . . 4 |- ((z e. RR /\ z =/= 0) -> (E.x e. RR (z x. x) = 1 -> 1 e. RR))
4034, 39mpd 26 . . 3 |- ((z e. RR /\ z =/= 0) -> 1 e. RR)
4140r19.23aiva 1741 . 2 |- (E.z e. RR z =/= 0 -> 1 e. RR)
4233, 41ax-mp 7 1 |- 1 e. RR
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223   = wceq 954   e. wcel 956   =/= wne 1582  E.wrex 1643  (class class class)co 3954  CCcc 5212  RRcr 5213  0cc0 5214  1c1 5215  ici 5216   + caddc 5217   x. cmul 5219
This theorem is referenced by:  peano2re 5416  renegclt 5417  0reALT 5421  peano2rem 5422  lt01 5661  redivclz 5763  rereccl 5765  rerecclz 5766  rerecclt 5767  eqneg 5768  ltp1t 5775  recgt0i 5778  ltm1t 5779  prodgt0 5783  ltmul1 5786  ltdiv1 5788  mulgt1t 5809  ltmulgt11t 5810  lemulge11t 5812  recgt0t 5823  ltrec 5835  reclt1t 5854  recgt1t 5855  recgt1it 5856  recp1lt1 5857  recrecltt 5858  halfpos 5860  ledivp1 5862  ltdivp1 5863  posex 5864  nnssre 5883  nnge1t 5899  nngt1ne1t 5900  nnle1eq1t 5901  nngt0t 5902  lt1nnn 5903  nnrecgt0t 5908  nnleltp1t 5909  nnltp1let 5910  nnsub 5911  nnaddm1clt 5913  2re 5934  3re 5936  4re 5937  5re 5938  6re 5939  7re 5940  8re 5941  9re 5942  10re 5943  2pos 5944  3pos 5946  4pos 5947  5pos 5948  6pos 5949  7pos 5950  8pos 5951  9pos 5952  10pos 5953  1lt2 5983  halflt1 5985  nnunb 6025  nnreclt 6027  xrub 6035  lt0nnn0 6071  nn0ltp1let 6082  nn0leltp1t 6083  nn0ltlem1t 6084  elnnz1 6110  znnnlt1t 6111  elnn0nn 6126  zltp1let 6136  zleltp1t 6137  recnzt 6146  gtndivt 6148  nneo 6152  dfuz 6158  uzindOLD 6164  nn0ind-raph 6170  zbtwnre 6177  rebtwnz 6178  qbtwnre 6224  qbtwnxr 6225  monoord 6239  seq1lem2 6255  eluzp1m1t 6373  eluzp1p1t 6375  reexpclt 6520  rpexpclt 6522  expge0t 6530  expge1t 6532  expordit 6539  expwordit 6542  expword2it 6544  expmwordit 6545  exple1t 6546  bernneq 6591  bernneq2 6592  expnbndt 6593  discrlem2 6595  discrlem3 6596  nnlesq 6599  nnesq 6600  sqrlem1 6611  sqrlem2 6612  sqrlem3 6613  sqrlem6 6616  sqrlem8 6618  sqrlem9 6619  sqrlem10 6620  sqrlem11 6621  sqrlem16 6626  sqrlem19 6629  sqrlem20 6630  sqrlem21 6631  sqrlem22 6632  sqrth 6637  sqrcl 6638  sqrgt0 6639  sqr1 6654  sqr2gt1lt2 6657  sqr2irrlem1 6662  inelr 6673  nthruz 6685  cjexpt 6760  re1 6765  im1 6766  rei 6767  imi 6768  absexpt 6811  abs1m 6849  seq1bnd 6855  caubnd 6871  facwordit 6889  faclbnd3 6892  faclbnd4lem1 6893  faclbnd4lem4 6896  facavgt 6900  bcnp11t 6911  bcnp1nt 6912  bcpasc2 6913  bcpasc2t 6914  bcpasc 6915  bccl2t 6917  climmullem1 7064  climmullem2 7065  climmullem3 7066  climmullem4 7067  climmullem5 7068  serzf0 7113  ser1f0 7114  fnsmnt 7169  expcnvlem1 7170  expcnvlem2 7171  expcnvlem4 7173  expcnvlem5 7174  geolimilem 7178  geolim1i 7181  georeclim 7183  geoisumr 7186  geoisum1c 7188  0.999... 7189  mulc1cncf 7222  efcltlem1 7254  erelem7 7275  ele3lem 7276  ege2lem2 7278  ege2le3lem2 7279  ere 7280  efaddlem1 7288  efaddlem2 7289  efaddlem7 7294  efaddlem8 7295  efaddlem10 7297  efaddlem12 7299  efaddlem13 7300  efaddlem15 7302  efaddlem20 7307  ef01tllem2 7334  ef01tlub 7335  absef01tlub 7337  eirrlem1 7338  eirrlem3 7340  eirrlem4 7341  abspef01tlub 7344  efgt1 7352  efgt0 7353  eflt 7355  reeff1 7358  eflegeolem2 7362  efm1legeo 7365  efcnlem1 7367  efcnlem2 7368  efcnlem4 7370  reeff1olem1 7372  reeff1olem1OLD 7374  reeff1o 7376  resin4pt 7386  recos4pt 7387  sinbndt 7415  cosbndt 7416  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  cos1bnd 7424  cos2bnd 7425  sin01gt0 7426  cos01gt0 7427  sin02gt0 7428  sincos1sgn 7429  infpn2 7460  ruclem8 7468  ruclem13 7473  ruclem25 7485  blex 7801  opnm 7812  tgioolem 7866  dscmet 7870  lmnn 7887  caun0 7896  bcthlem16 7964  bcthlem18 7966  nvm1 8244  nvmtri 8251  nv1 8256  sm1cnilem 8294  ipid 8310  nmosetn0 8373  nmoub3i 8381  nmo0 8396  nmlno0lem 8398  blocnilem 8408  ipasslem10 8443  minveclem25 8513  htthlem6 8568  sinhalfpilem 8617  sinperlem1 8624  sincos4thpi 8646  sincos6thpi 8647  efifolem1 8656  efifolem3 8658  efifolem4 8659  efifolem5 8660  efifolem6 8661  efifolem7 8662  circgrpOLD 8677  log1 8705  loge 8706  hisubcom 8909  normlem9 8923  normlem7tALT 8924  norm-ii 8943  normsub 8947  bcs2t 8988  norm1t 9060  projlem1 9125  projlem2 9126  projlem4 9128  projlem6 9130  projlem28 9152  projlem29 9153  nmopsetn0 9732  nmfnsetn0 9745  nmopub2tALT 9773  nmopge0t 9774  nmfnleub2t 9789  nmfnge0t 9790  0cnop 9842  0cnfn 9843  nmop0 9849  nmfn0 9850  nmlnop0ALT 9858  nmopunt 9877  unopbdt 9878  hmopdt 9885  nmcopexlem2 9890  nmcopexlem5 9893  nmcfnexlem2 9919  nmcfnexlem5 9922  nmopadjlem 9960  nmopco 9966  nmopcoadj 9972  branmfnt 9976  pjnmop 10013  pjbdln 10014  hstle1t 10091  hstlet 10095  hstlest 10096  stge1 10103  stles 10106  stadd 10111  stadd3 10113  strlem1 10115  strlem3a 10117  strlem5 10120  strlem6 10121  hstrlem6 10129  jplem1 10133  cdj1 10294  iintlem2 10513
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-iun 2563  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-fv 3193  df-rdg 3923  df-opr 3956  df-oprab 3957  df-1st 4069  df-2nd 4070  df-1o 4123  df-oadd 4125  df-omul 4126  df-er 4251  df-ec 4253  df-qs 4256  df-ni 4980  df-pli 4981  df-mi 4982  df-lti 4983  df-plpq 5015  df-mpq 5016  df-enq 5017  df-nq 5018  df-plq 5019  df-mq 5020  df-rq 5021  df-ltq 5022  df-1q 5023  df-np 5066  df-1p 5067  df-plp 5068  df-mp 5069  df-ltp 5070  df-plpr 5144  df-mpr 5145  df-enr 5146  df-nr 5147  df-plr 5148  df-mr 5149  df-ltr 5150  df-0r 5151  df-1r 5152  df-m1r 5153  df-c 5220  df-0 5221  df-1 5222  df-i 5223  df-r 5224  df-plus 5225  df-mul 5226  df-sub 5336  df-neg 5338
Copyright terms: Public domain