Theorem modn0mul

Description: If an integer is not 0 modulo a positive integer, this integer must be the sum of a multiple of the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020)

	Ref	Expression
Assertion	modn0mul	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 mod 𝑁 ) ≠ 0 → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ( 1 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) )

Proof

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 ..^ 𝑁 ) 𝐴 = ( ( 𝑥 · 𝑁 ) + 𝑦 ) ) )