Metamath Proof Explorer


Theorem fourierdlem44

Description: A condition for having ( sin( A / 2 ) ) nonzero. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion fourierdlem44 AππA0sinA20

Proof

Step Hyp Ref Expression
1 0xr 0*
2 1 a1i Aππ0<A0*
3 2re 2
4 pire π
5 3 4 remulcli 2π
6 5 rexri 2π*
7 6 a1i Aππ0<A2π*
8 4 renegcli π
9 8 a1i Aπππ
10 4 a1i Aπππ
11 id AππAππ
12 eliccre ππAππA
13 9 10 11 12 syl3anc AππA
14 13 adantr Aππ0<AA
15 simpr Aππ0<A0<A
16 5 a1i Aππ2π
17 9 rexrd Aπππ*
18 10 rexrd Aπππ*
19 iccleub π*π*AππAπ
20 17 18 11 19 syl3anc AππAπ
21 pirp π+
22 2timesgt π+π<2π
23 21 22 ax-mp π<2π
24 23 a1i Aπππ<2π
25 13 10 16 20 24 lelttrd AππA<2π
26 25 adantr Aππ0<AA<2π
27 2 7 14 15 26 eliood Aππ0<AA02π
28 27 adantlr AππA00<AA02π
29 sinaover2ne0 A02πsinA20
30 28 29 syl AππA00<AsinA20
31 simpll AππA0¬0<AAππ
32 31 13 syl AππA0¬0<AA
33 0red AππA0¬0<A0
34 simplr AππA0¬0<AA0
35 simpr AππA0¬0<A¬0<A
36 32 33 34 35 lttri5d AππA0¬0<AA<0
37 13 recnd AππA
38 37 halfcld AππA2
39 sinneg A2sinA2=sinA2
40 38 39 syl AππsinA2=sinA2
41 2cnd Aππ2
42 2ne0 20
43 42 a1i Aππ20
44 37 41 43 divnegd AππA2=A2
45 44 fveq2d AππsinA2=sinA2
46 40 45 eqtr3d AππsinA2=sinA2
47 46 adantr AππA<0sinA2=sinA2
48 1 a1i AππA<00*
49 6 a1i AππA<02π*
50 13 renegcld AππA
51 50 adantr AππA<0A
52 simpr AππA<0A<0
53 13 adantr AππA<0A
54 53 lt0neg1d AππA<0A<00<A
55 52 54 mpbid AππA<00<A
56 5 renegcli 2π
57 56 a1i AππA<02π
58 8 a1i AππA<0π
59 4 5 ltnegi π<2π2π<π
60 23 59 mpbi 2π<π
61 60 a1i AππA<02π<π
62 iccgelb π*π*AπππA
63 17 18 11 62 syl3anc AπππA
64 63 adantr AππA<0πA
65 57 58 53 61 64 ltletrd AππA<02π<A
66 57 53 ltnegd AππA<02π<AA<2π
67 65 66 mpbid AππA<0A<2π
68 16 recnd Aππ2π
69 68 negnegd Aππ2π=2π
70 69 adantr AππA<02π=2π
71 67 70 breqtrd AππA<0A<2π
72 48 49 51 55 71 eliood AππA<0A02π
73 sinaover2ne0 A02πsinA20
74 72 73 syl AππA<0sinA20
75 47 74 eqnetrd AππA<0sinA20
76 75 neneqd AππA<0¬sinA2=0
77 38 sincld AππsinA2
78 77 adantr AππA<0sinA2
79 78 negeq0d AππA<0sinA2=0sinA2=0
80 76 79 mtbird AππA<0¬sinA2=0
81 80 neqned AππA<0sinA20
82 31 36 81 syl2anc AππA0¬0<AsinA20
83 30 82 pm2.61dan AππA0sinA20