Theorem mulid1 9614

Description: is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
mulid1

Proof of Theorem mulid1

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnre 9613	. 2
2		recn 9603	. . . . . 6
3		ax-icn 9572	. . . . . . 7
4		recn 9603	. . . . . . 7
5		mulcl 9597	. . . . . . 7
6	3, 4, 5	sylancr 663	. . . . . 6
7		ax-1cn 9571	. . . . . . 7
8		adddir 9608	. . . . . . 7
9	7, 8	mp3an3 1313	. . . . . 6
10	2, 6, 9	syl2an 477	. . . . 5
11		ax-1rid 9583	. . . . . 6
12		mulass 9601	. . . . . . . . 9
13	3, 7, 12	mp3an13 1315	. . . . . . . 8
14	4, 13	syl 16	. . . . . . 7
15		ax-1rid 9583	. . . . . . . 8
16	15	oveq2d 6312	. . . . . . 7
17	14, 16	eqtrd 2498	. . . . . 6
18	11, 17	oveqan12d 6315	. . . . 5
19	10, 18	eqtrd 2498	. . . 4
20		oveq1 6303	. . . . 5
21		id 22	. . . . 5
22	20, 21	eqeq12d 2479	. . . 4
23	19, 22	syl5ibrcom 222	. . 3
24	23	rexlimivv 2954	. 2
25	1, 24	syl 16	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  E.wrex 2808  (class class class)co 6296  cc 9511  cr 9512  1c1 9514  ci 9515  caddc 9516  cmul 9518

This theorem is referenced by:  mulid2  9615  mulid1i  9619  mulid1d  9634  muleqadd  10218  divdiv1  10280  conjmul  10286  nnmulcl  10584  expmul  12211  binom21  12284  sq01  12288  bernneq  12292  hashiun  13636  fprodcvg  13737  prodmolem2a  13741  efexp  13836  cncrng  18439  cnfld1  18443  0dgr  22642  ecxp  23054  dvcxp1  23116  efrlim  23299  lgsdilem2  23606  axcontlem7  24273  gxnn0mul  25279  cnrngo  25405  ipasslem2  25747  addltmulALT  27365  zrhnm  27950  dvcncxp1  30100  2even  32739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-mulcom 9577  ax-mulass 9579  ax-distr 9580  ax-1rid 9583  ax-cnre 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299