Proof of Theorem irrmul
Step | Hyp | Ref
| Expression |
1 | | eldif 3130 |
. . 3
⊢ (𝐴 ∈ (ℝ ∖
ℚ) ↔ (𝐴 ∈
ℝ ∧ ¬ 𝐴
∈ ℚ)) |
2 | | qre 9573 |
. . . . . . 7
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℝ) |
3 | | remulcl 7891 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) |
4 | 2, 3 | sylan2 284 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℚ) → (𝐴 · 𝐵) ∈ ℝ) |
5 | 4 | ad2ant2r 506 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝐵 ∈ ℚ ∧
𝐵 ≠ 0)) → (𝐴 · 𝐵) ∈ ℝ) |
6 | | qdivcl 9591 |
. . . . . . . . . . . . 13
⊢ (((𝐴 · 𝐵) ∈ ℚ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐵) / 𝐵) ∈ ℚ) |
7 | 6 | 3expb 1199 |
. . . . . . . . . . . 12
⊢ (((𝐴 · 𝐵) ∈ ℚ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) / 𝐵) ∈ ℚ) |
8 | 7 | expcom 115 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐵) ∈ ℚ → ((𝐴 · 𝐵) / 𝐵) ∈ ℚ)) |
9 | 8 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) ∈ ℚ → ((𝐴 · 𝐵) / 𝐵) ∈ ℚ)) |
10 | | recn 7896 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
11 | 10 | 3ad2ant1 1013 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → 𝐴 ∈
ℂ) |
12 | | qcn 9582 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℚ → 𝐵 ∈
ℂ) |
13 | 12 | 3ad2ant2 1014 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → 𝐵 ∈
ℂ) |
14 | | simp3 994 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → 𝐵 ≠ 0) |
15 | | 0z 9212 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℤ |
16 | | zq 9574 |
. . . . . . . . . . . . . . . . 17
⊢ (0 ∈
ℤ → 0 ∈ ℚ) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℚ |
18 | | qapne 9587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ ℚ ∧ 0 ∈
ℚ) → (𝐵 # 0
↔ 𝐵 ≠
0)) |
19 | 17, 18 | mpan2 423 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℚ → (𝐵 # 0 ↔ 𝐵 ≠ 0)) |
20 | 19 | 3ad2ant2 1014 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (𝐵 # 0 ↔ 𝐵 ≠ 0)) |
21 | 14, 20 | mpbird 166 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → 𝐵 # 0) |
22 | 11, 13, 21 | divcanap4d 8702 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴) |
23 | 22 | 3expb 1199 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) / 𝐵) = 𝐴) |
24 | 23 | eleq1d 2239 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (((𝐴 · 𝐵) / 𝐵) ∈ ℚ ↔ 𝐴 ∈ ℚ)) |
25 | 9, 24 | sylibd 148 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → ((𝐴 · 𝐵) ∈ ℚ → 𝐴 ∈ ℚ)) |
26 | 25 | con3d 626 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (¬ 𝐴 ∈ ℚ → ¬
(𝐴 · 𝐵) ∈
ℚ)) |
27 | 26 | ex 114 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((𝐵 ∈ ℚ ∧ 𝐵 ≠ 0) → (¬ 𝐴 ∈ ℚ → ¬
(𝐴 · 𝐵) ∈
ℚ))) |
28 | 27 | com23 78 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (¬
𝐴 ∈ ℚ →
((𝐵 ∈ ℚ ∧
𝐵 ≠ 0) → ¬
(𝐴 · 𝐵) ∈
ℚ))) |
29 | 28 | imp31 254 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝐵 ∈ ℚ ∧
𝐵 ≠ 0)) → ¬
(𝐴 · 𝐵) ∈
ℚ) |
30 | 5, 29 | jca 304 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
(𝐵 ∈ ℚ ∧
𝐵 ≠ 0)) → ((𝐴 · 𝐵) ∈ ℝ ∧ ¬ (𝐴 · 𝐵) ∈ ℚ)) |
31 | 30 | 3impb 1194 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ ¬
𝐴 ∈ ℚ) ∧
𝐵 ∈ ℚ ∧
𝐵 ≠ 0) → ((𝐴 · 𝐵) ∈ ℝ ∧ ¬ (𝐴 · 𝐵) ∈ ℚ)) |
32 | 1, 31 | syl3an1b 1269 |
. 2
⊢ ((𝐴 ∈ (ℝ ∖
ℚ) ∧ 𝐵 ∈
ℚ ∧ 𝐵 ≠ 0)
→ ((𝐴 · 𝐵) ∈ ℝ ∧ ¬
(𝐴 · 𝐵) ∈
ℚ)) |
33 | | eldif 3130 |
. 2
⊢ ((𝐴 · 𝐵) ∈ (ℝ ∖ ℚ) ↔
((𝐴 · 𝐵) ∈ ℝ ∧ ¬
(𝐴 · 𝐵) ∈
ℚ)) |
34 | 32, 33 | sylibr 133 |
1
⊢ ((𝐴 ∈ (ℝ ∖
ℚ) ∧ 𝐵 ∈
ℚ ∧ 𝐵 ≠ 0)
→ (𝐴 · 𝐵) ∈ (ℝ ∖
ℚ)) |