Metamath Proof Explorer


Theorem atandm3

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

Ref Expression
Assertion atandm3 A dom arctan A A 2 1

Proof

Step Hyp Ref Expression
1 3anass A A i A i A A i A i
2 atandm A dom arctan A A i A i
3 ax-icn i
4 sqeqor A i A 2 = i 2 A = i A = i
5 3 4 mpan2 A A 2 = i 2 A = i A = i
6 i2 i 2 = 1
7 6 eqeq2i A 2 = i 2 A 2 = 1
8 orcom A = i A = i A = i A = i
9 5 7 8 3bitr3g A A 2 = 1 A = i A = i
10 9 necon3abid A A 2 1 ¬ A = i A = i
11 neanior A i A i ¬ A = i A = i
12 10 11 bitr4di A A 2 1 A i A i
13 12 pm5.32i A A 2 1 A A i A i
14 1 2 13 3bitr4i A dom arctan A A 2 1