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 ( ( ( 𝑃 ∈ ℂ ∧ 𝑃 ≠ 0 ) ∧ ( 𝑄 ∈ ℂ ∧ 𝑄 ≠ 0 ) ) → ( ( ( 1 / 𝑃 ) + ( 1 / 𝑄 ) ) = 1 ↔ ( ( 𝑃 − 1 ) · ( 𝑄 − 1 ) ) = 1 ) )

Proof

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