snmlff

Description: The function F from snmlval is a mapping from positive integers to real numbers in the range [ 0 , 1 ] . (Contributed by Mario Carneiro, 6-Apr-2015)

		Ref	Expression
	Hypothesis	snmlff.f	$⊢ F = (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n})$
	Assertion	snmlff	$⊢ F : ℕ ⟶ [0, 1]$

Proof

Step	Hyp	Ref	Expression
1		snmlff.f	$⊢ F = (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n})$
2		fzfid	$⊢ n \in ℕ \to (1 \dots n) \in Fin$
3		ssrab2	$⊢ \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} \subseteq (1 \dots n)$
4		ssfi	$⊢ ((1 \dots n) \in Fin \land \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} \subseteq (1 \dots n)) \to \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} \in Fin$
5	2 3 4	sylancl	$⊢ n \in ℕ \to \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} \in Fin$
6		hashcl	$⊢ \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} \in Fin \to \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \in ℕ_{0}$
7	5 6	syl	$⊢ n \in ℕ \to \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \in ℕ_{0}$
8	7	nn0red	$⊢ n \in ℕ \to \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \in ℝ$
9		nndivre	$⊢ (\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \in ℝ \land n \in ℕ) \to \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \in ℝ$
10	8 9	mpancom	$⊢ n \in ℕ \to \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \in ℝ$
11	7	nn0ge0d	$⊢ n \in ℕ \to 0 \leq \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|$
12		nnre	$⊢ n \in ℕ \to n \in ℝ$
13		nngt0	$⊢ n \in ℕ \to 0 < n$
14		divge0	$⊢ ((\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \in ℝ \land 0 \leq \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|) \land (n \in ℝ \land 0 < n)) \to 0 \leq \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n}$
15	8 11 12 13 14	syl22anc	$⊢ n \in ℕ \to 0 \leq \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n}$
16		ssdomg	$⊢ (1 \dots n) \in Fin \to (\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} \subseteq (1 \dots n) \to \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} ≼ (1 \dots n))$
17	2 3 16	mpisyl	$⊢ n \in ℕ \to \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} ≼ (1 \dots n)$
18		hashdom	$⊢ (\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} \in Fin \land (1 \dots n) \in Fin) \to (\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \leq \|(1 \dots n)\| \leftrightarrow \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} ≼ (1 \dots n))$
19	5 2 18	syl2anc	$⊢ n \in ℕ \to (\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \leq \|(1 \dots n)\| \leftrightarrow \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\} ≼ (1 \dots n))$
20	17 19	mpbird	$⊢ n \in ℕ \to \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \leq \|(1 \dots n)\|$
21		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
22		hashfz1	$⊢ n \in ℕ_{0} \to \|(1 \dots n)\| = n$
23	21 22	syl	$⊢ n \in ℕ \to \|(1 \dots n)\| = n$
24	20 23	breqtrd	$⊢ n \in ℕ \to \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \leq n$
25		nncn	$⊢ n \in ℕ \to n \in ℂ$
26	25	mulridd	$⊢ n \in ℕ \to n \cdot 1 = n$
27	24 26	breqtrrd	$⊢ n \in ℕ \to \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \leq n \cdot 1$
28		1red	$⊢ n \in ℕ \to 1 \in ℝ$
29		ledivmul	$⊢ (\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \in ℝ \land 1 \in ℝ \land (n \in ℝ \land 0 < n)) \to (\frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \leq 1 \leftrightarrow \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \leq n \cdot 1)$
30	8 28 12 13 29	syl112anc	$⊢ n \in ℕ \to (\frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \leq 1 \leftrightarrow \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\| \leq n \cdot 1)$
31	27 30	mpbird	$⊢ n \in ℕ \to \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \leq 1$
32		elicc01	$⊢ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \in [0, 1] \leftrightarrow (\frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \in ℝ \land 0 \leq \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \land \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \leq 1)$
33	10 15 31 32	syl3anbrc	$⊢ n \in ℕ \to \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n} \in [0, 1]$
34	1 33	fmpti	$⊢ F : ℕ ⟶ [0, 1]$

Metamath Proof Explorer

Theorem snmlff

Proof