| | β’ |
β’
|
Proof of lemma1 |
β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ π΄ β β ) |
Step | Hyp | Expression |
1 | | β’ ( π΄ β β βΆ (sinβπ΄) = (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) )
|
2 | | β’ ( (sinβπ΄) = 0 βΆ (sinβπ΄) = 0 )
|
3 | 1, 2 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) = 0 )
|
4 | | β’ i β β
|
5 | | β’ 2 β β
|
6 | 4, 5 | β’ (2 Β· i) β β
|
7 | | β’ ( π΄ β β βΆ π΄ β β )
|
8 | 4, 7 | β’ ( π΄ β β βΆ (i Β· π΄) β β )
|
9 | 8 | β’ ( π΄ β β βΆ (expβ(i Β· π΄)) β β )
|
10 | 4 | β’ -i β β
|
11 | 10, 7 | β’ ( π΄ β β βΆ (-i Β· π΄) β β )
|
12 | 11 | β’ ( π΄ β β βΆ (expβ(-i Β· π΄)) β β )
|
13 | 9, 12 | β’ ( π΄ β β βΆ ((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) β β )
|
14 | | β’ i β 0
|
15 | | β’ 2 β 0
|
16 | 5, 4, 14, 15 | β’ (2 Β· i) β 0
|
17 | 13, 6, 16 | β’ ( π΄ β β βΆ ((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) = 0 β ((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) = 0) )
|
18 | 3, 17 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ ((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) = 0 )
|
19 | 9, 12 | β’ ( π΄ β β βΆ (((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) = 0 β (expβ(i Β· π΄)) = (expβ(-i Β· π΄))) )
|
20 | 19, 18 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (expβ(i Β· π΄)) = (expβ(-i Β· π΄)) )
|
21 | 20 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ ((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(-i Β· π΄))) )
|
22 | 8, 11 | β’ ( π΄ β β βΆ (expβ((i Β· π΄) + (-i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(-i Β· π΄))) )
|
23 | 4 | β’ (i + -i) = 0
|
24 | 23 | β’ ((i + -i) Β· π΄) = (0 Β· π΄)
|
25 | 7, 4, 10 | β’ ( π΄ β β βΆ ((i + -i) Β· π΄) = ((i Β· π΄) + (-i Β· π΄)) )
|
26 | 24, 25 | β’ ( π΄ β β βΆ ((i Β· π΄) + (-i Β· π΄)) = (0 Β· π΄) )
|
27 | 7 | β’ ( π΄ β β βΆ (0 Β· π΄) = 0 )
|
28 | 26, 27 | β’ ( π΄ β β βΆ ((i Β· π΄) + (-i Β· π΄)) = 0 )
|
29 | 28 | β’ ( π΄ β β βΆ (expβ((i Β· π΄) + (-i Β· π΄))) = (expβ0) )
|
30 | | β’ (expβ0) = 1
|
31 | 22, 21 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ ((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) = (expβ((i Β· π΄) + (-i Β· π΄))) )
|
32 | 29, 30, 31 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ ((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) = 1 )
|
33 | 8, 8 | β’ ( π΄ β β βΆ (expβ((i Β· π΄) + (i Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) )
|
34 | 8 | β’ ( π΄ β β βΆ (2 Β· (i Β· π΄)) = ((i Β· π΄) + (i Β· π΄)) )
|
35 | 5, 4, 7 | β’ ( π΄ β β βΆ (2 Β· (i Β· π΄)) = (i Β· (2 Β· π΄)) )
|
36 | 34, 35 | β’ ( π΄ β β βΆ (i Β· (2 Β· π΄)) = ((i Β· π΄) + (i Β· π΄)) )
|
37 | 36 | β’ ( π΄ β β βΆ (expβ(i Β· (2 Β· π΄))) = (expβ((i Β· π΄) + (i Β· π΄))) )
|
38 | 33, 37 | β’ ( π΄ β β βΆ (expβ(i Β· (2 Β· π΄))) = ((expβ(i Β· π΄)) Β· (expβ(i Β· π΄))) )
|
39 | 32, 38 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (expβ(i Β· (2 Β· π΄))) = 1 )
|
40 | 39 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(expβ(i Β· (2 Β· π΄)))) = (absβ1) )
|
41 | | β’ (absβ1) = 1
|
42 | 40, 41 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(expβ(i Β· (2 Β· π΄)))) = 1 )
|
43 | 7, 5 | β’ ( π΄ β β βΆ (2 Β· π΄) β β )
|
44 | 43, 42 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (2 Β· π΄) β β )
|
45 | 5 | β’ 2 β β
|
lemma1 | 15, 45, 7, 44 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ π΄ β β )
|
β’
|
Proof of lemma2 |
β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(sinβ(π΄ + (-(ββ(π΄ / π)) Β· π)))) = (absβ(sinβ(π΄ β (π Β· (ββ(π΄ / π)))))) ) |
Step | Hyp | Expression |
47 | | β’ π β β
|
48 | | β’ 0 < π
|
49 | | β’ 0 β β
|
50 | 49, 47, 48 | β’ 0 β€ π
|
51 | 47, 50, 48 | β’ π β 0
|
52 | 47, lemma1, 51 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ / π) β β )
|
53 | 52 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (ββ(π΄ / π)) β β€ )
|
54 | 53 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (ββ(π΄ / π)) β β )
|
55 | 47 | β’ π β β
|
56 | 54, 55 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (-(ββ(π΄ / π)) Β· π) = -((ββ(π΄ / π)) Β· π) )
|
57 | 54, 55 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ ((ββ(π΄ / π)) Β· π) = (π Β· (ββ(π΄ / π))) )
|
58 | 57 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ -((ββ(π΄ / π)) Β· π) = -(π Β· (ββ(π΄ / π))) )
|
59 | 56, 58 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (-(ββ(π΄ / π)) Β· π) = -(π Β· (ββ(π΄ / π))) )
|
60 | 55, 54 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π Β· (ββ(π΄ / π))) β β )
|
61 | 7, 60 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ + -(π Β· (ββ(π΄ / π)))) = (π΄ β (π Β· (ββ(π΄ / π)))) )
|
62 | 60 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ -(π Β· (ββ(π΄ / π))) β β )
|
63 | 54 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ -(ββ(π΄ / π)) β β )
|
64 | 63, 55 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (-(ββ(π΄ / π)) Β· π) β β )
|
65 | 59, 7, 62, 64 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ + (-(ββ(π΄ / π)) Β· π)) = (π΄ + -(π Β· (ββ(π΄ / π)))) )
|
66 | 65, 61 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ + (-(ββ(π΄ / π)) Β· π)) = (π΄ β (π Β· (ββ(π΄ / π)))) )
|
67 | 66 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (sinβ(π΄ + (-(ββ(π΄ / π)) Β· π))) = (sinβ(π΄ β (π Β· (ββ(π΄ / π))))) )
|
lemma2 | 67 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(sinβ(π΄ + (-(ββ(π΄ / π)) Β· π)))) = (absβ(sinβ(π΄ β (π Β· (ββ(π΄ / π)))))) )
|
β’
|
Proof of lemma3 |
β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (sinβ(π΄ mod π)) = 0 ) |
Step | Hyp | Expression |
69 | | β’ ( ( π΄ β β , π β β+ ) βΆ (π΄ mod π) = (π΄ β (π Β· (ββ(π΄ / π)))) )
|
70 | 69 | β’ ( ( π΄ β β , π β β+ ) βΆ (sinβ(π΄ mod π)) = (sinβ(π΄ β (π Β· (ββ(π΄ / π))))) )
|
71 | 70 | β’ ( ( π΄ β β , π β β+ ) βΆ (absβ(sinβ(π΄ mod π))) = (absβ(sinβ(π΄ β (π Β· (ββ(π΄ / π)))))) )
|
72 | | β’ ( ( π΄ β β , -(ββ(π΄ / π)) β β€ ) βΆ (absβ(sinβπ΄)) = (absβ(sinβ(π΄ + (-(ββ(π΄ / π)) Β· π)))) )
|
73 | 72 | β’ ( π΄ β β βΆ (-(ββ(π΄ / π)) β β€ β (absβ(sinβπ΄)) = (absβ(sinβ(π΄ + (-(ββ(π΄ / π)) Β· π))))) )
|
74 | 53 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ -(ββ(π΄ / π)) β β€ )
|
75 | 73, 74 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(sinβπ΄)) = (absβ(sinβ(π΄ + (-(ββ(π΄ / π)) Β· π)))) )
|
76 | 47, 48 | β’ π β β+
|
77 | 71, 76 | β’ ( π΄ β β βΆ (absβ(sinβ(π΄ mod π))) = (absβ(sinβ(π΄ β (π Β· (ββ(π΄ / π)))))) )
|
78 | lemma1, 77 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(sinβ(π΄ mod π))) = (absβ(sinβ(π΄ β (π Β· (ββ(π΄ / π)))))) )
|
79 | 75, lemma2 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(sinβπ΄)) = (absβ(sinβ(π΄ β (π Β· (ββ(π΄ / π)))))) )
|
80 | 79, 78 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(sinβπ΄)) = (absβ(sinβ(π΄ mod π))) )
|
81 | 2 | β’ ( (sinβπ΄) = 0 βΆ (absβ(sinβπ΄)) = (absβ0) )
|
82 | | β’ (absβ0) = 0
|
83 | 81, 82 | β’ ( (sinβπ΄) = 0 βΆ (absβ(sinβπ΄)) = 0 )
|
84 | 80, 83 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (absβ(sinβ(π΄ mod π))) = 0 )
|
85 | lemma1, 76 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ mod π) β β )
|
86 | 85 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ mod π) β β )
|
87 | 86 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (sinβ(π΄ mod π)) β β )
|
lemma3 | 87, 84 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (sinβ(π΄ mod π)) = 0 )
|
β’
|
Proof of lemma4 |
β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ Β¬ 0 < (π΄ mod π) ) |
Step | Hyp | Expression |
89 | | β’ ( ( 0 β β , 0 < (sinβ(π΄ mod π)) ) βΆ (sinβ(π΄ mod π)) β 0 )
|
90 | 89 | β’ ( ( 0 β β , 0 < (sinβ(π΄ mod π)) ) βΆ Β¬ (sinβ(π΄ mod π)) = 0 )
|
91 | 90 | β’ ( 0 < (sinβ(π΄ mod π)) βΆ (0 β β β Β¬ (sinβ(π΄ mod π)) = 0) )
|
92 | 91, 49 | β’ ( 0 < (sinβ(π΄ mod π)) βΆ Β¬ (sinβ(π΄ mod π)) = 0 )
|
93 | 92 | β’ (Β¬ Β¬ (sinβ(π΄ mod π)) = 0 β Β¬ 0 < (sinβ(π΄ mod π)))
|
94 | | β’ (Β¬ Β¬ (sinβ(π΄ mod π)) = 0 β (sinβ(π΄ mod π)) = 0)
|
95 | 93, 94 | β’ ((sinβ(π΄ mod π)) = 0 β Β¬ 0 < (sinβ(π΄ mod π)))
|
96 | lemma3, 95 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ Β¬ 0 < (sinβ(π΄ mod π)) )
|
97 | | β’ ((π΄ mod π) β (0(,)π) β 0 < (sinβ(π΄ mod π)))
|
98 | 96, 97 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ Β¬ (π΄ mod π) β (0(,)π) )
|
99 | 49 | β’ 0 β β*
|
100 | 47 | β’ π β β*
|
101 | 99, 100 | β’ ((π΄ mod π) β (0(,)π) β ((π΄ mod π) β β β§ 0 < (π΄ mod π) β§ (π΄ mod π) < π))
|
102 | 101 | β’ (Β¬ (π΄ mod π) β (0(,)π) β Β¬ ((π΄ mod π) β β β§ 0 < (π΄ mod π) β§ (π΄ mod π) < π))
|
103 | 98, 102 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ Β¬ ((π΄ mod π) β β β§ 0 < (π΄ mod π) β§ (π΄ mod π) < π) )
|
104 | | β’ (((π΄ mod π) β β β§ 0 < (π΄ mod π) β§ (π΄ mod π) < π) β (0 < (π΄ mod π) β§ ((π΄ mod π) β β β§ (π΄ mod π) < π)))
|
105 | 104 | β’ (Β¬ ((π΄ mod π) β β β§ 0 < (π΄ mod π) β§ (π΄ mod π) < π) β Β¬ (0 < (π΄ mod π) β§ ((π΄ mod π) β β β§ (π΄ mod π) < π)))
|
106 | 103, 105 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ Β¬ (0 < (π΄ mod π) β§ ((π΄ mod π) β β β§ (π΄ mod π) < π)) )
|
107 | 76, lemma1 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ mod π) < π )
|
108 | 85, 107 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ ((π΄ mod π) β β β§ (π΄ mod π) < π) )
|
lemma4 | 106, 108 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ Β¬ 0 < (π΄ mod π) )
|
β’
|
Proof of sineq0ALTVD |
β’ ( π΄ β β βΆ ((sinβπ΄) = 0 β (π΄ / π) β β€) ) |
Step | Hyp | Expression |
110 | lemma1, 76 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ 0 β€ (π΄ mod π) )
|
111 | 49, 85, 110 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (0 < (π΄ mod π) β¨ 0 = (π΄ mod π)) )
|
112 | lemma4, 111 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ 0 = (π΄ mod π) )
|
113 | 112 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ mod π) = 0 )
|
114 | lemma1, 76, 113 | β’ ( ( π΄ β β , (sinβπ΄) = 0 ) βΆ (π΄ / π) β β€ )
|
115 | 114 | β’ ( π΄ β β βΆ ((sinβπ΄) = 0 β (π΄ / π) β β€) )
|
116 | | β’ ( (π΄ / π) β β€ βΆ (π΄ / π) β β€ )
|
117 | 116 | β’ ( (π΄ / π) β β€ βΆ (sinβ((π΄ / π) Β· π)) = 0 )
|
118 | 7, 55, 51 | β’ ( π΄ β β βΆ ((π΄ / π) Β· π) = π΄ )
|
119 | 118 | β’ ( π΄ β β βΆ (sinβ((π΄ / π) Β· π)) = (sinβπ΄) )
|
120 | 117, 119 | β’ ( ( π΄ β β , (π΄ / π) β β€ ) βΆ (sinβπ΄) = 0 )
|
121 | 120 | β’ ( π΄ β β βΆ ((π΄ / π) β β€ β (sinβπ΄) = 0) )
|
qed | 115, 121 | β’ ( π΄ β β βΆ ((sinβπ΄) = 0 β (π΄ / π) β β€) )
|