Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem conjmult 5753

Description: Two numbers whose reciprocals add to 1 are called "conjugates" and satisfy this relationship. Equation 5 of [Kreyszig] p. 12.

Assertion

Ref	Expression
conjmult

---

Proof of Theorem conjmult

Step	Hyp	Ref	Expression
1		mul23t 5391	. . . . . . 7
2		simpll 412	. . . . . . 7
3		simprl 414	. . . . . . 7
4		recclt 5684	. . . . . . . 8
5	4	adantr 389	. . . . . . 7
6	1, 2, 3, 5	syl3anc 856	. . . . . 6
7		recidt 5698	. . . . . . . 8
8	7	opreq1d 3960	. . . . . . 7
9	8	adantr 389	. . . . . 6
10		mulid2t 5389	. . . . . . 7
11	10	ad2antrl 406	. . . . . 6
12	6, 9, 11	3eqtrd 1503	. . . . 5
13		axmulass 5250	. . . . . . 7
14		recclt 5684	. . . . . . . 8
15	14	adantl 388	. . . . . . 7
16	13, 2, 3, 15	syl3anc 856	. . . . . 6
17		recidt 5698	. . . . . . . 8
18	17	opreq2d 3961	. . . . . . 7
19	18	adantl 388	. . . . . 6
20		ax1id 5254	. . . . . . 7
21	20	ad2antrr 404	. . . . . 6
22	16, 19, 21	3eqtrd 1503	. . . . 5
23	12, 22	opreq12d 3963	. . . 4
24		axdistr 5251	. . . . 5
25		axmulcl 5245	. . . . . 6
26	25	ad2ant2r 409	. . . . 5
27	24, 26, 5, 15	syl3anc 856	. . . 4
28		axaddcom 5247	. . . . 5
29	28	ad2ant2r 409	. . . 4
30	23, 27, 29	3eqtr4d 1509	. . 3
31		ax1id 5254	. . . . 5
32	25, 31	syl 10	. . . 4
33	32	ad2ant2r 409	. . 3
34	30, 33	eqeq12d 1481	. 2
35		ax1cn 5241	. . . 4
36		mulcant 5661	. . . 4
37	35, 36	mp3anl3 909	. . 3
38		axaddcl 5243	. . . . 5
39	38, 4, 14	syl2an 454	. . . 4
40	26, 39	jca 288	. . 3
41		muln0t 5667	. . 3
42	37, 40, 41	sylanc 471	. 2
43		muleqaddt 5669	. . . 4
44		eqcom 1469	. . . 4
45	43, 44	syl5bb 530	. . 3
46	45	ad2ant2r 409	. 2
47	34, 42, 46	3bitr3d 546	1

Colors of variables: wff set class

Syntax hints:   wi 3   wb 146   wa 223   wceq 953   wcel 955   wne 1577  (class class class)co 3948  cc 5204  cc0 5206  c1 5207   caddc 5209   cmul 5211   cmin 5264   cdiv 5266

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq