| 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 zeroth power. Under our definition, 0↑0 = 1 (0exp0e1 14107), following standard convention, for instance 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 12624 | . . 3 ⊢ 0 ∈ ℤ | |
| 2 | expval 14104 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) | |
| 3 | 1, 2 | mpan2 691 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) |
| 4 | eqid 2737 | . . 3 ⊢ 0 = 0 | |
| 5 | 4 | iftruei 4532 | . 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1 |
| 6 | 3, 5 | eqtrdi 2793 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ifcif 4525 {csn 4626 class class class wbr 5143 × cxp 5683 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 0cc0 11155 1c1 11156 · cmul 11160 < clt 11295 -cneg 11493 / cdiv 11920 ℕcn 12266 ℤcz 12613 seqcseq 14042 ↑cexp 14102 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-1cn 11213 ax-addrcl 11216 ax-rnegex 11226 ax-cnre 11228 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-iota 6514 df-fun 6563 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-neg 11495 df-z 12614 df-seq 14043 df-exp 14103 |
| This theorem is referenced by: 0exp0e1 14107 expp1 14109 expneg 14110 expcllem 14113 mulexp 14142 expadd 14145 expmul 14148 exp0d 14180 leexp1a 14215 exple1 14216 bernneq 14268 modexp 14277 faclbnd4lem1 14332 faclbnd4lem3 14334 faclbnd4lem4 14335 cjexp 15189 absexp 15343 binom 15866 incexclem 15872 incexc 15873 climcndslem1 15885 pwdif 15904 fprodconst 16014 fallfac0 16064 bpoly0 16086 ege2le3 16126 eft0val 16148 demoivreALT 16237 pwp1fsum 16428 bits0 16465 0bits 16476 bitsinv1 16479 sadcadd 16495 smumullem 16529 numexp0 17113 psgnunilem4 19515 psgn0fv0 19529 psgnsn 19538 psgnprfval1 19540 cnfldexp 21417 expmhm 21454 expcn 24896 expcnOLD 24898 iblcnlem1 25823 itgcnlem 25825 dvexp 25991 dvexp2 25992 plyconst 26245 0dgr 26284 0dgrb 26285 aaliou3lem2 26385 cxp0 26712 1cubr 26885 log2ublem3 26991 basellem2 27125 basellem5 27128 lgsquad2lem2 27429 0dp2dp 32891 fldext2chn 33769 oddpwdc 34356 breprexp 34648 subfacval2 35192 fwddifn0 36165 stoweidlem19 46034 fmtno0 47527 bits0ALTV 47666 0dig2nn0e 48533 0dig2nn0o 48534 nn0sumshdiglemA 48540 nn0sumshdiglemB 48541 nn0sumshdiglem1 48542 nn0sumshdiglem2 48543 |
| Copyright terms: Public domain | W3C validator |