# Metamath Proof Explorer

## Theorem nndivsub

Description: Please add description here. (Contributed by Jeff Hoffman, 17-Jun-2008)

Ref Expression
Assertion nndivsub ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge {A}<{B}\right)\right)\to \left(\frac{{B}}{{C}}\in ℕ↔\frac{{B}-{A}}{{C}}\in ℕ\right)$

### Proof

Step Hyp Ref Expression
1 nnre ${⊢}{A}\in ℕ\to {A}\in ℝ$
2 nnre ${⊢}{B}\in ℕ\to {B}\in ℝ$
3 nnre ${⊢}{C}\in ℕ\to {C}\in ℝ$
4 nngt0 ${⊢}{C}\in ℕ\to 0<{C}$
5 3 4 jca ${⊢}{C}\in ℕ\to \left({C}\in ℝ\wedge 0<{C}\right)$
6 ltdiv1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}<{B}↔\frac{{A}}{{C}}<\frac{{B}}{{C}}\right)$
7 1 2 5 6 syl3an ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left({A}<{B}↔\frac{{A}}{{C}}<\frac{{B}}{{C}}\right)$
8 nnsub ${⊢}\left(\frac{{A}}{{C}}\in ℕ\wedge \frac{{B}}{{C}}\in ℕ\right)\to \left(\frac{{A}}{{C}}<\frac{{B}}{{C}}↔\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
9 7 8 sylan9bb ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge \frac{{B}}{{C}}\in ℕ\right)\right)\to \left({A}<{B}↔\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
10 9 biimpd ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge \frac{{B}}{{C}}\in ℕ\right)\right)\to \left({A}<{B}\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
11 10 exp32 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left(\frac{{A}}{{C}}\in ℕ\to \left(\frac{{B}}{{C}}\in ℕ\to \left({A}<{B}\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)\right)\right)$
12 11 com34 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left(\frac{{A}}{{C}}\in ℕ\to \left({A}<{B}\to \left(\frac{{B}}{{C}}\in ℕ\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)\right)\right)$
13 12 imp32 ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge {A}<{B}\right)\right)\to \left(\frac{{B}}{{C}}\in ℕ\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
14 nnaddcl ${⊢}\left(\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\wedge \frac{{A}}{{C}}\in ℕ\right)\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)+\left(\frac{{A}}{{C}}\right)\in ℕ$
15 14 expcom ${⊢}\frac{{A}}{{C}}\in ℕ\to \left(\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)+\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
16 nnsscn ${⊢}ℕ\subseteq ℂ$
17 nnne0 ${⊢}{C}\in ℕ\to {C}\ne 0$
18 divcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to \frac{{A}}{{C}}\in ℂ$
19 16 17 18 nnssi2 ${⊢}\left({A}\in ℕ\wedge {C}\in ℕ\right)\to \frac{{A}}{{C}}\in ℂ$
20 divcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to \frac{{B}}{{C}}\in ℂ$
21 16 17 20 nnssi2 ${⊢}\left({B}\in ℕ\wedge {C}\in ℕ\right)\to \frac{{B}}{{C}}\in ℂ$
22 19 21 anim12i ${⊢}\left(\left({A}\in ℕ\wedge {C}\in ℕ\right)\wedge \left({B}\in ℕ\wedge {C}\in ℕ\right)\right)\to \left(\frac{{A}}{{C}}\in ℂ\wedge \frac{{B}}{{C}}\in ℂ\right)$
23 22 3impdir ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left(\frac{{A}}{{C}}\in ℂ\wedge \frac{{B}}{{C}}\in ℂ\right)$
24 npcan ${⊢}\left(\frac{{B}}{{C}}\in ℂ\wedge \frac{{A}}{{C}}\in ℂ\right)\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)+\left(\frac{{A}}{{C}}\right)=\frac{{B}}{{C}}$
25 24 ancoms ${⊢}\left(\frac{{A}}{{C}}\in ℂ\wedge \frac{{B}}{{C}}\in ℂ\right)\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)+\left(\frac{{A}}{{C}}\right)=\frac{{B}}{{C}}$
26 23 25 syl ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)+\left(\frac{{A}}{{C}}\right)=\frac{{B}}{{C}}$
27 26 eleq1d ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left(\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)+\left(\frac{{A}}{{C}}\right)\in ℕ↔\frac{{B}}{{C}}\in ℕ\right)$
28 27 biimpd ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left(\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)+\left(\frac{{A}}{{C}}\right)\in ℕ\to \frac{{B}}{{C}}\in ℕ\right)$
29 15 28 sylan9r ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \frac{{A}}{{C}}\in ℕ\right)\to \left(\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\to \frac{{B}}{{C}}\in ℕ\right)$
30 29 adantrr ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge {A}<{B}\right)\right)\to \left(\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\to \frac{{B}}{{C}}\in ℕ\right)$
31 13 30 impbid ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge {A}<{B}\right)\right)\to \left(\frac{{B}}{{C}}\in ℕ↔\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
32 nncn ${⊢}{B}\in ℕ\to {B}\in ℂ$
33 32 3ad2ant2 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {B}\in ℂ$
34 nncn ${⊢}{A}\in ℕ\to {A}\in ℂ$
35 34 3ad2ant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to {A}\in ℂ$
36 nncn ${⊢}{C}\in ℕ\to {C}\in ℂ$
37 36 17 jca ${⊢}{C}\in ℕ\to \left({C}\in ℂ\wedge {C}\ne 0\right)$
38 37 3ad2ant3 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left({C}\in ℂ\wedge {C}\ne 0\right)$
39 divsubdir ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{B}-{A}}{{C}}=\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)$
40 33 35 38 39 syl3anc ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \frac{{B}-{A}}{{C}}=\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)$
41 40 eleq1d ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\to \left(\frac{{B}-{A}}{{C}}\in ℕ↔\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
42 41 adantr ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge {A}<{B}\right)\right)\to \left(\frac{{B}-{A}}{{C}}\in ℕ↔\left(\frac{{B}}{{C}}\right)-\left(\frac{{A}}{{C}}\right)\in ℕ\right)$
43 31 42 bitr4d ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℕ\right)\wedge \left(\frac{{A}}{{C}}\in ℕ\wedge {A}<{B}\right)\right)\to \left(\frac{{B}}{{C}}\in ℕ↔\frac{{B}-{A}}{{C}}\in ℕ\right)$