Proof of Theorem snmlff
Step | Hyp | Ref
| Expression |
1 | | snmlff.f |
. 2
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛)) |
2 | | fzfid 12772 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
(1...𝑛) ∈
Fin) |
3 | | ssrab2 3687 |
. . . . . . 7
⊢ {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ⊆ (1...𝑛) |
4 | | ssfi 8180 |
. . . . . . 7
⊢
(((1...𝑛) ∈ Fin
∧ {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ⊆ (1...𝑛)) → {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ∈ Fin) |
5 | 2, 3, 4 | sylancl 694 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ∈ Fin) |
6 | | hashcl 13147 |
. . . . . 6
⊢ ({𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ∈ Fin → (#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ∈
ℕ0) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ∈
ℕ0) |
8 | 7 | nn0red 11352 |
. . . 4
⊢ (𝑛 ∈ ℕ →
(#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ∈ ℝ) |
9 | | nndivre 11056 |
. . . 4
⊢
(((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ∈ ℝ ∧ 𝑛 ∈ ℕ) → ((#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ∈ ℝ) |
10 | 8, 9 | mpancom 703 |
. . 3
⊢ (𝑛 ∈ ℕ →
((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ∈ ℝ) |
11 | 7 | nn0ge0d 11354 |
. . . 4
⊢ (𝑛 ∈ ℕ → 0 ≤
(#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵})) |
12 | | nnre 11027 |
. . . 4
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℝ) |
13 | | nngt0 11049 |
. . . 4
⊢ (𝑛 ∈ ℕ → 0 <
𝑛) |
14 | | divge0 10892 |
. . . 4
⊢
((((#‘{𝑘
∈ (1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ∈ ℝ ∧ 0 ≤
(#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵})) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → 0 ≤
((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛)) |
15 | 8, 11, 12, 13, 14 | syl22anc 1327 |
. . 3
⊢ (𝑛 ∈ ℕ → 0 ≤
((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛)) |
16 | | ssdomg 8001 |
. . . . . . . 8
⊢
((1...𝑛) ∈ Fin
→ ({𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵} ⊆ (1...𝑛) → {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ≼ (1...𝑛))) |
17 | 2, 3, 16 | mpisyl 21 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ≼ (1...𝑛)) |
18 | | hashdom 13168 |
. . . . . . . 8
⊢ (({𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ∈ Fin ∧ (1...𝑛) ∈ Fin) → ((#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ≤ (#‘(1...𝑛)) ↔ {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ≼ (1...𝑛))) |
19 | 5, 2, 18 | syl2anc 693 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ →
((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ≤ (#‘(1...𝑛)) ↔ {𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵} ≼ (1...𝑛))) |
20 | 17, 19 | mpbird 247 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ≤ (#‘(1...𝑛))) |
21 | | nnnn0 11299 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
22 | | hashfz1 13134 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ (#‘(1...𝑛)) =
𝑛) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ (𝑛 ∈ ℕ →
(#‘(1...𝑛)) = 𝑛) |
24 | 20, 23 | breqtrd 4679 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ≤ 𝑛) |
25 | | nncn 11028 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
26 | 25 | mulid1d 10057 |
. . . . 5
⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛) |
27 | 24, 26 | breqtrrd 4681 |
. . . 4
⊢ (𝑛 ∈ ℕ →
(#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ≤ (𝑛 · 1)) |
28 | | 1red 10055 |
. . . . 5
⊢ (𝑛 ∈ ℕ → 1 ∈
ℝ) |
29 | | ledivmul 10899 |
. . . . 5
⊢
(((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ∈ ℝ ∧ 1 ∈ ℝ
∧ (𝑛 ∈ ℝ
∧ 0 < 𝑛)) →
(((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ≤ 1 ↔ (#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ≤ (𝑛 · 1))) |
30 | 8, 28, 12, 13, 29 | syl112anc 1330 |
. . . 4
⊢ (𝑛 ∈ ℕ →
(((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ≤ 1 ↔ (#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) ≤ (𝑛 · 1))) |
31 | 27, 30 | mpbird 247 |
. . 3
⊢ (𝑛 ∈ ℕ →
((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ≤ 1) |
32 | | 0re 10040 |
. . . 4
⊢ 0 ∈
ℝ |
33 | | 1re 10039 |
. . . 4
⊢ 1 ∈
ℝ |
34 | 32, 33 | elicc2i 12239 |
. . 3
⊢
(((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ∈ (0[,]1) ↔ (((#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ∈ ℝ ∧ 0 ≤
((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ∧ ((#‘{𝑘 ∈ (1...𝑛) ∣ (⌊‘((𝐴 · (𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ≤ 1)) |
35 | 10, 15, 31, 34 | syl3anbrc 1246 |
. 2
⊢ (𝑛 ∈ ℕ →
((#‘{𝑘 ∈
(1...𝑛) ∣
(⌊‘((𝐴 ·
(𝑅↑𝑘)) mod 𝑅)) = 𝐵}) / 𝑛) ∈ (0[,]1)) |
36 | 1, 35 | fmpti 6383 |
1
⊢ 𝐹:ℕ⟶(0[,]1) |