Metamath Proof Explorer

Theorem conjmul

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 ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→1P+1Q=1↔P−1⁢Q−1=1

Proof

Step Hyp Ref Expression
1 simpll ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P∈ℂ
2 simprl ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→Q∈ℂ
3 reccl ⊢P∈ℂ∧P≠0→1P∈ℂ
4 3 adantr ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→1P∈ℂ
5 1 2 4 mul32d ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1P=P⁢1P⁢Q
6 recid ⊢P∈ℂ∧P≠0→P⁢1P=1
7 6 oveq1d ⊢P∈ℂ∧P≠0→P⁢1P⁢Q=1⁢Q
8 7 adantr ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢1P⁢Q=1⁢Q
9 mullid ⊢Q∈ℂ→1⁢Q=Q
10 9 ad2antrl ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→1⁢Q=Q
11 5 8 10 3eqtrd ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1P=Q
12 reccl ⊢Q∈ℂ∧Q≠0→1Q∈ℂ
13 12 adantl ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→1Q∈ℂ
14 1 2 13 mulassd ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1Q=P⁢Q⁢1Q
15 recid ⊢Q∈ℂ∧Q≠0→Q⁢1Q=1
16 15 oveq2d ⊢Q∈ℂ∧Q≠0→P⁢Q⁢1Q=P⋅1
17 16 adantl ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1Q=P⋅1
18 mulrid ⊢P∈ℂ→P⋅1=P
19 18 ad2antrr ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⋅1=P
20 14 17 19 3eqtrd ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1Q=P
21 11 20 oveq12d ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1P+P⁢Q⁢1Q=Q+P
22 mulcl ⊢P∈ℂ∧Q∈ℂ→P⁢Q∈ℂ
23 22 ad2ant2r ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q∈ℂ
24 23 4 13 adddid ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1P+1Q=P⁢Q⁢1P+P⁢Q⁢1Q
25 addcom ⊢P∈ℂ∧Q∈ℂ→P+Q=Q+P
26 25 ad2ant2r ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P+Q=Q+P
27 21 24 26 3eqtr4d ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1P+1Q=P+Q
28 22 mulridd ⊢P∈ℂ∧Q∈ℂ→P⁢Q⋅1=P⁢Q
29 28 ad2ant2r ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⋅1=P⁢Q
30 27 29 eqeq12d ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1P+1Q=P⁢Q⋅1↔P+Q=P⁢Q
31 addcl ⊢1P∈ℂ∧1Q∈ℂ→1P+1Q∈ℂ
32 3 12 31 syl2an ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→1P+1Q∈ℂ
33 mulne0 ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q≠0
34 ax-1cn ⊢1∈ℂ
35 mulcan ⊢1P+1Q∈ℂ∧1∈ℂ∧P⁢Q∈ℂ∧P⁢Q≠0→P⁢Q⁢1P+1Q=P⁢Q⋅1↔1P+1Q=1
36 34 35 mp3an2 ⊢1P+1Q∈ℂ∧P⁢Q∈ℂ∧P⁢Q≠0→P⁢Q⁢1P+1Q=P⁢Q⋅1↔1P+1Q=1
37 32 23 33 36 syl12anc ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P⁢Q⁢1P+1Q=P⁢Q⋅1↔1P+1Q=1
38 eqcom ⊢P+Q=P⁢Q↔P⁢Q=P+Q
39 muleqadd ⊢P∈ℂ∧Q∈ℂ→P⁢Q=P+Q↔P−1⁢Q−1=1
40 38 39 bitrid ⊢P∈ℂ∧Q∈ℂ→P+Q=P⁢Q↔P−1⁢Q−1=1
41 40 ad2ant2r ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→P+Q=P⁢Q↔P−1⁢Q−1=1
42 30 37 41 3bitr3d ⊢P∈ℂ∧P≠0∧Q∈ℂ∧Q≠0→1P+1Q=1↔P−1⁢Q−1=1