Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > exp0 | Structured version Visualization version GIF version |
Description: Value of a complex number raised to the 0th power. Note that under our definition, 0↑0 = 1, following the convention used by Gleason. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by NM, 20-May-2004.) (Revised by Mario Carneiro, 4-Jun-2014.) |
Ref | Expression |
---|---|
exp0 | ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0z 11980 | . . 3 ⊢ 0 ∈ ℤ | |
2 | expval 13419 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) | |
3 | 1, 2 | mpan2 687 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) |
4 | eqid 2818 | . . 3 ⊢ 0 = 0 | |
5 | 4 | iftruei 4470 | . 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1 |
6 | 3, 5 | syl6eq 2869 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ifcif 4463 {csn 4557 class class class wbr 5057 × cxp 5546 ‘cfv 6348 (class class class)co 7145 ℂcc 10523 0cc0 10525 1c1 10526 · cmul 10530 < clt 10663 -cneg 10859 / cdiv 11285 ℕcn 11626 ℤcz 11969 seqcseq 13357 ↑cexp 13417 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 ax-1cn 10583 ax-addrcl 10586 ax-rnegex 10596 ax-cnre 10598 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-iota 6307 df-fun 6350 df-fv 6356 df-ov 7148 df-oprab 7149 df-mpo 7150 df-wrecs 7936 df-recs 7997 df-rdg 8035 df-neg 10861 df-z 11970 df-seq 13358 df-exp 13418 |
This theorem is referenced by: 0exp0e1 13422 expp1 13424 expneg 13425 expcllem 13428 mulexp 13456 expadd 13459 expmul 13462 exp0d 13492 leexp1a 13527 exple1 13528 bernneq 13578 modexp 13587 faclbnd4lem1 13641 faclbnd4lem3 13643 faclbnd4lem4 13644 cjexp 14497 absexp 14652 binom 15173 incexclem 15179 incexc 15180 climcndslem1 15192 pwdif 15211 fprodconst 15320 fallfac0 15370 bpoly0 15392 ege2le3 15431 eft0val 15453 demoivreALT 15542 pwp1fsum 15730 bits0 15765 0bits 15776 bitsinv1 15779 sadcadd 15795 smumullem 15829 numexp0 16400 psgnunilem4 18554 psgn0fv0 18568 psgnsn 18577 psgnprfval1 18579 cnfldexp 20506 expmhm 20542 expcn 23407 iblcnlem1 24315 itgcnlem 24317 dvexp 24477 dvexp2 24478 plyconst 24723 0dgr 24762 0dgrb 24763 aaliou3lem2 24859 cxp0 25180 1cubr 25347 log2ublem3 25453 basellem2 25586 basellem5 25589 lgsquad2lem2 25888 0dp2dp 30512 oddpwdc 31511 breprexp 31803 subfacval2 32331 fwddifn0 33522 stoweidlem19 42181 fmtno0 43579 bits0ALTV 43721 0dig2nn0e 44600 0dig2nn0o 44601 nn0sumshdiglemA 44607 nn0sumshdiglemB 44608 nn0sumshdiglem1 44609 nn0sumshdiglem2 44610 |
Copyright terms: Public domain | W3C validator |