Theorem cos01gt0 7427

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	|- (A e. (0(,]1) -> 0 < (cos` A))

Proof of Theorem cos01gt0

Step	Hyp	Ref	Expression
1		0re 5420	. . . . . . . . . . 11 |- 0 e. RR
2		1re 5415	. . . . . . . . . . 11 |- 1 e. RR
3		elioc2t 6330	. . . . . . . . . . 11 |- ((0 e. RR /\ 1 e. RR) -> (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1)))
4	1, 2, 3	mp2an 696	. . . . . . . . . 10 |- (A e. (0(,]1) <-> (A e. RR /\ 0 < A /\ A <_ 1))
5	4	biimp 151	. . . . . . . . 9 |- (A e. (0(,]1) -> (A e. RR /\ 0 < A /\ A <_ 1))
6	5	3simp1d 793	. . . . . . . 8 |- (A e. (0(,]1) -> A e. RR)
7		resqclt 6560	. . . . . . . 8 |- (A e. RR -> (A^2) e. RR)
8	6, 7	syl 10	. . . . . . 7 |- (A e. (0(,]1) -> (A^2) e. RR)
9	8	recnd 5295	. . . . . 6 |- (A e. (0(,]1) -> (A^2) e. CC)
10		2cn 5935	. . . . . . 7 |- 2 e. CC
11		3re 5936	. . . . . . . 8 |- 3 e. RR
12	11	recn 5294	. . . . . . 7 |- 3 e. CC
13		3nn 5955	. . . . . . . . 9 |- 3 e. NN
14	13	nnne0 5907	. . . . . . . 8 |- 3 =/= 0
15		div12t 5715	. . . . . . . 8 |- (((2 e. CC /\ (A^2) e. CC /\ 3 e. CC) /\ 3 =/= 0) -> (2 x. ((A^2) / 3)) = ((A^2) x. (2 / 3)))
16	14, 15	mpan2 695	. . . . . . 7 |- ((2 e. CC /\ (A^2) e. CC /\ 3 e. CC) -> (2 x. ((A^2) / 3)) = ((A^2) x. (2 / 3)))
17	10, 12, 16	mp3an13 905	. . . . . 6 |- ((A^2) e. CC -> (2 x. ((A^2) / 3)) = ((A^2) x. (2 / 3)))
18	9, 17	syl 10	. . . . 5 |- (A e. (0(,]1) -> (2 x. ((A^2) / 3)) = ((A^2) x. (2 / 3)))
19		2re 5934	. . . . . . . . 9 |- 2 e. RR
20	19, 11, 14	redivcl 5762	. . . . . . . 8 |- (2 / 3) e. RR
21	19	ltp1 5777	. . . . . . . . . . . . 13 |- 2 < (2 + 1)
22		df-3 5926	. . . . . . . . . . . . 13 |- 3 = (2 + 1)
23	21, 22	breqtrr 2635	. . . . . . . . . . . 12 |- 2 < 3
24		3pos 5946	. . . . . . . . . . . . 13 |- 0 < 3
25	19, 11, 11, 24	ltdiv1i 5787	. . . . . . . . . . . 12 |- (2 < 3 <-> (2 / 3) < (3 / 3))
26	23, 25	mpbi 189	. . . . . . . . . . 11 |- (2 / 3) < (3 / 3)
27	12, 14	divid 5734	. . . . . . . . . . 11 |- (3 / 3) = 1
28	26, 27	breqtr 2633	. . . . . . . . . 10 |- (2 / 3) < 1
29		ltmul2t 5795	. . . . . . . . . 10 |- ((((2 / 3) e. RR /\ 1 e. RR /\ (A^2) e. RR) /\ 0 < (A^2)) -> ((2 / 3) < 1 <-> ((A^2) x. (2 / 3)) < ((A^2) x. 1)))
30	28, 29	mpbii 193	. . . . . . . . 9 |- ((((2 / 3) e. RR /\ 1 e. RR /\ (A^2) e. RR) /\ 0 < (A^2)) -> ((A^2) x. (2 / 3)) < ((A^2) x. 1))
31	30	ex 373	. . . . . . . 8 |- (((2 / 3) e. RR /\ 1 e. RR /\ (A^2) e. RR) -> (0 < (A^2) -> ((A^2) x. (2 / 3)) < ((A^2) x. 1)))
32	20, 2, 31	mp3an12 904	. . . . . . 7 |- ((A^2) e. RR -> (0 < (A^2) -> ((A^2) x. (2 / 3)) < ((A^2) x. 1)))
33		2nn0 6070	. . . . . . . . . 10 |- 2 e. NN0
34		expgt0t 6528	. . . . . . . . . 10 |- ((A e. RR /\ 2 e. NN0 /\ 0 < A) -> 0 < (A^2))
35	33, 34	mp3an2 902	. . . . . . . . 9 |- ((A e. RR /\ 0 < A) -> 0 < (A^2))
36	35	3adant3 798	. . . . . . . 8 |- ((A e. RR /\ 0 < A /\ A <_ 1) -> 0 < (A^2))
37	4, 36	sylbi 199	. . . . . . 7 |- (A e. (0(,]1) -> 0 < (A^2))
38	32, 8, 37	sylc 68	. . . . . 6 |- (A e. (0(,]1) -> ((A^2) x. (2 / 3)) < ((A^2) x. 1))
39		ax1id 5262	. . . . . . 7 |- ((A^2) e. CC -> ((A^2) x. 1) = (A^2))
40	9, 39	syl 10	. . . . . 6 |- (A e. (0(,]1) -> ((A^2) x. 1) = (A^2))
41	38, 40	breqtrd 2634	. . . . 5 |- (A e. (0(,]1) -> ((A^2) x. (2 / 3)) < (A^2))
42	18, 41	eqbrtrd 2630	. . . 4 |- (A e. (0(,]1) -> (2 x. ((A^2) / 3)) < (A^2))
43		le2sqit 6571	. . . . . . . . 9 |- (((A e. RR /\ 0 <_ A) /\ (1 e. RR /\ A <_ 1)) -> (A^2) <_ (1^2))
44	2, 43	mpanr1 708	. . . . . . . 8 |- (((A e. RR /\ 0 <_ A) /\ A <_ 1) -> (A^2) <_ (1^2))
45		ltlet 5501	. . . . . . . . . 10 |- ((0 e. RR /\ A e. RR) -> (0 < A -> 0 <_ A))
46	1, 45	mpan 694	. . . . . . . . 9 |- (A e. RR -> (0 < A -> 0 <_ A))
47	46	imdistani 443	. . . . . . . 8 |- ((A e. RR /\ 0 < A) -> (A e. RR /\ 0 <_ A))
48	44, 47	sylan 448	. . . . . . 7 |- (((A e. RR /\ 0 < A) /\ A <_ 1) -> (A^2) <_ (1^2))
49	48	3impa 827	. . . . . 6 |- ((A e. RR /\ 0 < A /\ A <_ 1) -> (A^2) <_ (1^2))
50	4, 49	sylbi 199	. . . . 5 |- (A e. (0(,]1) -> (A^2) <_ (1^2))
51		sq1 6576	. . . . 5 |- (1^2) = 1
52	50, 51	syl6breq 2649	. . . 4 |- (A e. (0(,]1) -> (A^2) <_ 1)
53		ltletrt 5505	. . . . . 6 |- (((2 x. ((A^2) / 3)) e. RR /\ (A^2) e. RR /\ 1 e. RR) -> (((2 x. ((A^2) / 3)) < (A^2) /\ (A^2) <_ 1) -> (2 x. ((A^2) / 3)) < 1))
54	2, 53	mp3an3 903	. . . . 5 |- (((2 x. ((A^2) / 3)) e. RR /\ (A^2) e. RR) -> (((2 x. ((A^2) / 3)) < (A^2) /\ (A^2) <_ 1) -> (2 x. ((A^2) / 3)) < 1))
55		redivclt 5764	. . . . . . . 8 |- (((A^2) e. RR /\ 3 e. RR /\ 3 =/= 0) -> ((A^2) / 3) e. RR)
56	11, 14, 55	mp3an23 906	. . . . . . 7 |- ((A^2) e. RR -> ((A^2) / 3) e. RR)
57	8, 56	syl 10	. . . . . 6 |- (A e. (0(,]1) -> ((A^2) / 3) e. RR)
58		axmulrcl 5254	. . . . . . 7 |- ((2 e. RR /\ ((A^2) / 3) e. RR) -> (2 x. ((A^2) / 3)) e. RR)
59	19, 58	mpan 694	. . . . . 6 |- (((A^2) / 3) e. RR -> (2 x. ((A^2) / 3)) e. RR)
60	57, 59	syl 10	. . . . 5 |- (A e. (0(,]1) -> (2 x. ((A^2) / 3)) e. RR)
61	54, 60, 8	sylanc 471	. . . 4 |- (A e. (0(,]1) -> (((2 x. ((A^2) / 3)) < (A^2) /\ (A^2) <_ 1) -> (2 x. ((A^2) / 3)) < 1))
62	42, 52, 61	mp2and 702	. . 3 |- (A e. (0(,]1) -> (2 x. ((A^2) / 3)) < 1)
63		posdift 5635	. . . . 5 |- (((2 x. ((A^2) / 3)) e. RR /\ 1 e. RR) -> ((2 x. ((A^2) / 3)) < 1 <-> 0 < (1 - (2 x. ((A^2) / 3)))))
64	2, 63	mpan2 695	. . . 4 |- ((2 x. ((A^2) / 3)) e. RR -> ((2 x. ((A^2) / 3)) < 1 <-> 0 < (1 - (2 x. ((A^2) / 3)))))
65	60, 64	syl 10	. . 3 |- (A e. (0(,]1) -> ((2 x. ((A^2) / 3)) < 1 <-> 0 < (1 - (2 x. ((A^2) / 3)))))
66	62, 65	mpbid 195	. 2 |- (A e. (0(,]1) -> 0 < (1 - (2 x. ((A^2) / 3))))
67		cos01bnd 7423	. . 3 |- (A e. (0(,]1) -> ((1 - (2 x. ((A^2) / 3))) < (cos` A) /\ (cos` A) < (1 - ((A^2) / 3))))
68	67	pm3.26d 321	. 2 |- (A e. (0(,]1) -> (1 - (2 x. ((A^2) / 3))) < (cos` A))
69		axlttrn 5484	. . . 4 |- ((0 e. RR /\ (1 - (2 x. ((A^2) / 3))) e. RR /\ (cos` A) e. RR) -> ((0 < (1 - (2 x. ((A^2) / 3))) /\ (1 - (2 x. ((A^2) / 3))) < (cos` A)) -> 0 < (cos` A)))
70	1, 69	mp3an1 901	. . 3 |- (((1 - (2 x. ((A^2) / 3))) e. RR /\ (cos` A) e. RR) -> ((0 < (1 - (2 x. ((A^2) / 3))) /\ (1 - (2 x. ((A^2) / 3))) < (cos` A))