Theorem cos01gt0 15605

Description: The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.)

Assertion

Ref	Expression
cos01gt0	⊢ (𝐴 ∈ (0(,]1) → 0 < (cos‘𝐴))

Proof of Theorem cos01gt0

Step	Hyp	Ref	Expression
1		0xr 10739	. . . . . . . . . 10 ⊢ 0 ∈ ℝ*
2		1re 10692	. . . . . . . . . 10 ⊢ 1 ∈ ℝ
3		elioc2 12855	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 1 ∈ ℝ) → (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1)))
4	1, 2, 3	mp2an 691	. . . . . . . . 9 ⊢ (𝐴 ∈ (0(,]1) ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1))
5	4	simp1bi 1142	. . . . . . . 8 ⊢ (𝐴 ∈ (0(,]1) → 𝐴 ∈ ℝ)
6	5	resqcld 13674	. . . . . . 7 ⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈ ℝ)
7	6	recnd 10720	. . . . . 6 ⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ∈ ℂ)
8		2cn 11762	. . . . . . 7 ⊢ 2 ∈ ℂ
9		3cn 11768	. . . . . . . 8 ⊢ 3 ∈ ℂ
10		3ne0 11793	. . . . . . . 8 ⊢ 3 ≠ 0
11	9, 10	pm3.2i 474	. . . . . . 7 ⊢ (3 ∈ ℂ ∧ 3 ≠ 0)
12		div12 11371	. . . . . . 7 ⊢ ((2 ∈ ℂ ∧ (𝐴↑2) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 ≠ 0)) → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3)))
13	8, 11, 12	mp3an13 1449	. . . . . 6 ⊢ ((𝐴↑2) ∈ ℂ → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3)))
14	7, 13	syl 17	. . . . 5 ⊢ (𝐴 ∈ (0(,]1) → (2 · ((𝐴↑2) / 3)) = ((𝐴↑2) · (2 / 3)))
15		2z 12066	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
16		expgt0 13525	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 2 ∈ ℤ ∧ 0 < 𝐴) → 0 < (𝐴↑2))
17	15, 16	mp3an2 1446	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 0 < (𝐴↑2))
18	17	3adant3 1129	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1) → 0 < (𝐴↑2))
19	4, 18	sylbi 220	. . . . . . 7 ⊢ (𝐴 ∈ (0(,]1) → 0 < (𝐴↑2))
20		2lt3 11859	. . . . . . . . . 10 ⊢ 2 < 3
21		2re 11761	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
22		3re 11767	. . . . . . . . . . 11 ⊢ 3 ∈ ℝ
23		3pos 11792	. . . . . . . . . . 11 ⊢ 0 < 3
24	21, 22, 22, 23	ltdiv1ii 11620	. . . . . . . . . 10 ⊢ (2 < 3 ↔ (2 / 3) < (3 / 3))
25	20, 24	mpbi 233	. . . . . . . . 9 ⊢ (2 / 3) < (3 / 3)
26	9, 10	dividi 11424	. . . . . . . . 9 ⊢ (3 / 3) = 1
27	25, 26	breqtri 5061	. . . . . . . 8 ⊢ (2 / 3) < 1
28	21, 22, 10	redivcli 11458	. . . . . . . . 9 ⊢ (2 / 3) ∈ ℝ
29		ltmul2 11542	. . . . . . . . 9 ⊢ (((2 / 3) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐴↑2) ∈ ℝ ∧ 0 < (𝐴↑2))) → ((2 / 3) < 1 ↔ ((𝐴↑2) · (2 / 3)) < ((𝐴↑2) · 1)))
30	28, 2, 29	mp3an12 1448	. . . . . . . 8 ⊢ (((𝐴↑2) ∈ ℝ ∧ 0 < (𝐴↑2)) → ((2 / 3) < 1 ↔ ((𝐴↑2) · (2 / 3)) < ((𝐴↑2) · 1)))
31	27, 30	mpbii 236	. . . . . . 7 ⊢ (((𝐴↑2) ∈ ℝ ∧ 0 < (𝐴↑2)) → ((𝐴↑2) · (2 / 3)) < ((𝐴↑2) · 1))
32	6, 19, 31	syl2anc 587	. . . . . 6 ⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (2 / 3)) < ((𝐴↑2) · 1))
33	7	mulid1d 10709	. . . . . 6 ⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · 1) = (𝐴↑2))
34	32, 33	breqtrd 5062	. . . . 5 ⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) · (2 / 3)) < (𝐴↑2))
35	14, 34	eqbrtrd 5058	. . . 4 ⊢ (𝐴 ∈ (0(,]1) → (2 · ((𝐴↑2) / 3)) < (𝐴↑2))
36		0re 10694	. . . . . . . . 9 ⊢ 0 ∈ ℝ
37		ltle 10780	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (0 < 𝐴 → 0 ≤ 𝐴))
38	36, 37	mpan 689	. . . . . . . 8 ⊢ (𝐴 ∈ ℝ → (0 < 𝐴 → 0 ≤ 𝐴))
39	38	imdistani 572	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))
40		le2sq2 13563	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (1 ∈ ℝ ∧ 𝐴 ≤ 1)) → (𝐴↑2) ≤ (1↑2))
41	2, 40	mpanr1 702	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ 1) → (𝐴↑2) ≤ (1↑2))
42	39, 41	stoic3 1778	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 ≤ 1) → (𝐴↑2) ≤ (1↑2))
43	4, 42	sylbi 220	. . . . 5 ⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ≤ (1↑2))
44		sq1 13621	. . . . 5 ⊢ (1↑2) = 1
45	43, 44	breqtrdi 5077	. . . 4 ⊢ (𝐴 ∈ (0(,]1) → (𝐴↑2) ≤ 1)
46		redivcl 11410	. . . . . . . 8 ⊢ (((𝐴↑2) ∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → ((𝐴↑2) / 3) ∈ ℝ)
47	22, 10, 46	mp3an23 1450	. . . . . . 7 ⊢ ((𝐴↑2) ∈ ℝ → ((𝐴↑2) / 3) ∈ ℝ)
48	6, 47	syl 17	. . . . . 6 ⊢ (𝐴 ∈ (0(,]1) → ((𝐴↑2) / 3) ∈ ℝ)
49		remulcl 10673	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ ((𝐴↑2) / 3) ∈ ℝ) → (2 · ((𝐴↑2) / 3)) ∈ ℝ)
50	21, 48, 49	sylancr 590	. . . . 5 ⊢ (𝐴 ∈ (0(,]1) → (2 · ((𝐴↑2) / 3)) ∈ ℝ)
51		ltletr 10783	. . . . . 6 ⊢ (((2 · ((𝐴↑2) / 3)) ∈ ℝ ∧ (𝐴↑2) ∈ ℝ ∧ 1 ∈ ℝ) → (((2 · ((𝐴↑2) / 3)) < (𝐴↑2) ∧ (𝐴↑2) ≤ 1) → (2 · ((𝐴↑2) / 3)) < 1))
52	2, 51	mp3an3 1447	. . . . 5 ⊢ (((2 · ((𝐴↑2) / 3)) ∈ ℝ ∧ (𝐴↑2) ∈ ℝ) → (((2 · ((𝐴↑2) / 3)) < (𝐴↑2) ∧ (𝐴↑2) ≤ 1) → (2 · ((𝐴↑2) / 3)) < 1))
53	50, 6, 52	syl2anc 587	. . . 4 ⊢ (𝐴 ∈ (0(,]1) → (((2 · ((𝐴↑2) / 3)) < (𝐴↑2) ∧ (𝐴↑2) ≤ 1) → (2 · ((𝐴↑2) / 3)) < 1))
54	35, 45, 53	mp2and 698	. . 3 ⊢ (𝐴 ∈ (0(,]1) → (2 · ((𝐴↑2) / 3)) < 1)
55		posdif 11184	. . . 4 ⊢ (((2 · ((𝐴↑2) / 3)) ∈ ℝ ∧ 1 ∈ ℝ) → ((2 · ((𝐴↑2) / 3)) < 1 ↔ 0 < (1 − (2 · ((𝐴↑2) / 3)))))
56	50, 2, 55	sylancl 589	. . 3 ⊢ (𝐴 ∈ (0(,]1) → ((2 · ((𝐴↑2) / 3)) < 1 ↔ 0 < (1 − (2 · ((𝐴↑2) / 3)))))
57	54, 56	mpbid 235	. 2 ⊢ (𝐴 ∈ (0(,]1) → 0 < (1 − (2 · ((𝐴↑2) / 3))))
58		cos01bnd 15600	. . 3 ⊢ (𝐴 ∈ (0(,]1) → ((1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴) ∧ (cos‘𝐴) < (1 − ((𝐴↑2) / 3))))
59	58	simpld 498	. 2 ⊢ (𝐴 ∈ (0(,]1) → (1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴))
60		resubcl 11001	. . . 4 ⊢ ((1 ∈ ℝ ∧ (2 · ((𝐴↑2) / 3)) ∈ ℝ) → (1 − (2 · ((𝐴↑2) / 3))) ∈ ℝ)
61	2, 50, 60	sylancr 590	. . 3 ⊢ (𝐴 ∈ (0(,]1) → (1 − (2 · ((𝐴↑2) / 3))) ∈ ℝ)
62	5	recoscld 15558	. . 3 ⊢ (𝐴 ∈ (0(,]1) → (cos‘𝐴) ∈ ℝ)
63		lttr 10768	. . 3 ⊢ ((0 ∈ ℝ ∧ (1 − (2 · ((𝐴↑2) / 3))) ∈ ℝ ∧ (cos‘𝐴) ∈ ℝ) → ((0 < (1 − (2 · ((𝐴↑2) / 3))) ∧ (1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴)) → 0 < (cos‘𝐴)))
64	36, 61, 62, 63	mp3an2i 1463	. 2 ⊢ (𝐴 ∈ (0(,]1) → ((0 < (1 − (2 · ((𝐴↑2) / 3))) ∧ (1 − (2 · ((𝐴↑2) / 3))) < (cos‘𝐴)) → 0 < (cos‘𝐴)))
65	57, 59, 64	mp2and 698	1 ⊢ (𝐴 ∈ (0(,]1) → 0 < (cos‘𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951   class class class wbr 5036  ‘cfv 6340  (class class class)co 7156  ℂcc 10586  ℝcr 10587  0cc0 10588  1c1 10589   · cmul 10593  ℝ^*cxr 10725   < clt 10726   ≤ cle 10727   − cmin 10921   / cdiv 11348  2c2 11742  3c3 11743  ℤcz 12033  (,]cioc 12793  ↑cexp 13492  cosccos 15479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-inf2 9150  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665  ax-pre-sup 10666  ax-addf 10667  ax-mulf 10668

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6131  df-ord 6177  df-on 6178  df-lim 6179  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-isom 6349  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7586  df-1st 7699  df-2nd 7700  df-wrecs 7963  df-recs 8024  df-rdg 8062  df-1o 8118  df-er 8305  df-pm 8425  df-en 8541  df-dom 8542  df-sdom 8543  df-fin 8544  df-sup 8952  df-inf 8953  df-oi 9020  df-card 9414  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-div 11349  df-nn 11688  df-2 11750  df-3 11751  df-4 11752  df-5 11753  df-6 11754  df-7 11755  df-8 11756  df-n0 11948  df-z 12034  df-uz 12296  df-rp 12444  df-ioc 12797  df-ico 12798  df-fz 12953  df-fzo 13096  df-fl 13224  df-seq 13432  df-exp 13493  df-fac 13697  df-hash 13754  df-shft 14487  df-cj 14519  df-re 14520  df-im 14521  df-sqrt 14655  df-abs 14656  df-limsup 14889  df-clim 14906  df-rlim 14907  df-sum 15104  df-ef 15482  df-cos 15485

This theorem is referenced by:  sin02gt0  15606  sincos1sgn  15607  tangtx  25210