Theorem div1d 12112

Description: A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
div1d.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
div1d	⊢ (𝜑 → (𝐴 / 1) = 𝐴)

Proof of Theorem div1d

Step	Hyp	Ref	Expression
1		div1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		div1 12033	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐴 / 1) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225  1c1 11228   / cdiv 12000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-resscn 11284  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-addrcl 11288  ax-mulcl 11289  ax-mulrcl 11290  ax-mulcom 11291  ax-addass 11292  ax-mulass 11293  ax-distr 11294  ax-i2m1 11295  ax-1ne0 11296  ax-1rid 11297  ax-rnegex 11298  ax-rrecex 11299  ax-cnre 11300  ax-pre-lttri 11301  ax-pre-lttrn 11302  ax-pre-ltadd 11303  ax-pre-mulgt0 11304

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-riota 7400  df-ov 7446  df-oprab 7447  df-mpo 7448  df-er 8745  df-en 9002  df-dom 9003  df-sdom 9004  df-pnf 11372  df-mnf 11373  df-xr 11374  df-ltxr 11375  df-le 11376  df-sub 11570  df-neg 11571  df-div 12001

This theorem is used by:  zq  13108  divlt1lt  13218  divle1le  13219  nnledivrp  13261  modfrac  14051  iexpcyc  14378  geo2sum2  16072  fallfacfac  16240  bpolysum  16248  sin01gt0  16387  bits0  16627  cncongrcoprm  16874  isprm6  16919  divdenle  16954  qden1elz  16962  pczpre  17054  prmreclem2  17124  mul4sq  17161  psgnunilem4  19741  znidomb  21897  iblcnlem1  26138  itgcnlem  26140  iblabsr  26180  iblmulc2  26181  aaliou2b  26698  aaliou3lem3  26701  tayl0  26719  logtayl2  27020  root1cj  27114  elogb  27128  logblog  27150  ang180lem4  27170  isosctrlem3  27178  dquartlem1  27209  efrlim  27327  amgmlem  27347  fsumharmonic  27369  lgamgulmlem5  27390  lgamcvg2  27412  1sgm2ppw  27557  logexprlim  27582  perfectlem2  27587  sum2dchr  27631  dchrvmasum2lem  27853  dchrisum0flblem2  27866  dchrisum0lem1  27873  mulog2sumlem2  27892  selbergb  27906  selberg2b  27909  selberg3lem1  27914  selberg3lem2  27915  pntrmax  27921  pntrlog2bndlem2  27935  pntrlog2bndlem4  27937  pntrlog2bndlem6a  27939  pntrlog2bnd  27941  pntlemk  27963  kbpj  32588  znumd  33474  zdend  33475  cos9thpiminplylem2  34485  faclimlem1  36686  knoppndvlem17  37572  iblmulc2nc  38795  lcmineqlem11  43281  aks4d1p8  43329  aks6d1c1  43358  tan3rdpi  43596  expgrowth  45511  bccn1  45520  binomcxplemnotnn0  45532  ltdivgt1  46573  0ellimcdiv  46864  sinaover2ne0  47083  dvnxpaek  47157  stoweidlem7  47222  stoweidlem36  47251  stoweidlem42  47257  stoweidlem51  47266  stoweidlem59  47274  stirlinglem6  47294  stirlinglem7  47295  stirlinglem10  47298  stirlinglem15  47303  dirkertrigeq  47316  fourierdlem60  47381  fourierdlem61  47382  etransclem14  47463  etransclem24  47473  etransclem25  47474  etransclem35  47484  bits0ALTV  48982  perfectALTVlem2  49025  0dig2nn0e  49929  0dig2nn0o  49930  line2  50069  amgmwlem  51267