Step |
Hyp |
Ref |
Expression |
0 |
|
vn |
|- n |
1 |
|
vz |
|- z |
2 |
|
cz |
|- ZZ |
3 |
|
c2 |
|- 2 |
4 |
|
cdvds |
|- || |
5 |
1
|
cv |
|- z |
6 |
3 5 4
|
wbr |
|- 2 || z |
7 |
6
|
wn |
|- -. 2 || z |
8 |
7 1 2
|
crab |
|- { z e. ZZ | -. 2 || z } |
9 |
|
c1 |
|- 1 |
10 |
|
cc0 |
|- 0 |
11 |
9 10
|
cdc |
|- ; 1 0 |
12 |
|
cexp |
|- ^ |
13 |
|
c7 |
|- 7 |
14 |
3 13
|
cdc |
|- ; 2 7 |
15 |
11 14 12
|
co |
|- ( ; 1 0 ^ ; 2 7 ) |
16 |
|
cle |
|- <_ |
17 |
0
|
cv |
|- n |
18 |
15 17 16
|
wbr |
|- ( ; 1 0 ^ ; 2 7 ) <_ n |
19 |
|
vh |
|- h |
20 |
|
cico |
|- [,) |
21 |
|
cpnf |
|- +oo |
22 |
10 21 20
|
co |
|- ( 0 [,) +oo ) |
23 |
|
cmap |
|- ^m |
24 |
|
cn |
|- NN |
25 |
22 24 23
|
co |
|- ( ( 0 [,) +oo ) ^m NN ) |
26 |
|
vk |
|- k |
27 |
|
vm |
|- m |
28 |
26
|
cv |
|- k |
29 |
27
|
cv |
|- m |
30 |
29 28
|
cfv |
|- ( k ` m ) |
31 |
|
cdp |
|- . |
32 |
|
c9 |
|- 9 |
33 |
|
c5 |
|- 5 |
34 |
33 33
|
cdp2 |
|- _ 5 5 |
35 |
32 34
|
cdp2 |
|- _ 9 _ 5 5 |
36 |
32 35
|
cdp2 |
|- _ 9 _ 9 _ 5 5 |
37 |
13 36
|
cdp2 |
|- _ 7 _ 9 _ 9 _ 5 5 |
38 |
10 37
|
cdp2 |
|- _ 0 _ 7 _ 9 _ 9 _ 5 5 |
39 |
9 38 31
|
co |
|- ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) |
40 |
30 39 16
|
wbr |
|- ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) |
41 |
40 27 24
|
wral |
|- A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) |
42 |
19
|
cv |
|- h |
43 |
29 42
|
cfv |
|- ( h ` m ) |
44 |
|
c4 |
|- 4 |
45 |
9 44
|
cdp2 |
|- _ 1 4 |
46 |
44 45
|
cdp2 |
|- _ 4 _ 1 4 |
47 |
9 46 31
|
co |
|- ( 1 . _ 4 _ 1 4 ) |
48 |
43 47 16
|
wbr |
|- ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) |
49 |
48 27 24
|
wral |
|- A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) |
50 |
|
c8 |
|- 8 |
51 |
44 50
|
cdp2 |
|- _ 4 8 |
52 |
3 51
|
cdp2 |
|- _ 2 _ 4 8 |
53 |
3 52
|
cdp2 |
|- _ 2 _ 2 _ 4 8 |
54 |
44 53
|
cdp2 |
|- _ 4 _ 2 _ 2 _ 4 8 |
55 |
10 54
|
cdp2 |
|- _ 0 _ 4 _ 2 _ 2 _ 4 8 |
56 |
10 55
|
cdp2 |
|- _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 |
57 |
10 56
|
cdp2 |
|- _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 |
58 |
10 57 31
|
co |
|- ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) |
59 |
|
cmul |
|- x. |
60 |
17 3 12
|
co |
|- ( n ^ 2 ) |
61 |
58 60 59
|
co |
|- ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) |
62 |
|
cioo |
|- (,) |
63 |
10 9 62
|
co |
|- ( 0 (,) 1 ) |
64 |
|
cvma |
|- Lam |
65 |
59
|
cof |
|- oF x. |
66 |
64 42 65
|
co |
|- ( Lam oF x. h ) |
67 |
|
cvts |
|- vts |
68 |
66 17 67
|
co |
|- ( ( Lam oF x. h ) vts n ) |
69 |
|
vx |
|- x |
70 |
69
|
cv |
|- x |
71 |
70 68
|
cfv |
|- ( ( ( Lam oF x. h ) vts n ) ` x ) |
72 |
64 28 65
|
co |
|- ( Lam oF x. k ) |
73 |
72 17 67
|
co |
|- ( ( Lam oF x. k ) vts n ) |
74 |
70 73
|
cfv |
|- ( ( ( Lam oF x. k ) vts n ) ` x ) |
75 |
74 3 12
|
co |
|- ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) |
76 |
71 75 59
|
co |
|- ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) |
77 |
|
ce |
|- exp |
78 |
|
ci |
|- _i |
79 |
|
cpi |
|- _pi |
80 |
3 79 59
|
co |
|- ( 2 x. _pi ) |
81 |
78 80 59
|
co |
|- ( _i x. ( 2 x. _pi ) ) |
82 |
17
|
cneg |
|- -u n |
83 |
82 70 59
|
co |
|- ( -u n x. x ) |
84 |
81 83 59
|
co |
|- ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) |
85 |
84 77
|
cfv |
|- ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) |
86 |
76 85 59
|
co |
|- ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) |
87 |
69 63 86
|
citg |
|- S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x |
88 |
61 87 16
|
wbr |
|- ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x |
89 |
41 49 88
|
w3a |
|- ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) |
90 |
89 26 25
|
wrex |
|- E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) |
91 |
90 19 25
|
wrex |
|- E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) |
92 |
18 91
|
wi |
|- ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) ) |
93 |
92 0 8
|
wral |
|- A. n e. { z e. ZZ | -. 2 || z } ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) ) |