Description: Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. Equation 5 of Kreyszig p. 12. (Contributed by NM, 12-Nov-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | conjmul | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll | |
|
2 | simprl | |
|
3 | reccl | |
|
4 | 3 | adantr | |
5 | 1 2 4 | mul32d | |
6 | recid | |
|
7 | 6 | oveq1d | |
8 | 7 | adantr | |
9 | mulid2 | |
|
10 | 9 | ad2antrl | |
11 | 5 8 10 | 3eqtrd | |
12 | reccl | |
|
13 | 12 | adantl | |
14 | 1 2 13 | mulassd | |
15 | recid | |
|
16 | 15 | oveq2d | |
17 | 16 | adantl | |
18 | mulid1 | |
|
19 | 18 | ad2antrr | |
20 | 14 17 19 | 3eqtrd | |
21 | 11 20 | oveq12d | |
22 | mulcl | |
|
23 | 22 | ad2ant2r | |
24 | 23 4 13 | adddid | |
25 | addcom | |
|
26 | 25 | ad2ant2r | |
27 | 21 24 26 | 3eqtr4d | |
28 | 22 | mulid1d | |
29 | 28 | ad2ant2r | |
30 | 27 29 | eqeq12d | |
31 | addcl | |
|
32 | 3 12 31 | syl2an | |
33 | mulne0 | |
|
34 | ax-1cn | |
|
35 | mulcan | |
|
36 | 34 35 | mp3an2 | |
37 | 32 23 33 36 | syl12anc | |
38 | eqcom | |
|
39 | muleqadd | |
|
40 | 38 39 | syl5bb | |
41 | 40 | ad2ant2r | |
42 | 30 37 41 | 3bitr3d | |