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→¬BA∈ℤ

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<BA
16 simp3 ⊢A∈ℝ∧B∈ℕ∧B<A→B<A
17 1re ⊢1∈ℝ
18 ltdivmul2 ⊢B∈ℝ∧1∈ℝ∧A∈ℝ∧0<A→BA<1↔B<1⁢A
19 17 18 mp3an2 ⊢B∈ℝ∧A∈ℝ∧0<A→BA<1↔B<1⁢A
20 3 4 14 19 syl12anc ⊢A∈ℝ∧B∈ℕ∧B<A→BA<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→BA<1↔B<A
26 16 25 mpbird ⊢A∈ℝ∧B∈ℕ∧B<A→BA<1
27 0p1e1 ⊢0+1=1
28 26 27 breqtrrdi ⊢A∈ℝ∧B∈ℕ∧B<A→BA<0+1
29 btwnnz ⊢0∈ℤ∧0<BA∧BA<0+1→¬BA∈ℤ
30 1 15 28 29 mp3an2i ⊢A∈ℝ∧B∈ℕ∧B<A→¬BA∈ℤ