Step | Hyp | Ref
| Expression |
1 | | cosord.2 |
. . . . . . 7
β’ (π β π΅ β (0[,]Ο)) |
2 | | 0re 11162 |
. . . . . . . 8
β’ 0 β
β |
3 | | pire 25831 |
. . . . . . . 8
β’ Ο
β β |
4 | 2, 3 | elicc2i 13336 |
. . . . . . 7
β’ (π΅ β (0[,]Ο) β (π΅ β β β§ 0 β€
π΅ β§ π΅ β€ Ο)) |
5 | 1, 4 | sylib 217 |
. . . . . 6
β’ (π β (π΅ β β β§ 0 β€ π΅ β§ π΅ β€ Ο)) |
6 | 5 | simp1d 1143 |
. . . . 5
β’ (π β π΅ β β) |
7 | 6 | recnd 11188 |
. . . 4
β’ (π β π΅ β β) |
8 | | cosord.1 |
. . . . . . 7
β’ (π β π΄ β (0[,]Ο)) |
9 | 2, 3 | elicc2i 13336 |
. . . . . . 7
β’ (π΄ β (0[,]Ο) β (π΄ β β β§ 0 β€
π΄ β§ π΄ β€ Ο)) |
10 | 8, 9 | sylib 217 |
. . . . . 6
β’ (π β (π΄ β β β§ 0 β€ π΄ β§ π΄ β€ Ο)) |
11 | 10 | simp1d 1143 |
. . . . 5
β’ (π β π΄ β β) |
12 | 11 | recnd 11188 |
. . . 4
β’ (π β π΄ β β) |
13 | | subcos 16062 |
. . . 4
β’ ((π΅ β β β§ π΄ β β) β
((cosβπ΄) β
(cosβπ΅)) = (2
Β· ((sinβ((π΅ +
π΄) / 2)) Β·
(sinβ((π΅ β
π΄) /
2))))) |
14 | 7, 12, 13 | syl2anc 585 |
. . 3
β’ (π β ((cosβπ΄) β (cosβπ΅)) = (2 Β·
((sinβ((π΅ + π΄) / 2)) Β·
(sinβ((π΅ β
π΄) /
2))))) |
15 | | 2rp 12925 |
. . . 4
β’ 2 β
β+ |
16 | 6, 11 | readdcld 11189 |
. . . . . . . 8
β’ (π β (π΅ + π΄) β β) |
17 | 16 | rehalfcld 12405 |
. . . . . . 7
β’ (π β ((π΅ + π΄) / 2) β β) |
18 | 17 | resincld 16030 |
. . . . . 6
β’ (π β (sinβ((π΅ + π΄) / 2)) β β) |
19 | 2 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 0 β
β) |
20 | 10 | simp2d 1144 |
. . . . . . . . . . 11
β’ (π β 0 β€ π΄) |
21 | | cosord.3 |
. . . . . . . . . . 11
β’ (π β π΄ < π΅) |
22 | 19, 11, 6, 20, 21 | lelttrd 11318 |
. . . . . . . . . 10
β’ (π β 0 < π΅) |
23 | 6, 11, 22, 20 | addgtge0d 11734 |
. . . . . . . . 9
β’ (π β 0 < (π΅ + π΄)) |
24 | | 2re 12232 |
. . . . . . . . . 10
β’ 2 β
β |
25 | | 2pos 12261 |
. . . . . . . . . 10
β’ 0 <
2 |
26 | | divgt0 12028 |
. . . . . . . . . 10
β’ ((((π΅ + π΄) β β β§ 0 < (π΅ + π΄)) β§ (2 β β β§ 0 < 2))
β 0 < ((π΅ + π΄) / 2)) |
27 | 24, 25, 26 | mpanr12 704 |
. . . . . . . . 9
β’ (((π΅ + π΄) β β β§ 0 < (π΅ + π΄)) β 0 < ((π΅ + π΄) / 2)) |
28 | 16, 23, 27 | syl2anc 585 |
. . . . . . . 8
β’ (π β 0 < ((π΅ + π΄) / 2)) |
29 | 3 | a1i 11 |
. . . . . . . . 9
β’ (π β Ο β
β) |
30 | 11, 6, 6, 21 | ltadd2dd 11319 |
. . . . . . . . . . 11
β’ (π β (π΅ + π΄) < (π΅ + π΅)) |
31 | 7 | 2timesd 12401 |
. . . . . . . . . . 11
β’ (π β (2 Β· π΅) = (π΅ + π΅)) |
32 | 30, 31 | breqtrrd 5134 |
. . . . . . . . . 10
β’ (π β (π΅ + π΄) < (2 Β· π΅)) |
33 | 24 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 2 β
β) |
34 | 25 | a1i 11 |
. . . . . . . . . . 11
β’ (π β 0 < 2) |
35 | | ltdivmul 12035 |
. . . . . . . . . . 11
β’ (((π΅ + π΄) β β β§ π΅ β β β§ (2 β β
β§ 0 < 2)) β (((π΅ + π΄) / 2) < π΅ β (π΅ + π΄) < (2 Β· π΅))) |
36 | 16, 6, 33, 34, 35 | syl112anc 1375 |
. . . . . . . . . 10
β’ (π β (((π΅ + π΄) / 2) < π΅ β (π΅ + π΄) < (2 Β· π΅))) |
37 | 32, 36 | mpbird 257 |
. . . . . . . . 9
β’ (π β ((π΅ + π΄) / 2) < π΅) |
38 | 5 | simp3d 1145 |
. . . . . . . . 9
β’ (π β π΅ β€ Ο) |
39 | 17, 6, 29, 37, 38 | ltletrd 11320 |
. . . . . . . 8
β’ (π β ((π΅ + π΄) / 2) < Ο) |
40 | | 0xr 11207 |
. . . . . . . . 9
β’ 0 β
β* |
41 | 3 | rexri 11218 |
. . . . . . . . 9
β’ Ο
β β* |
42 | | elioo2 13311 |
. . . . . . . . 9
β’ ((0
β β* β§ Ο β β*) β
(((π΅ + π΄) / 2) β (0(,)Ο) β (((π΅ + π΄) / 2) β β β§ 0 < ((π΅ + π΄) / 2) β§ ((π΅ + π΄) / 2) < Ο))) |
43 | 40, 41, 42 | mp2an 691 |
. . . . . . . 8
β’ (((π΅ + π΄) / 2) β (0(,)Ο) β (((π΅ + π΄) / 2) β β β§ 0 < ((π΅ + π΄) / 2) β§ ((π΅ + π΄) / 2) < Ο)) |
44 | 17, 28, 39, 43 | syl3anbrc 1344 |
. . . . . . 7
β’ (π β ((π΅ + π΄) / 2) β (0(,)Ο)) |
45 | | sinq12gt0 25880 |
. . . . . . 7
β’ (((π΅ + π΄) / 2) β (0(,)Ο) β 0 <
(sinβ((π΅ + π΄) / 2))) |
46 | 44, 45 | syl 17 |
. . . . . 6
β’ (π β 0 < (sinβ((π΅ + π΄) / 2))) |
47 | 18, 46 | elrpd 12959 |
. . . . 5
β’ (π β (sinβ((π΅ + π΄) / 2)) β
β+) |
48 | 6, 11 | resubcld 11588 |
. . . . . . . 8
β’ (π β (π΅ β π΄) β β) |
49 | 48 | rehalfcld 12405 |
. . . . . . 7
β’ (π β ((π΅ β π΄) / 2) β β) |
50 | 49 | resincld 16030 |
. . . . . 6
β’ (π β (sinβ((π΅ β π΄) / 2)) β β) |
51 | 11, 6 | posdifd 11747 |
. . . . . . . . . 10
β’ (π β (π΄ < π΅ β 0 < (π΅ β π΄))) |
52 | 21, 51 | mpbid 231 |
. . . . . . . . 9
β’ (π β 0 < (π΅ β π΄)) |
53 | | divgt0 12028 |
. . . . . . . . . 10
β’ ((((π΅ β π΄) β β β§ 0 < (π΅ β π΄)) β§ (2 β β β§ 0 < 2))
β 0 < ((π΅ β
π΄) / 2)) |
54 | 24, 25, 53 | mpanr12 704 |
. . . . . . . . 9
β’ (((π΅ β π΄) β β β§ 0 < (π΅ β π΄)) β 0 < ((π΅ β π΄) / 2)) |
55 | 48, 52, 54 | syl2anc 585 |
. . . . . . . 8
β’ (π β 0 < ((π΅ β π΄) / 2)) |
56 | | rehalfcl 12384 |
. . . . . . . . . 10
β’ (Ο
β β β (Ο / 2) β β) |
57 | 3, 56 | mp1i 13 |
. . . . . . . . 9
β’ (π β (Ο / 2) β
β) |
58 | 6, 11 | subge02d 11752 |
. . . . . . . . . . . 12
β’ (π β (0 β€ π΄ β (π΅ β π΄) β€ π΅)) |
59 | 20, 58 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (π΅ β π΄) β€ π΅) |
60 | 48, 6, 29, 59, 38 | letrd 11317 |
. . . . . . . . . 10
β’ (π β (π΅ β π΄) β€ Ο) |
61 | | lediv1 12025 |
. . . . . . . . . . 11
β’ (((π΅ β π΄) β β β§ Ο β β
β§ (2 β β β§ 0 < 2)) β ((π΅ β π΄) β€ Ο β ((π΅ β π΄) / 2) β€ (Ο / 2))) |
62 | 48, 29, 33, 34, 61 | syl112anc 1375 |
. . . . . . . . . 10
β’ (π β ((π΅ β π΄) β€ Ο β ((π΅ β π΄) / 2) β€ (Ο / 2))) |
63 | 60, 62 | mpbid 231 |
. . . . . . . . 9
β’ (π β ((π΅ β π΄) / 2) β€ (Ο / 2)) |
64 | | pirp 25834 |
. . . . . . . . . 10
β’ Ο
β β+ |
65 | | rphalflt 12949 |
. . . . . . . . . 10
β’ (Ο
β β+ β (Ο / 2) < Ο) |
66 | 64, 65 | mp1i 13 |
. . . . . . . . 9
β’ (π β (Ο / 2) <
Ο) |
67 | 49, 57, 29, 63, 66 | lelttrd 11318 |
. . . . . . . 8
β’ (π β ((π΅ β π΄) / 2) < Ο) |
68 | | elioo2 13311 |
. . . . . . . . 9
β’ ((0
β β* β§ Ο β β*) β
(((π΅ β π΄) / 2) β (0(,)Ο) β
(((π΅ β π΄) / 2) β β β§ 0
< ((π΅ β π΄) / 2) β§ ((π΅ β π΄) / 2) < Ο))) |
69 | 40, 41, 68 | mp2an 691 |
. . . . . . . 8
β’ (((π΅ β π΄) / 2) β (0(,)Ο) β (((π΅ β π΄) / 2) β β β§ 0 < ((π΅ β π΄) / 2) β§ ((π΅ β π΄) / 2) < Ο)) |
70 | 49, 55, 67, 69 | syl3anbrc 1344 |
. . . . . . 7
β’ (π β ((π΅ β π΄) / 2) β (0(,)Ο)) |
71 | | sinq12gt0 25880 |
. . . . . . 7
β’ (((π΅ β π΄) / 2) β (0(,)Ο) β 0 <
(sinβ((π΅ β
π΄) / 2))) |
72 | 70, 71 | syl 17 |
. . . . . 6
β’ (π β 0 < (sinβ((π΅ β π΄) / 2))) |
73 | 50, 72 | elrpd 12959 |
. . . . 5
β’ (π β (sinβ((π΅ β π΄) / 2)) β
β+) |
74 | 47, 73 | rpmulcld 12978 |
. . . 4
β’ (π β ((sinβ((π΅ + π΄) / 2)) Β· (sinβ((π΅ β π΄) / 2))) β
β+) |
75 | | rpmulcl 12943 |
. . . 4
β’ ((2
β β+ β§ ((sinβ((π΅ + π΄) / 2)) Β· (sinβ((π΅ β π΄) / 2))) β β+) β
(2 Β· ((sinβ((π΅
+ π΄) / 2)) Β·
(sinβ((π΅ β
π΄) / 2)))) β
β+) |
76 | 15, 74, 75 | sylancr 588 |
. . 3
β’ (π β (2 Β·
((sinβ((π΅ + π΄) / 2)) Β·
(sinβ((π΅ β
π΄) / 2)))) β
β+) |
77 | 14, 76 | eqeltrd 2834 |
. 2
β’ (π β ((cosβπ΄) β (cosβπ΅)) β
β+) |
78 | 6 | recoscld 16031 |
. . 3
β’ (π β (cosβπ΅) β
β) |
79 | 11 | recoscld 16031 |
. . 3
β’ (π β (cosβπ΄) β
β) |
80 | | difrp 12958 |
. . 3
β’
(((cosβπ΅)
β β β§ (cosβπ΄) β β) β ((cosβπ΅) < (cosβπ΄) β ((cosβπ΄) β (cosβπ΅)) β
β+)) |
81 | 78, 79, 80 | syl2anc 585 |
. 2
β’ (π β ((cosβπ΅) < (cosβπ΄) β ((cosβπ΄) β (cosβπ΅)) β
β+)) |
82 | 77, 81 | mpbird 257 |
1
β’ (π β (cosβπ΅) < (cosβπ΄)) |