digit1

Description: Two ways to express the K th digit in the decimal expansion of a number A (when base B = 1 0 ). K = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 3-Jan-2009)

		Ref	Expression
	Assertion	digit1	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ \mod B = (⌊B^{K} A⌋ \mod B^{K}) - (B ⌊B^{K - 1} A⌋ \mod B^{K})$

Proof

Step	Hyp	Ref	Expression
1		digit2	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ \mod B = ⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋$
2	1	3coml	$⊢ (B \in ℕ \land K \in ℕ \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B = ⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋$
3	2	3expa	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B = ⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋$
4	3	oveq1d	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to (⌊B^{K} A⌋ \mod B) \mod B^{K} = (⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋) \mod B^{K}$
5		nnre	$⊢ B \in ℕ \to B \in ℝ$
6		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
7		reexpcl	$⊢ (B \in ℝ \land K \in ℕ_{0}) \to B^{K} \in ℝ$
8	5 6 7	syl2an	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K} \in ℝ$
9		remulcl	$⊢ (B^{K} \in ℝ \land A \in ℝ) \to B^{K} A \in ℝ$
10	8 9	sylan	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K} A \in ℝ$
11		reflcl	$⊢ B^{K} A \in ℝ \to ⌊B^{K} A⌋ \in ℝ$
12	10 11	syl	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ \in ℝ$
13		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
14	13	ad2antrr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B \in ℝ^{+}$
15	12 14	modcld	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B \in ℝ$
16		nnexpcl	$⊢ (B \in ℕ \land K \in ℕ_{0}) \to B^{K} \in ℕ$
17	6 16	sylan2	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K} \in ℕ$
18	17	nnrpd	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K} \in ℝ^{+}$
19	18	adantr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K} \in ℝ^{+}$
20		modge0	$⊢ (⌊B^{K} A⌋ \in ℝ \land B \in ℝ^{+}) \to 0 \leq ⌊B^{K} A⌋ \mod B$
21	12 14 20	syl2anc	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to 0 \leq ⌊B^{K} A⌋ \mod B$
22	5	ad2antrr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B \in ℝ$
23	8	adantr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K} \in ℝ$
24		modlt	$⊢ (⌊B^{K} A⌋ \in ℝ \land B \in ℝ^{+}) \to ⌊B^{K} A⌋ \mod B < B$
25	12 14 24	syl2anc	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B < B$
26		nncn	$⊢ B \in ℕ \to B \in ℂ$
27		exp1	$⊢ B \in ℂ \to B^{1} = B$
28	26 27	syl	$⊢ B \in ℕ \to B^{1} = B$
29	28	adantr	$⊢ (B \in ℕ \land K \in ℕ) \to B^{1} = B$
30	5	adantr	$⊢ (B \in ℕ \land K \in ℕ) \to B \in ℝ$
31		nnge1	$⊢ B \in ℕ \to 1 \leq B$
32	31	adantr	$⊢ (B \in ℕ \land K \in ℕ) \to 1 \leq B$
33		simpr	$⊢ (B \in ℕ \land K \in ℕ) \to K \in ℕ$
34		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
35	33 34	eleqtrdi	$⊢ (B \in ℕ \land K \in ℕ) \to K \in ℤ_{\geq 1}$
36		leexp2a	$⊢ (B \in ℝ \land 1 \leq B \land K \in ℤ_{\geq 1}) \to B^{1} \leq B^{K}$
37	30 32 35 36	syl3anc	$⊢ (B \in ℕ \land K \in ℕ) \to B^{1} \leq B^{K}$
38	29 37	eqbrtrrd	$⊢ (B \in ℕ \land K \in ℕ) \to B \leq B^{K}$
39	38	adantr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B \leq B^{K}$
40	15 22 23 25 39	ltletrd	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B < B^{K}$
41		modid	$⊢ ((⌊B^{K} A⌋ \mod B \in ℝ \land B^{K} \in ℝ^{+}) \land (0 \leq ⌊B^{K} A⌋ \mod B \land ⌊B^{K} A⌋ \mod B < B^{K})) \to (⌊B^{K} A⌋ \mod B) \mod B^{K} = ⌊B^{K} A⌋ \mod B$
42	15 19 21 40 41	syl22anc	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to (⌊B^{K} A⌋ \mod B) \mod B^{K} = ⌊B^{K} A⌋ \mod B$
43		simpll	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B \in ℕ$
44		nnm1nn0	$⊢ K \in ℕ \to K - 1 \in ℕ_{0}$
45		reexpcl	$⊢ (B \in ℝ \land K - 1 \in ℕ_{0}) \to B^{K - 1} \in ℝ$
46	5 44 45	syl2an	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K - 1} \in ℝ$
47		remulcl	$⊢ (B^{K - 1} \in ℝ \land A \in ℝ) \to B^{K - 1} A \in ℝ$
48	46 47	sylan	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K - 1} A \in ℝ$
49		nnexpcl	$⊢ (B \in ℕ \land K - 1 \in ℕ_{0}) \to B^{K - 1} \in ℕ$
50	44 49	sylan2	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K - 1} \in ℕ$
51	50	adantr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K - 1} \in ℕ$
52		modmulnn	$⊢ (B \in ℕ \land B^{K - 1} A \in ℝ \land B^{K - 1} \in ℕ) \to B ⌊B^{K - 1} A⌋ \mod B B^{K - 1} \leq ⌊B B^{K - 1} A⌋ \mod B B^{K - 1}$
53	43 48 51 52	syl3anc	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B ⌊B^{K - 1} A⌋ \mod B B^{K - 1} \leq ⌊B B^{K - 1} A⌋ \mod B B^{K - 1}$
54		expm1t	$⊢ (B \in ℂ \land K \in ℕ) \to B^{K} = B^{K - 1} B$
55		expcl	$⊢ (B \in ℂ \land K - 1 \in ℕ_{0}) \to B^{K - 1} \in ℂ$
56	44 55	sylan2	$⊢ (B \in ℂ \land K \in ℕ) \to B^{K - 1} \in ℂ$
57		simpl	$⊢ (B \in ℂ \land K \in ℕ) \to B \in ℂ$
58	56 57	mulcomd	$⊢ (B \in ℂ \land K \in ℕ) \to B^{K - 1} B = B B^{K - 1}$
59	54 58	eqtrd	$⊢ (B \in ℂ \land K \in ℕ) \to B^{K} = B B^{K - 1}$
60	26 59	sylan	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K} = B B^{K - 1}$
61	60	adantr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K} = B B^{K - 1}$
62	61	oveq2d	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B ⌊B^{K - 1} A⌋ \mod B^{K} = B ⌊B^{K - 1} A⌋ \mod B B^{K - 1}$
63	61	oveq1d	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K} A = B B^{K - 1} A$
64	26	ad2antrr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B \in ℂ$
65	26 44 55	syl2an	$⊢ (B \in ℕ \land K \in ℕ) \to B^{K - 1} \in ℂ$
66	65	adantr	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K - 1} \in ℂ$
67		recn	$⊢ A \in ℝ \to A \in ℂ$
68	67	adantl	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to A \in ℂ$
69	64 66 68	mulassd	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B B^{K - 1} A = B B^{K - 1} A$
70	63 69	eqtrd	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B^{K} A = B B^{K - 1} A$
71	70	fveq2d	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ = ⌊B B^{K - 1} A⌋$
72	71 61	oveq12d	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B^{K} = ⌊B B^{K - 1} A⌋ \mod B B^{K - 1}$
73	53 62 72	3brtr4d	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B ⌊B^{K - 1} A⌋ \mod B^{K} \leq ⌊B^{K} A⌋ \mod B^{K}$
74		reflcl	$⊢ B^{K - 1} A \in ℝ \to ⌊B^{K - 1} A⌋ \in ℝ$
75	48 74	syl	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K - 1} A⌋ \in ℝ$
76		remulcl	$⊢ (B \in ℝ \land ⌊B^{K - 1} A⌋ \in ℝ) \to B ⌊B^{K - 1} A⌋ \in ℝ$
77	22 75 76	syl2anc	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to B ⌊B^{K - 1} A⌋ \in ℝ$
78		modsubdir	$⊢ (⌊B^{K} A⌋ \in ℝ \land B ⌊B^{K - 1} A⌋ \in ℝ \land B^{K} \in ℝ^{+}) \to (B ⌊B^{K - 1} A⌋ \mod B^{K} \leq ⌊B^{K} A⌋ \mod B^{K} \leftrightarrow (⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋) \mod B^{K} = (⌊B^{K} A⌋ \mod B^{K}) - (B ⌊B^{K - 1} A⌋ \mod B^{K}))$
79	12 77 19 78	syl3anc	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to (B ⌊B^{K - 1} A⌋ \mod B^{K} \leq ⌊B^{K} A⌋ \mod B^{K} \leftrightarrow (⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋) \mod B^{K} = (⌊B^{K} A⌋ \mod B^{K}) - (B ⌊B^{K - 1} A⌋ \mod B^{K}))$
80	73 79	mpbid	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to (⌊B^{K} A⌋ - B ⌊B^{K - 1} A⌋) \mod B^{K} = (⌊B^{K} A⌋ \mod B^{K}) - (B ⌊B^{K - 1} A⌋ \mod B^{K})$
81	4 42 80	3eqtr3d	$⊢ ((B \in ℕ \land K \in ℕ) \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B = (⌊B^{K} A⌋ \mod B^{K}) - (B ⌊B^{K - 1} A⌋ \mod B^{K})$
82	81	3impa	$⊢ (B \in ℕ \land K \in ℕ \land A \in ℝ) \to ⌊B^{K} A⌋ \mod B = (⌊B^{K} A⌋ \mod B^{K}) - (B ⌊B^{K - 1} A⌋ \mod B^{K})$
83	82	3comr	$⊢ (A \in ℝ \land B \in ℕ \land K \in ℕ) \to ⌊B^{K} A⌋ \mod B = (⌊B^{K} A⌋ \mod B^{K}) - (B ⌊B^{K - 1} A⌋ \mod B^{K})$

Metamath Proof Explorer

Theorem digit1

Proof