Theorem nndivlub

Description: A factor of a positive integer cannot exceed it. (Contributed by Jeff Hoffman, 17-Jun-2008)

	Ref	Expression
Assertion	nndivlub	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / 𝐵 ) ∈ ℕ → 𝐵 ≤ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nnre	⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ )
2		nngt0	⊢ ( 𝐵 ∈ ℕ → 0 < 𝐵 )
3	1 2	jca	⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
4		nnre	⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
5		nngt0	⊢ ( 𝐴 ∈ ℕ → 0 < 𝐴 )
6	4 5	jca	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
7		nnge1	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℕ → 1 ≤ ( 𝐴 / 𝐵 ) )
8		lediv2	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐵 ≤ 𝐴 ↔ ( 𝐴 / 𝐴 ) ≤ ( 𝐴 / 𝐵 ) ) )
9	8	3anidm23	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐵 ≤ 𝐴 ↔ ( 𝐴 / 𝐴 ) ≤ ( 𝐴 / 𝐵 ) ) )
10		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
11	10	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
12		gt0ne0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
13		divid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 / 𝐴 ) = 1 )
14	13	breq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 𝐴 / 𝐴 ) ≤ ( 𝐴 / 𝐵 ) ↔ 1 ≤ ( 𝐴 / 𝐵 ) ) )
15	11 12 14	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 𝐴 / 𝐴 ) ≤ ( 𝐴 / 𝐵 ) ↔ 1 ≤ ( 𝐴 / 𝐵 ) ) )
16	15	adantl	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 𝐴 / 𝐴 ) ≤ ( 𝐴 / 𝐵 ) ↔ 1 ≤ ( 𝐴 / 𝐵 ) ) )
17	9 16	bitrd	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐵 ≤ 𝐴 ↔ 1 ≤ ( 𝐴 / 𝐵 ) ) )
18	7 17	imbitrrid	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 𝐴 / 𝐵 ) ∈ ℕ → 𝐵 ≤ 𝐴 ) )
19	3 6 18	syl2anr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 / 𝐵 ) ∈ ℕ → 𝐵 ≤ 𝐴 ) )