cosq14gt0 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cosq14gt0		GIF version

Theorem cosq14gt0 16059

Description: The cosine of a number strictly between -π / 2 and π / 2 is positive. (Contributed by Mario Carneiro, 25-Feb-2015.)

**Assertion**
Ref	Expression
cosq14gt0	⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → 0 < (cos‘𝐴))

**Proof of Theorem cosq14gt0**
Step	Hyp	Ref	Expression
1		halfpire 16019	. . . . 5 ⊢ (π / 2) ∈ ℝ
2		elioore 10331	. . . . 5 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → 𝐴 ∈ ℝ)
3		resubcl 8597	. . . . 5 ⊢ (((π / 2) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((π / 2) − 𝐴) ∈ ℝ)
4	1, 2, 3	sylancr 418	. . . 4 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → ((π / 2) − 𝐴) ∈ ℝ)
5		neghalfpirx 16021	. . . . . . 7 ⊢ -(π / 2) ∈ ℝ^*
6	1	rexri 8389	. . . . . . 7 ⊢ (π / 2) ∈ ℝ^*
7		elioo2 10340	. . . . . . 7 ⊢ (( -(π / 2) ∈ ℝ^* ∧ (π / 2) ∈ ℝ^*) → (𝐴 ∈ ( -(π / 2)(,)(π / 2)) ↔ (𝐴 ∈ ℝ ∧ -(π / 2) < 𝐴 ∧ 𝐴 < (π / 2))))
8	5, 6, 7	mp2an 430	. . . . . 6 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) ↔ (𝐴 ∈ ℝ ∧ -(π / 2) < 𝐴 ∧ 𝐴 < (π / 2)))
9	8	simp3bi 1045	. . . . 5 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → 𝐴 < (π / 2))
10		posdif 8790	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ (π / 2) ∈ ℝ) → (𝐴 < (π / 2) ↔ 0 < ((π / 2) − 𝐴)))
11	2, 1, 10	sylancl 417	. . . . 5 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → (𝐴 < (π / 2) ↔ 0 < ((π / 2) − 𝐴)))
12	9, 11	mpbid 147	. . . 4 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → 0 < ((π / 2) − 𝐴))
13		picn 16014	. . . . . . . 8 ⊢ π ∈ ℂ
14		halfcl 9542	. . . . . . . 8 ⊢ (π ∈ ℂ → (π / 2) ∈ ℂ)
15	13, 14	ax-mp 5	. . . . . . 7 ⊢ (π / 2) ∈ ℂ
16	15	negcli 8601	. . . . . . 7 ⊢ -(π / 2) ∈ ℂ
17	13, 15	negsubi 8611	. . . . . . . 8 ⊢ (π + -(π / 2)) = (π − (π / 2))
18		pidiv2halves 16022	. . . . . . . . 9 ⊢ ((π / 2) + (π / 2)) = π
19	13, 15, 15, 18	subaddrii 8622	. . . . . . . 8 ⊢ (π − (π / 2)) = (π / 2)
20	17, 19	eqtri 2259	. . . . . . 7 ⊢ (π + -(π / 2)) = (π / 2)
21	15, 13, 16, 20	subaddrii 8622	. . . . . 6 ⊢ ((π / 2) − π) = -(π / 2)
22	8	simp2bi 1044	. . . . . 6 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → -(π / 2) < 𝐴)
23	21, 22	eqbrtrid 4166	. . . . 5 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → ((π / 2) − π) < 𝐴)
24		pire 16013	. . . . . . 7 ⊢ π ∈ ℝ
25		ltsub23 8777	. . . . . . 7 ⊢ (((π / 2) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ π ∈ ℝ) → (((π / 2) − 𝐴) < π ↔ ((π / 2) − π) < 𝐴))
26	1, 24, 25	mp3an13 1369	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (((π / 2) − 𝐴) < π ↔ ((π / 2) − π) < 𝐴))
27	2, 26	syl 14	. . . . 5 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → (((π / 2) − 𝐴) < π ↔ ((π / 2) − π) < 𝐴))
28	23, 27	mpbird 167	. . . 4 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → ((π / 2) − 𝐴) < π)
29		0xr 8378	. . . . 5 ⊢ 0 ∈ ℝ^*
30	24	rexri 8389	. . . . 5 ⊢ π ∈ ℝ^*
31		elioo2 10340	. . . . 5 ⊢ ((0 ∈ ℝ^* ∧ π ∈ ℝ^*) → (((π / 2) − 𝐴) ∈ (0(,)π) ↔ (((π / 2) − 𝐴) ∈ ℝ ∧ 0 < ((π / 2) − 𝐴) ∧ ((π / 2) − 𝐴) < π)))
32	29, 30, 31	mp2an 430	. . . 4 ⊢ (((π / 2) − 𝐴) ∈ (0(,)π) ↔ (((π / 2) − 𝐴) ∈ ℝ ∧ 0 < ((π / 2) − 𝐴) ∧ ((π / 2) − 𝐴) < π))
33	4, 12, 28, 32	syl3anbrc 1212	. . 3 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → ((π / 2) − 𝐴) ∈ (0(,)π))
34		sinq12gt0 16057	. . 3 ⊢ (((π / 2) − 𝐴) ∈ (0(,)π) → 0 < (sin‘((π / 2) − 𝐴)))
35	33, 34	syl 14	. 2 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → 0 < (sin‘((π / 2) − 𝐴)))
36	2	recnd 8360	. . 3 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → 𝐴 ∈ ℂ)
37		sinhalfpim 16048	. . 3 ⊢ (𝐴 ∈ ℂ → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
38	36, 37	syl 14	. 2 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → (sin‘((π / 2) − 𝐴)) = (cos‘𝐴))
39	35, 38	breqtrd 4157	1 ⊢ (𝐴 ∈ ( -(π / 2)(,)(π / 2)) → 0 < (cos‘𝐴))

