Metamath Proof Explorer

Theorem dvdsadd2b

Description: Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014)

Ref Expression
Assertion dvdsadd2b 
|- ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || B ) -> A e. ZZ )
2 simpl3l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || B ) -> C e. ZZ )
3 simpl2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || B ) -> B e. ZZ )
4 simpl3r 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || B ) -> A || C )
5 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || B ) -> A || B )
6 1 2 3 4 5 dvds2addd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || B ) -> A || ( C + B ) )
7 simpl1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> A e. ZZ )
8 simp3l 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> C e. ZZ )
9 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> B e. ZZ )
10 zaddcl 
 |-  ( ( C e. ZZ /\ B e. ZZ ) -> ( C + B ) e. ZZ )
11 8 9 10 syl2anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> ( C + B ) e. ZZ )
12 11 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> ( C + B ) e. ZZ )
13 8 znegcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> -u C e. ZZ )
14 13 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> -u C e. ZZ )
15 simpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> A || ( C + B ) )
16 simpl3r 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> A || C )
17 simpl3l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> C e. ZZ )
18 dvdsnegb 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> ( A || C <-> A || -u C ) )
19 7 17 18 syl2anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> ( A || C <-> A || -u C ) )
20 16 19 mpbid 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> A || -u C )
21 7 12 14 15 20 dvds2addd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> A || ( ( C + B ) + -u C ) )
22 simpl2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> B e. ZZ )
23 10 ancoms 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( C + B ) e. ZZ )
24 23 zcnd 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( C + B ) e. CC )
25 zcn 
 |-  ( C e. ZZ -> C e. CC )
26 25 adantl 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> C e. CC )
27 24 26 negsubd 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( ( C + B ) + -u C ) = ( ( C + B ) - C ) )
28 zcn 
 |-  ( B e. ZZ -> B e. CC )
29 28 adantr 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> B e. CC )
30 26 29 pncan2d 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( ( C + B ) - C ) = B )
31 27 30 eqtrd 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( ( C + B ) + -u C ) = B )
32 22 17 31 syl2anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> ( ( C + B ) + -u C ) = B )
33 21 32 breqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) /\ A || ( C + B ) ) -> A || B )
34 6 33 impbida 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) )