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 ) )