Metamath Proof Explorer

Theorem dvdsaddre2b

Description: Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b only requiring B to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 dvdsadd2b 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) )
2 1 a1d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> ( B e. RR -> ( A || B <-> A || ( C + B ) ) ) )
3 2 3exp 
 |-  ( A e. ZZ -> ( B e. ZZ -> ( ( C e. ZZ /\ A || C ) -> ( B e. RR -> ( A || B <-> A || ( C + B ) ) ) ) ) )
4 3 com24 
 |-  ( A e. ZZ -> ( B e. RR -> ( ( C e. ZZ /\ A || C ) -> ( B e. ZZ -> ( A || B <-> A || ( C + B ) ) ) ) ) )
5 4 3imp 
 |-  ( ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) -> ( B e. ZZ -> ( A || B <-> A || ( C + B ) ) ) )
6 5 com12 
 |-  ( B e. ZZ -> ( ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) ) )
7 dvdszrcl 
 |-  ( A || B -> ( A e. ZZ /\ B e. ZZ ) )
8 pm2.24 
 |-  ( B e. ZZ -> ( -. B e. ZZ -> A || ( C + B ) ) )
9 7 8 simpl2im 
 |-  ( A || B -> ( -. B e. ZZ -> A || ( C + B ) ) )
10 9 com12 
 |-  ( -. B e. ZZ -> ( A || B -> A || ( C + B ) ) )
11 10 adantr 
 |-  ( ( -. B e. ZZ /\ ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) ) -> ( A || B -> A || ( C + B ) ) )
12 dvdszrcl 
 |-  ( A || ( C + B ) -> ( A e. ZZ /\ ( C + B ) e. ZZ ) )
13 zcn 
 |-  ( C e. ZZ -> C e. CC )
14 13 adantr 
 |-  ( ( C e. ZZ /\ ( B e. RR /\ -. B e. ZZ ) ) -> C e. CC )
15 recn 
 |-  ( B e. RR -> B e. CC )
16 15 ad2antrl 
 |-  ( ( C e. ZZ /\ ( B e. RR /\ -. B e. ZZ ) ) -> B e. CC )
17 14 16 addcomd 
 |-  ( ( C e. ZZ /\ ( B e. RR /\ -. B e. ZZ ) ) -> ( C + B ) = ( B + C ) )
18 eldif 
 |-  ( B e. ( RR \ ZZ ) <-> ( B e. RR /\ -. B e. ZZ ) )
19 nzadd 
 |-  ( ( B e. ( RR \ ZZ ) /\ C e. ZZ ) -> ( B + C ) e. ( RR \ ZZ ) )
20 19 eldifbd 
 |-  ( ( B e. ( RR \ ZZ ) /\ C e. ZZ ) -> -. ( B + C ) e. ZZ )
21 20 expcom 
 |-  ( C e. ZZ -> ( B e. ( RR \ ZZ ) -> -. ( B + C ) e. ZZ ) )
22 18 21 syl5bir 
 |-  ( C e. ZZ -> ( ( B e. RR /\ -. B e. ZZ ) -> -. ( B + C ) e. ZZ ) )
23 22 imp 
 |-  ( ( C e. ZZ /\ ( B e. RR /\ -. B e. ZZ ) ) -> -. ( B + C ) e. ZZ )
24 17 23 eqneltrd 
 |-  ( ( C e. ZZ /\ ( B e. RR /\ -. B e. ZZ ) ) -> -. ( C + B ) e. ZZ )
25 24 exp32 
 |-  ( C e. ZZ -> ( B e. RR -> ( -. B e. ZZ -> -. ( C + B ) e. ZZ ) ) )
26 pm2.21 
 |-  ( -. ( C + B ) e. ZZ -> ( ( C + B ) e. ZZ -> A || B ) )
27 25 26 syl8 
 |-  ( C e. ZZ -> ( B e. RR -> ( -. B e. ZZ -> ( ( C + B ) e. ZZ -> A || B ) ) ) )
28 27 adantr 
 |-  ( ( C e. ZZ /\ A || C ) -> ( B e. RR -> ( -. B e. ZZ -> ( ( C + B ) e. ZZ -> A || B ) ) ) )
29 28 com12 
 |-  ( B e. RR -> ( ( C e. ZZ /\ A || C ) -> ( -. B e. ZZ -> ( ( C + B ) e. ZZ -> A || B ) ) ) )
30 29 a1i 
 |-  ( A e. ZZ -> ( B e. RR -> ( ( C e. ZZ /\ A || C ) -> ( -. B e. ZZ -> ( ( C + B ) e. ZZ -> A || B ) ) ) ) )
31 30 3imp 
 |-  ( ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) -> ( -. B e. ZZ -> ( ( C + B ) e. ZZ -> A || B ) ) )
32 31 impcom 
 |-  ( ( -. B e. ZZ /\ ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) ) -> ( ( C + B ) e. ZZ -> A || B ) )
33 32 com12 
 |-  ( ( C + B ) e. ZZ -> ( ( -. B e. ZZ /\ ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) ) -> A || B ) )
34 12 33 simpl2im 
 |-  ( A || ( C + B ) -> ( ( -. B e. ZZ /\ ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) ) -> A || B ) )
35 34 com12 
 |-  ( ( -. B e. ZZ /\ ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) ) -> ( A || ( C + B ) -> A || B ) )
36 11 35 impbid 
 |-  ( ( -. B e. ZZ /\ ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) ) -> ( A || B <-> A || ( C + B ) ) )
37 36 ex 
 |-  ( -. B e. ZZ -> ( ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) ) )
38 6 37 pm2.61i 
 |-  ( ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) )