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

Theorem cos01bnd 11779
Description: Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
Assertion
Ref Expression
cos01bnd (๐ด โˆˆ (0(,]1) โ†’ ((1 โˆ’ (2 ยท ((๐ดโ†‘2) / 3))) < (cosโ€˜๐ด) โˆง (cosโ€˜๐ด) < (1 โˆ’ ((๐ดโ†‘2) / 3))))

Proof of Theorem cos01bnd
Dummy variables ๐‘˜ ๐‘› are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0xr 8017 . . . . . . . . 9 0 โˆˆ โ„*
2 1re 7969 . . . . . . . . 9 1 โˆˆ โ„
3 elioc2 9949 . . . . . . . . 9 ((0 โˆˆ โ„* โˆง 1 โˆˆ โ„) โ†’ (๐ด โˆˆ (0(,]1) โ†” (๐ด โˆˆ โ„ โˆง 0 < ๐ด โˆง ๐ด โ‰ค 1)))
41, 2, 3mp2an 426 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†” (๐ด โˆˆ โ„ โˆง 0 < ๐ด โˆง ๐ด โ‰ค 1))
54simp1bi 1013 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ ๐ด โˆˆ โ„)
6 eqid 2187 . . . . . . . 8 (๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›))) = (๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))
76recos4p 11740 . . . . . . 7 (๐ด โˆˆ โ„ โ†’ (cosโ€˜๐ด) = ((1 โˆ’ ((๐ดโ†‘2) / 2)) + (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))))
85, 7syl 14 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (cosโ€˜๐ด) = ((1 โˆ’ ((๐ดโ†‘2) / 2)) + (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))))
98eqcomd 2193 . . . . 5 (๐ด โˆˆ (0(,]1) โ†’ ((1 โˆ’ ((๐ดโ†‘2) / 2)) + (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))) = (cosโ€˜๐ด))
105recoscld 11745 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ (cosโ€˜๐ด) โˆˆ โ„)
1110recnd 7999 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (cosโ€˜๐ด) โˆˆ โ„‚)
125resqcld 10693 . . . . . . . . 9 (๐ด โˆˆ (0(,]1) โ†’ (๐ดโ†‘2) โˆˆ โ„)
1312rehalfcld 9178 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) / 2) โˆˆ โ„)
14 resubcl 8234 . . . . . . . 8 ((1 โˆˆ โ„ โˆง ((๐ดโ†‘2) / 2) โˆˆ โ„) โ†’ (1 โˆ’ ((๐ดโ†‘2) / 2)) โˆˆ โ„)
152, 13, 14sylancr 414 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ (1 โˆ’ ((๐ดโ†‘2) / 2)) โˆˆ โ„)
1615recnd 7999 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (1 โˆ’ ((๐ดโ†‘2) / 2)) โˆˆ โ„‚)
17 ax-icn 7919 . . . . . . . . . 10 i โˆˆ โ„‚
185recnd 7999 . . . . . . . . . 10 (๐ด โˆˆ (0(,]1) โ†’ ๐ด โˆˆ โ„‚)
19 mulcl 7951 . . . . . . . . . 10 ((i โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚) โ†’ (i ยท ๐ด) โˆˆ โ„‚)
2017, 18, 19sylancr 414 . . . . . . . . 9 (๐ด โˆˆ (0(,]1) โ†’ (i ยท ๐ด) โˆˆ โ„‚)
21 4nn0 9208 . . . . . . . . 9 4 โˆˆ โ„•0
226eftlcl 11709 . . . . . . . . 9 (((i ยท ๐ด) โˆˆ โ„‚ โˆง 4 โˆˆ โ„•0) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜) โˆˆ โ„‚)
2320, 21, 22sylancl 413 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜) โˆˆ โ„‚)
2423recld 10960 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)) โˆˆ โ„)
2524recnd 7999 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)) โˆˆ โ„‚)
2611, 16, 25subaddd 8299 . . . . 5 (๐ด โˆˆ (0(,]1) โ†’ (((cosโ€˜๐ด) โˆ’ (1 โˆ’ ((๐ดโ†‘2) / 2))) = (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)) โ†” ((1 โˆ’ ((๐ดโ†‘2) / 2)) + (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))) = (cosโ€˜๐ด)))
279, 26mpbird 167 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ ((cosโ€˜๐ด) โˆ’ (1 โˆ’ ((๐ดโ†‘2) / 2))) = (โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)))
2827fveq2d 5531 . . 3 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜((cosโ€˜๐ด) โˆ’ (1 โˆ’ ((๐ดโ†‘2) / 2)))) = (absโ€˜(โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))))
2925abscld 11203 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜(โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))) โˆˆ โ„)
3023abscld 11203 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)) โˆˆ โ„)
31 6nn 9097 . . . . 5 6 โˆˆ โ„•
32 nndivre 8968 . . . . 5 (((๐ดโ†‘2) โˆˆ โ„ โˆง 6 โˆˆ โ„•) โ†’ ((๐ดโ†‘2) / 6) โˆˆ โ„)
3312, 31, 32sylancl 413 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) / 6) โˆˆ โ„)
34 absrele 11105 . . . . 5 (ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜) โˆˆ โ„‚ โ†’ (absโ€˜(โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))) โ‰ค (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)))
3523, 34syl 14 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜(โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))) โ‰ค (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)))
36 reexpcl 10550 . . . . . . 7 ((๐ด โˆˆ โ„ โˆง 4 โˆˆ โ„•0) โ†’ (๐ดโ†‘4) โˆˆ โ„)
375, 21, 36sylancl 413 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (๐ดโ†‘4) โˆˆ โ„)
38 nndivre 8968 . . . . . 6 (((๐ดโ†‘4) โˆˆ โ„ โˆง 6 โˆˆ โ„•) โ†’ ((๐ดโ†‘4) / 6) โˆˆ โ„)
3937, 31, 38sylancl 413 . . . . 5 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘4) / 6) โˆˆ โ„)
406ef01bndlem 11777 . . . . 5 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)) < ((๐ดโ†‘4) / 6))
41 2nn0 9206 . . . . . . . 8 2 โˆˆ โ„•0
4241a1i 9 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ 2 โˆˆ โ„•0)
43 4z 9296 . . . . . . . . 9 4 โˆˆ โ„ค
44 2re 9002 . . . . . . . . . 10 2 โˆˆ โ„
45 4re 9009 . . . . . . . . . 10 4 โˆˆ โ„
46 2lt4 9105 . . . . . . . . . 10 2 < 4
4744, 45, 46ltleii 8073 . . . . . . . . 9 2 โ‰ค 4
48 2z 9294 . . . . . . . . . 10 2 โˆˆ โ„ค
4948eluz1i 9548 . . . . . . . . 9 (4 โˆˆ (โ„คโ‰ฅโ€˜2) โ†” (4 โˆˆ โ„ค โˆง 2 โ‰ค 4))
5043, 47, 49mpbir2an 943 . . . . . . . 8 4 โˆˆ (โ„คโ‰ฅโ€˜2)
5150a1i 9 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ 4 โˆˆ (โ„คโ‰ฅโ€˜2))
524simp2bi 1014 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ 0 < ๐ด)
53 0re 7970 . . . . . . . . 9 0 โˆˆ โ„
54 ltle 8058 . . . . . . . . 9 ((0 โˆˆ โ„ โˆง ๐ด โˆˆ โ„) โ†’ (0 < ๐ด โ†’ 0 โ‰ค ๐ด))
5553, 5, 54sylancr 414 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ (0 < ๐ด โ†’ 0 โ‰ค ๐ด))
5652, 55mpd 13 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ 0 โ‰ค ๐ด)
574simp3bi 1015 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ ๐ด โ‰ค 1)
585, 42, 51, 56, 57leexp2rd 10697 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (๐ดโ†‘4) โ‰ค (๐ดโ†‘2))
59 6re 9013 . . . . . . . 8 6 โˆˆ โ„
6059a1i 9 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ 6 โˆˆ โ„)
61 6pos 9033 . . . . . . . 8 0 < 6
6261a1i 9 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ 0 < 6)
63 lediv1 8839 . . . . . . 7 (((๐ดโ†‘4) โˆˆ โ„ โˆง (๐ดโ†‘2) โˆˆ โ„ โˆง (6 โˆˆ โ„ โˆง 0 < 6)) โ†’ ((๐ดโ†‘4) โ‰ค (๐ดโ†‘2) โ†” ((๐ดโ†‘4) / 6) โ‰ค ((๐ดโ†‘2) / 6)))
6437, 12, 60, 62, 63syl112anc 1252 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘4) โ‰ค (๐ดโ†‘2) โ†” ((๐ดโ†‘4) / 6) โ‰ค ((๐ดโ†‘2) / 6)))
6558, 64mpbid 147 . . . . 5 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘4) / 6) โ‰ค ((๐ดโ†‘2) / 6))
6630, 39, 33, 40, 65ltletrd 8393 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜)) < ((๐ดโ†‘2) / 6))
6729, 30, 33, 35, 66lelttrd 8095 . . 3 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜(โ„œโ€˜ฮฃ๐‘˜ โˆˆ (โ„คโ‰ฅโ€˜4)((๐‘› โˆˆ โ„•0 โ†ฆ (((i ยท ๐ด)โ†‘๐‘›) / (!โ€˜๐‘›)))โ€˜๐‘˜))) < ((๐ดโ†‘2) / 6))
6828, 67eqbrtrd 4037 . 2 (๐ด โˆˆ (0(,]1) โ†’ (absโ€˜((cosโ€˜๐ด) โˆ’ (1 โˆ’ ((๐ดโ†‘2) / 2)))) < ((๐ดโ†‘2) / 6))
6910, 15, 33absdifltd 11200 . . 3 (๐ด โˆˆ (0(,]1) โ†’ ((absโ€˜((cosโ€˜๐ด) โˆ’ (1 โˆ’ ((๐ดโ†‘2) / 2)))) < ((๐ดโ†‘2) / 6) โ†” (((1 โˆ’ ((๐ดโ†‘2) / 2)) โˆ’ ((๐ดโ†‘2) / 6)) < (cosโ€˜๐ด) โˆง (cosโ€˜๐ด) < ((1 โˆ’ ((๐ดโ†‘2) / 2)) + ((๐ดโ†‘2) / 6)))))
70 1cnd 7986 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ 1 โˆˆ โ„‚)
7113recnd 7999 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) / 2) โˆˆ โ„‚)
7233recnd 7999 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) / 6) โˆˆ โ„‚)
7370, 71, 72subsub4d 8312 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ ((1 โˆ’ ((๐ดโ†‘2) / 2)) โˆ’ ((๐ดโ†‘2) / 6)) = (1 โˆ’ (((๐ดโ†‘2) / 2) + ((๐ดโ†‘2) / 6))))
74 halfpm6th 9152 . . . . . . . . . . 11 (((1 / 2) โˆ’ (1 / 6)) = (1 / 3) โˆง ((1 / 2) + (1 / 6)) = (2 / 3))
7574simpri 113 . . . . . . . . . 10 ((1 / 2) + (1 / 6)) = (2 / 3)
7675oveq2i 5899 . . . . . . . . 9 ((๐ดโ†‘2) ยท ((1 / 2) + (1 / 6))) = ((๐ดโ†‘2) ยท (2 / 3))
7712recnd 7999 . . . . . . . . . 10 (๐ด โˆˆ (0(,]1) โ†’ (๐ดโ†‘2) โˆˆ โ„‚)
78 2cn 9003 . . . . . . . . . . . 12 2 โˆˆ โ„‚
79 2ap0 9025 . . . . . . . . . . . 12 2 # 0
8078, 79recclapi 8712 . . . . . . . . . . 11 (1 / 2) โˆˆ โ„‚
81 6cn 9014 . . . . . . . . . . . 12 6 โˆˆ โ„‚
8231nnap0i 8963 . . . . . . . . . . . 12 6 # 0
8381, 82recclapi 8712 . . . . . . . . . . 11 (1 / 6) โˆˆ โ„‚
84 adddi 7956 . . . . . . . . . . 11 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง (1 / 2) โˆˆ โ„‚ โˆง (1 / 6) โˆˆ โ„‚) โ†’ ((๐ดโ†‘2) ยท ((1 / 2) + (1 / 6))) = (((๐ดโ†‘2) ยท (1 / 2)) + ((๐ดโ†‘2) ยท (1 / 6))))
8580, 83, 84mp3an23 1339 . . . . . . . . . 10 ((๐ดโ†‘2) โˆˆ โ„‚ โ†’ ((๐ดโ†‘2) ยท ((1 / 2) + (1 / 6))) = (((๐ดโ†‘2) ยท (1 / 2)) + ((๐ดโ†‘2) ยท (1 / 6))))
8677, 85syl 14 . . . . . . . . 9 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) ยท ((1 / 2) + (1 / 6))) = (((๐ดโ†‘2) ยท (1 / 2)) + ((๐ดโ†‘2) ยท (1 / 6))))
8776, 86eqtr3id 2234 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) ยท (2 / 3)) = (((๐ดโ†‘2) ยท (1 / 2)) + ((๐ดโ†‘2) ยท (1 / 6))))
88 3cn 9007 . . . . . . . . . . 11 3 โˆˆ โ„‚
89 3ap0 9028 . . . . . . . . . . 11 3 # 0
9088, 89pm3.2i 272 . . . . . . . . . 10 (3 โˆˆ โ„‚ โˆง 3 # 0)
91 div12ap 8664 . . . . . . . . . 10 ((2 โˆˆ โ„‚ โˆง (๐ดโ†‘2) โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 # 0)) โ†’ (2 ยท ((๐ดโ†‘2) / 3)) = ((๐ดโ†‘2) ยท (2 / 3)))
9278, 90, 91mp3an13 1338 . . . . . . . . 9 ((๐ดโ†‘2) โˆˆ โ„‚ โ†’ (2 ยท ((๐ดโ†‘2) / 3)) = ((๐ดโ†‘2) ยท (2 / 3)))
9377, 92syl 14 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ (2 ยท ((๐ดโ†‘2) / 3)) = ((๐ดโ†‘2) ยท (2 / 3)))
94 divrecap 8658 . . . . . . . . . . 11 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง 2 # 0) โ†’ ((๐ดโ†‘2) / 2) = ((๐ดโ†‘2) ยท (1 / 2)))
9578, 79, 94mp3an23 1339 . . . . . . . . . 10 ((๐ดโ†‘2) โˆˆ โ„‚ โ†’ ((๐ดโ†‘2) / 2) = ((๐ดโ†‘2) ยท (1 / 2)))
9677, 95syl 14 . . . . . . . . 9 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) / 2) = ((๐ดโ†‘2) ยท (1 / 2)))
97 divrecap 8658 . . . . . . . . . . 11 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง 6 โˆˆ โ„‚ โˆง 6 # 0) โ†’ ((๐ดโ†‘2) / 6) = ((๐ดโ†‘2) ยท (1 / 6)))
9881, 82, 97mp3an23 1339 . . . . . . . . . 10 ((๐ดโ†‘2) โˆˆ โ„‚ โ†’ ((๐ดโ†‘2) / 6) = ((๐ดโ†‘2) ยท (1 / 6)))
9977, 98syl 14 . . . . . . . . 9 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) / 6) = ((๐ดโ†‘2) ยท (1 / 6)))
10096, 99oveq12d 5906 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ (((๐ดโ†‘2) / 2) + ((๐ดโ†‘2) / 6)) = (((๐ดโ†‘2) ยท (1 / 2)) + ((๐ดโ†‘2) ยท (1 / 6))))
10187, 93, 1003eqtr4rd 2231 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ (((๐ดโ†‘2) / 2) + ((๐ดโ†‘2) / 6)) = (2 ยท ((๐ดโ†‘2) / 3)))
102101oveq2d 5904 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (1 โˆ’ (((๐ดโ†‘2) / 2) + ((๐ดโ†‘2) / 6))) = (1 โˆ’ (2 ยท ((๐ดโ†‘2) / 3))))
10373, 102eqtrd 2220 . . . . 5 (๐ด โˆˆ (0(,]1) โ†’ ((1 โˆ’ ((๐ดโ†‘2) / 2)) โˆ’ ((๐ดโ†‘2) / 6)) = (1 โˆ’ (2 ยท ((๐ดโ†‘2) / 3))))
104103breq1d 4025 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ (((1 โˆ’ ((๐ดโ†‘2) / 2)) โˆ’ ((๐ดโ†‘2) / 6)) < (cosโ€˜๐ด) โ†” (1 โˆ’ (2 ยท ((๐ดโ†‘2) / 3))) < (cosโ€˜๐ด)))
10570, 71, 72subsubd 8309 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (1 โˆ’ (((๐ดโ†‘2) / 2) โˆ’ ((๐ดโ†‘2) / 6))) = ((1 โˆ’ ((๐ดโ†‘2) / 2)) + ((๐ดโ†‘2) / 6)))
10674simpli 111 . . . . . . . . . 10 ((1 / 2) โˆ’ (1 / 6)) = (1 / 3)
107106oveq2i 5899 . . . . . . . . 9 ((๐ดโ†‘2) ยท ((1 / 2) โˆ’ (1 / 6))) = ((๐ดโ†‘2) ยท (1 / 3))
108 subdi 8355 . . . . . . . . . . 11 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง (1 / 2) โˆˆ โ„‚ โˆง (1 / 6) โˆˆ โ„‚) โ†’ ((๐ดโ†‘2) ยท ((1 / 2) โˆ’ (1 / 6))) = (((๐ดโ†‘2) ยท (1 / 2)) โˆ’ ((๐ดโ†‘2) ยท (1 / 6))))
10980, 83, 108mp3an23 1339 . . . . . . . . . 10 ((๐ดโ†‘2) โˆˆ โ„‚ โ†’ ((๐ดโ†‘2) ยท ((1 / 2) โˆ’ (1 / 6))) = (((๐ดโ†‘2) ยท (1 / 2)) โˆ’ ((๐ดโ†‘2) ยท (1 / 6))))
11077, 109syl 14 . . . . . . . . 9 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) ยท ((1 / 2) โˆ’ (1 / 6))) = (((๐ดโ†‘2) ยท (1 / 2)) โˆ’ ((๐ดโ†‘2) ยท (1 / 6))))
111107, 110eqtr3id 2234 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) ยท (1 / 3)) = (((๐ดโ†‘2) ยท (1 / 2)) โˆ’ ((๐ดโ†‘2) ยท (1 / 6))))
112 divrecap 8658 . . . . . . . . . 10 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง 3 โˆˆ โ„‚ โˆง 3 # 0) โ†’ ((๐ดโ†‘2) / 3) = ((๐ดโ†‘2) ยท (1 / 3)))
11388, 89, 112mp3an23 1339 . . . . . . . . 9 ((๐ดโ†‘2) โˆˆ โ„‚ โ†’ ((๐ดโ†‘2) / 3) = ((๐ดโ†‘2) ยท (1 / 3)))
11477, 113syl 14 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ ((๐ดโ†‘2) / 3) = ((๐ดโ†‘2) ยท (1 / 3)))
11596, 99oveq12d 5906 . . . . . . . 8 (๐ด โˆˆ (0(,]1) โ†’ (((๐ดโ†‘2) / 2) โˆ’ ((๐ดโ†‘2) / 6)) = (((๐ดโ†‘2) ยท (1 / 2)) โˆ’ ((๐ดโ†‘2) ยท (1 / 6))))
116111, 114, 1153eqtr4rd 2231 . . . . . . 7 (๐ด โˆˆ (0(,]1) โ†’ (((๐ดโ†‘2) / 2) โˆ’ ((๐ดโ†‘2) / 6)) = ((๐ดโ†‘2) / 3))
117116oveq2d 5904 . . . . . 6 (๐ด โˆˆ (0(,]1) โ†’ (1 โˆ’ (((๐ดโ†‘2) / 2) โˆ’ ((๐ดโ†‘2) / 6))) = (1 โˆ’ ((๐ดโ†‘2) / 3)))
118105, 117eqtr3d 2222 . . . . 5 (๐ด โˆˆ (0(,]1) โ†’ ((1 โˆ’ ((๐ดโ†‘2) / 2)) + ((๐ดโ†‘2) / 6)) = (1 โˆ’ ((๐ดโ†‘2) / 3)))
119118breq2d 4027 . . . 4 (๐ด โˆˆ (0(,]1) โ†’ ((cosโ€˜๐ด) < ((1 โˆ’ ((๐ดโ†‘2) / 2)) + ((๐ดโ†‘2) / 6)) โ†” (cosโ€˜๐ด) < (1 โˆ’ ((๐ดโ†‘2) / 3))))
120104, 119anbi12d 473 . . 3 (๐ด โˆˆ (0(,]1) โ†’ ((((1 โˆ’ ((๐ดโ†‘2) / 2)) โˆ’ ((๐ดโ†‘2) / 6)) < (cosโ€˜๐ด) โˆง (cosโ€˜๐ด) < ((1 โˆ’ ((๐ดโ†‘2) / 2)) + ((๐ดโ†‘2) / 6))) โ†” ((1 โˆ’ (2 ยท ((๐ดโ†‘2) / 3))) < (cosโ€˜๐ด) โˆง (cosโ€˜๐ด) < (1 โˆ’ ((๐ดโ†‘2) / 3)))))
12169, 120bitrd 188 . 2 (๐ด โˆˆ (0(,]1) โ†’ ((absโ€˜((cosโ€˜๐ด) โˆ’ (1 โˆ’ ((๐ดโ†‘2) / 2)))) < ((๐ดโ†‘2) / 6) โ†” ((1 โˆ’ (2 ยท ((๐ดโ†‘2) / 3))) < (cosโ€˜๐ด) โˆง (cosโ€˜๐ด) < (1 โˆ’ ((๐ดโ†‘2) / 3)))))
12268, 121mpbid 147 1 (๐ด โˆˆ (0(,]1) โ†’ ((1 โˆ’ (2 ยท ((๐ดโ†‘2) / 3))) < (cosโ€˜๐ด) โˆง (cosโ€˜๐ด) < (1 โˆ’ ((๐ดโ†‘2) / 3))))
Colors of variables: wff set class
Syntax hints:   โ†’ wi 4   โˆง wa 104   โ†” wb 105   โˆง w3a 979   = wceq 1363   โˆˆ wcel 2158   class class class wbr 4015   โ†ฆ cmpt 4076  โ€˜cfv 5228  (class class class)co 5888  โ„‚cc 7822  โ„cr 7823  0cc0 7824  1c1 7825  ici 7826   + caddc 7827   ยท cmul 7829  โ„*cxr 8004   < clt 8005   โ‰ค cle 8006   โˆ’ cmin 8141   # cap 8551   / cdiv 8642  โ„•cn 8932  2c2 8983  3c3 8984  4c4 8985  6c6 8987  โ„•0cn0 9189  โ„คcz 9266  โ„คโ‰ฅcuz 9541  (,]cioc 9902  โ†‘cexp 10532  !cfa 10718  โ„œcre 10862  abscabs 11019  ฮฃcsu 11374  cosccos 11666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-mulrcl 7923  ax-addcom 7924  ax-mulcom 7925  ax-addass 7926  ax-mulass 7927  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-1rid 7931  ax-0id 7932  ax-rnegex 7933  ax-precex 7934  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-apti 7939  ax-pre-ltadd 7940  ax-pre-mulgt0 7941  ax-pre-mulext 7942  ax-arch 7943  ax-caucvg 7944
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rmo 2473  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-isom 5237  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-frec 6405  df-1o 6430  df-oadd 6434  df-er 6548  df-en 6754  df-dom 6755  df-fin 6756  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-reap 8545  df-ap 8552  df-div 8643  df-inn 8933  df-2 8991  df-3 8992  df-4 8993  df-5 8994  df-6 8995  df-7 8996  df-8 8997  df-n0 9190  df-z 9267  df-uz 9542  df-q 9633  df-rp 9667  df-ioc 9906  df-ico 9907  df-fz 10022  df-fzo 10156  df-seqfrec 10459  df-exp 10533  df-fac 10719  df-ihash 10769  df-shft 10837  df-cj 10864  df-re 10865  df-im 10866  df-rsqrt 11020  df-abs 11021  df-clim 11300  df-sumdc 11375  df-ef 11669  df-cos 11672
This theorem is referenced by:  cos1bnd  11780  cos01gt0  11783  tangtx  14499
  Copyright terms: Public domain W3C validator