goldratmolem2 - Mathbox for Ender Ting

	Mathbox for Ender Ting		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > goldratmolem2		Structured version Visualization version GIF version

Theorem goldratmolem2 47933

Description: Lemma 2 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026.)

**Hypothesis**
Ref	Expression
goldra.val	⊢ 𝐹 = (2 · (cos‘(π / 5)))

**Assertion**
Ref	Expression
goldratmolem2	⊢ -1 = ((((𝐹↑5) / 2) − (5 · ((𝐹↑3) / 2))) + (5 · (𝐹 / 2)))

**Proof of Theorem goldratmolem2**
Step	Hyp	Ref	Expression
1		goldra.val	. . 3 ⊢ 𝐹 = (2 · (cos‘(π / 5)))
2	1	goldracos5teq 47932	. 2 ⊢ (cos‘π) = (((;16 · ((𝐹 / 2)↑5)) − (;20 · ((𝐹 / 2)↑3))) + (5 · (𝐹 / 2)))
3		cospi 26801	. 2 ⊢ (cos‘π) = -1
4	1	goldrarr 47928	. . . . . . . 8 ⊢ 𝐹 ∈ ℝ
5	4	recni 11323	. . . . . . 7 ⊢ 𝐹 ∈ ℂ
6		2cnne0 12555	. . . . . . 7 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
7		5nn0 12626	. . . . . . 7 ⊢ 5 ∈ ℕ₀
8		expdiv 14256	. . . . . . 7 ⊢ ((𝐹 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ 5 ∈ ℕ₀) → ((𝐹 / 2)↑5) = ((𝐹↑5) / (2↑5)))
9	5, 6, 7, 8	mp3an 1490	. . . . . 6 ⊢ ((𝐹 / 2)↑5) = ((𝐹↑5) / (2↑5))
10	9	oveq2i 7431	. . . . 5 ⊢ (;16 · ((𝐹 / 2)↑5)) = (;16 · ((𝐹↑5) / (2↑5)))
11		expcl 14222	. . . . . . . 8 ⊢ ((𝐹 ∈ ℂ ∧ 5 ∈ ℕ₀) → (𝐹↑5) ∈ ℂ)
12	5, 7, 11	mp2an 705	. . . . . . 7 ⊢ (𝐹↑5) ∈ ℂ
13		2cn 12418	. . . . . . . . 9 ⊢ 2 ∈ ℂ
14		expcl 14222	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ 5 ∈ ℕ₀) → (2↑5) ∈ ℂ)
15	13, 7, 14	mp2an 705	. . . . . . . 8 ⊢ (2↑5) ∈ ℂ
16		2ne0 12449	. . . . . . . . 9 ⊢ 2 ≠ 0
17		5nn 12429	. . . . . . . . . 10 ⊢ 5 ∈ ℕ
18	17	nnzi 12720	. . . . . . . . 9 ⊢ 5 ∈ ℤ
19		expne0i 14237	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 5 ∈ ℤ) → (2↑5) ≠ 0)
20	13, 16, 18, 19	mp3an 1490	. . . . . . . 8 ⊢ (2↑5) ≠ 0
21	15, 20	pm3.2i 476	. . . . . . 7 ⊢ ((2↑5) ∈ ℂ ∧ (2↑5) ≠ 0)
22		16nn0 12832	. . . . . . . . 9 ⊢ ;16 ∈ ℕ₀
23	22	nn0cni 12618	. . . . . . . 8 ⊢ ;16 ∈ ℂ
24		1nn0 12622	. . . . . . . . . 10 ⊢ 1 ∈ ℕ₀
25		6nn 12432	. . . . . . . . . 10 ⊢ 6 ∈ ℕ
26	24, 25	decnncl 12838	. . . . . . . . 9 ⊢ ;16 ∈ ℕ
27	26	nnne0i 12378	. . . . . . . 8 ⊢ ;16 ≠ 0
28	23, 27	pm3.2i 476	. . . . . . 7 ⊢ (;16 ∈ ℂ ∧ ;16 ≠ 0)
29		divdiv2 12029	. . . . . . 7 ⊢ (((𝐹↑5) ∈ ℂ ∧ ((2↑5) ∈ ℂ ∧ (2↑5) ≠ 0) ∧ (;16 ∈ ℂ ∧ ;16 ≠ 0)) → ((𝐹↑5) / ((2↑5) / ;16)) = (((𝐹↑5) · ;16) / (2↑5)))
30	12, 21, 28, 29	mp3an 1490	. . . . . 6 ⊢ ((𝐹↑5) / ((2↑5) / ;16)) = (((𝐹↑5) · ;16) / (2↑5))
31	12, 23	mulcomi 11317	. . . . . . 7 ⊢ ((𝐹↑5) · ;16) = (;16 · (𝐹↑5))
32	31	oveq1i 7430	. . . . . 6 ⊢ (((𝐹↑5) · ;16) / (2↑5)) = ((;16 · (𝐹↑5)) / (2↑5))
33	23, 12, 15, 20	divassi 12073	. . . . . 6 ⊢ ((;16 · (𝐹↑5)) / (2↑5)) = (;16 · ((𝐹↑5) / (2↑5)))
34	30, 32, 33	3eqtrri 2788	. . . . 5 ⊢ (;16 · ((𝐹↑5) / (2↑5))) = ((𝐹↑5) / ((2↑5) / ;16))
35		exp1 14210	. . . . . . . . . . 11 ⊢ (2 ∈ ℂ → (2↑1) = 2)
36	13, 35	ax-mp 5	. . . . . . . . . 10 ⊢ (2↑1) = 2
37	36	eqcomi 2769	. . . . . . . . 9 ⊢ 2 = (2↑1)
38		4cn 12428	. . . . . . . . . . 11 ⊢ 4 ∈ ℂ
39		ax-1cn 11258	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
40		4p1e5 12488	. . . . . . . . . . 11 ⊢ (4 + 1) = 5
41	38, 39, 40	mvlladdi 11576	. . . . . . . . . 10 ⊢ 1 = (5 − 4)
42	41	oveq2i 7431	. . . . . . . . 9 ⊢ (2↑1) = (2↑(5 − 4))
43	37, 42	eqtri 2783	. . . . . . . 8 ⊢ 2 = (2↑(5 − 4))
44		4z 12730	. . . . . . . . . 10 ⊢ 4 ∈ ℤ
45	18, 44	pm3.2i 476	. . . . . . . . 9 ⊢ (5 ∈ ℤ ∧ 4 ∈ ℤ)
46		expsub 14253	. . . . . . . . 9 ⊢ (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (5 ∈ ℤ ∧ 4 ∈ ℤ)) → (2↑(5 − 4)) = ((2↑5) / (2↑4)))
47	6, 45, 46	mp2an 705	. . . . . . . 8 ⊢ (2↑(5 − 4)) = ((2↑5) / (2↑4))
48		2exp4 17262	. . . . . . . . 9 ⊢ (2↑4) = ;16
49	48	oveq2i 7431	. . . . . . . 8 ⊢ ((2↑5) / (2↑4)) = ((2↑5) / ;16)
50	43, 47, 49	3eqtri 2787	. . . . . . 7 ⊢ 2 = ((2↑5) / ;16)
51	50	eqcomi 2769	. . . . . 6 ⊢ ((2↑5) / ;16) = 2
52	51	oveq2i 7431	. . . . 5 ⊢ ((𝐹↑5) / ((2↑5) / ;16)) = ((𝐹↑5) / 2)
53	10, 34, 52	3eqtri 2787	. . . 4 ⊢ (;16 · ((𝐹 / 2)↑5)) = ((𝐹↑5) / 2)
54		3nn0 12624	. . . . . . 7 ⊢ 3 ∈ ℕ₀
55		expdiv 14256	. . . . . . 7 ⊢ ((𝐹 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ 3 ∈ ℕ₀) → ((𝐹 / 2)↑3) = ((𝐹↑3) / (2↑3)))
56	5, 6, 54, 55	mp3an 1490	. . . . . 6 ⊢ ((𝐹 / 2)↑3) = ((𝐹↑3) / (2↑3))
57	56	oveq2i 7431	. . . . 5 ⊢ (;20 · ((𝐹 / 2)↑3)) = (;20 · ((𝐹↑3) / (2↑3)))
58		5t4e20 12921	. . . . . . . 8 ⊢ (5 · 4) = ;20
59	58	eqcomi 2769	. . . . . . 7 ⊢ ;20 = (5 · 4)
60	59	oveq1i 7430	. . . . . 6 ⊢ (;20 · ((𝐹↑3) / (2↑3))) = ((5 · 4) · ((𝐹↑3) / (2↑3)))
61		5cn 12431	. . . . . . 7 ⊢ 5 ∈ ℂ
62		expcl 14222	. . . . . . . . 9 ⊢ ((𝐹 ∈ ℂ ∧ 3 ∈ ℕ₀) → (𝐹↑3) ∈ ℂ)
63	5, 54, 62	mp2an 705	. . . . . . . 8 ⊢ (𝐹↑3) ∈ ℂ
64		expcl 14222	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ 3 ∈ ℕ₀) → (2↑3) ∈ ℂ)
65	13, 54, 64	mp2an 705	. . . . . . . 8 ⊢ (2↑3) ∈ ℂ
66		3z 12729	. . . . . . . . 9 ⊢ 3 ∈ ℤ
67		expne0i 14237	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 3 ∈ ℤ) → (2↑3) ≠ 0)
68	13, 16, 66, 67	mp3an 1490	. . . . . . . 8 ⊢ (2↑3) ≠ 0
69	63, 65, 68	divcli 12059	. . . . . . 7 ⊢ ((𝐹↑3) / (2↑3)) ∈ ℂ
70	61, 38, 69	mulassi 11320	. . . . . 6 ⊢ ((5 · 4) · ((𝐹↑3) / (2↑3))) = (5 · (4 · ((𝐹↑3) / (2↑3))))
71	60, 70	eqtri 2783	. . . . 5 ⊢ (;20 · ((𝐹↑3) / (2↑3))) = (5 · (4 · ((𝐹↑3) / (2↑3))))
72	65, 68	pm3.2i 476	. . . . . . . . 9 ⊢ ((2↑3) ∈ ℂ ∧ (2↑3) ≠ 0)
73		4ne0 12454	. . . . . . . . . 10 ⊢ 4 ≠ 0
74	38, 73	pm3.2i 476	. . . . . . . . 9 ⊢ (4 ∈ ℂ ∧ 4 ≠ 0)
75		divdiv2 12029	. . . . . . . . 9 ⊢ (((𝐹↑3) ∈ ℂ ∧ ((2↑3) ∈ ℂ ∧ (2↑3) ≠ 0) ∧ (4 ∈ ℂ ∧ 4 ≠ 0)) → ((𝐹↑3) / ((2↑3) / 4)) = (((𝐹↑3) · 4) / (2↑3)))
76	63, 72, 74, 75	mp3an 1490	. . . . . . . 8 ⊢ ((𝐹↑3) / ((2↑3) / 4)) = (((𝐹↑3) · 4) / (2↑3))
77	63, 38	mulcomi 11317	. . . . . . . . 9 ⊢ ((𝐹↑3) · 4) = (4 · (𝐹↑3))
78	77	oveq1i 7430	. . . . . . . 8 ⊢ (((𝐹↑3) · 4) / (2↑3)) = ((4 · (𝐹↑3)) / (2↑3))
79	38, 63, 65, 68	divassi 12073	. . . . . . . 8 ⊢ ((4 · (𝐹↑3)) / (2↑3)) = (4 · ((𝐹↑3) / (2↑3)))
80	76, 78, 79	3eqtrri 2788	. . . . . . 7 ⊢ (4 · ((𝐹↑3) / (2↑3))) = ((𝐹↑3) / ((2↑3) / 4))
81		4t2e8 12511	. . . . . . . . . 10 ⊢ (4 · 2) = 8
82		cu2 14343	. . . . . . . . . . 11 ⊢ (2↑3) = 8
83	82	eqcomi 2769	. . . . . . . . . 10 ⊢ 8 = (2↑3)
84	81, 83	eqtri 2783	. . . . . . . . 9 ⊢ (4 · 2) = (2↑3)
85	65, 38, 13, 73	divmuli 12071	. . . . . . . . 9 ⊢ (((2↑3) / 4) = 2 ↔ (4 · 2) = (2↑3))
86	84, 85	mpbir 234	. . . . . . . 8 ⊢ ((2↑3) / 4) = 2
87	86	oveq2i 7431	. . . . . . 7 ⊢ ((𝐹↑3) / ((2↑3) / 4)) = ((𝐹↑3) / 2)
88	80, 87	eqtri 2783	. . . . . 6 ⊢ (4 · ((𝐹↑3) / (2↑3))) = ((𝐹↑3) / 2)
89	88	oveq2i 7431	. . . . 5 ⊢ (5 · (4 · ((𝐹↑3) / (2↑3)))) = (5 · ((𝐹↑3) / 2))
90	57, 71, 89	3eqtri 2787	. . . 4 ⊢ (;20 · ((𝐹 / 2)↑3)) = (5 · ((𝐹↑3) / 2))
91	53, 90	oveq12i 7432	. . 3 ⊢ ((;16 · ((𝐹 / 2)↑5)) − (;20 · ((𝐹 / 2)↑3))) = (((𝐹↑5) / 2) − (5 · ((𝐹↑3) / 2)))
92	91	oveq1i 7430	. 2 ⊢ (((;16 · ((𝐹 / 2)↑5)) − (;20 · ((𝐹 / 2)↑3))) + (5 · (𝐹 / 2))) = ((((𝐹↑5) / 2) − (5 · ((𝐹↑3) / 2))) + (5 · (𝐹 / 2)))
93	2, 3, 92	3eqtr3i 2791	1 ⊢ -1 = ((((𝐹↑5) / 2) − (5 · ((𝐹↑3) / 2))) + (5 · (𝐹 / 2)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 − cmin 11541 -cneg 11542 / cdiv 11973 2c2 12397 3c3 12398 4c4 12399 5c5 12400 6c6 12401 8c8 12403 ℕ₀cn0 12606 ℤcz 12693 cdc 12814 ↑cexp 14204 cosccos 16230 πcpi 16232

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-ioo 13480 df-ioc 13481 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-fl 13932 df-seq 14145 df-exp 14205 df-fac 14418 df-bc 14447 df-hash 14475 df-shft 15220 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-limsup 15638 df-clim 15655 df-rlim 15656 df-sum 15854 df-ef 16233 df-sin 16235 df-cos 16236 df-pi 16238 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-rest 17593 df-topn 17594 df-0g 17612 df-gsum 17613 df-topgen 17614 df-pt 17615 df-prds 17618 df-xrs 17674 df-qtop 17679 df-imas 17680 df-xps 17682 df-mre 17756 df-mrc 17757 df-acs 17759 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-submnd 18979 df-mulg 19278 df-cntz 19531 df-cmn 19996 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-fbas 21675 df-fg 21676 df-cnfld 21679 df-top 23212 df-topon 23229 df-topsp 23251 df-bases 23264 df-cld 23337 df-ntr 23338 df-cls 23339 df-nei 23416 df-lp 23454 df-perf 23455 df-cn 23545 df-cnp 23546 df-haus 23633 df-tx 23881 df-hmeo 24074 df-fil 24165 df-fm 24257 df-flim 24258 df-flf 24259 df-xms 24639 df-ms 24640 df-tms 24641 df-cncf 25199 df-limc 26186 df-dv 26187

This theorem is used by: goldratmolem3 47934

W3C validator