1cubrlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 1cubrlem		Structured version Visualization version GIF version

Theorem 1cubrlem 26336

Description: The cube roots of unity. (Contributed by Mario Carneiro, 23-Apr-2015.)

**Assertion**
Ref	Expression
1cubrlem	⊢ ((-1↑_𝑐(2 / 3)) = ((-1 + (i · (√‘3))) / 2) ∧ ((-1↑_𝑐(2 / 3))↑2) = ((-1 − (i · (√‘3))) / 2))

**Proof of Theorem 1cubrlem**
Step	Hyp	Ref	Expression
1		neg1cn 12323	. . . 4 ⊢ -1 ∈ ℂ
2		neg1ne0 12325	. . . 4 ⊢ -1 ≠ 0
3		2re 12283	. . . . . 6 ⊢ 2 ∈ ℝ
4		3nn 12288	. . . . . 6 ⊢ 3 ∈ ℕ
5		nndivre 12250	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ 3 ∈ ℕ) → (2 / 3) ∈ ℝ)
6	3, 4, 5	mp2an 691	. . . . 5 ⊢ (2 / 3) ∈ ℝ
7	6	recni 11225	. . . 4 ⊢ (2 / 3) ∈ ℂ
8		cxpef 26165	. . . 4 ⊢ ((-1 ∈ ℂ ∧ -1 ≠ 0 ∧ (2 / 3) ∈ ℂ) → (-1↑_𝑐(2 / 3)) = (exp‘((2 / 3) · (log‘-1))))
9	1, 2, 7, 8	mp3an 1462	. . 3 ⊢ (-1↑_𝑐(2 / 3)) = (exp‘((2 / 3) · (log‘-1)))
10		logm1 26089	. . . . . 6 ⊢ (log‘-1) = (i · π)
11	10	oveq2i 7417	. . . . 5 ⊢ ((2 / 3) · (log‘-1)) = ((2 / 3) · (i · π))
12		ax-icn 11166	. . . . . 6 ⊢ i ∈ ℂ
13		pire 25960	. . . . . . 7 ⊢ π ∈ ℝ
14	13	recni 11225	. . . . . 6 ⊢ π ∈ ℂ
15	7, 12, 14	mul12i 11406	. . . . 5 ⊢ ((2 / 3) · (i · π)) = (i · ((2 / 3) · π))
16	11, 15	eqtri 2761	. . . 4 ⊢ ((2 / 3) · (log‘-1)) = (i · ((2 / 3) · π))
17	16	fveq2i 6892	. . 3 ⊢ (exp‘((2 / 3) · (log‘-1))) = (exp‘(i · ((2 / 3) · π)))
18		6nn 12298	. . . . . . . . 9 ⊢ 6 ∈ ℕ
19		nndivre 12250	. . . . . . . . 9 ⊢ ((π ∈ ℝ ∧ 6 ∈ ℕ) → (π / 6) ∈ ℝ)
20	13, 18, 19	mp2an 691	. . . . . . . 8 ⊢ (π / 6) ∈ ℝ
21	20	recni 11225	. . . . . . 7 ⊢ (π / 6) ∈ ℂ
22		coshalfpip 25996	. . . . . . 7 ⊢ ((π / 6) ∈ ℂ → (cos‘((π / 2) + (π / 6))) = -(sin‘(π / 6)))
23	21, 22	ax-mp 5	. . . . . 6 ⊢ (cos‘((π / 2) + (π / 6))) = -(sin‘(π / 6))
24		2cn 12284	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
25		2ne0 12313	. . . . . . . . . 10 ⊢ 2 ≠ 0
26		divrec2 11886	. . . . . . . . . 10 ⊢ ((π ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (π / 2) = ((1 / 2) · π))
27	14, 24, 25, 26	mp3an 1462	. . . . . . . . 9 ⊢ (π / 2) = ((1 / 2) · π)
28		6cn 12300	. . . . . . . . . 10 ⊢ 6 ∈ ℂ
29	18	nnne0i 12249	. . . . . . . . . 10 ⊢ 6 ≠ 0
30		divrec2 11886	. . . . . . . . . 10 ⊢ ((π ∈ ℂ ∧ 6 ∈ ℂ ∧ 6 ≠ 0) → (π / 6) = ((1 / 6) · π))
31	14, 28, 29, 30	mp3an 1462	. . . . . . . . 9 ⊢ (π / 6) = ((1 / 6) · π)
32	27, 31	oveq12i 7418	. . . . . . . 8 ⊢ ((π / 2) + (π / 6)) = (((1 / 2) · π) + ((1 / 6) · π))
33	24, 25	reccli 11941	. . . . . . . . 9 ⊢ (1 / 2) ∈ ℂ
34	28, 29	reccli 11941	. . . . . . . . 9 ⊢ (1 / 6) ∈ ℂ
35	33, 34, 14	adddiri 11224	. . . . . . . 8 ⊢ (((1 / 2) + (1 / 6)) · π) = (((1 / 2) · π) + ((1 / 6) · π))
36		halfpm6th 12430	. . . . . . . . . 10 ⊢ (((1 / 2) − (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 / 3))
37	36	simpri 487	. . . . . . . . 9 ⊢ ((1 / 2) + (1 / 6)) = (2 / 3)
38	37	oveq1i 7416	. . . . . . . 8 ⊢ (((1 / 2) + (1 / 6)) · π) = ((2 / 3) · π)
39	32, 35, 38	3eqtr2i 2767	. . . . . . 7 ⊢ ((π / 2) + (π / 6)) = ((2 / 3) · π)
40	39	fveq2i 6892	. . . . . 6 ⊢ (cos‘((π / 2) + (π / 6))) = (cos‘((2 / 3) · π))
41		sincos6thpi 26017	. . . . . . . . 9 ⊢ ((sin‘(π / 6)) = (1 / 2) ∧ (cos‘(π / 6)) = ((√‘3) / 2))
42	41	simpli 485	. . . . . . . 8 ⊢ (sin‘(π / 6)) = (1 / 2)
43	42	negeqi 11450	. . . . . . 7 ⊢ -(sin‘(π / 6)) = -(1 / 2)
44		ax-1cn 11165	. . . . . . . 8 ⊢ 1 ∈ ℂ
45		divneg 11903	. . . . . . . 8 ⊢ ((1 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → -(1 / 2) = (-1 / 2))
46	44, 24, 25, 45	mp3an 1462	. . . . . . 7 ⊢ -(1 / 2) = (-1 / 2)
47	43, 46	eqtri 2761	. . . . . 6 ⊢ -(sin‘(π / 6)) = (-1 / 2)
48	23, 40, 47	3eqtr3i 2769	. . . . 5 ⊢ (cos‘((2 / 3) · π)) = (-1 / 2)
49		sinhalfpip 25994	. . . . . . . . 9 ⊢ ((π / 6) ∈ ℂ → (sin‘((π / 2) + (π / 6))) = (cos‘(π / 6)))
50	21, 49	ax-mp 5	. . . . . . . 8 ⊢ (sin‘((π / 2) + (π / 6))) = (cos‘(π / 6))
51	39	fveq2i 6892	. . . . . . . 8 ⊢ (sin‘((π / 2) + (π / 6))) = (sin‘((2 / 3) · π))
52	41	simpri 487	. . . . . . . 8 ⊢ (cos‘(π / 6)) = ((√‘3) / 2)
53	50, 51, 52	3eqtr3i 2769	. . . . . . 7 ⊢ (sin‘((2 / 3) · π)) = ((√‘3) / 2)
54	53	oveq2i 7417	. . . . . 6 ⊢ (i · (sin‘((2 / 3) · π))) = (i · ((√‘3) / 2))
55		3re 12289	. . . . . . . . 9 ⊢ 3 ∈ ℝ
56		3nn0 12487	. . . . . . . . . 10 ⊢ 3 ∈ ℕ₀
57	56	nn0ge0i 12496	. . . . . . . . 9 ⊢ 0 ≤ 3
58		resqrtcl 15197	. . . . . . . . 9 ⊢ ((3 ∈ ℝ ∧ 0 ≤ 3) → (√‘3) ∈ ℝ)
59	55, 57, 58	mp2an 691	. . . . . . . 8 ⊢ (√‘3) ∈ ℝ
60	59	recni 11225	. . . . . . 7 ⊢ (√‘3) ∈ ℂ
61	12, 60, 24, 25	divassi 11967	. . . . . 6 ⊢ ((i · (√‘3)) / 2) = (i · ((√‘3) / 2))
62	54, 61	eqtr4i 2764	. . . . 5 ⊢ (i · (sin‘((2 / 3) · π))) = ((i · (√‘3)) / 2)
63	48, 62	oveq12i 7418	. . . 4 ⊢ ((cos‘((2 / 3) · π)) + (i · (sin‘((2 / 3) · π)))) = ((-1 / 2) + ((i · (√‘3)) / 2))
64	7, 14	mulcli 11218	. . . . 5 ⊢ ((2 / 3) · π) ∈ ℂ
65		efival 16092	. . . . 5 ⊢ (((2 / 3) · π) ∈ ℂ → (exp‘(i · ((2 / 3) · π))) = ((cos‘((2 / 3) · π)) + (i · (sin‘((2 / 3) · π)))))
66	64, 65	ax-mp 5	. . . 4 ⊢ (exp‘(i · ((2 / 3) · π))) = ((cos‘((2 / 3) · π)) + (i · (sin‘((2 / 3) · π))))
67	12, 60	mulcli 11218	. . . . 5 ⊢ (i · (√‘3)) ∈ ℂ
68	1, 67, 24, 25	divdiri 11968	. . . 4 ⊢ ((-1 + (i · (√‘3))) / 2) = ((-1 / 2) + ((i · (√‘3)) / 2))
69	63, 66, 68	3eqtr4i 2771	. . 3 ⊢ (exp‘(i · ((2 / 3) · π))) = ((-1 + (i · (√‘3))) / 2)
70	9, 17, 69	3eqtri 2765	. 2 ⊢ (-1↑_𝑐(2 / 3)) = ((-1 + (i · (√‘3))) / 2)
71		1z 12589	. . . 4 ⊢ 1 ∈ ℤ
72		root1cj 26254	. . . 4 ⊢ ((3 ∈ ℕ ∧ 1 ∈ ℤ) → (∗‘((-1↑_𝑐(2 / 3))↑1)) = ((-1↑_𝑐(2 / 3))↑(3 − 1)))
73	4, 71, 72	mp2an 691	. . 3 ⊢ (∗‘((-1↑_𝑐(2 / 3))↑1)) = ((-1↑_𝑐(2 / 3))↑(3 − 1))
74		cxpcl 26174	. . . . . . . 8 ⊢ ((-1 ∈ ℂ ∧ (2 / 3) ∈ ℂ) → (-1↑_𝑐(2 / 3)) ∈ ℂ)
75	1, 7, 74	mp2an 691	. . . . . . 7 ⊢ (-1↑_𝑐(2 / 3)) ∈ ℂ
76		exp1 14030	. . . . . . 7 ⊢ ((-1↑_𝑐(2 / 3)) ∈ ℂ → ((-1↑_𝑐(2 / 3))↑1) = (-1↑_𝑐(2 / 3)))
77	75, 76	ax-mp 5	. . . . . 6 ⊢ ((-1↑_𝑐(2 / 3))↑1) = (-1↑_𝑐(2 / 3))
78	77, 70	eqtri 2761	. . . . 5 ⊢ ((-1↑_𝑐(2 / 3))↑1) = ((-1 + (i · (√‘3))) / 2)
79	78	fveq2i 6892	. . . 4 ⊢ (∗‘((-1↑_𝑐(2 / 3))↑1)) = (∗‘((-1 + (i · (√‘3))) / 2))
80	1, 67	addcli 11217	. . . . . 6 ⊢ (-1 + (i · (√‘3))) ∈ ℂ
81	80, 24	cjdivi 15135	. . . . 5 ⊢ (2 ≠ 0 → (∗‘((-1 + (i · (√‘3))) / 2)) = ((∗‘(-1 + (i · (√‘3)))) / (∗‘2)))
82	25, 81	ax-mp 5	. . . 4 ⊢ (∗‘((-1 + (i · (√‘3))) / 2)) = ((∗‘(-1 + (i · (√‘3)))) / (∗‘2))
83	1, 67	cjaddi 15132	. . . . . 6 ⊢ (∗‘(-1 + (i · (√‘3)))) = ((∗‘-1) + (∗‘(i · (√‘3))))
84		neg1rr 12324	. . . . . . . 8 ⊢ -1 ∈ ℝ
85		cjre 15083	. . . . . . . 8 ⊢ (-1 ∈ ℝ → (∗‘-1) = -1)
86	84, 85	ax-mp 5	. . . . . . 7 ⊢ (∗‘-1) = -1
87	12, 60	cjmuli 15133	. . . . . . . 8 ⊢ (∗‘(i · (√‘3))) = ((∗‘i) · (∗‘(√‘3)))
88		cji 15103	. . . . . . . . 9 ⊢ (∗‘i) = -i
89		cjre 15083	. . . . . . . . . 10 ⊢ ((√‘3) ∈ ℝ → (∗‘(√‘3)) = (√‘3))
90	59, 89	ax-mp 5	. . . . . . . . 9 ⊢ (∗‘(√‘3)) = (√‘3)
91	88, 90	oveq12i 7418	. . . . . . . 8 ⊢ ((∗‘i) · (∗‘(√‘3))) = (-i · (√‘3))
92	12, 60	mulneg1i 11657	. . . . . . . 8 ⊢ (-i · (√‘3)) = -(i · (√‘3))
93	87, 91, 92	3eqtri 2765	. . . . . . 7 ⊢ (∗‘(i · (√‘3))) = -(i · (√‘3))
94	86, 93	oveq12i 7418	. . . . . 6 ⊢ ((∗‘-1) + (∗‘(i · (√‘3)))) = (-1 + -(i · (√‘3)))
95	1, 67	negsubi 11535	. . . . . 6 ⊢ (-1 + -(i · (√‘3))) = (-1 − (i · (√‘3)))
96	83, 94, 95	3eqtri 2765	. . . . 5 ⊢ (∗‘(-1 + (i · (√‘3)))) = (-1 − (i · (√‘3)))
97		cjre 15083	. . . . . 6 ⊢ (2 ∈ ℝ → (∗‘2) = 2)
98	3, 97	ax-mp 5	. . . . 5 ⊢ (∗‘2) = 2
99	96, 98	oveq12i 7418	. . . 4 ⊢ ((∗‘(-1 + (i · (√‘3)))) / (∗‘2)) = ((-1 − (i · (√‘3))) / 2)
100	79, 82, 99	3eqtri 2765	. . 3 ⊢ (∗‘((-1↑_𝑐(2 / 3))↑1)) = ((-1 − (i · (√‘3))) / 2)
101		3m1e2 12337	. . . 4 ⊢ (3 − 1) = 2
102	101	oveq2i 7417	. . 3 ⊢ ((-1↑_𝑐(2 / 3))↑(3 − 1)) = ((-1↑_𝑐(2 / 3))↑2)
103	73, 100, 102	3eqtr3ri 2770	. 2 ⊢ ((-1↑_𝑐(2 / 3))↑2) = ((-1 − (i · (√‘3))) / 2)
104	70, 103	pm3.2i 472	1 ⊢ ((-1↑_𝑐(2 / 3)) = ((-1 + (i · (√‘3))) / 2) ∧ ((-1↑_𝑐(2 / 3))↑2) = ((-1 − (i · (√‘3))) / 2))

Colors of variables: wff setvar class

Syntax hints: ∧ wa 397 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 class class class wbr 5148 ‘cfv 6541 (class class class)co 7406 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 ici 11109 + caddc 11110 · cmul 11112 ≤ cle 11246 − cmin 11441 -cneg 11442 / cdiv 11868 ℕcn 12209 2c2 12264 3c3 12265 6c6 12268 ℤcz 12555 ↑cexp 14024 ∗ccj 15040 √csqrt 15177 expce 16002 sincsin 16004 cosccos 16005 πcpi 16007 logclog 26055 ↑_𝑐ccxp 26056

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ioc 13326 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-ef 16008 df-sin 16010 df-cos 16011 df-pi 16013 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-limc 25375 df-dv 25376 df-log 26057 df-cxp 26058

This theorem is referenced by: 1cubr 26337

W3C validator