Theorem dignn0fr

Description: The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020)

	Ref	Expression
Assertion	dignn0fr	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑁 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ )
2		eldifi	⊢ ( 𝐾 ∈ ( ℤ ∖ ℕ0 ) → 𝐾 ∈ ℤ )
3		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
4		nn0ge0	⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
5		elrege0	⊢ ( 𝑁 ∈ ( 0 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 0 ≤ 𝑁 ) )
6	3 4 5	sylanbrc	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 [,) +∞ ) )
7		digval	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ( 0 [,) +∞ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑁 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ) mod 𝐵 ) )
8	1 2 6 7	syl3an	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑁 ) = ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ) mod 𝐵 ) )
9		nnz	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
10		eldif	⊢ ( 𝐾 ∈ ( ℤ ∖ ℕ0 ) ↔ ( 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ℕ0 ) )
11		znnn0nn	⊢ ( ( 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ ℕ0 ) → - 𝐾 ∈ ℕ )
12	10 11	sylbi	⊢ ( 𝐾 ∈ ( ℤ ∖ ℕ0 ) → - 𝐾 ∈ ℕ )
13	12	nnnn0d	⊢ ( 𝐾 ∈ ( ℤ ∖ ℕ0 ) → - 𝐾 ∈ ℕ0 )
14		zexpcl	⊢ ( ( 𝐵 ∈ ℤ ∧ - 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℤ )
15	9 13 14	syl2an	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℤ )
16	15	3adant3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℤ )
17		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
18	17	3ad2ant3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
19	16 18	zmulcld	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ∈ ℤ )
20		flid	⊢ ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ∈ ℤ → ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ) = ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) )
21	19 20	syl	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ) = ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) )
22	21	oveq1d	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ) mod 𝐵 ) = ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) mod 𝐵 ) )
23		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
24		reexpcl	⊢ ( ( 𝐵 ∈ ℝ ∧ - 𝐾 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℝ )
25	23 13 24	syl2an	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℝ )
26	25	recnd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℂ )
27	26	3adant3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℂ )
28		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
29	28	3ad2ant3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
30		nncn	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℂ )
31		nnne0	⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
32	30 31	jca	⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
33	32	3ad2ant1	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) )
34		div23	⊢ ( ( ( 𝐵 ↑ - 𝐾 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) / 𝐵 ) = ( ( ( 𝐵 ↑ - 𝐾 ) / 𝐵 ) · 𝑁 ) )
35	27 29 33 34	syl3anc	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) / 𝐵 ) = ( ( ( 𝐵 ↑ - 𝐾 ) / 𝐵 ) · 𝑁 ) )
36	30	3ad2ant1	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
37	31	3ad2ant1	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ≠ 0 )
38	12	nnzd	⊢ ( 𝐾 ∈ ( ℤ ∖ ℕ0 ) → - 𝐾 ∈ ℤ )
39	38	3ad2ant2	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → - 𝐾 ∈ ℤ )
40	36 37 39	expm1d	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ ( - 𝐾 − 1 ) ) = ( ( 𝐵 ↑ - 𝐾 ) / 𝐵 ) )
41	40	eqcomd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐵 ↑ - 𝐾 ) / 𝐵 ) = ( 𝐵 ↑ ( - 𝐾 − 1 ) ) )
42	41	oveq1d	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐵 ↑ - 𝐾 ) / 𝐵 ) · 𝑁 ) = ( ( 𝐵 ↑ ( - 𝐾 − 1 ) ) · 𝑁 ) )
43	35 42	eqtrd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) / 𝐵 ) = ( ( 𝐵 ↑ ( - 𝐾 − 1 ) ) · 𝑁 ) )
44		nnm1nn0	⊢ ( - 𝐾 ∈ ℕ → ( - 𝐾 − 1 ) ∈ ℕ0 )
45	12 44	syl	⊢ ( 𝐾 ∈ ( ℤ ∖ ℕ0 ) → ( - 𝐾 − 1 ) ∈ ℕ0 )
46		zexpcl	⊢ ( ( 𝐵 ∈ ℤ ∧ ( - 𝐾 − 1 ) ∈ ℕ0 ) → ( 𝐵 ↑ ( - 𝐾 − 1 ) ) ∈ ℤ )
47	9 45 46	syl2an	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ) → ( 𝐵 ↑ ( - 𝐾 − 1 ) ) ∈ ℤ )
48	47	3adant3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ ( - 𝐾 − 1 ) ) ∈ ℤ )
49	48 18	zmulcld	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐵 ↑ ( - 𝐾 − 1 ) ) · 𝑁 ) ∈ ℤ )
50	43 49	eqeltrd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) / 𝐵 ) ∈ ℤ )
51	25	3adant3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐵 ↑ - 𝐾 ) ∈ ℝ )
52	3	3ad2ant3	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
53	51 52	remulcld	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ∈ ℝ )
54		nnrp	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ+ )
55	54	3ad2ant1	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → 𝐵 ∈ ℝ+ )
56		mod0	⊢ ( ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) mod 𝐵 ) = 0 ↔ ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) / 𝐵 ) ∈ ℤ ) )
57	53 55 56	syl2anc	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) mod 𝐵 ) = 0 ↔ ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) / 𝐵 ) ∈ ℤ ) )
58	50 57	mpbird	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) mod 𝐵 ) = 0 )
59	22 58	eqtrd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( ⌊ ‘ ( ( 𝐵 ↑ - 𝐾 ) · 𝑁 ) ) mod 𝐵 ) = 0 )
60	8 59	eqtrd	⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ( digit ‘ 𝐵 ) 𝑁 ) = 0 )