Theorem 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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod 𝐵 ) = ( ( ( ⌊ ‘ ( ( 𝐵 ↑ 𝐾 ) · 𝐴 ) ) mod ( 𝐵 ↑ 𝐾 ) ) − ( ( 𝐵 · ( ⌊ ‘ ( ( 𝐵 ↑ ( 𝐾 − 1 ) ) · 𝐴 ) ) ) mod ( 𝐵 ↑ 𝐾 ) ) ) )

Proof

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