dignn0fr

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

		Ref	Expression
	Assertion	dignn0fr	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to K digit (B) N = 0$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ B \in ℕ \to B \in ℕ$
2		eldifi	$⊢ K \in (ℤ ∖ ℕ_{0}) \to K \in ℤ$
3		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
4		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
5		elrege0	$⊢ N \in [0, +∞) \leftrightarrow (N \in ℝ \land 0 \leq N)$
6	3 4 5	sylanbrc	$⊢ N \in ℕ_{0} \to N \in [0, +∞)$
7		digval	$⊢ (B \in ℕ \land K \in ℤ \land N \in [0, +∞)) \to K digit (B) N = ⌊B^{- K} \cdot N⌋ \mod B$
8	1 2 6 7	syl3an	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to K digit (B) N = ⌊B^{- K} \cdot N⌋ \mod B$
9		nnz	$⊢ B \in ℕ \to B \in ℤ$
10		eldif	$⊢ K \in (ℤ ∖ ℕ_{0}) \leftrightarrow (K \in ℤ \land \neg K \in ℕ_{0})$
11		znnn0nn	$⊢ (K \in ℤ \land \neg K \in ℕ_{0}) \to - K \in ℕ$
12	10 11	sylbi	$⊢ K \in (ℤ ∖ ℕ_{0}) \to - K \in ℕ$
13	12	nnnn0d	$⊢ K \in (ℤ ∖ ℕ_{0}) \to - K \in ℕ_{0}$
14		zexpcl	$⊢ (B \in ℤ \land - K \in ℕ_{0}) \to B^{- K} \in ℤ$
15	9 13 14	syl2an	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0})) \to B^{- K} \in ℤ$
16	15	3adant3	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K} \in ℤ$
17		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
18	17	3ad2ant3	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to N \in ℤ$
19	16 18	zmulcld	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K} \cdot N \in ℤ$
20		flid	$⊢ B^{- K} \cdot N \in ℤ \to ⌊B^{- K} \cdot N⌋ = B^{- K} \cdot N$
21	19 20	syl	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to ⌊B^{- K} \cdot N⌋ = B^{- K} \cdot N$
22	21	oveq1d	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to ⌊B^{- K} \cdot N⌋ \mod B = B^{- K} \cdot N \mod B$
23		nnre	$⊢ B \in ℕ \to B \in ℝ$
24		reexpcl	$⊢ (B \in ℝ \land - K \in ℕ_{0}) \to B^{- K} \in ℝ$
25	23 13 24	syl2an	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0})) \to B^{- K} \in ℝ$
26	25	recnd	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0})) \to B^{- K} \in ℂ$
27	26	3adant3	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K} \in ℂ$
28		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
29	28	3ad2ant3	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to N \in ℂ$
30		nncn	$⊢ B \in ℕ \to B \in ℂ$
31		nnne0	$⊢ B \in ℕ \to B \neq 0$
32	30 31	jca	$⊢ B \in ℕ \to (B \in ℂ \land B \neq 0)$
33	32	3ad2ant1	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to (B \in ℂ \land B \neq 0)$
34		div23	$⊢ (B^{- K} \in ℂ \land N \in ℂ \land (B \in ℂ \land B \neq 0)) \to \frac{B^{- K} \cdot N}{B} = (\frac{B^{- K}}{B}) \cdot N$
35	27 29 33 34	syl3anc	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to \frac{B^{- K} \cdot N}{B} = (\frac{B^{- K}}{B}) \cdot N$
36	30	3ad2ant1	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B \in ℂ$
37	31	3ad2ant1	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B \neq 0$
38	12	nnzd	$⊢ K \in (ℤ ∖ ℕ_{0}) \to - K \in ℤ$
39	38	3ad2ant2	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to - K \in ℤ$
40	36 37 39	expm1d	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K - 1} = \frac{B^{- K}}{B}$
41	40	eqcomd	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to \frac{B^{- K}}{B} = B^{- K - 1}$
42	41	oveq1d	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to (\frac{B^{- K}}{B}) \cdot N = B^{- K - 1} \cdot N$
43	35 42	eqtrd	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to \frac{B^{- K} \cdot N}{B} = B^{- K - 1} \cdot N$
44		nnm1nn0	$⊢ - K \in ℕ \to - K - 1 \in ℕ_{0}$
45	12 44	syl	$⊢ K \in (ℤ ∖ ℕ_{0}) \to - K - 1 \in ℕ_{0}$
46		zexpcl	$⊢ (B \in ℤ \land - K - 1 \in ℕ_{0}) \to B^{- K - 1} \in ℤ$
47	9 45 46	syl2an	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0})) \to B^{- K - 1} \in ℤ$
48	47	3adant3	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K - 1} \in ℤ$
49	48 18	zmulcld	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K - 1} \cdot N \in ℤ$
50	43 49	eqeltrd	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to \frac{B^{- K} \cdot N}{B} \in ℤ$
51	25	3adant3	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K} \in ℝ$
52	3	3ad2ant3	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to N \in ℝ$
53	51 52	remulcld	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K} \cdot N \in ℝ$
54		nnrp	$⊢ B \in ℕ \to B \in ℝ^{+}$
55	54	3ad2ant1	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B \in ℝ^{+}$
56		mod0	$⊢ (B^{- K} \cdot N \in ℝ \land B \in ℝ^{+}) \to (B^{- K} \cdot N \mod B = 0 \leftrightarrow \frac{B^{- K} \cdot N}{B} \in ℤ)$
57	53 55 56	syl2anc	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to (B^{- K} \cdot N \mod B = 0 \leftrightarrow \frac{B^{- K} \cdot N}{B} \in ℤ)$
58	50 57	mpbird	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to B^{- K} \cdot N \mod B = 0$
59	22 58	eqtrd	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to ⌊B^{- K} \cdot N⌋ \mod B = 0$
60	8 59	eqtrd	$⊢ (B \in ℕ \land K \in (ℤ ∖ ℕ_{0}) \land N \in ℕ_{0}) \to K digit (B) N = 0$

Metamath Proof Explorer

Theorem dignn0fr

Proof