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