Metamath Proof Explorer

Theorem cjreb

Description: A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of Gleason p. 133. (Contributed by NM, 2-Jul-2005) (Revised by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion cjreb ⊢ A ∈ ℂ → A ∈ ℝ ↔ A ‾ = A

Proof

Step Hyp Ref Expression
1 recl ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℝ
2 1 recnd ⊢ A ∈ ℂ → ℜ ⁡ A ∈ ℂ
3 ax-icn ⊢ i ∈ ℂ
4 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
5 4 recnd ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℂ
6 mulcl ⊢ i ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → i ⁢ ℑ ⁡ A ∈ ℂ
7 3 5 6 sylancr ⊢ A ∈ ℂ → i ⁢ ℑ ⁡ A ∈ ℂ
8 2 7 negsubd ⊢ A ∈ ℂ → ℜ ⁡ A + − i ⁢ ℑ ⁡ A = ℜ ⁡ A − i ⁢ ℑ ⁡ A
9 mulneg2 ⊢ i ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
10 3 5 9 sylancr ⊢ A ∈ ℂ → i ⁢ − ℑ ⁡ A = − i ⁢ ℑ ⁡ A
11 10 oveq2d ⊢ A ∈ ℂ → ℜ ⁡ A + i ⁢ − ℑ ⁡ A = ℜ ⁡ A + − i ⁢ ℑ ⁡ A
12 remim ⊢ A ∈ ℂ → A ‾ = ℜ ⁡ A − i ⁢ ℑ ⁡ A
13 8 11 12 3eqtr4rd ⊢ A ∈ ℂ → A ‾ = ℜ ⁡ A + i ⁢ − ℑ ⁡ A
14 replim ⊢ A ∈ ℂ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
15 13 14 eqeq12d ⊢ A ∈ ℂ → A ‾ = A ↔ ℜ ⁡ A + i ⁢ − ℑ ⁡ A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
16 5 negcld ⊢ A ∈ ℂ → − ℑ ⁡ A ∈ ℂ
17 mulcl ⊢ i ∈ ℂ ∧ − ℑ ⁡ A ∈ ℂ → i ⁢ − ℑ ⁡ A ∈ ℂ
18 3 16 17 sylancr ⊢ A ∈ ℂ → i ⁢ − ℑ ⁡ A ∈ ℂ
19 2 18 7 addcand ⊢ A ∈ ℂ → ℜ ⁡ A + i ⁢ − ℑ ⁡ A = ℜ ⁡ A + i ⁢ ℑ ⁡ A ↔ i ⁢ − ℑ ⁡ A = i ⁢ ℑ ⁡ A
20 eqcom ⊢ − ℑ ⁡ A = ℑ ⁡ A ↔ ℑ ⁡ A = − ℑ ⁡ A
21 5 eqnegd ⊢ A ∈ ℂ → ℑ ⁡ A = − ℑ ⁡ A ↔ ℑ ⁡ A = 0
22 20 21 bitrid ⊢ A ∈ ℂ → − ℑ ⁡ A = ℑ ⁡ A ↔ ℑ ⁡ A = 0
23 ine0 ⊢ i ≠ 0
24 3 23 pm3.2i ⊢ i ∈ ℂ ∧ i ≠ 0
25 24 a1i ⊢ A ∈ ℂ → i ∈ ℂ ∧ i ≠ 0
26 mulcan ⊢ − ℑ ⁡ A ∈ ℂ ∧ ℑ ⁡ A ∈ ℂ ∧ i ∈ ℂ ∧ i ≠ 0 → i ⁢ − ℑ ⁡ A = i ⁢ ℑ ⁡ A ↔ − ℑ ⁡ A = ℑ ⁡ A
27 16 5 25 26 syl3anc ⊢ A ∈ ℂ → i ⁢ − ℑ ⁡ A = i ⁢ ℑ ⁡ A ↔ − ℑ ⁡ A = ℑ ⁡ A
28 reim0b ⊢ A ∈ ℂ → A ∈ ℝ ↔ ℑ ⁡ A = 0
29 22 27 28 3bitr4d ⊢ A ∈ ℂ → i ⁢ − ℑ ⁡ A = i ⁢ ℑ ⁡ A ↔ A ∈ ℝ
30 15 19 29 3bitrrd ⊢ A ∈ ℂ → A ∈ ℝ ↔ A ‾ = A