This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem quoremnn0

Description: Quotient and remainder of a nonnegative integer divided by a positive integer. (Contributed by NM, 14-Aug-2008)

		Ref	Expression
	Hypotheses	quorem.1	⊢ 𝑄 = ( ⌊ ‘ ( 𝐴 / 𝐵 ) )
		quorem.2	⊢ 𝑅 = ( 𝐴 − ( 𝐵 · 𝑄 ) )
	Assertion	quoremnn0	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑄 ∈ ℕ₀ ∧ 𝑅 ∈ ℕ₀ ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		quorem.1	⊢ 𝑄 = ( ⌊ ‘ ( 𝐴 / 𝐵 ) )
2		quorem.2	⊢ 𝑅 = ( 𝐴 − ( 𝐵 · 𝑄 ) )
3		fldivnn0	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ ) → ( ⌊ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℕ₀ )
4	1 3	eqeltrid	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ ) → 𝑄 ∈ ℕ₀ )
5		nn0z	⊢ ( 𝐴 ∈ ℕ₀ → 𝐴 ∈ ℤ )
6	1 2	quoremz	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ₀ ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )
7	5 6	sylan	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ₀ ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )
8		simpl	⊢ ( ( 𝑄 ∈ ℕ₀ ∧ 𝑄 ∈ ℤ ) → 𝑄 ∈ ℕ₀ )
9	8	anim1i	⊢ ( ( ( 𝑄 ∈ ℕ₀ ∧ 𝑄 ∈ ℤ ) ∧ 𝑅 ∈ ℕ₀ ) → ( 𝑄 ∈ ℕ₀ ∧ 𝑅 ∈ ℕ₀ ) )
10	9	anasss	⊢ ( ( 𝑄 ∈ ℕ₀ ∧ ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ₀ ) ) → ( 𝑄 ∈ ℕ₀ ∧ 𝑅 ∈ ℕ₀ ) )
11	10	anim1i	⊢ ( ( ( 𝑄 ∈ ℕ₀ ∧ ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ₀ ) ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) → ( ( 𝑄 ∈ ℕ₀ ∧ 𝑅 ∈ ℕ₀ ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )
12	11	anasss	⊢ ( ( 𝑄 ∈ ℕ₀ ∧ ( ( 𝑄 ∈ ℤ ∧ 𝑅 ∈ ℕ₀ ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) ) → ( ( 𝑄 ∈ ℕ₀ ∧ 𝑅 ∈ ℕ₀ ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )
13	4 7 12	syl2anc	⊢ ( ( 𝐴 ∈ ℕ₀ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑄 ∈ ℕ₀ ∧ 𝑅 ∈ ℕ₀ ) ∧ ( 𝑅 < 𝐵 ∧ 𝐴 = ( ( 𝐵 · 𝑄 ) + 𝑅 ) ) ) )