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 11265 | . . 3 ⊢ 0 ∈ ℤ | |
2 | expval 12724 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) | |
3 | 1, 2 | mpan2 703 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) |
4 | eqid 2610 | . . 3 ⊢ 0 = 0 | |
5 | 4 | iftruei 4043 | . 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1 |
6 | 3, 5 | syl6eq 2660 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ifcif 4036 {csn 4125 class class class wbr 4583 × cxp 5036 ‘cfv 5804 (class class class)co 6549 ℂcc 9813 0cc0 9815 1c1 9816 · cmul 9820 < clt 9953 -cneg 10146 / cdiv 10563 ℕcn 10897 ℤcz 11254 seqcseq 12663 ↑cexp 12722 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-i2m1 9883 ax-1ne0 9884 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-iota 5768 df-fun 5806 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-neg 10148 df-z 11255 df-seq 12664 df-exp 12723 |
This theorem is referenced by: 0exp0e1 12727 expp1 12729 expneg 12730 expcllem 12733 mulexp 12761 expadd 12764 expmul 12767 leexp1a 12781 exple1 12782 bernneq 12852 modexp 12861 exp0d 12864 faclbnd4lem1 12942 faclbnd4lem3 12944 faclbnd4lem4 12945 cjexp 13738 absexp 13892 binom 14401 incexclem 14407 incexc 14408 climcndslem1 14420 fprodconst 14547 fallfac0 14598 bpoly0 14620 ege2le3 14659 eft0val 14681 demoivreALT 14770 pwp1fsum 14952 bits0 14988 0bits 14999 bitsinv1 15002 sadcadd 15018 smumullem 15052 numexp0 15618 psgnunilem4 17740 psgn0fv0 17754 psgnsn 17763 psgnprfval1 17765 cnfldexp 19598 expmhm 19634 expcn 22483 iblcnlem1 23360 itgcnlem 23362 dvexp 23522 dvexp2 23523 plyconst 23766 0dgr 23805 0dgrb 23806 aaliou3lem2 23902 cxp0 24216 1cubr 24369 log2ublem3 24475 basellem2 24608 basellem5 24611 lgsquad2lem2 24910 rusgranumwlk 26484 oddpwdc 29743 subfacval2 30423 fwddifn0 31441 stoweidlem19 38912 fmtno0 39990 pwdif 40039 bits0ALTV 40128 0dig2nn0e 42204 0dig2nn0o 42205 nn0sumshdiglemA 42211 nn0sumshdiglemB 42212 nn0sumshdiglem1 42213 nn0sumshdiglem2 42214 |
Copyright terms: Public domain | W3C validator |