Metamath Proof Explorer

Definition df-dig

Description: Definition of an operation to obtain the k th digit of a nonnegative real number r in the positional system with base b . k = - 1 corresponds to the first digit of the fractional part (for b = 10 the first digit after the decimal point), k = 0 corresponds to the last digit of the integer part (for b = 10 the first digit before the decimal point). See also digit1 . Examples (not formal): ( 234.567 ( digit `10 ) 0 ) = 4; ( 2.567 ( digit10 ) -2 ) = 6; ( 2345.67 ( digit` 10 ) 2 ) = 3. (Contributed by AV, 16-May-2020)

Ref Expression
Assertion df-dig ⊢digit=b∈ℕ⟼k∈ℤ,r∈0+∞⟼b−k⁢rmodb

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdig classdigit
1 vb setvarb
2 cn classℕ
3 vk setvark
4 cz classℤ
5 vr setvarr
6 cc0 class0
7 cico class.
8 cpnf class+∞
9 6 8 7 co class0+∞
10 cfl class.
11 1 cv setvarb
12 cexp class^
13 3 cv setvark
14 13 cneg class−k
15 11 14 12 co classb−k
16 cmul class×
17 5 cv setvarr
18 15 17 16 co classb−k⁢r
19 18 10 cfv classb−k⁢r
20 cmo classmod
21 19 11 20 co classb−k⁢rmodb
22 3 5 4 9 21 cmpo classk∈ℤ,r∈0+∞⟼b−k⁢rmodb
23 1 2 22 cmpt classb∈ℕ⟼k∈ℤ,r∈0+∞⟼b−k⁢rmodb
24 0 23 wceq wffdigit=b∈ℕ⟼k∈ℤ,r∈0+∞⟼b−k⁢rmodb