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 \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to ((\frac{1}{P}) + (\frac{1}{Q}) = 1 \leftrightarrow (P - 1) (Q - 1) = 1)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P \in ℂ$
2		simprl	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to Q \in ℂ$
3		reccl	$⊢ (P \in ℂ \land P \neq 0) \to \frac{1}{P} \in ℂ$
4	3	adantr	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to \frac{1}{P} \in ℂ$
5	1 2 4	mul32d	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q (\frac{1}{P}) = P (\frac{1}{P}) Q$
6		recid	$⊢ (P \in ℂ \land P \neq 0) \to P (\frac{1}{P}) = 1$
7	6	oveq1d	$⊢ (P \in ℂ \land P \neq 0) \to P (\frac{1}{P}) Q = 1 Q$
8	7	adantr	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P (\frac{1}{P}) Q = 1 Q$
9		mulid2	$⊢ Q \in ℂ \to 1 Q = Q$
10	9	ad2antrl	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to 1 Q = Q$
11	5 8 10	3eqtrd	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q (\frac{1}{P}) = Q$
12		reccl	$⊢ (Q \in ℂ \land Q \neq 0) \to \frac{1}{Q} \in ℂ$
13	12	adantl	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to \frac{1}{Q} \in ℂ$
14	1 2 13	mulassd	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q (\frac{1}{Q}) = P Q (\frac{1}{Q})$
15		recid	$⊢ (Q \in ℂ \land Q \neq 0) \to Q (\frac{1}{Q}) = 1$
16	15	oveq2d	$⊢ (Q \in ℂ \land Q \neq 0) \to P Q (\frac{1}{Q}) = P \cdot 1$
17	16	adantl	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q (\frac{1}{Q}) = P \cdot 1$
18		mulid1	$⊢ P \in ℂ \to P \cdot 1 = P$
19	18	ad2antrr	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P \cdot 1 = P$
20	14 17 19	3eqtrd	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q (\frac{1}{Q}) = P$
21	11 20	oveq12d	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q (\frac{1}{P}) + P Q (\frac{1}{Q}) = Q + P$
22		mulcl	$⊢ (P \in ℂ \land Q \in ℂ) \to P Q \in ℂ$
23	22	ad2ant2r	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q \in ℂ$
24	23 4 13	adddid	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q ((\frac{1}{P}) + (\frac{1}{Q})) = P Q (\frac{1}{P}) + P Q (\frac{1}{Q})$
25		addcom	$⊢ (P \in ℂ \land Q \in ℂ) \to P + Q = Q + P$
26	25	ad2ant2r	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P + Q = Q + P$
27	21 24 26	3eqtr4d	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q ((\frac{1}{P}) + (\frac{1}{Q})) = P + Q$
28	22	mulid1d	$⊢ (P \in ℂ \land Q \in ℂ) \to P Q \cdot 1 = P Q$
29	28	ad2ant2r	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q \cdot 1 = P Q$
30	27 29	eqeq12d	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to (P Q ((\frac{1}{P}) + (\frac{1}{Q})) = P Q \cdot 1 \leftrightarrow P + Q = P Q)$
31		addcl	$⊢ (\frac{1}{P} \in ℂ \land \frac{1}{Q} \in ℂ) \to (\frac{1}{P}) + (\frac{1}{Q}) \in ℂ$
32	3 12 31	syl2an	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to (\frac{1}{P}) + (\frac{1}{Q}) \in ℂ$
33		mulne0	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to P Q \neq 0$
34		ax-1cn	$⊢ 1 \in ℂ$
35		mulcan	$⊢ ((\frac{1}{P}) + (\frac{1}{Q}) \in ℂ \land 1 \in ℂ \land (P Q \in ℂ \land P Q \neq 0)) \to (P Q ((\frac{1}{P}) + (\frac{1}{Q})) = P Q \cdot 1 \leftrightarrow (\frac{1}{P}) + (\frac{1}{Q}) = 1)$
36	34 35	mp3an2	$⊢ ((\frac{1}{P}) + (\frac{1}{Q}) \in ℂ \land (P Q \in ℂ \land P Q \neq 0)) \to (P Q ((\frac{1}{P}) + (\frac{1}{Q})) = P Q \cdot 1 \leftrightarrow (\frac{1}{P}) + (\frac{1}{Q}) = 1)$
37	32 23 33 36	syl12anc	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to (P Q ((\frac{1}{P}) + (\frac{1}{Q})) = P Q \cdot 1 \leftrightarrow (\frac{1}{P}) + (\frac{1}{Q}) = 1)$
38		eqcom	$⊢ P + Q = P Q \leftrightarrow P Q = P + Q$
39		muleqadd	$⊢ (P \in ℂ \land Q \in ℂ) \to (P Q = P + Q \leftrightarrow (P - 1) (Q - 1) = 1)$
40	38 39	syl5bb	$⊢ (P \in ℂ \land Q \in ℂ) \to (P + Q = P Q \leftrightarrow (P - 1) (Q - 1) = 1)$
41	40	ad2ant2r	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to (P + Q = P Q \leftrightarrow (P - 1) (Q - 1) = 1)$
42	30 37 41	3bitr3d	$⊢ ((P \in ℂ \land P \neq 0) \land (Q \in ℂ \land Q \neq 0)) \to ((\frac{1}{P}) + (\frac{1}{Q}) = 1 \leftrightarrow (P - 1) (Q - 1) = 1)$

Metamath Proof Explorer

Theorem conjmul

Proof