MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-exp Structured version   Visualization version   GIF version

Definition df-exp 14031
Description: Define exponentiation of complex numbers with integer exponents. For example, (5โ†‘2) = 25 (ex-exp 30208). Terminology: In general, "exponentiation" is the operation of raising a "base" ๐‘ฅ to the power of the "exponent" ๐‘ฆ, resulting in the "power" (๐‘ฅโ†‘๐‘ฆ), also called "x to the power of y". In this case, "integer exponentiation" is the operation of raising a complex "base" ๐‘ฅ to the power of an integer ๐‘ฆ, resulting in the "integer power" (๐‘ฅโ†‘๐‘ฆ).

This definition is not meant to be used directly; instead, exp0 14034 and expp1 14037 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we do not have superscripts.

10-Jun-2005: The definition was extended from positive exponents to nonegative exponent, so that 0โ†‘0 = 1, following standard convention, for instance Definition 10-4.1 of [Gleason] p. 134 (0exp0e1 14035).

4-Jun-2014: The definition was extended to integer exponents. For example, (-3โ†‘-2) = (1 / 9) (ex-exp 30208). The case ๐‘ฅ = 0, ๐‘ฆ < 0 gives the "value" (1 / 0); relying on this should be avoided in applications.

For a definition of exponentiation including complex exponents see df-cxp 26442 (complex exponentiation). Both definitions are equivalent for integer exponents, see cxpexpz 26552. (Contributed by Raph Levien, 20-May-2004.) (Revised by NM, 15-Oct-2004.)

Assertion
Ref Expression
df-exp โ†‘ = (๐‘ฅ โˆˆ โ„‚, ๐‘ฆ โˆˆ โ„ค โ†ฆ if(๐‘ฆ = 0, 1, if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)))))
Distinct variable group:   ๐‘ฅ,๐‘ฆ

Detailed syntax breakdown of Definition df-exp
StepHypRef Expression
1 cexp 14030 . 2 class โ†‘
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 cc 11107 . . 3 class โ„‚
5 cz 12559 . . 3 class โ„ค
63cv 1532 . . . . 5 class ๐‘ฆ
7 cc0 11109 . . . . 5 class 0
86, 7wceq 1533 . . . 4 wff ๐‘ฆ = 0
9 c1 11110 . . . 4 class 1
10 clt 11249 . . . . . 6 class <
117, 6, 10wbr 5141 . . . . 5 wff 0 < ๐‘ฆ
12 cmul 11114 . . . . . . 7 class ยท
13 cn 12213 . . . . . . . 8 class โ„•
142cv 1532 . . . . . . . . 9 class ๐‘ฅ
1514csn 4623 . . . . . . . 8 class {๐‘ฅ}
1613, 15cxp 5667 . . . . . . 7 class (โ„• ร— {๐‘ฅ})
1712, 16, 9cseq 13969 . . . . . 6 class seq1( ยท , (โ„• ร— {๐‘ฅ}))
186, 17cfv 6536 . . . . 5 class (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ)
196cneg 11446 . . . . . . 7 class -๐‘ฆ
2019, 17cfv 6536 . . . . . 6 class (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)
21 cdiv 11872 . . . . . 6 class /
229, 20, 21co 7404 . . . . 5 class (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ))
2311, 18, 22cif 4523 . . . 4 class if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)))
248, 9, 23cif 4523 . . 3 class if(๐‘ฆ = 0, 1, if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ))))
252, 3, 4, 5, 24cmpo 7406 . 2 class (๐‘ฅ โˆˆ โ„‚, ๐‘ฆ โˆˆ โ„ค โ†ฆ if(๐‘ฆ = 0, 1, if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)))))
261, 25wceq 1533 1 wff โ†‘ = (๐‘ฅ โˆˆ โ„‚, ๐‘ฆ โˆˆ โ„ค โ†ฆ if(๐‘ฆ = 0, 1, if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)))))
Colors of variables: wff setvar class
This definition is referenced by:  expval  14032
  Copyright terms: Public domain W3C validator