Step | Hyp | Ref
| Expression |
1 | | 1t1e1 9030 |
. . . . 5
|
2 | | prod0 11548 |
. . . . . 6
|
3 | | prod0 11548 |
. . . . . 6
|
4 | 2, 3 | oveq12i 5865 |
. . . . 5
|
5 | | prod0 11548 |
. . . . 5
|
6 | 1, 4, 5 | 3eqtr4ri 2202 |
. . . 4
|
7 | | prodeq1 11516 |
. . . 4
|
8 | | prodeq1 11516 |
. . . . 5
|
9 | | prodeq1 11516 |
. . . . 5
|
10 | 8, 9 | oveq12d 5871 |
. . . 4
|
11 | 6, 7, 10 | 3eqtr4a 2229 |
. . 3
|
12 | 11 | a1i 9 |
. 2
|
13 | | simprl 526 |
. . . . . . . . 9
♯ ♯ ♯ |
14 | | nnuz 9522 |
. . . . . . . . 9
|
15 | 13, 14 | eleqtrdi 2263 |
. . . . . . . 8
♯ ♯ ♯ |
16 | | elnnuz 9523 |
. . . . . . . . . . . 12
|
17 | 16 | biimpri 132 |
. . . . . . . . . . 11
|
18 | 17 | adantl 275 |
. . . . . . . . . 10
♯ ♯
|
19 | | fprodmul.2 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | fmpttd 5651 |
. . . . . . . . . . . . . . 15
|
21 | 20 | adantr 274 |
. . . . . . . . . . . . . 14
♯ ♯ |
22 | | f1of 5442 |
. . . . . . . . . . . . . . 15
♯ ♯ |
23 | 22 | ad2antll 488 |
. . . . . . . . . . . . . 14
♯ ♯ ♯ |
24 | | fco 5363 |
. . . . . . . . . . . . . 14
♯ ♯ |
25 | 21, 23, 24 | syl2anc 409 |
. . . . . . . . . . . . 13
♯ ♯ ♯ |
26 | 25 | ad2antrr 485 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
27 | | simpr 109 |
. . . . . . . . . . . . 13
♯ ♯
♯ ♯ |
28 | | simplr 525 |
. . . . . . . . . . . . . 14
♯ ♯
♯
|
29 | 13 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
♯ ♯
♯ ♯ |
30 | 29 | nnzd 9333 |
. . . . . . . . . . . . . 14
♯ ♯
♯ ♯ |
31 | | elfz5 9973 |
. . . . . . . . . . . . . 14
♯ ♯
♯ |
32 | 28, 30, 31 | syl2anc 409 |
. . . . . . . . . . . . 13
♯ ♯
♯ ♯
♯ |
33 | 27, 32 | mpbird 166 |
. . . . . . . . . . . 12
♯ ♯
♯
♯ |
34 | 26, 33 | ffvelrnd 5632 |
. . . . . . . . . . 11
♯ ♯
♯ |
35 | | 1cnd 7936 |
. . . . . . . . . . 11
♯ ♯
♯
|
36 | 18 | nnzd 9333 |
. . . . . . . . . . . 12
♯ ♯
|
37 | 13 | adantr 274 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
38 | 37 | nnzd 9333 |
. . . . . . . . . . . 12
♯ ♯
♯ |
39 | | zdcle 9288 |
. . . . . . . . . . . 12
♯
DECID
♯ |
40 | 36, 38, 39 | syl2anc 409 |
. . . . . . . . . . 11
♯ ♯
DECID
♯ |
41 | 34, 35, 40 | ifcldadc 3555 |
. . . . . . . . . 10
♯ ♯
♯ |
42 | | breq1 3992 |
. . . . . . . . . . . 12
♯
♯ |
43 | | fveq2 5496 |
. . . . . . . . . . . 12
|
44 | 42, 43 | ifbieq1d 3548 |
. . . . . . . . . . 11
♯ ♯ |
45 | | eqid 2170 |
. . . . . . . . . . 11
♯ ♯ |
46 | 44, 45 | fvmptg 5572 |
. . . . . . . . . 10
♯ ♯ ♯ |
47 | 18, 41, 46 | syl2anc 409 |
. . . . . . . . 9
♯ ♯
♯ ♯ |
48 | 47, 41 | eqeltrd 2247 |
. . . . . . . 8
♯ ♯
♯ |
49 | | fprodmul.3 |
. . . . . . . . . . . . . . . 16
|
50 | 49 | fmpttd 5651 |
. . . . . . . . . . . . . . 15
|
51 | 50 | adantr 274 |
. . . . . . . . . . . . . 14
♯ ♯ |
52 | | fco 5363 |
. . . . . . . . . . . . . 14
♯ ♯ |
53 | 51, 23, 52 | syl2anc 409 |
. . . . . . . . . . . . 13
♯ ♯ ♯ |
54 | 53 | ad2antrr 485 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
55 | 54, 33 | ffvelrnd 5632 |
. . . . . . . . . . 11
♯ ♯
♯ |
56 | 55, 35, 40 | ifcldadc 3555 |
. . . . . . . . . 10
♯ ♯
♯ |
57 | | fveq2 5496 |
. . . . . . . . . . . 12
|
58 | 42, 57 | ifbieq1d 3548 |
. . . . . . . . . . 11
♯ ♯ |
59 | | eqid 2170 |
. . . . . . . . . . 11
♯ ♯ |
60 | 58, 59 | fvmptg 5572 |
. . . . . . . . . 10
♯ ♯ ♯ |
61 | 18, 56, 60 | syl2anc 409 |
. . . . . . . . 9
♯ ♯
♯ ♯ |
62 | 61, 56 | eqeltrd 2247 |
. . . . . . . 8
♯ ♯
♯ |
63 | 23 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
♯ ♯
♯ ♯ |
64 | 63, 33 | ffvelrnd 5632 |
. . . . . . . . . . . . . 14
♯ ♯
♯ |
65 | | csbov12g 5892 |
. . . . . . . . . . . . . 14
|
66 | 64, 65 | syl 14 |
. . . . . . . . . . . . 13
♯ ♯
♯
|
67 | 19, 49 | mulcld 7940 |
. . . . . . . . . . . . . . . . 17
|
68 | 67 | ralrimiva 2543 |
. . . . . . . . . . . . . . . 16
|
69 | 68 | ad3antrrr 489 |
. . . . . . . . . . . . . . 15
♯ ♯
♯
|
70 | | nfcsb1v 3082 |
. . . . . . . . . . . . . . . . 17
|
71 | 70 | nfel1 2323 |
. . . . . . . . . . . . . . . 16
|
72 | | csbeq1a 3058 |
. . . . . . . . . . . . . . . . 17
|
73 | 72 | eleq1d 2239 |
. . . . . . . . . . . . . . . 16
|
74 | 71, 73 | rspc 2828 |
. . . . . . . . . . . . . . 15
|
75 | 64, 69, 74 | sylc 62 |
. . . . . . . . . . . . . 14
♯ ♯
♯
|
76 | | eqid 2170 |
. . . . . . . . . . . . . . 15
|
77 | 76 | fvmpts 5574 |
. . . . . . . . . . . . . 14
|
78 | 64, 75, 77 | syl2anc 409 |
. . . . . . . . . . . . 13
♯ ♯
♯
|
79 | 19 | ralrimiva 2543 |
. . . . . . . . . . . . . . . . 17
|
80 | 79 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
♯ ♯
♯
|
81 | | nfcsb1v 3082 |
. . . . . . . . . . . . . . . . . 18
|
82 | 81 | nfel1 2323 |
. . . . . . . . . . . . . . . . 17
|
83 | | csbeq1a 3058 |
. . . . . . . . . . . . . . . . . 18
|
84 | 83 | eleq1d 2239 |
. . . . . . . . . . . . . . . . 17
|
85 | 82, 84 | rspc 2828 |
. . . . . . . . . . . . . . . 16
|
86 | 64, 80, 85 | sylc 62 |
. . . . . . . . . . . . . . 15
♯ ♯
♯
|
87 | | eqid 2170 |
. . . . . . . . . . . . . . . 16
|
88 | 87 | fvmpts 5574 |
. . . . . . . . . . . . . . 15
|
89 | 64, 86, 88 | syl2anc 409 |
. . . . . . . . . . . . . 14
♯ ♯
♯ |
90 | 49 | ralrimiva 2543 |
. . . . . . . . . . . . . . . . 17
|
91 | 90 | ad3antrrr 489 |
. . . . . . . . . . . . . . . 16
♯ ♯
♯
|
92 | | nfcsb1v 3082 |
. . . . . . . . . . . . . . . . . 18
|
93 | 92 | nfel1 2323 |
. . . . . . . . . . . . . . . . 17
|
94 | | csbeq1a 3058 |
. . . . . . . . . . . . . . . . . 18
|
95 | 94 | eleq1d 2239 |
. . . . . . . . . . . . . . . . 17
|
96 | 93, 95 | rspc 2828 |
. . . . . . . . . . . . . . . 16
|
97 | 64, 91, 96 | sylc 62 |
. . . . . . . . . . . . . . 15
♯ ♯
♯
|
98 | | eqid 2170 |
. . . . . . . . . . . . . . . 16
|
99 | 98 | fvmpts 5574 |
. . . . . . . . . . . . . . 15
|
100 | 64, 97, 99 | syl2anc 409 |
. . . . . . . . . . . . . 14
♯ ♯
♯ |
101 | 89, 100 | oveq12d 5871 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
102 | 66, 78, 101 | 3eqtr4d 2213 |
. . . . . . . . . . . 12
♯ ♯
♯ |
103 | | fvco3 5567 |
. . . . . . . . . . . . 13
♯
♯ |
104 | 63, 33, 103 | syl2anc 409 |
. . . . . . . . . . . 12
♯ ♯
♯ |
105 | | fvco3 5567 |
. . . . . . . . . . . . . 14
♯
♯ |
106 | 63, 33, 105 | syl2anc 409 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
107 | | fvco3 5567 |
. . . . . . . . . . . . . 14
♯
♯ |
108 | 63, 33, 107 | syl2anc 409 |
. . . . . . . . . . . . 13
♯ ♯
♯ |
109 | 106, 108 | oveq12d 5871 |
. . . . . . . . . . . 12
♯ ♯
♯ |
110 | 102, 104,
109 | 3eqtr4d 2213 |
. . . . . . . . . . 11
♯ ♯
♯ |
111 | 27 | iftrued 3533 |
. . . . . . . . . . 11
♯ ♯
♯ ♯ |
112 | 27 | iftrued 3533 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
113 | 27 | iftrued 3533 |
. . . . . . . . . . . 12
♯ ♯
♯ ♯ |
114 | 112, 113 | oveq12d 5871 |
. . . . . . . . . . 11
♯ ♯
♯ ♯
♯ |
115 | 110, 111,
114 | 3eqtr4d 2213 |
. . . . . . . . . 10
♯ ♯
♯ ♯
♯ ♯ |
116 | 1 | eqcomi 2174 |
. . . . . . . . . . 11
|
117 | | simpr 109 |
. . . . . . . . . . . 12
♯ ♯
♯
♯ |
118 | 117 | iffalsed 3536 |
. . . . . . . . . . 11
♯ ♯
♯
♯ |
119 | 117 | iffalsed 3536 |
. . . . . . . . . . . 12
♯ ♯
♯
♯ |
120 | 117 | iffalsed 3536 |
. . . . . . . . . . . 12
♯ ♯
♯
♯ |
121 | 119, 120 | oveq12d 5871 |
. . . . . . . . . . 11
♯ ♯
♯
♯ ♯ |
122 | 116, 118,
121 | 3eqtr4a 2229 |
. . . . . . . . . 10
♯ ♯
♯
♯ ♯
♯ |
123 | | exmiddc 831 |
. . . . . . . . . . 11
DECID ♯ ♯ ♯ |
124 | 40, 123 | syl 14 |
. . . . . . . . . 10
♯ ♯
♯ ♯ |
125 | 115, 122,
124 | mpjaodan 793 |
. . . . . . . . 9
♯ ♯
♯ ♯
♯ |
126 | 78, 75 | eqeltrd 2247 |
. . . . . . . . . . . 12
♯ ♯
♯ |
127 | 104, 126 | eqeltrd 2247 |
. . . . . . . . . . 11
♯ ♯
♯ |
128 | 127, 35, 40 | ifcldadc 3555 |
. . . . . . . . . 10
♯ ♯
♯ |
129 | | fveq2 5496 |
. . . . . . . . . . . 12
|
130 | 42, 129 | ifbieq1d 3548 |
. . . . . . . . . . 11
♯ ♯ |
131 | | eqid 2170 |
. . . . . . . . . . 11
♯ ♯ |
132 | 130, 131 | fvmptg 5572 |
. . . . . . . . . 10
♯ ♯ ♯ |
133 | 18, 128, 132 | syl2anc 409 |
. . . . . . . . 9
♯ ♯
♯ ♯ |
134 | 47, 61 | oveq12d 5871 |
. . . . . . . . 9
♯ ♯
♯
♯
♯ ♯ |
135 | 125, 133,
134 | 3eqtr4d 2213 |
. . . . . . . 8
♯ ♯
♯ ♯
♯ |
136 | 15, 48, 62, 135 | prod3fmul 11504 |
. . . . . . 7
♯ ♯ ♯ ♯
♯ ♯ ♯ ♯ |
137 | | fveq2 5496 |
. . . . . . . 8
|
138 | | simprr 527 |
. . . . . . . 8
♯ ♯ ♯ |
139 | 67 | fmpttd 5651 |
. . . . . . . . . 10
|
140 | 139 | adantr 274 |
. . . . . . . . 9
♯ ♯ |
141 | 140 | ffvelrnda 5631 |
. . . . . . . 8
♯ ♯ |
142 | | fvco3 5567 |
. . . . . . . . 9
♯
♯ |
143 | 23, 142 | sylan 281 |
. . . . . . . 8
♯ ♯ ♯ |
144 | 137, 13, 138, 141, 143 | fprodseq 11546 |
. . . . . . 7
♯ ♯ ♯ ♯ |
145 | | fveq2 5496 |
. . . . . . . . 9
|
146 | 21 | ffvelrnda 5631 |
. . . . . . . . 9
♯ ♯ |
147 | | fvco3 5567 |
. . . . . . . . . 10
♯
♯ |
148 | 23, 147 | sylan 281 |
. . . . . . . . 9
♯ ♯ ♯ |
149 | 145, 13, 138, 146, 148 | fprodseq 11546 |
. . . . . . . 8
♯ ♯ ♯ ♯ |
150 | | fveq2 5496 |
. . . . . . . . 9
|
151 | 51 | ffvelrnda 5631 |
. . . . . . . . 9
♯ ♯ |
152 | | fvco3 5567 |
. . . . . . . . . 10
♯
♯ |
153 | 23, 152 | sylan 281 |
. . . . . . . . 9
♯ ♯ ♯ |
154 | 150, 13, 138, 151, 153 | fprodseq 11546 |
. . . . . . . 8
♯ ♯ ♯ ♯ |
155 | 149, 154 | oveq12d 5871 |
. . . . . . 7
♯ ♯ ♯ ♯ ♯ ♯ |
156 | 136, 144,
155 | 3eqtr4d 2213 |
. . . . . 6
♯ ♯
|
157 | | prodfct 11550 |
. . . . . . . 8
|
158 | 68, 157 | syl 14 |
. . . . . . 7
|
159 | 158 | adantr 274 |
. . . . . 6
♯ ♯
|
160 | | prodfct 11550 |
. . . . . . . . 9
|
161 | 79, 160 | syl 14 |
. . . . . . . 8
|
162 | | prodfct 11550 |
. . . . . . . . 9
|
163 | 90, 162 | syl 14 |
. . . . . . . 8
|
164 | 161, 163 | oveq12d 5871 |
. . . . . . 7
|
165 | 164 | adantr 274 |
. . . . . 6
♯ ♯ |
166 | 156, 159,
165 | 3eqtr3d 2211 |
. . . . 5
♯ ♯
|
167 | 166 | expr 373 |
. . . 4
♯ ♯
|
168 | 167 | exlimdv 1812 |
. . 3
♯ ♯
|
169 | 168 | expimpd 361 |
. 2
♯ ♯
|
170 | | fprodmul.1 |
. . 3
|
171 | | fz1f1o 11338 |
. . 3
♯ ♯ |
172 | 170, 171 | syl 14 |
. 2
♯ ♯ |
173 | 12, 169, 172 | mpjaod 713 |
1
|