Theorem ine0 11106

Description: The imaginary unit i is not zero. (Contributed by NM, 6-May-1999.)

Assertion

Ref	Expression
ine0	⊢ i ≠ 0

Proof of Theorem ine0

Step	Hyp	Ref	Expression
1		ax-1ne0 10637	. . . 4 ⊢ 1 ≠ 0
2	1	neii 2954	. . 3 ⊢ ¬ 1 = 0
3		oveq2 7159	. . . . . 6 ⊢ (i = 0 → (i · i) = (i · 0))
4		ax-icn 10627	. . . . . . 7 ⊢ i ∈ ℂ
5	4	mul01i 10861	. . . . . 6 ⊢ (i · 0) = 0
6	3, 5	eqtr2di 2811	. . . . 5 ⊢ (i = 0 → 0 = (i · i))
7	6	oveq1d 7166	. . . 4 ⊢ (i = 0 → (0 + 1) = ((i · i) + 1))
8		ax-1cn 10626	. . . . 5 ⊢ 1 ∈ ℂ
9	8	addid2i 10859	. . . 4 ⊢ (0 + 1) = 1
10		ax-i2m1 10636	. . . 4 ⊢ ((i · i) + 1) = 0
11	7, 9, 10	3eqtr3g 2817	. . 3 ⊢ (i = 0 → 1 = 0)
12	2, 11	mto 200	. 2 ⊢ ¬ i = 0
13	12	neir 2955	1 ⊢ i ≠ 0

Syntax hints:   = wceq 1539   ≠ wne 2952  (class class class)co 7151  0cc0 10568  1c1 10569  ici 10570   + caddc 10571   · cmul 10573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-po 5444  df-so 5445  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-ltxr 10711

This theorem is referenced by:  inelr  11657  2muline0  11891  irec  13607  iexpcyc  13612  imre  14508  reim  14509  crim  14515  cjreb  14523  cnpart  14640  tanval2  15527  tanval3  15528  efival  15546  sinhval  15548  retanhcl  15553  tanhlt1  15554  tanhbnd  15555  itgz  24473  ibl0  24479  iblcnlem1  24480  itgcnlem  24482  iblss  24497  iblss2  24498  itgss  24504  itgeqa  24506  iblconst  24510  iblabsr  24522  iblmulc2  24523  itgsplit  24528  dvsincos  24673  efeq1  25212  tanregt0  25223  efif1olem4  25229  eflogeq  25285  cxpsqrtlem  25385  root1eq1  25436  ang180lem1  25487  ang180lem2  25488  ang180lem3  25489  atandm2  25555  2efiatan  25596  atantan  25601  dvatan  25613  atantayl2  25616  log2cnv  25622  ccfldextdgrr  31256  itgexpif  32098  logi  33208  iexpire  33209  iblmulc2nc  35395  ftc1anclem6  35408  proot1ex  40511  iblsplit  42967  sinh-conventional  45649