# Metamath Proof Explorer

## Theorem atandm3

Description: A compact form of atandm . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atandm3 ${⊢}{A}\in \mathrm{dom}arctan↔\left({A}\in ℂ\wedge {{A}}^{2}\ne -1\right)$

### Proof

Step Hyp Ref Expression
1 3anass ${⊢}\left({A}\in ℂ\wedge {A}\ne -\mathrm{i}\wedge {A}\ne \mathrm{i}\right)↔\left({A}\in ℂ\wedge \left({A}\ne -\mathrm{i}\wedge {A}\ne \mathrm{i}\right)\right)$
2 atandm ${⊢}{A}\in \mathrm{dom}arctan↔\left({A}\in ℂ\wedge {A}\ne -\mathrm{i}\wedge {A}\ne \mathrm{i}\right)$
3 ax-icn ${⊢}\mathrm{i}\in ℂ$
4 sqeqor ${⊢}\left({A}\in ℂ\wedge \mathrm{i}\in ℂ\right)\to \left({{A}}^{2}={\mathrm{i}}^{2}↔\left({A}=\mathrm{i}\vee {A}=-\mathrm{i}\right)\right)$
5 3 4 mpan2 ${⊢}{A}\in ℂ\to \left({{A}}^{2}={\mathrm{i}}^{2}↔\left({A}=\mathrm{i}\vee {A}=-\mathrm{i}\right)\right)$
6 i2 ${⊢}{\mathrm{i}}^{2}=-1$
7 6 eqeq2i ${⊢}{{A}}^{2}={\mathrm{i}}^{2}↔{{A}}^{2}=-1$
8 orcom ${⊢}\left({A}=\mathrm{i}\vee {A}=-\mathrm{i}\right)↔\left({A}=-\mathrm{i}\vee {A}=\mathrm{i}\right)$
9 5 7 8 3bitr3g ${⊢}{A}\in ℂ\to \left({{A}}^{2}=-1↔\left({A}=-\mathrm{i}\vee {A}=\mathrm{i}\right)\right)$
10 9 necon3abid ${⊢}{A}\in ℂ\to \left({{A}}^{2}\ne -1↔¬\left({A}=-\mathrm{i}\vee {A}=\mathrm{i}\right)\right)$
11 neanior ${⊢}\left({A}\ne -\mathrm{i}\wedge {A}\ne \mathrm{i}\right)↔¬\left({A}=-\mathrm{i}\vee {A}=\mathrm{i}\right)$
12 10 11 syl6bbr ${⊢}{A}\in ℂ\to \left({{A}}^{2}\ne -1↔\left({A}\ne -\mathrm{i}\wedge {A}\ne \mathrm{i}\right)\right)$
13 12 pm5.32i ${⊢}\left({A}\in ℂ\wedge {{A}}^{2}\ne -1\right)↔\left({A}\in ℂ\wedge \left({A}\ne -\mathrm{i}\wedge {A}\ne \mathrm{i}\right)\right)$
14 1 2 13 3bitr4i ${⊢}{A}\in \mathrm{dom}arctan↔\left({A}\in ℂ\wedge {{A}}^{2}\ne -1\right)$