Colors of variables: wff set class

This proof depends on syntax axioms: → wi 4 ↔ wb 105 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 class class class wbr 4131 ‘cfv 5380 (class class class)co 6088 ℂcc 8183 ℝcr 8184 0cc0 8185 + caddc 8188 ℝ^*cxr 8365 < clt 8366 − cmin 8504 -cneg 8505 / cdiv 9010 2c2 9364 (,)cioo 10307 sincsin 12436 cosccos 12437 πcpi 12439

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305 ax-pre-suploc 8306 ax-addf 8307 ax-mulf 8308

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-of 6305 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-oadd 6695 df-er 6811 df-map 6928 df-pm 6929 df-en 7027 df-dom 7028 df-fin 7029 df-sup 7330 df-inf 7331 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-5 9375 df-6 9376 df-7 9377 df-8 9378 df-9 9379 df-n0 9575 df-z 9656 df-uz 9938 df-q 10036 df-rp 10072 df-xneg 10191 df-xadd 10192 df-ioo 10311 df-ioc 10312 df-ico 10313 df-icc 10314 df-fz 10429 df-fzo 10567 df-seqfrec 10906 df-exp 10997 df-fac 11186 df-bc 11208 df-ihash 11237 df-shft 11602 df-cj 11629 df-re 11630 df-im 11631 df-rsqrt 11786 df-abs 11787 df-clim 12070 df-sumdc 12145 df-ef 12440 df-sin 12442 df-cos 12443 df-pi 12445 df-rest 13654 df-topgen 13673 df-psmet 14989 df-xmet 14990 df-met 14991 df-bl 14992 df-mopn 14993 df-top 15224 df-topon 15237 df-bases 15269 df-ntr 15322 df-cn 15414 df-cnp 15415 df-tx 15479 df-cncf 15797 df-limced 15882 df-dvap 15883

This theorem is used by: coseq0q4123 16061

W3C validator