snmlval

Description: The property " A is simply normal in base R ". A number is simply normal if each digit 0 <_ b < R occurs in the base- R digit string of A with frequency 1 / R (which is consistent with the expectation in an infinite random string of numbers selected from 0 ... R - 1 ). (Contributed by Mario Carneiro, 6-Apr-2015)

		Ref	Expression
	Hypothesis	snml.s	$⊢ S = (r \in ℤ_{\geq 2} ⟼ \{x \in ℝ \| \forall b \in (0 \dots r - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) ⇝ (\frac{1}{r})\})$
	Assertion	snmlval	$⊢ A \in S (R) \leftrightarrow (R \in ℤ_{\geq 2} \land A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$

Proof

Step	Hyp	Ref	Expression
1		snml.s	$⊢ S = (r \in ℤ_{\geq 2} ⟼ \{x \in ℝ \| \forall b \in (0 \dots r - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) ⇝ (\frac{1}{r})\})$
2		oveq1	$⊢ r = R \to r - 1 = R - 1$
3	2	oveq2d	$⊢ r = R \to (0 \dots r - 1) = (0 \dots R - 1)$
4		oveq1	$⊢ r = R \to r^{k} = R^{k}$
5	4	oveq2d	$⊢ r = R \to x r^{k} = x R^{k}$
6		id	$⊢ r = R \to r = R$
7	5 6	oveq12d	$⊢ r = R \to x r^{k} \mod r = x R^{k} \mod R$
8	7	fveqeq2d	$⊢ r = R \to (⌊x r^{k} \mod r⌋ = b \leftrightarrow ⌊x R^{k} \mod R⌋ = b)$
9	8	rabbidv	$⊢ r = R \to \{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\} = \{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}$
10	9	fveq2d	$⊢ r = R \to \|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\| = \|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|$
11	10	oveq1d	$⊢ r = R \to \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n} = \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}$
12	11	mpteq2dv	$⊢ r = R \to (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) = (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n})$
13		oveq2	$⊢ r = R \to \frac{1}{r} = \frac{1}{R}$
14	12 13	breq12d	$⊢ r = R \to ((n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) ⇝ (\frac{1}{r}) \leftrightarrow (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$
15	3 14	raleqbidv	$⊢ r = R \to (\forall b \in (0 \dots r - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) ⇝ (\frac{1}{r}) \leftrightarrow \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$
16	15	rabbidv	$⊢ r = R \to \{x \in ℝ \| \forall b \in (0 \dots r - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) ⇝ (\frac{1}{r})\} = \{x \in ℝ \| \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})\}$
17		reex	$⊢ ℝ \in V$
18	17	rabex	$⊢ \{x \in ℝ \| \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})\} \in V$
19	16 1 18	fvmpt	$⊢ R \in ℤ_{\geq 2} \to S (R) = \{x \in ℝ \| \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})\}$
20	19	eleq2d	$⊢ R \in ℤ_{\geq 2} \to (A \in S (R) \leftrightarrow A \in \{x \in ℝ \| \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})\})$
21		oveq1	$⊢ x = A \to x R^{k} = A R^{k}$
22	21	fvoveq1d	$⊢ x = A \to ⌊x R^{k} \mod R⌋ = ⌊A R^{k} \mod R⌋$
23	22	eqeq1d	$⊢ x = A \to (⌊x R^{k} \mod R⌋ = b \leftrightarrow ⌊A R^{k} \mod R⌋ = b)$
24	23	rabbidv	$⊢ x = A \to \{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\} = \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}$
25	24	fveq2d	$⊢ x = A \to \|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\| = \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|$
26	25	oveq1d	$⊢ x = A \to \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n} = \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}$
27	26	mpteq2dv	$⊢ x = A \to (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) = (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n})$
28	27	breq1d	$⊢ x = A \to ((n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}) \leftrightarrow (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$
29	28	ralbidv	$⊢ x = A \to (\forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}) \leftrightarrow \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$
30	29	elrab	$⊢ A \in \{x \in ℝ \| \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})\} \leftrightarrow (A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$
31	20 30	bitrdi	$⊢ R \in ℤ_{\geq 2} \to (A \in S (R) \leftrightarrow (A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})))$
32	31	pm5.32i	$⊢ (R \in ℤ_{\geq 2} \land A \in S (R)) \leftrightarrow (R \in ℤ_{\geq 2} \land (A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})))$
33	1	dmmptss	$⊢ dom S \subseteq ℤ_{\geq 2}$
34		elfvdm	$⊢ A \in S (R) \to R \in dom S$
35	33 34	sselid	$⊢ A \in S (R) \to R \in ℤ_{\geq 2}$
36	35	pm4.71ri	$⊢ A \in S (R) \leftrightarrow (R \in ℤ_{\geq 2} \land A \in S (R))$
37		3anass	$⊢ (R \in ℤ_{\geq 2} \land A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})) \leftrightarrow (R \in ℤ_{\geq 2} \land (A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})))$
38	32 36 37	3bitr4i	$⊢ A \in S (R) \leftrightarrow (R \in ℤ_{\geq 2} \land A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$

Metamath Proof Explorer

Theorem snmlval

Proof