ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-exp GIF version

Definition df-exp 10520
Description: Define exponentiation to nonnegative integer powers. For example, (5โ†‘2) = 25 (see ex-exp 14482).

This definition is not meant to be used directly; instead, exp0 10524 and expp1 10527 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 don't have superscripts.

10-Jun-2005: The definition was extended to include zero exponents, so that 0โ†‘0 = 1 per the convention of Definition 10-4.1 of [Gleason] p. 134 (see 0exp0e1 10525).

4-Jun-2014: The definition was extended to include negative integer exponents. For example, (-3โ†‘-2) = (1 / 9) (ex-exp 14482). The case ๐‘ฅ = 0, ๐‘ฆ < 0 gives the value (1 / 0), so we will avoid this case in our theorems. (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 10519 . 2 class โ†‘
2 vx . . 3 setvar ๐‘ฅ
3 vy . . 3 setvar ๐‘ฆ
4 cc 7809 . . 3 class โ„‚
5 cz 9253 . . 3 class โ„ค
63cv 1352 . . . . 5 class ๐‘ฆ
7 cc0 7811 . . . . 5 class 0
86, 7wceq 1353 . . . 4 wff ๐‘ฆ = 0
9 c1 7812 . . . 4 class 1
10 clt 7992 . . . . . 6 class <
117, 6, 10wbr 4004 . . . . 5 wff 0 < ๐‘ฆ
12 cmul 7816 . . . . . . 7 class ยท
13 cn 8919 . . . . . . . 8 class โ„•
142cv 1352 . . . . . . . . 9 class ๐‘ฅ
1514csn 3593 . . . . . . . 8 class {๐‘ฅ}
1613, 15cxp 4625 . . . . . . 7 class (โ„• ร— {๐‘ฅ})
1712, 16, 9cseq 10445 . . . . . 6 class seq1( ยท , (โ„• ร— {๐‘ฅ}))
186, 17cfv 5217 . . . . 5 class (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ)
196cneg 8129 . . . . . . 7 class -๐‘ฆ
2019, 17cfv 5217 . . . . . 6 class (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)
21 cdiv 8629 . . . . . 6 class /
229, 20, 21co 5875 . . . . 5 class (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ))
2311, 18, 22cif 3535 . . . 4 class if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)))
248, 9, 23cif 3535 . . 3 class if(๐‘ฆ = 0, 1, if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ))))
252, 3, 4, 5, 24cmpo 5877 . 2 class (๐‘ฅ โˆˆ โ„‚, ๐‘ฆ โˆˆ โ„ค โ†ฆ if(๐‘ฆ = 0, 1, if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)))))
261, 25wceq 1353 1 wff โ†‘ = (๐‘ฅ โˆˆ โ„‚, ๐‘ฆ โˆˆ โ„ค โ†ฆ if(๐‘ฆ = 0, 1, if(0 < ๐‘ฆ, (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜๐‘ฆ), (1 / (seq1( ยท , (โ„• ร— {๐‘ฅ}))โ€˜-๐‘ฆ)))))
Colors of variables: wff set class
This definition is referenced by:  exp3val  10522
  Copyright terms: Public domain W3C validator