Metamath Proof Explorer

Theorem gtndiv

Description: A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005)

Ref Expression
Assertion gtndiv ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → ¬ B A ∈ ℤ

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 nnre ⊢ B ∈ ℕ → B ∈ ℝ
3 2 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → B ∈ ℝ
4 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → A ∈ ℝ
5 nngt0 ⊢ B ∈ ℕ → 0 < B
6 5 3ad2ant2 ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → 0 < B
7 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℕ → 0 < B
8 0re ⊢ 0 ∈ ℝ
9 lttr ⊢ 0 ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ → 0 < B ∧ B < A → 0 < A
10 8 9 mp3an1 ⊢ B ∈ ℝ ∧ A ∈ ℝ → 0 < B ∧ B < A → 0 < A
11 2 10 sylan ⊢ B ∈ ℕ ∧ A ∈ ℝ → 0 < B ∧ B < A → 0 < A
12 11 ancoms ⊢ A ∈ ℝ ∧ B ∈ ℕ → 0 < B ∧ B < A → 0 < A
13 7 12 mpand ⊢ A ∈ ℝ ∧ B ∈ ℕ → B < A → 0 < A
14 13 3impia ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → 0 < A
15 3 4 6 14 divgt0d ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → 0 < B A
16 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → B < A
17 1re ⊢ 1 ∈ ℝ
18 ltdivmul2 ⊢ B ∈ ℝ ∧ 1 ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → B A < 1 ↔ B < 1 ⁢ A
19 17 18 mp3an2 ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → B A < 1 ↔ B < 1 ⁢ A
20 3 4 14 19 syl12anc ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → B A < 1 ↔ B < 1 ⁢ A
21 recn ⊢ A ∈ ℝ → A ∈ ℂ
22 21 mullidd ⊢ A ∈ ℝ → 1 ⁢ A = A
23 22 breq2d ⊢ A ∈ ℝ → B < 1 ⁢ A ↔ B < A
24 23 3ad2ant1 ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → B < 1 ⁢ A ↔ B < A
25 20 24 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → B A < 1 ↔ B < A
26 16 25 mpbird ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → B A < 1
27 0p1e1 ⊢ 0 + 1 = 1
28 26 27 breqtrrdi ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → B A < 0 + 1
29 btwnnz ⊢ 0 ∈ ℤ ∧ 0 < B A ∧ B A < 0 + 1 → ¬ B A ∈ ℤ
30 1 15 28 29 mp3an2i ⊢ A ∈ ℝ ∧ B ∈ ℕ ∧ B < A → ¬ B A ∈ ℤ