MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4cn Structured version   Visualization version   GIF version

Theorem 4cn 11716
Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
Assertion
Ref Expression
4cn 4 ∈ ℂ

Proof of Theorem 4cn
StepHypRef Expression
1 df-4 11696 . 2 4 = (3 + 1)
2 3cn 11712 . . 3 3 ∈ ℂ
3 ax-1cn 10589 . . 3 1 ∈ ℂ
42, 3addcli 10641 . 2 (3 + 1) ∈ ℂ
51, 4eqeltri 2914 1 4 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7150  cc 10529  1c1 10532   + caddc 10534  3c3 11687  4c4 11688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798  ax-1cn 10589  ax-addcl 10591
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-clel 2898  df-2 11694  df-3 11695  df-4 11696
This theorem is referenced by:  5cn  11719  5m1e4  11761  4p2e6  11784  4p3e7  11785  4p4e8  11786  4t2e8  11799  4d2e2  11801  8th4div3  11851  div4p1lem1div2  11886  5p5e10  12163  4t4e16  12191  6t5e30  12199  fldiv4p1lem1div2  13200  sq4e2t8  13557  discr  13596  sqoddm1div8  13599  4bc2eq6  13684  bpoly3  15407  bpoly4  15408  cos2bnd  15536  flodddiv4  15759  6gcd4e2  15881  6lcm4e12  15955  pythagtriplem1  16148  13prm  16444  43prm  16450  163prm  16453  317prm  16454  631prm  16455  1259lem1  16459  1259lem2  16460  1259lem3  16461  1259lem4  16462  1259lem5  16463  1259prm  16464  2503lem1  16465  2503lem2  16466  2503lem3  16467  2503prm  16468  4001lem1  16469  4001lem2  16470  4001lem3  16471  4001lem4  16472  4001prm  16473  cphipval2  23778  4cphipval2  23779  minveclem2  23963  minveclem3  23966  minveclem7  23972  uniioombl  24124  dveflem  24510  sincosq4sgn  25021  sincos6thpi  25035  ang180lem2  25320  heron  25348  quad2  25349  quad  25350  dcubic2  25354  dcubic  25356  mcubic  25357  cubic2  25358  cubic  25359  dquartlem1  25361  dquartlem2  25362  dquart  25363  quart1cl  25364  quart1lem  25365  quart1  25366  quartlem1  25367  quartlem2  25368  quartlem4  25370  quart  25371  log2cnv  25455  log2tlbnd  25456  log2ublem3  25459  log2ub  25460  bclbnd  25789  bposlem8  25800  bposlem9  25801  2lgslem3a  25905  2lgslem3b  25906  2lgslem3c  25907  2lgslem3d  25908  2lgsoddprmlem2  25918  2lgsoddprmlem3c  25921  2lgsoddprmlem3d  25922  addsqnreup  25952  addsq2nreurex  25953  pntibndlem2  26100  pntlemb  26106  ex-opab  28144  ex-exp  28162  ex-fac  28163  ex-bc  28164  ex-ind-dvds  28173  4ipval2  28418  ipidsq  28420  dipcl  28422  dipcj  28424  dip0r  28427  dipcn  28430  ip1ilem  28536  ipasslem10  28549  minvecolem2  28585  minvecolem7  28593  normpar2i  28866  polid2i  28867  lnopeq0i  29717  fib5  31568  fib6  31569  hgt750lemd  31824  hgt750lem  31827  hgt750lem2  31828  quad3  32816  235t711  39061  inductionexd  40389  lhe4.4ex1a  40545  limclner  41816  stoweidlem13  42183  wallispi2lem1  42241  wallispi2lem2  42242  stirlinglem3  42246  stirlinglem10  42253  stirlinglem12  42255  sqwvfourb  42399  fouriersw  42401  fmtnorec4  43562  fmtno5lem4  43569  257prm  43574  fmtnofac1  43583  fmtno4prmfac  43585  fmtno5faclem1  43592  fmtno5faclem2  43593  139prmALT  43610  2exp11  43616  mod42tp1mod8  43618  3exp4mod41  43632  41prothprmlem1  43633  41prothprmlem2  43634  41prothprm  43635  quad1  43636  8even  43729  2exp340mod341  43749  8exp8mod9  43752  mogoldbb  43801  nnsum4primeseven  43816  nnsum4primesevenALTV  43817  bgoldbtbndlem2  43822  zlmodzxzequap  44456  itsclc0yqsollem1  44651  itscnhlinecirc02plem1  44671  5m4e1  44800
  Copyright terms: Public domain W3C validator