![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ixi | Structured version Visualization version GIF version |
Description: i times itself is minus 1. (Contributed by NM, 6-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Ref | Expression |
---|---|
ixi | ⊢ (i · i) = -1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-neg 10588 | . 2 ⊢ -1 = (0 − 1) | |
2 | ax-i2m1 10320 | . . 3 ⊢ ((i · i) + 1) = 0 | |
3 | 0cn 10348 | . . . 4 ⊢ 0 ∈ ℂ | |
4 | ax-1cn 10310 | . . . 4 ⊢ 1 ∈ ℂ | |
5 | ax-icn 10311 | . . . . 5 ⊢ i ∈ ℂ | |
6 | 5, 5 | mulcli 10364 | . . . 4 ⊢ (i · i) ∈ ℂ |
7 | 3, 4, 6 | subadd2i 10690 | . . 3 ⊢ ((0 − 1) = (i · i) ↔ ((i · i) + 1) = 0) |
8 | 2, 7 | mpbir 223 | . 2 ⊢ (0 − 1) = (i · i) |
9 | 1, 8 | eqtr2i 2850 | 1 ⊢ (i · i) = -1 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 (class class class)co 6905 0cc0 10252 1c1 10253 ici 10254 + caddc 10255 · cmul 10257 − cmin 10585 -cneg 10586 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-8 2166 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5005 ax-nul 5013 ax-pow 5065 ax-pr 5127 ax-un 7209 ax-resscn 10309 ax-1cn 10310 ax-icn 10311 ax-addcl 10312 ax-addrcl 10313 ax-mulcl 10314 ax-mulrcl 10315 ax-mulcom 10316 ax-addass 10317 ax-mulass 10318 ax-distr 10319 ax-i2m1 10320 ax-1ne0 10321 ax-1rid 10322 ax-rnegex 10323 ax-rrecex 10324 ax-cnre 10325 ax-pre-lttri 10326 ax-pre-lttrn 10327 ax-pre-ltadd 10328 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3or 1112 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ne 3000 df-nel 3103 df-ral 3122 df-rex 3123 df-reu 3124 df-rab 3126 df-v 3416 df-sbc 3663 df-csb 3758 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-op 4404 df-uni 4659 df-br 4874 df-opab 4936 df-mpt 4953 df-id 5250 df-po 5263 df-so 5264 df-xp 5348 df-rel 5349 df-cnv 5350 df-co 5351 df-dm 5352 df-rn 5353 df-res 5354 df-ima 5355 df-iota 6086 df-fun 6125 df-fn 6126 df-f 6127 df-f1 6128 df-fo 6129 df-f1o 6130 df-fv 6131 df-riota 6866 df-ov 6908 df-oprab 6909 df-mpt2 6910 df-er 8009 df-en 8223 df-dom 8224 df-sdom 8225 df-pnf 10393 df-mnf 10394 df-ltxr 10396 df-sub 10587 df-neg 10588 |
This theorem is referenced by: recextlem1 10982 inelr 11340 cju 11346 irec 13258 i2 13259 crre 14231 remim 14234 remullem 14245 sqrtneglem 14384 absi 14403 sinhval 15256 coshval 15257 cosadd 15267 absefib 15300 efieq1re 15301 demoivreALT 15303 ncvspi 23325 cphipval2 23409 itgmulc2 23999 tanarg 24764 atandm2 25017 efiasin 25028 asinsinlem 25031 asinsin 25032 asin1 25034 efiatan 25052 atanlogsublem 25055 efiatan2 25057 2efiatan 25058 tanatan 25059 atantan 25063 atans2 25071 dvatan 25075 log2cnv 25084 nvpi 28066 ipasslem10 28238 polid2i 28558 lnophmlem2 29420 iexpire 32152 itgmulc2nc 34014 dvasin 34032 |
Copyright terms: Public domain | W3C validator |