Step | Hyp | Ref
| Expression |
1 | | circlemethhgt.n |
. . 3
|
2 | | 3nn 11186 |
. . . 4
|
3 | 2 | a1i 11 |
. . 3
|
4 | | s3len 13639 |
. . . . . 6
Λ
Λ Λ
|
5 | 4 | eqcomi 2631 |
. . . . 5
Λ Λ
Λ
|
6 | 5 | a1i 11 |
. . . 4
Λ
Λ Λ
|
7 | | simprl 794 |
. . . . . . . . 9
|
8 | | simprr 796 |
. . . . . . . . 9
|
9 | 7, 8 | remulcld 10070 |
. . . . . . . 8
|
10 | 9 | recnd 10068 |
. . . . . . 7
|
11 | | vmaf 24845 |
. . . . . . . 8
Λ |
12 | 11 | a1i 11 |
. . . . . . 7
Λ |
13 | | circlemethhgt.h |
. . . . . . 7
|
14 | | nnex 11026 |
. . . . . . . 8
|
15 | 14 | a1i 11 |
. . . . . . 7
|
16 | | inidm 3822 |
. . . . . . 7
|
17 | 10, 12, 13, 15, 15, 16 | off 6912 |
. . . . . 6
Λ |
18 | | cnex 10017 |
. . . . . . 7
|
19 | 18, 14 | elmap 7886 |
. . . . . 6
Λ
Λ |
20 | 17, 19 | sylibr 224 |
. . . . 5
Λ |
21 | | circlemethhgt.k |
. . . . . . 7
|
22 | 10, 12, 21, 15, 15, 16 | off 6912 |
. . . . . 6
Λ |
23 | 18, 14 | elmap 7886 |
. . . . . 6
Λ
Λ |
24 | 22, 23 | sylibr 224 |
. . . . 5
Λ |
25 | 20, 24, 24 | s3cld 13617 |
. . . 4
Λ
Λ Λ
Word |
26 | 6, 25 | wrdfd 30616 |
. . 3
Λ
Λ Λ
..^ |
27 | 1, 3, 26 | circlemeth 30718 |
. 2
repr ..^Λ Λ Λ
..^Λ Λ Λ
vts
|
28 | | fveq2 6191 |
. . . . . 6
Λ Λ
Λ
Λ Λ
Λ
|
29 | | fveq2 6191 |
. . . . . 6
|
30 | 28, 29 | fveq12d 6197 |
. . . . 5
Λ
Λ Λ
Λ Λ
Λ
|
31 | | fveq2 6191 |
. . . . . 6
Λ Λ
Λ
Λ Λ
Λ
|
32 | | fveq2 6191 |
. . . . . 6
|
33 | 31, 32 | fveq12d 6197 |
. . . . 5
Λ
Λ Λ
Λ Λ
Λ
|
34 | | fveq2 6191 |
. . . . . 6
Λ Λ
Λ
Λ Λ
Λ
|
35 | | fveq2 6191 |
. . . . . 6
|
36 | 34, 35 | fveq12d 6197 |
. . . . 5
Λ
Λ Λ
Λ Λ
Λ
|
37 | 26 | adantr 481 |
. . . . . . . 8
repr Λ
Λ Λ
..^ |
38 | 37 | ffvelrnda 6359 |
. . . . . . 7
repr ..^
Λ Λ
Λ
|
39 | | elmapi 7879 |
. . . . . . 7
Λ Λ
Λ
Λ Λ Λ
|
40 | 38, 39 | syl 17 |
. . . . . 6
repr ..^
Λ Λ
Λ
|
41 | | ssid 3624 |
. . . . . . . . 9
|
42 | 41 | a1i 11 |
. . . . . . . 8
repr |
43 | 1 | nn0zd 11480 |
. . . . . . . . 9
|
44 | 43 | adantr 481 |
. . . . . . . 8
repr |
45 | | 3nn0 11310 |
. . . . . . . . 9
|
46 | 45 | a1i 11 |
. . . . . . . 8
repr |
47 | | simpr 477 |
. . . . . . . 8
repr repr |
48 | 42, 44, 46, 47 | reprf 30690 |
. . . . . . 7
repr ..^ |
49 | 48 | ffvelrnda 6359 |
. . . . . 6
repr ..^
|
50 | 40, 49 | ffvelrnd 6360 |
. . . . 5
repr ..^
Λ Λ
Λ
|
51 | 30, 33, 36, 50 | prodfzo03 30681 |
. . . 4
repr ..^Λ Λ Λ
Λ Λ Λ
Λ Λ Λ
Λ Λ
Λ
|
52 | | ovex 6678 |
. . . . . . . 8
Λ
|
53 | | s3fv0 13636 |
. . . . . . . 8
Λ
Λ Λ
Λ
Λ
|
54 | 52, 53 | mp1i 13 |
. . . . . . 7
repr Λ Λ Λ
Λ
|
55 | 54 | fveq1d 6193 |
. . . . . 6
repr Λ Λ
Λ
Λ |
56 | | simpl 473 |
. . . . . . 7
repr |
57 | | c0ex 10034 |
. . . . . . . . . . 11
|
58 | 57 | tpid1 4303 |
. . . . . . . . . 10
|
59 | | fzo0to3tp 12554 |
. . . . . . . . . 10
..^ |
60 | 58, 59 | eleqtrri 2700 |
. . . . . . . . 9
..^ |
61 | 60 | a1i 11 |
. . . . . . . 8
repr ..^ |
62 | 48, 61 | ffvelrnd 6360 |
. . . . . . 7
repr |
63 | | ffn 6045 |
. . . . . . . . . 10
Λ
Λ |
64 | 11, 63 | ax-mp 5 |
. . . . . . . . 9
Λ |
65 | 64 | a1i 11 |
. . . . . . . 8
Λ |
66 | 13 | ffnd 6046 |
. . . . . . . 8
|
67 | | eqidd 2623 |
. . . . . . . 8
Λ Λ |
68 | | eqidd 2623 |
. . . . . . . 8
|
69 | 65, 66, 15, 15, 16, 67, 68 | ofval 6906 |
. . . . . . 7
Λ Λ |
70 | 56, 62, 69 | syl2anc 693 |
. . . . . 6
repr Λ
Λ |
71 | 55, 70 | eqtrd 2656 |
. . . . 5
repr Λ Λ
Λ
Λ |
72 | | ovex 6678 |
. . . . . . . . 9
Λ
|
73 | | s3fv1 13637 |
. . . . . . . . 9
Λ
Λ Λ
Λ
Λ
|
74 | 72, 73 | mp1i 13 |
. . . . . . . 8
repr Λ Λ Λ
Λ
|
75 | 74 | fveq1d 6193 |
. . . . . . 7
repr Λ Λ
Λ
Λ |
76 | | 1ex 10035 |
. . . . . . . . . . . 12
|
77 | 76 | tpid2 4304 |
. . . . . . . . . . 11
|
78 | 77, 59 | eleqtrri 2700 |
. . . . . . . . . 10
..^ |
79 | 78 | a1i 11 |
. . . . . . . . 9
repr ..^ |
80 | 48, 79 | ffvelrnd 6360 |
. . . . . . . 8
repr |
81 | 21 | ffnd 6046 |
. . . . . . . . 9
|
82 | | eqidd 2623 |
. . . . . . . . 9
Λ Λ |
83 | | eqidd 2623 |
. . . . . . . . 9
|
84 | 65, 81, 15, 15, 16, 82, 83 | ofval 6906 |
. . . . . . . 8
Λ Λ |
85 | 56, 80, 84 | syl2anc 693 |
. . . . . . 7
repr Λ
Λ |
86 | 75, 85 | eqtrd 2656 |
. . . . . 6
repr Λ Λ
Λ
Λ |
87 | | s3fv2 13638 |
. . . . . . . . 9
Λ
Λ Λ
Λ
Λ
|
88 | 72, 87 | mp1i 13 |
. . . . . . . 8
repr Λ Λ Λ
Λ
|
89 | 88 | fveq1d 6193 |
. . . . . . 7
repr Λ Λ
Λ
Λ |
90 | | 2ex 11092 |
. . . . . . . . . . . 12
|
91 | 90 | tpid3 4307 |
. . . . . . . . . . 11
|
92 | 91, 59 | eleqtrri 2700 |
. . . . . . . . . 10
..^ |
93 | 92 | a1i 11 |
. . . . . . . . 9
repr ..^ |
94 | 48, 93 | ffvelrnd 6360 |
. . . . . . . 8
repr |
95 | | eqidd 2623 |
. . . . . . . . 9
Λ Λ |
96 | | eqidd 2623 |
. . . . . . . . 9
|
97 | 65, 81, 15, 15, 16, 95, 96 | ofval 6906 |
. . . . . . . 8
Λ Λ |
98 | 56, 94, 97 | syl2anc 693 |
. . . . . . 7
repr Λ
Λ |
99 | 89, 98 | eqtrd 2656 |
. . . . . 6
repr Λ Λ
Λ
Λ |
100 | 86, 99 | oveq12d 6668 |
. . . . 5
repr Λ Λ
Λ
Λ Λ
Λ
Λ Λ |
101 | 71, 100 | oveq12d 6668 |
. . . 4
repr Λ Λ
Λ
Λ Λ Λ
Λ Λ
Λ
Λ Λ Λ |
102 | 51, 101 | eqtrd 2656 |
. . 3
repr ..^Λ Λ Λ
Λ Λ Λ |
103 | 102 | sumeq2dv 14433 |
. 2
repr ..^Λ Λ Λ
reprΛ Λ Λ |
104 | | nfv 1843 |
. . . . . 6
|
105 | | nfcv 2764 |
. . . . . 6
Λ
vts |
106 | | fzofi 12773 |
. . . . . . 7
..^ |
107 | 106 | a1i 11 |
. . . . . 6
..^ |
108 | 57 | a1i 11 |
. . . . . 6
|
109 | | eqid 2622 |
. . . . . . . . 9
|
110 | 109 | orci 405 |
. . . . . . . 8
|
111 | | 0elfz 12436 |
. . . . . . . . 9
|
112 | | elfznelfzob 12574 |
. . . . . . . . 9
..^
|
113 | 45, 111, 112 | mp2b 10 |
. . . . . . . 8
..^
|
114 | 110, 113 | mpbir 221 |
. . . . . . 7
..^ |
115 | 114 | a1i 11 |
. . . . . 6
..^ |
116 | 1 | ad2antrr 762 |
. . . . . . 7
..^
|
117 | | ioossre 12235 |
. . . . . . . . . . 11
|
118 | | ax-resscn 9993 |
. . . . . . . . . . 11
|
119 | 117, 118 | sstri 3612 |
. . . . . . . . . 10
|
120 | 119 | a1i 11 |
. . . . . . . . 9
|
121 | 120 | sselda 3603 |
. . . . . . . 8
|
122 | 121 | adantr 481 |
. . . . . . 7
..^
|
123 | 26 | ad2antrr 762 |
. . . . . . . . 9
..^
Λ Λ Λ
..^ |
124 | | fzo0ss1 12498 |
. . . . . . . . . . 11
..^ ..^ |
125 | 124 | a1i 11 |
. . . . . . . . . 10
..^ ..^ |
126 | 125 | sselda 3603 |
. . . . . . . . 9
..^
..^ |
127 | 123, 126 | ffvelrnd 6360 |
. . . . . . . 8
..^
Λ Λ
Λ
|
128 | 127, 39 | syl 17 |
. . . . . . 7
..^
Λ Λ
Λ
|
129 | 116, 122,
128 | vtscl 30716 |
. . . . . 6
..^
Λ
Λ Λ
vts |
130 | 52, 53 | ax-mp 5 |
. . . . . . . . 9
Λ Λ
Λ
Λ |
131 | 28, 130 | syl6eq 2672 |
. . . . . . . 8
Λ Λ
Λ
Λ
|
132 | 131 | oveq1d 6665 |
. . . . . . 7
Λ
Λ Λ
vts Λ
vts |
133 | 132 | fveq1d 6193 |
. . . . . 6
Λ Λ Λ
vts Λ
vts |
134 | 1 | adantr 481 |
. . . . . . 7
|
135 | 17 | adantr 481 |
. . . . . . 7
Λ |
136 | 134, 121,
135 | vtscl 30716 |
. . . . . 6
Λ
vts |
137 | 104, 105,
107, 108, 115, 129, 133, 136 | fprodsplitsn 14720 |
. . . . 5
..^ Λ Λ Λ
vts ..^Λ Λ Λ
vts Λ
vts |
138 | | uncom 3757 |
. . . . . . . 8
..^ ..^ |
139 | | fzo0sn0fzo1 12557 |
. . . . . . . . 9
..^ ..^ |
140 | 2, 139 | ax-mp 5 |
. . . . . . . 8
..^ ..^ |
141 | 138, 140 | eqtr4i 2647 |
. . . . . . 7
..^ ..^ |
142 | 141 | a1i 11 |
. . . . . 6
..^ ..^ |
143 | 142 | prodeq1d 14651 |
. . . . 5
..^ Λ Λ Λ
vts
..^Λ Λ Λ
vts |
144 | | fzo13pr 12552 |
. . . . . . . . . . . . . . 15
..^ |
145 | 144 | eleq2i 2693 |
. . . . . . . . . . . . . 14
..^ |
146 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
147 | 146 | elpr 4198 |
. . . . . . . . . . . . . 14
|
148 | 145, 147 | bitri 264 |
. . . . . . . . . . . . 13
..^ |
149 | 31 | adantl 482 |
. . . . . . . . . . . . . . 15
Λ Λ
Λ
Λ Λ
Λ
|
150 | 72, 73 | mp1i 13 |
. . . . . . . . . . . . . . 15
Λ Λ
Λ
Λ
|
151 | 149, 150 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Λ Λ
Λ
Λ
|
152 | 34 | adantl 482 |
. . . . . . . . . . . . . . 15
Λ Λ
Λ
Λ Λ
Λ
|
153 | 72, 87 | mp1i 13 |
. . . . . . . . . . . . . . 15
Λ Λ
Λ
Λ
|
154 | 152, 153 | eqtrd 2656 |
. . . . . . . . . . . . . 14
Λ Λ
Λ
Λ
|
155 | 151, 154 | jaodan 826 |
. . . . . . . . . . . . 13
Λ Λ Λ
Λ
|
156 | 148, 155 | sylan2b 492 |
. . . . . . . . . . . 12
..^ Λ Λ Λ
Λ
|
157 | 156 | adantlr 751 |
. . . . . . . . . . 11
..^
Λ Λ
Λ
Λ |
158 | 157 | oveq1d 6665 |
. . . . . . . . . 10
..^
Λ Λ
Λ
vts Λ
vts |
159 | 158 | fveq1d 6193 |
. . . . . . . . 9
..^
Λ
Λ Λ
vts Λ
vts |
160 | 159 | prodeq2dv 14653 |
. . . . . . . 8
..^Λ Λ
Λ
vts
..^Λ vts |
161 | 22 | adantr 481 |
. . . . . . . . . 10
Λ |
162 | 134, 121,
161 | vtscl 30716 |
. . . . . . . . 9
Λ
vts |
163 | | fprodconst 14708 |
. . . . . . . . 9
..^ Λ
vts ..^Λ
vts Λ
vts..^ |
164 | 107, 162,
163 | syl2anc 693 |
. . . . . . . 8
..^Λ
vts Λ
vts..^ |
165 | | nnuz 11723 |
. . . . . . . . . . . . 13
|
166 | 2, 165 | eleqtri 2699 |
. . . . . . . . . . . 12
|
167 | | hashfzo 13216 |
. . . . . . . . . . . 12
..^ |
168 | 166, 167 | ax-mp 5 |
. . . . . . . . . . 11
..^ |
169 | | 3m1e2 11137 |
. . . . . . . . . . 11
|
170 | 168, 169 | eqtri 2644 |
. . . . . . . . . 10
..^ |
171 | 170 | a1i 11 |
. . . . . . . . 9
..^ |
172 | 171 | oveq2d 6666 |
. . . . . . . 8
Λ
vts..^ Λ
vts |
173 | 160, 164,
172 | 3eqtrd 2660 |
. . . . . . 7
..^Λ Λ
Λ
vts Λ
vts |
174 | 173 | oveq1d 6665 |
. . . . . 6
..^Λ Λ Λ
vts Λ
vts Λ
vts Λ vts |
175 | 162 | sqcld 13006 |
. . . . . . 7
Λ
vts |
176 | 136, 175 | mulcomd 10061 |
. . . . . 6
Λ
vts Λ vts Λ vts Λ
vts |
177 | 174, 176 | eqtr4d 2659 |
. . . . 5
..^Λ Λ Λ
vts Λ
vts Λ
vts Λ vts |
178 | 137, 143,
177 | 3eqtr3d 2664 |
. . . 4
..^Λ Λ
Λ
vts Λ
vts Λ
vts |
179 | 178 | oveq1d 6665 |
. . 3
..^Λ Λ Λ
vts
Λ vts Λ
vts |
180 | 179 | itgeq2dv 23548 |
. 2
..^Λ Λ Λ
vts
Λ vts Λ
vts |
181 | 27, 103, 180 | 3eqtr3d 2664 |
1
reprΛ Λ Λ Λ vts Λ
vts |