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 ⁢ r mod b

Detailed syntax breakdown

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