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

Metamath Proof Explorer

Theorem nzadd

Description: The sum of a real number not being an integer and an integer is not an integer. (Contributed by AV, 19-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( A e. ( RR \ ZZ ) <-> ( A e. RR /\ -. A e. ZZ ) )
2 zre 
 |-  ( B e. ZZ -> B e. RR )
3 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4 2 3 sylan2 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( A + B ) e. RR )
5 4 adantlr 
 |-  ( ( ( A e. RR /\ -. A e. ZZ ) /\ B e. ZZ ) -> ( A + B ) e. RR )
6 zsubcl 
 |-  ( ( ( A + B ) e. ZZ /\ B e. ZZ ) -> ( ( A + B ) - B ) e. ZZ )
7 6 expcom 
 |-  ( B e. ZZ -> ( ( A + B ) e. ZZ -> ( ( A + B ) - B ) e. ZZ ) )
8 7 adantl 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( A + B ) e. ZZ -> ( ( A + B ) - B ) e. ZZ ) )
9 recn 
 |-  ( A e. RR -> A e. CC )
10 zcn 
 |-  ( B e. ZZ -> B e. CC )
11 pncan 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )
12 9 10 11 syl2an 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( A + B ) - B ) = A )
13 12 eleq1d 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( ( A + B ) - B ) e. ZZ <-> A e. ZZ ) )
14 8 13 sylibd 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( ( A + B ) e. ZZ -> A e. ZZ ) )
15 14 con3d 
 |-  ( ( A e. RR /\ B e. ZZ ) -> ( -. A e. ZZ -> -. ( A + B ) e. ZZ ) )
16 15 ex 
 |-  ( A e. RR -> ( B e. ZZ -> ( -. A e. ZZ -> -. ( A + B ) e. ZZ ) ) )
17 16 com23 
 |-  ( A e. RR -> ( -. A e. ZZ -> ( B e. ZZ -> -. ( A + B ) e. ZZ ) ) )
18 17 imp31 
 |-  ( ( ( A e. RR /\ -. A e. ZZ ) /\ B e. ZZ ) -> -. ( A + B ) e. ZZ )
19 5 18 jca 
 |-  ( ( ( A e. RR /\ -. A e. ZZ ) /\ B e. ZZ ) -> ( ( A + B ) e. RR /\ -. ( A + B ) e. ZZ ) )
20 1 19 sylanb 
 |-  ( ( A e. ( RR \ ZZ ) /\ B e. ZZ ) -> ( ( A + B ) e. RR /\ -. ( A + B ) e. ZZ ) )
21 eldif 
 |-  ( ( A + B ) e. ( RR \ ZZ ) <-> ( ( A + B ) e. RR /\ -. ( A + B ) e. ZZ ) )
22 20 21 sylibr 
 |-  ( ( A e. ( RR \ ZZ ) /\ B e. ZZ ) -> ( A + B ) e. ( RR \ ZZ ) )