Metamath Proof Explorer

Theorem irrmul

Description: The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008)

Ref Expression
Assertion irrmul ⊢ A ∈ ℝ ∖ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℝ ∖ ℚ

Proof

Step Hyp Ref Expression
1 eldif ⊢ A ∈ ℝ ∖ ℚ ↔ A ∈ ℝ ∧ ¬ A ∈ ℚ
2 qre ⊢ B ∈ ℚ → B ∈ ℝ
3 remulcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ⁢ B ∈ ℝ
4 2 3 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℚ → A ⁢ B ∈ ℝ
5 4 ad2ant2r ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℝ
6 qdivcl ⊢ A ⁢ B ∈ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B B ∈ ℚ
7 6 3expb ⊢ A ⁢ B ∈ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B B ∈ ℚ
8 7 expcom ⊢ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℚ → A ⁢ B B ∈ ℚ
9 8 adantl ⊢ A ∈ ℝ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℚ → A ⁢ B B ∈ ℚ
10 qcn ⊢ B ∈ ℚ → B ∈ ℂ
11 recn ⊢ A ∈ ℝ → A ∈ ℂ
12 divcan4 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ B B = A
13 11 12 syl3an1 ⊢ A ∈ ℝ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ B B = A
14 10 13 syl3an2 ⊢ A ∈ ℝ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B B = A
15 14 3expb ⊢ A ∈ ℝ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B B = A
16 15 eleq1d ⊢ A ∈ ℝ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B B ∈ ℚ ↔ A ∈ ℚ
17 9 16 sylibd ⊢ A ∈ ℝ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℚ → A ∈ ℚ
18 17 con3d ⊢ A ∈ ℝ ∧ B ∈ ℚ ∧ B ≠ 0 → ¬ A ∈ ℚ → ¬ A ⁢ B ∈ ℚ
19 18 ex ⊢ A ∈ ℝ → B ∈ ℚ ∧ B ≠ 0 → ¬ A ∈ ℚ → ¬ A ⁢ B ∈ ℚ
20 19 com23 ⊢ A ∈ ℝ → ¬ A ∈ ℚ → B ∈ ℚ ∧ B ≠ 0 → ¬ A ⁢ B ∈ ℚ
21 20 imp31 ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → ¬ A ⁢ B ∈ ℚ
22 5 21 jca ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℝ ∧ ¬ A ⁢ B ∈ ℚ
23 22 3impb ⊢ A ∈ ℝ ∧ ¬ A ∈ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℝ ∧ ¬ A ⁢ B ∈ ℚ
24 1 23 syl3an1b ⊢ A ∈ ℝ ∖ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℝ ∧ ¬ A ⁢ B ∈ ℚ
25 eldif ⊢ A ⁢ B ∈ ℝ ∖ ℚ ↔ A ⁢ B ∈ ℝ ∧ ¬ A ⁢ B ∈ ℚ
26 24 25 sylibr ⊢ A ∈ ℝ ∖ ℚ ∧ B ∈ ℚ ∧ B ≠ 0 → A ⁢ B ∈ ℝ ∖ ℚ