Metamath Proof Explorer


Theorem pilem2

Description: Lemma for pire , pigt2lt4 and sinpi . (Contributed by Mario Carneiro, 12-Jun-2014) (Revised by AV, 14-Sep-2020)

Ref Expression
Hypotheses pilem2.1 φ A 2 4
pilem2.2 φ B +
pilem2.3 φ sin A = 0
pilem2.4 φ sin B = 0
Assertion pilem2 φ π + A 2 B

Proof

Step Hyp Ref Expression
1 pilem2.1 φ A 2 4
2 pilem2.2 φ B +
3 pilem2.3 φ sin A = 0
4 pilem2.4 φ sin B = 0
5 df-pi π = sup + sin -1 0 <
6 inss1 + sin -1 0 +
7 rpssre +
8 6 7 sstri + sin -1 0
9 8 a1i φ + sin -1 0
10 0re 0
11 elinel1 y + sin -1 0 y +
12 11 rpge0d y + sin -1 0 0 y
13 12 rgen y + sin -1 0 0 y
14 breq1 x = 0 x y 0 y
15 14 ralbidv x = 0 y + sin -1 0 x y y + sin -1 0 0 y
16 15 rspcev 0 y + sin -1 0 0 y x y + sin -1 0 x y
17 10 13 16 mp2an x y + sin -1 0 x y
18 17 a1i φ x y + sin -1 0 x y
19 2re 2
20 2 rpred φ B
21 remulcl 2 B 2 B
22 19 20 21 sylancr φ 2 B
23 elioore A 2 4 A
24 1 23 syl φ A
25 22 24 resubcld φ 2 B A
26 4re 4
27 26 a1i φ 4
28 eliooord A 2 4 2 < A A < 4
29 1 28 syl φ 2 < A A < 4
30 29 simprd φ A < 4
31 2t2e4 2 2 = 4
32 19 a1i φ 2
33 0red φ 0
34 2pos 0 < 2
35 34 a1i φ 0 < 2
36 29 simpld φ 2 < A
37 33 32 24 35 36 lttrd φ 0 < A
38 24 37 elrpd φ A +
39 pilem1 A + sin -1 0 A + sin A = 0
40 38 3 39 sylanbrc φ A + sin -1 0
41 40 ne0d φ + sin -1 0
42 infrecl + sin -1 0 + sin -1 0 x y + sin -1 0 x y sup + sin -1 0 <
43 8 17 42 mp3an13 + sin -1 0 sup + sin -1 0 <
44 41 43 syl φ sup + sin -1 0 <
45 pilem1 x + sin -1 0 x + sin x = 0
46 rpre x + x
47 46 adantl φ x + x
48 letric 2 x 2 x x 2
49 19 47 48 sylancr φ x + 2 x x 2
50 49 ord φ x + ¬ 2 x x 2
51 46 ad2antlr φ x + x 2 x
52 rpgt0 x + 0 < x
53 52 ad2antlr φ x + x 2 0 < x
54 simpr φ x + x 2 x 2
55 0xr 0 *
56 elioc2 0 * 2 x 0 2 x 0 < x x 2
57 55 19 56 mp2an x 0 2 x 0 < x x 2
58 51 53 54 57 syl3anbrc φ x + x 2 x 0 2
59 sin02gt0 x 0 2 0 < sin x
60 58 59 syl φ x + x 2 0 < sin x
61 60 gt0ne0d φ x + x 2 sin x 0
62 61 ex φ x + x 2 sin x 0
63 50 62 syld φ x + ¬ 2 x sin x 0
64 63 necon4bd φ x + sin x = 0 2 x
65 64 expimpd φ x + sin x = 0 2 x
66 45 65 syl5bi φ x + sin -1 0 2 x
67 66 ralrimiv φ x + sin -1 0 2 x
68 infregelb + sin -1 0 + sin -1 0 x y + sin -1 0 x y 2 2 sup + sin -1 0 < x + sin -1 0 2 x
69 9 41 18 32 68 syl31anc φ 2 sup + sin -1 0 < x + sin -1 0 2 x
70 67 69 mpbird φ 2 sup + sin -1 0 <
71 pilem1 B + sin -1 0 B + sin B = 0
72 2 4 71 sylanbrc φ B + sin -1 0
73 infrelb + sin -1 0 x y + sin -1 0 x y B + sin -1 0 sup + sin -1 0 < B
74 9 18 72 73 syl3anc φ sup + sin -1 0 < B
75 32 44 20 70 74 letrd φ 2 B
76 19 34 pm3.2i 2 0 < 2
77 76 a1i φ 2 0 < 2
78 lemul2 2 B 2 0 < 2 2 B 2 2 2 B
79 32 20 77 78 syl3anc φ 2 B 2 2 2 B
80 75 79 mpbid φ 2 2 2 B
81 31 80 eqbrtrrid φ 4 2 B
82 24 27 22 30 81 ltletrd φ A < 2 B
83 24 22 posdifd φ A < 2 B 0 < 2 B A
84 82 83 mpbid φ 0 < 2 B A
85 25 84 elrpd φ 2 B A +
86 22 recnd φ 2 B
87 24 recnd φ A
88 sinsub 2 B A sin 2 B A = sin 2 B cos A cos 2 B sin A
89 86 87 88 syl2anc φ sin 2 B A = sin 2 B cos A cos 2 B sin A
90 20 recnd φ B
91 sin2t B sin 2 B = 2 sin B cos B
92 90 91 syl φ sin 2 B = 2 sin B cos B
93 4 oveq1d φ sin B cos B = 0 cos B
94 90 coscld φ cos B
95 94 mul02d φ 0 cos B = 0
96 93 95 eqtrd φ sin B cos B = 0
97 96 oveq2d φ 2 sin B cos B = 2 0
98 2t0e0 2 0 = 0
99 97 98 syl6eq φ 2 sin B cos B = 0
100 92 99 eqtrd φ sin 2 B = 0
101 100 oveq1d φ sin 2 B cos A = 0 cos A
102 87 coscld φ cos A
103 102 mul02d φ 0 cos A = 0
104 101 103 eqtrd φ sin 2 B cos A = 0
105 3 oveq2d φ cos 2 B sin A = cos 2 B 0
106 86 coscld φ cos 2 B
107 106 mul01d φ cos 2 B 0 = 0
108 105 107 eqtrd φ cos 2 B sin A = 0
109 104 108 oveq12d φ sin 2 B cos A cos 2 B sin A = 0 0
110 0m0e0 0 0 = 0
111 109 110 syl6eq φ sin 2 B cos A cos 2 B sin A = 0
112 89 111 eqtrd φ sin 2 B A = 0
113 pilem1 2 B A + sin -1 0 2 B A + sin 2 B A = 0
114 85 112 113 sylanbrc φ 2 B A + sin -1 0
115 infrelb + sin -1 0 x y + sin -1 0 x y 2 B A + sin -1 0 sup + sin -1 0 < 2 B A
116 9 18 114 115 syl3anc φ sup + sin -1 0 < 2 B A
117 5 116 eqbrtrid φ π 2 B A
118 5 44 eqeltrid φ π
119 leaddsub π A 2 B π + A 2 B π 2 B A
120 118 24 22 119 syl3anc φ π + A 2 B π 2 B A
121 117 120 mpbird φ π + A 2 B
122 118 24 readdcld φ π + A
123 ledivmul π + A B 2 0 < 2 π + A 2 B π + A 2 B
124 122 20 77 123 syl3anc φ π + A 2 B π + A 2 B
125 121 124 mpbird φ π + A 2 B