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 ∈ ℝ ∖ ℤ ∧ B ∈ ℤ → A + B ∈ ℝ ∖ ℤ

Proof

Step Hyp Ref Expression
1 eldif ⊢ A ∈ ℝ ∖ ℤ ↔ A ∈ ℝ ∧ ¬ A ∈ ℤ
2 zre ⊢ B ∈ ℤ → B ∈ ℝ
3 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
4 2 3 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℤ → A + B ∈ ℝ
5 4 adantlr ⊢ A ∈ ℝ ∧ ¬ A ∈ ℤ ∧ B ∈ ℤ → A + B ∈ ℝ
6 zsubcl ⊢ A + B ∈ ℤ ∧ B ∈ ℤ → A + B - B ∈ ℤ
7 6 expcom ⊢ B ∈ ℤ → A + B ∈ ℤ → A + B - B ∈ ℤ
8 7 adantl ⊢ A ∈ ℝ ∧ B ∈ ℤ → A + B ∈ ℤ → A + B - B ∈ ℤ
9 recn ⊢ A ∈ ℝ → A ∈ ℂ
10 zcn ⊢ B ∈ ℤ → B ∈ ℂ
11 pncan ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - B = A
12 9 10 11 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℤ → A + B - B = A
13 12 eleq1d ⊢ A ∈ ℝ ∧ B ∈ ℤ → A + B - B ∈ ℤ ↔ A ∈ ℤ
14 8 13 sylibd ⊢ A ∈ ℝ ∧ B ∈ ℤ → A + B ∈ ℤ → A ∈ ℤ
15 14 con3d ⊢ A ∈ ℝ ∧ B ∈ ℤ → ¬ A ∈ ℤ → ¬ A + B ∈ ℤ
16 15 ex ⊢ A ∈ ℝ → B ∈ ℤ → ¬ A ∈ ℤ → ¬ A + B ∈ ℤ
17 16 com23 ⊢ A ∈ ℝ → ¬ A ∈ ℤ → B ∈ ℤ → ¬ A + B ∈ ℤ
18 17 imp31 ⊢ A ∈ ℝ ∧ ¬ A ∈ ℤ ∧ B ∈ ℤ → ¬ A + B ∈ ℤ
19 5 18 jca ⊢ A ∈ ℝ ∧ ¬ A ∈ ℤ ∧ B ∈ ℤ → A + B ∈ ℝ ∧ ¬ A + B ∈ ℤ
20 1 19 sylanb ⊢ A ∈ ℝ ∖ ℤ ∧ B ∈ ℤ → A + B ∈ ℝ ∧ ¬ A + B ∈ ℤ
21 eldif ⊢ A + B ∈ ℝ ∖ ℤ ↔ A + B ∈ ℝ ∧ ¬ A + B ∈ ℤ
22 20 21 sylibr ⊢ A ∈ ℝ ∖ ℤ ∧ B ∈ ℤ → A + B ∈ ℝ ∖ ℤ