Metamath Proof Explorer

Theorem irradd

Description: The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008)

Ref Expression
Assertion irradd ⊢ A ∈ ℝ ∖ ℚ ∧ B ∈ ℚ → A + B ∈ ℝ ∖ ℚ

Proof

Step Hyp Ref Expression
1 eldif ⊢ A ∈ ℝ ∖ ℚ ↔ A ∈ ℝ ∧ ¬ A ∈ ℚ
2 qre ⊢ 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 qsubcl ⊢ 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 qcn ⊢ 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 ∈ ℝ ∖ ℚ