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

Metamath Proof Explorer

Theorem gtndiv

Proof