Step |
Hyp |
Ref |
Expression |
1 |
|
snml.s |
⊢ 𝑆 = ( 𝑟 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑟 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) } ) |
2 |
|
snml.f |
⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ) |
3 |
1
|
snmlval |
⊢ ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ↔ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) ) |
4 |
3
|
simp3bi |
⊢ ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) → ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) |
5 |
|
eqeq2 |
⊢ ( 𝑏 = 𝐵 → ( ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 ↔ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 ) ) |
6 |
5
|
rabbidv |
⊢ ( 𝑏 = 𝐵 → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } = { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) |
7 |
6
|
fveq2d |
⊢ ( 𝑏 = 𝐵 → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) = ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) ) |
8 |
7
|
oveq1d |
⊢ ( 𝑏 = 𝐵 → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) = ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ) |
9 |
8
|
mpteq2dv |
⊢ ( 𝑏 = 𝐵 → ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ) ) |
10 |
9 2
|
eqtr4di |
⊢ ( 𝑏 = 𝐵 → ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) = 𝐹 ) |
11 |
10
|
breq1d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ↔ 𝐹 ⇝ ( 1 / 𝑅 ) ) ) |
12 |
11
|
rspccva |
⊢ ( ( ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ∧ 𝐵 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝐹 ⇝ ( 1 / 𝑅 ) ) |
13 |
4 12
|
sylan |
⊢ ( ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ∧ 𝐵 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝐹 ⇝ ( 1 / 𝑅 ) ) |