This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( ( A e. NN /\ B e. NN /\ C e. CC ) /\ ( ( B / A ) e. NN /\ ( C / B ) e. NN ) ) -> ( C / A ) e. NN )

Proof

Step Hyp Ref Expression
1 nnmulcl 
 |-  ( ( ( B / A ) e. NN /\ ( C / B ) e. NN ) -> ( ( B / A ) x. ( C / B ) ) e. NN )
2 nncn 
 |-  ( B e. NN -> B e. CC )
3 2 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> B e. CC )
4 simp3 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> C e. CC )
5 nncn 
 |-  ( A e. NN -> A e. CC )
6 nnne0 
 |-  ( A e. NN -> A =/= 0 )
7 5 6 jca 
 |-  ( A e. NN -> ( A e. CC /\ A =/= 0 ) )
8 7 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( A e. CC /\ A =/= 0 ) )
9 nnne0 
 |-  ( B e. NN -> B =/= 0 )
10 2 9 jca 
 |-  ( B e. NN -> ( B e. CC /\ B =/= 0 ) )
11 10 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( B e. CC /\ B =/= 0 ) )
12 divmul24 
 |-  ( ( ( B e. CC /\ C e. CC ) /\ ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) ) -> ( ( B / A ) x. ( C / B ) ) = ( ( B / B ) x. ( C / A ) ) )
13 3 4 8 11 12 syl22anc 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( ( B / A ) x. ( C / B ) ) = ( ( B / B ) x. ( C / A ) ) )
14 2 9 dividd 
 |-  ( B e. NN -> ( B / B ) = 1 )
15 14 oveq1d 
 |-  ( B e. NN -> ( ( B / B ) x. ( C / A ) ) = ( 1 x. ( C / A ) ) )
16 15 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( ( B / B ) x. ( C / A ) ) = ( 1 x. ( C / A ) ) )
17 divcl 
 |-  ( ( C e. CC /\ A e. CC /\ A =/= 0 ) -> ( C / A ) e. CC )
18 17 3expb 
 |-  ( ( C e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( C / A ) e. CC )
19 7 18 sylan2 
 |-  ( ( C e. CC /\ A e. NN ) -> ( C / A ) e. CC )
20 19 ancoms 
 |-  ( ( A e. NN /\ C e. CC ) -> ( C / A ) e. CC )
21 20 mullidd 
 |-  ( ( A e. NN /\ C e. CC ) -> ( 1 x. ( C / A ) ) = ( C / A ) )
22 21 3adant2 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( 1 x. ( C / A ) ) = ( C / A ) )
23 13 16 22 3eqtrd 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( ( B / A ) x. ( C / B ) ) = ( C / A ) )
24 23 eleq1d 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( ( ( B / A ) x. ( C / B ) ) e. NN <-> ( C / A ) e. NN ) )
25 1 24 imbitrid 
 |-  ( ( A e. NN /\ B e. NN /\ C e. CC ) -> ( ( ( B / A ) e. NN /\ ( C / B ) e. NN ) -> ( C / A ) e. NN ) )
26 25 imp 
 |-  ( ( ( A e. NN /\ B e. NN /\ C e. CC ) /\ ( ( B / A ) e. NN /\ ( C / B ) e. NN ) ) -> ( C / A ) e. NN )