# Metamath Proof Explorer

## Theorem nndivtr

Description: Transitive property of divisibility: if A divides B and B divides C , then A divides C . Typically, C would be an integer, although the theorem holds for complex C . (Contributed by NM, 3-May-2005)

Ref Expression
Assertion nndivtr ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\wedge \left(\frac{{B}}{{A}}\in ℕ\wedge \frac{{C}}{{B}}\in ℕ\right)\right)\to \frac{{C}}{{A}}\in ℕ$

### Proof

Step Hyp Ref Expression
1 nnmulcl ${⊢}\left(\frac{{B}}{{A}}\in ℕ\wedge \frac{{C}}{{B}}\in ℕ\right)\to \left(\frac{{B}}{{A}}\right)\left(\frac{{C}}{{B}}\right)\in ℕ$
2 nncn ${⊢}{B}\in ℕ\to {B}\in ℂ$
3 2 3ad2ant2 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to {B}\in ℂ$
4 simp3 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to {C}\in ℂ$
5 nncn ${⊢}{A}\in ℕ\to {A}\in ℂ$
6 nnne0 ${⊢}{A}\in ℕ\to {A}\ne 0$
7 5 6 jca ${⊢}{A}\in ℕ\to \left({A}\in ℂ\wedge {A}\ne 0\right)$
8 7 3ad2ant1 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to \left({A}\in ℂ\wedge {A}\ne 0\right)$
9 nnne0 ${⊢}{B}\in ℕ\to {B}\ne 0$
10 2 9 jca ${⊢}{B}\in ℕ\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
11 10 3ad2ant2 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
12 divmul24 ${⊢}\left(\left({B}\in ℂ\wedge {C}\in ℂ\right)\wedge \left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\right)\to \left(\frac{{B}}{{A}}\right)\left(\frac{{C}}{{B}}\right)=\left(\frac{{B}}{{B}}\right)\left(\frac{{C}}{{A}}\right)$
13 3 4 8 11 12 syl22anc ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to \left(\frac{{B}}{{A}}\right)\left(\frac{{C}}{{B}}\right)=\left(\frac{{B}}{{B}}\right)\left(\frac{{C}}{{A}}\right)$
14 2 9 dividd ${⊢}{B}\in ℕ\to \frac{{B}}{{B}}=1$
15 14 oveq1d ${⊢}{B}\in ℕ\to \left(\frac{{B}}{{B}}\right)\left(\frac{{C}}{{A}}\right)=1\left(\frac{{C}}{{A}}\right)$
16 15 3ad2ant2 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to \left(\frac{{B}}{{B}}\right)\left(\frac{{C}}{{A}}\right)=1\left(\frac{{C}}{{A}}\right)$
17 divcl ${⊢}\left({C}\in ℂ\wedge {A}\in ℂ\wedge {A}\ne 0\right)\to \frac{{C}}{{A}}\in ℂ$
18 17 3expb ${⊢}\left({C}\in ℂ\wedge \left({A}\in ℂ\wedge {A}\ne 0\right)\right)\to \frac{{C}}{{A}}\in ℂ$
19 7 18 sylan2 ${⊢}\left({C}\in ℂ\wedge {A}\in ℕ\right)\to \frac{{C}}{{A}}\in ℂ$
20 19 ancoms ${⊢}\left({A}\in ℕ\wedge {C}\in ℂ\right)\to \frac{{C}}{{A}}\in ℂ$
21 20 mulid2d ${⊢}\left({A}\in ℕ\wedge {C}\in ℂ\right)\to 1\left(\frac{{C}}{{A}}\right)=\frac{{C}}{{A}}$
22 21 3adant2 ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to 1\left(\frac{{C}}{{A}}\right)=\frac{{C}}{{A}}$
23 13 16 22 3eqtrd ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to \left(\frac{{B}}{{A}}\right)\left(\frac{{C}}{{B}}\right)=\frac{{C}}{{A}}$
24 23 eleq1d ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to \left(\left(\frac{{B}}{{A}}\right)\left(\frac{{C}}{{B}}\right)\in ℕ↔\frac{{C}}{{A}}\in ℕ\right)$
25 1 24 syl5ib ${⊢}\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\to \left(\left(\frac{{B}}{{A}}\in ℕ\wedge \frac{{C}}{{B}}\in ℕ\right)\to \frac{{C}}{{A}}\in ℕ\right)$
26 25 imp ${⊢}\left(\left({A}\in ℕ\wedge {B}\in ℕ\wedge {C}\in ℂ\right)\wedge \left(\frac{{B}}{{A}}\in ℕ\wedge \frac{{C}}{{B}}\in ℕ\right)\right)\to \frac{{C}}{{A}}\in ℕ$