Metamath Proof Explorer

Theorem 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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
Assertion snmlff 𝐹 : ℕ ⟶ ( 0 [,] 1 )

Proof

Step Hyp Ref Expression
1 snmlff.f ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
2 fzfid ⊢ ( 𝑛 ∈ ℕ → ( 1 ... 𝑛 ) ∈ Fin )
3 ssrab2 ⊢ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ⊆ ( 1 ... 𝑛 )
4 ssfi ⊢ ( ( ( 1 ... 𝑛 ) ∈ Fin ∧ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ⊆ ( 1 ... 𝑛 ) ) → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ∈ Fin )
5 2 3 4 sylancl ⊢ ( 𝑛 ∈ ℕ → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ∈ Fin )
6 hashcl ⊢ ( { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ∈ Fin → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ∈ ℕ0 )
7 5 6 syl ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ∈ ℕ0 )
8 7 nn0red ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ∈ ℝ )
9 nndivre ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ∈ ℝ )
10 8 9 mpancom ⊢ ( 𝑛 ∈ ℕ → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ∈ ℝ )
11 7 nn0ge0d ⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) )
12 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
13 nngt0 ⊢ ( 𝑛 ∈ ℕ → 0 < 𝑛 )
14 divge0 ⊢ ( ( ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ∈ ℝ ∧ 0 ≤ ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → 0 ≤ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
15 8 11 12 13 14 syl22anc ⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
16 ssdomg ⊢ ( ( 1 ... 𝑛 ) ∈ Fin → ( { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ⊆ ( 1 ... 𝑛 ) → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ≼ ( 1 ... 𝑛 ) ) )
17 2 3 16 mpisyl ⊢ ( 𝑛 ∈ ℕ → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ≼ ( 1 ... 𝑛 ) )
18 hashdom ⊢ ( ( { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ∈ Fin ∧ ( 1 ... 𝑛 ) ∈ Fin ) → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ≤ ( ♯ ‘ ( 1 ... 𝑛 ) ) ↔ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ≼ ( 1 ... 𝑛 ) ) )
19 5 2 18 syl2anc ⊢ ( 𝑛 ∈ ℕ → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ≤ ( ♯ ‘ ( 1 ... 𝑛 ) ) ↔ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ≼ ( 1 ... 𝑛 ) ) )
20 17 19 mpbird ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ≤ ( ♯ ‘ ( 1 ... 𝑛 ) ) )
21 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
22 hashfz1 ⊢ ( 𝑛 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
23 21 22 syl ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
24 20 23 breqtrd ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ≤ 𝑛 )
25 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
26 25 mulid1d ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · 1 ) = 𝑛 )
27 24 26 breqtrrd ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ≤ ( 𝑛 · 1 ) )
28 1red ⊢ ( 𝑛 ∈ ℕ → 1 ∈ ℝ )
29 ledivmul ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ≤ 1 ↔ ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ≤ ( 𝑛 · 1 ) ) )
30 8 28 12 13 29 syl112anc ⊢ ( 𝑛 ∈ ℕ → ( ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ≤ 1 ↔ ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ≤ ( 𝑛 · 1 ) ) )
31 27 30 mpbird ⊢ ( 𝑛 ∈ ℕ → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ≤ 1 )
32 elicc01 ⊢ ( ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ∈ ( 0 [,] 1 ) ↔ ( ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ∈ ℝ ∧ 0 ≤ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ∧ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ≤ 1 ) )
33 10 15 31 32 syl3anbrc ⊢ ( 𝑛 ∈ ℕ → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ∈ ( 0 [,] 1 ) )
34 1 33 fmpti ⊢ 𝐹 : ℕ ⟶ ( 0 [,] 1 )