Description: The rule sqrt ( z w ) = ( sqrt z ) ( sqrt w ) is not always true on the complex numbers, but it is true when the arguments of z and w sum to within the interval ( -upi , pi ] , so there are some cases such as this one with z = 1 +i A and w = 1 - i A which are true unconditionally. This result can also be stated as " sqrt ( 1 + z ) + sqrt ( 1 - z ) is analytic". (Contributed by Mario Carneiro, 3-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | atanlogadd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0red | |
|
2 | atandm2 | |
|
3 | 2 | simp1bi | |
4 | 3 | recld | |
5 | atanlogaddlem | |
|
6 | ax-1cn | |
|
7 | ax-icn | |
|
8 | mulcl | |
|
9 | 7 3 8 | sylancr | |
10 | addcl | |
|
11 | 6 9 10 | sylancr | |
12 | 2 | simp3bi | |
13 | 11 12 | logcld | |
14 | subcl | |
|
15 | 6 9 14 | sylancr | |
16 | 2 | simp2bi | |
17 | 15 16 | logcld | |
18 | 13 17 | addcomd | |
19 | mulneg2 | |
|
20 | 7 3 19 | sylancr | |
21 | 20 | oveq2d | |
22 | negsub | |
|
23 | 6 9 22 | sylancr | |
24 | 21 23 | eqtrd | |
25 | 24 | fveq2d | |
26 | 20 | oveq2d | |
27 | subneg | |
|
28 | 6 9 27 | sylancr | |
29 | 26 28 | eqtrd | |
30 | 29 | fveq2d | |
31 | 25 30 | oveq12d | |
32 | 18 31 | eqtr4d | |
33 | 32 | adantr | |
34 | atandmneg | |
|
35 | 4 | le0neg1d | |
36 | 35 | biimpa | |
37 | 3 | renegd | |
38 | 37 | adantr | |
39 | 36 38 | breqtrrd | |
40 | atanlogaddlem | |
|
41 | 34 39 40 | syl2an2r | |
42 | 33 41 | eqeltrd | |
43 | 1 4 5 42 | lecasei | |