![]() |
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 11739 | . . 3 ⊢ 0 ∈ ℤ | |
2 | expval 13180 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℤ) → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) | |
3 | 1, 2 | mpan2 681 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0))))) |
4 | eqid 2778 | . . 3 ⊢ 0 = 0 | |
5 | 4 | iftruei 4314 | . 2 ⊢ if(0 = 0, 1, if(0 < 0, (seq1( · , (ℕ × {𝐴}))‘0), (1 / (seq1( · , (ℕ × {𝐴}))‘-0)))) = 1 |
6 | 3, 5 | syl6eq 2830 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴↑0) = 1) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2107 ifcif 4307 {csn 4398 class class class wbr 4886 × cxp 5353 ‘cfv 6135 (class class class)co 6922 ℂcc 10270 0cc0 10272 1c1 10273 · cmul 10277 < clt 10411 -cneg 10607 / cdiv 11032 ℕcn 11374 ℤcz 11728 seqcseq 13119 ↑cexp 13178 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 ax-1cn 10330 ax-addrcl 10333 ax-rnegex 10343 ax-cnre 10345 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-mpt 4966 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-iota 6099 df-fun 6137 df-fv 6143 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-neg 10609 df-z 11729 df-seq 13120 df-exp 13179 |
This theorem is referenced by: 0exp0e1 13183 expp1 13185 expneg 13186 expcllem 13189 mulexp 13217 expadd 13220 expmul 13223 leexp1a 13237 exple1 13238 bernneq 13309 modexp 13318 exp0d 13321 faclbnd4lem1 13398 faclbnd4lem3 13400 faclbnd4lem4 13401 cjexp 14297 absexp 14451 binom 14966 incexclem 14972 incexc 14973 climcndslem1 14985 fprodconst 15111 fallfac0 15161 bpoly0 15183 ege2le3 15222 eft0val 15244 demoivreALT 15333 pwp1fsum 15521 bits0 15556 0bits 15567 bitsinv1 15570 sadcadd 15586 smumullem 15620 numexp0 16184 psgnunilem4 18301 psgn0fv0 18315 psgnsn 18324 psgnprfval1 18326 cnfldexp 20175 expmhm 20211 expcn 23083 iblcnlem1 23991 itgcnlem 23993 dvexp 24153 dvexp2 24154 plyconst 24399 0dgr 24438 0dgrb 24439 aaliou3lem2 24535 cxp0 24853 1cubr 25020 log2ublem3 25127 basellem2 25260 basellem5 25263 lgsquad2lem2 25562 0dp2dp 30179 oddpwdc 31014 breprexp 31313 subfacval2 31768 fwddifn0 32860 stoweidlem19 41163 fmtno0 42473 pwdif 42522 bits0ALTV 42615 0dig2nn0e 43421 0dig2nn0o 43422 nn0sumshdiglemA 43428 nn0sumshdiglemB 43429 nn0sumshdiglem1 43430 nn0sumshdiglem2 43431 |
Copyright terms: Public domain | W3C validator |