Step |
Hyp |
Ref |
Expression |
1 |
|
crrecz.1 |
|- A e. RR |
2 |
|
crrecz.2 |
|- B e. RR |
3 |
1
|
recni |
|- A e. CC |
4 |
3
|
sqcli |
|- ( A ^ 2 ) e. CC |
5 |
|
ax-icn |
|- _i e. CC |
6 |
2
|
recni |
|- B e. CC |
7 |
5 6
|
mulcli |
|- ( _i x. B ) e. CC |
8 |
7
|
sqcli |
|- ( ( _i x. B ) ^ 2 ) e. CC |
9 |
4 8
|
negsubi |
|- ( ( A ^ 2 ) + -u ( ( _i x. B ) ^ 2 ) ) = ( ( A ^ 2 ) - ( ( _i x. B ) ^ 2 ) ) |
10 |
5 6
|
sqmuli |
|- ( ( _i x. B ) ^ 2 ) = ( ( _i ^ 2 ) x. ( B ^ 2 ) ) |
11 |
|
i2 |
|- ( _i ^ 2 ) = -u 1 |
12 |
11
|
oveq1i |
|- ( ( _i ^ 2 ) x. ( B ^ 2 ) ) = ( -u 1 x. ( B ^ 2 ) ) |
13 |
|
ax-1cn |
|- 1 e. CC |
14 |
6
|
sqcli |
|- ( B ^ 2 ) e. CC |
15 |
13 14
|
mulneg1i |
|- ( -u 1 x. ( B ^ 2 ) ) = -u ( 1 x. ( B ^ 2 ) ) |
16 |
10 12 15
|
3eqtri |
|- ( ( _i x. B ) ^ 2 ) = -u ( 1 x. ( B ^ 2 ) ) |
17 |
16
|
negeqi |
|- -u ( ( _i x. B ) ^ 2 ) = -u -u ( 1 x. ( B ^ 2 ) ) |
18 |
13 14
|
mulcli |
|- ( 1 x. ( B ^ 2 ) ) e. CC |
19 |
18
|
negnegi |
|- -u -u ( 1 x. ( B ^ 2 ) ) = ( 1 x. ( B ^ 2 ) ) |
20 |
14
|
mulid2i |
|- ( 1 x. ( B ^ 2 ) ) = ( B ^ 2 ) |
21 |
17 19 20
|
3eqtri |
|- -u ( ( _i x. B ) ^ 2 ) = ( B ^ 2 ) |
22 |
21
|
oveq2i |
|- ( ( A ^ 2 ) + -u ( ( _i x. B ) ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) |
23 |
3 7
|
subsqi |
|- ( ( A ^ 2 ) - ( ( _i x. B ) ^ 2 ) ) = ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) |
24 |
9 22 23
|
3eqtr3ri |
|- ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) |
25 |
24
|
oveq1i |
|- ( ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) |
26 |
|
neorian |
|- ( ( A =/= 0 \/ B =/= 0 ) <-> -. ( A = 0 /\ B = 0 ) ) |
27 |
|
sumsqeq0 |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 ) ) |
28 |
1 2 27
|
mp2an |
|- ( ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) = 0 ) |
29 |
28
|
necon3bbii |
|- ( -. ( A = 0 /\ B = 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 ) |
30 |
26 29
|
bitri |
|- ( ( A =/= 0 \/ B =/= 0 ) <-> ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 ) |
31 |
3 7
|
addcli |
|- ( A + ( _i x. B ) ) e. CC |
32 |
3 7
|
subcli |
|- ( A - ( _i x. B ) ) e. CC |
33 |
4 14
|
addcli |
|- ( ( A ^ 2 ) + ( B ^ 2 ) ) e. CC |
34 |
31 32 33
|
divasszi |
|- ( ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 -> ( ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) ) |
35 |
30 34
|
sylbi |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( ( ( A + ( _i x. B ) ) x. ( A - ( _i x. B ) ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) ) |
36 |
|
divid |
|- ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) e. CC /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = 1 ) |
37 |
33 36
|
mpan |
|- ( ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = 1 ) |
38 |
30 37
|
sylbi |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) = 1 ) |
39 |
25 35 38
|
3eqtr3a |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 ) |
40 |
32 33
|
divclzi |
|- ( ( ( A ^ 2 ) + ( B ^ 2 ) ) =/= 0 -> ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC ) |
41 |
30 40
|
sylbi |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC ) |
42 |
31
|
a1i |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( A + ( _i x. B ) ) e. CC ) |
43 |
|
crne0 |
|- ( ( A e. RR /\ B e. RR ) -> ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 ) ) |
44 |
1 2 43
|
mp2an |
|- ( ( A =/= 0 \/ B =/= 0 ) <-> ( A + ( _i x. B ) ) =/= 0 ) |
45 |
44
|
biimpi |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( A + ( _i x. B ) ) =/= 0 ) |
46 |
|
divmul |
|- ( ( 1 e. CC /\ ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC /\ ( ( A + ( _i x. B ) ) e. CC /\ ( A + ( _i x. B ) ) =/= 0 ) ) -> ( ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) <-> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 ) ) |
47 |
13 46
|
mp3an1 |
|- ( ( ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) e. CC /\ ( ( A + ( _i x. B ) ) e. CC /\ ( A + ( _i x. B ) ) =/= 0 ) ) -> ( ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) <-> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 ) ) |
48 |
41 42 45 47
|
syl12anc |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) <-> ( ( A + ( _i x. B ) ) x. ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) = 1 ) ) |
49 |
39 48
|
mpbird |
|- ( ( A =/= 0 \/ B =/= 0 ) -> ( 1 / ( A + ( _i x. B ) ) ) = ( ( A - ( _i x. B ) ) / ( ( A ^ 2 ) + ( B ^ 2 ) ) ) ) |