coskpi - Metamath Proof Explorer

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

Theorem coskpi 26575

Description: The absolute value of the cosine of an integer multiple of π is 1. (Contributed by NM, 19-Aug-2008.)

**Assertion**
Ref	Expression
coskpi	⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1)

**Proof of Theorem coskpi**
Step	Hyp	Ref	Expression
1		zcn 12638	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
2		2cn 12362	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
3		picn 26511	. . . . . . . . . . 11 ⊢ π ∈ ℂ
4		mul12 11449	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℂ ∧ 2 ∈ ℂ ∧ π ∈ ℂ) → (𝐾 · (2 · π)) = (2 · (𝐾 · π)))
5	2, 3, 4	mp3an23 1453	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℂ → (𝐾 · (2 · π)) = (2 · (𝐾 · π)))
6	1, 5	syl 17	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → (𝐾 · (2 · π)) = (2 · (𝐾 · π)))
7	6	fveq2d 6919	. . . . . . . 8 ⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · (2 · π))) = (cos‘(2 · (𝐾 · π))))
8		cos2kpi 26536	. . . . . . . 8 ⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · (2 · π))) = 1)
9		zre 12637	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℝ)
10		pire 26510	. . . . . . . . . . 11 ⊢ π ∈ ℝ
11		remulcl 11263	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ ℝ ∧ π ∈ ℝ) → (𝐾 · π) ∈ ℝ)
12	9, 10, 11	sylancl 585	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → (𝐾 · π) ∈ ℝ)
13	12	recnd 11312	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → (𝐾 · π) ∈ ℂ)
14		cos2t 16220	. . . . . . . . 9 ⊢ ((𝐾 · π) ∈ ℂ → (cos‘(2 · (𝐾 · π))) = ((2 · ((cos‘(𝐾 · π))↑2)) − 1))
15	13, 14	syl 17	. . . . . . . 8 ⊢ (𝐾 ∈ ℤ → (cos‘(2 · (𝐾 · π))) = ((2 · ((cos‘(𝐾 · π))↑2)) − 1))
16	7, 8, 15	3eqtr3rd 2789	. . . . . . 7 ⊢ (𝐾 ∈ ℤ → ((2 · ((cos‘(𝐾 · π))↑2)) − 1) = 1)
17	12	recoscld 16186	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · π)) ∈ ℝ)
18	17	recnd 11312	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → (cos‘(𝐾 · π)) ∈ ℂ)
19	18	sqcld 14188	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → ((cos‘(𝐾 · π))↑2) ∈ ℂ)
20		mulcl 11262	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ ((cos‘(𝐾 · π))↑2) ∈ ℂ) → (2 · ((cos‘(𝐾 · π))↑2)) ∈ ℂ)
21	2, 19, 20	sylancr 586	. . . . . . . 8 ⊢ (𝐾 ∈ ℤ → (2 · ((cos‘(𝐾 · π))↑2)) ∈ ℂ)
22		ax-1cn 11236	. . . . . . . . 9 ⊢ 1 ∈ ℂ
23		subadd 11533	. . . . . . . . 9 ⊢ (((2 · ((cos‘(𝐾 · π))↑2)) ∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · ((cos‘(𝐾 · π))↑2)) − 1) = 1 ↔ (1 + 1) = (2 · ((cos‘(𝐾 · π))↑2))))
24	22, 22, 23	mp3an23 1453	. . . . . . . 8 ⊢ ((2 · ((cos‘(𝐾 · π))↑2)) ∈ ℂ → (((2 · ((cos‘(𝐾 · π))↑2)) − 1) = 1 ↔ (1 + 1) = (2 · ((cos‘(𝐾 · π))↑2))))
25	21, 24	syl 17	. . . . . . 7 ⊢ (𝐾 ∈ ℤ → (((2 · ((cos‘(𝐾 · π))↑2)) − 1) = 1 ↔ (1 + 1) = (2 · ((cos‘(𝐾 · π))↑2))))
26	16, 25	mpbid 232	. . . . . 6 ⊢ (𝐾 ∈ ℤ → (1 + 1) = (2 · ((cos‘(𝐾 · π))↑2)))
27		2t1e2 12450	. . . . . . 7 ⊢ (2 · 1) = 2
28		df-2 12350	. . . . . . 7 ⊢ 2 = (1 + 1)
29	27, 28	eqtr2i 2769	. . . . . 6 ⊢ (1 + 1) = (2 · 1)
30	26, 29	eqtr3di 2795	. . . . 5 ⊢ (𝐾 ∈ ℤ → (2 · ((cos‘(𝐾 · π))↑2)) = (2 · 1))
31		2cnne0 12497	. . . . . . 7 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
32		mulcan 11921	. . . . . . 7 ⊢ ((((cos‘(𝐾 · π))↑2) ∈ ℂ ∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((2 · ((cos‘(𝐾 · π))↑2)) = (2 · 1) ↔ ((cos‘(𝐾 · π))↑2) = 1))
33	22, 31, 32	mp3an23 1453	. . . . . 6 ⊢ (((cos‘(𝐾 · π))↑2) ∈ ℂ → ((2 · ((cos‘(𝐾 · π))↑2)) = (2 · 1) ↔ ((cos‘(𝐾 · π))↑2) = 1))
34	19, 33	syl 17	. . . . 5 ⊢ (𝐾 ∈ ℤ → ((2 · ((cos‘(𝐾 · π))↑2)) = (2 · 1) ↔ ((cos‘(𝐾 · π))↑2) = 1))
35	30, 34	mpbid 232	. . . 4 ⊢ (𝐾 ∈ ℤ → ((cos‘(𝐾 · π))↑2) = 1)
36		sq1 14238	. . . 4 ⊢ (1↑2) = 1
37	35, 36	eqtr4di 2798	. . 3 ⊢ (𝐾 ∈ ℤ → ((cos‘(𝐾 · π))↑2) = (1↑2))
38		1re 11284	. . . 4 ⊢ 1 ∈ ℝ
39		sqabs 15350	. . . 4 ⊢ (((cos‘(𝐾 · π)) ∈ ℝ ∧ 1 ∈ ℝ) → (((cos‘(𝐾 · π))↑2) = (1↑2) ↔ (abs‘(cos‘(𝐾 · π))) = (abs‘1)))
40	17, 38, 39	sylancl 585	. . 3 ⊢ (𝐾 ∈ ℤ → (((cos‘(𝐾 · π))↑2) = (1↑2) ↔ (abs‘(cos‘(𝐾 · π))) = (abs‘1)))
41	37, 40	mpbid 232	. 2 ⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = (abs‘1))
42		abs1 15340	. 2 ⊢ (abs‘1) = 1
43	41, 42	eqtrdi 2796	1 ⊢ (𝐾 ∈ ℤ → (abs‘(cos‘(𝐾 · π))) = 1)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 ‘cfv 6568 (class class class)co 7443 ℂcc 11176 ℝcr 11177 0cc0 11178 1c1 11179 + caddc 11181 · cmul 11183 − cmin 11514 2c2 12342 ℤcz 12633 ↑cexp 14106 abscabs 15277 cosccos 16106 πcpi 16108

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7764 ax-inf2 9704 ax-cnex 11234 ax-resscn 11235 ax-1cn 11236 ax-icn 11237 ax-addcl 11238 ax-addrcl 11239 ax-mulcl 11240 ax-mulrcl 11241 ax-mulcom 11242 ax-addass 11243 ax-mulass 11244 ax-distr 11245 ax-i2m1 11246 ax-1ne0 11247 ax-1rid 11248 ax-rnegex 11249 ax-rrecex 11250 ax-cnre 11251 ax-pre-lttri 11252 ax-pre-lttrn 11253 ax-pre-ltadd 11254 ax-pre-mulgt0 11255 ax-pre-sup 11256 ax-addf 11257

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5650 df-se 5651 df-we 5652 df-xp 5701 df-rel 5702 df-cnv 5703 df-co 5704 df-dm 5705 df-rn 5706 df-res 5707 df-ima 5708 df-pred 6327 df-ord 6393 df-on 6394 df-lim 6395 df-suc 6396 df-iota 6520 df-fun 6570 df-fn 6571 df-f 6572 df-f1 6573 df-fo 6574 df-f1o 6575 df-fv 6576 df-isom 6577 df-riota 7399 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7708 df-om 7898 df-1st 8024 df-2nd 8025 df-supp 8196 df-frecs 8316 df-wrecs 8347 df-recs 8421 df-rdg 8460 df-1o 8516 df-2o 8517 df-er 8757 df-map 8880 df-pm 8881 df-ixp 8950 df-en 8998 df-dom 8999 df-sdom 9000 df-fin 9001 df-fsupp 9426 df-fi 9474 df-sup 9505 df-inf 9506 df-oi 9573 df-card 10002 df-pnf 11320 df-mnf 11321 df-xr 11322 df-ltxr 11323 df-le 11324 df-sub 11516 df-neg 11517 df-div 11942 df-nn 12288 df-2 12350 df-3 12351 df-4 12352 df-5 12353 df-6 12354 df-7 12355 df-8 12356 df-9 12357 df-n0 12548 df-z 12634 df-dec 12753 df-uz 12898 df-q 13008 df-rp 13052 df-xneg 13169 df-xadd 13170 df-xmul 13171 df-ioo 13405 df-ioc 13406 df-ico 13407 df-icc 13408 df-fz 13562 df-fzo 13706 df-fl 13837 df-seq 14047 df-exp 14107 df-fac 14317 df-bc 14346 df-hash 14374 df-shft 15110 df-cj 15142 df-re 15143 df-im 15144 df-sqrt 15278 df-abs 15279 df-limsup 15511 df-clim 15528 df-rlim 15529 df-sum 15729 df-ef 16109 df-sin 16111 df-cos 16112 df-pi 16114 df-struct 17188 df-sets 17205 df-slot 17223 df-ndx 17235 df-base 17253 df-ress 17282 df-plusg 17318 df-mulr 17319 df-starv 17320 df-sca 17321 df-vsca 17322 df-ip 17323 df-tset 17324 df-ple 17325 df-ds 17327 df-unif 17328 df-hom 17329 df-cco 17330 df-rest 17476 df-topn 17477 df-0g 17495 df-gsum 17496 df-topgen 17497 df-pt 17498 df-prds 17501 df-xrs 17556 df-qtop 17561 df-imas 17562 df-xps 17564 df-mre 17638 df-mrc 17639 df-acs 17641 df-mgm 18672 df-sgrp 18751 df-mnd 18767 df-submnd 18813 df-mulg 19102 df-cntz 19351 df-cmn 19818 df-psmet 21373 df-xmet 21374 df-met 21375 df-bl 21376 df-mopn 21377 df-fbas 21378 df-fg 21379 df-cnfld 21382 df-top 22913 df-topon 22930 df-topsp 22952 df-bases 22966 df-cld 23040 df-ntr 23041 df-cls 23042 df-nei 23119 df-lp 23157 df-perf 23158 df-cn 23248 df-cnp 23249 df-haus 23336 df-tx 23583 df-hmeo 23776 df-fil 23867 df-fm 23959 df-flim 23960 df-flf 23961 df-xms 24343 df-ms 24344 df-tms 24345 df-cncf 24915 df-limc 25913 df-dv 25914

This theorem is referenced by: (None)

W3C validator