Step |
Hyp |
Ref |
Expression |
1 |
|
zre |
⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝐴 ∈ ℝ ) |
3 |
|
nnre |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ ) |
4 |
3
|
adantl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ ) |
5 |
|
nnne0 |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 ) |
6 |
5
|
adantl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 ) |
7 |
2 4 6
|
redivcld |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 / 𝑁 ) ∈ ℝ ) |
8 |
7
|
flcld |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ∈ ℤ ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ∈ ℤ ) |
10 |
|
zmodfzo |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ) |
11 |
10
|
anim1i |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( ( 𝐴 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) ) |
12 |
|
fzo1fzo0n0 |
⊢ ( ( 𝐴 mod 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ↔ ( ( 𝐴 mod 𝑁 ) ∈ ( 0 ..^ 𝑁 ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) ) |
13 |
11 12
|
sylibr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( 𝐴 mod 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ) |
14 |
|
nnrp |
⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ ) |
15 |
1 14
|
anim12i |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ) |
17 |
|
flpmodeq |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) = 𝐴 ) |
18 |
16 17
|
syl |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) = 𝐴 ) |
19 |
18
|
eqcomd |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) ) |
20 |
|
oveq1 |
⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) → ( 𝑥 · 𝑁 ) = ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) ) |
21 |
20
|
oveq1d |
⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) → ( ( 𝑥 · 𝑁 ) + 𝑦 ) = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) ) |
22 |
21
|
eqeq2d |
⊢ ( 𝑥 = ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) → ( 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ↔ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) ) ) |
23 |
|
oveq2 |
⊢ ( 𝑦 = ( 𝐴 mod 𝑁 ) → ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) ) |
24 |
23
|
eqeq2d |
⊢ ( 𝑦 = ( 𝐴 mod 𝑁 ) → ( 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + 𝑦 ) ↔ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) ) ) |
25 |
22 24
|
rspc2ev |
⊢ ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) ∈ ℤ ∧ ( 𝐴 mod 𝑁 ) ∈ ( 1 ..^ 𝑁 ) ∧ 𝐴 = ( ( ( ⌊ ‘ ( 𝐴 / 𝑁 ) ) · 𝑁 ) + ( 𝐴 mod 𝑁 ) ) ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) |
26 |
9 13 19 25
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) ∧ ( 𝐴 mod 𝑁 ) ≠ 0 ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) |
27 |
26
|
ex |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) ≠ 0 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) ) |