Metamath Proof Explorer

Theorem nndivlub

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

Ref Expression
Assertion nndivlub ⊢ A ∈ ℕ ∧ B ∈ ℕ → A B ∈ ℕ → B ≤ A

Proof

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