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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐵 < 𝐴 ) → ¬ ( 𝐵 / 𝐴 ) ∈ ℤ )

Proof

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