Step | Hyp | Ref
| Expression |
1 | | 3simpb 1059 |
. . . . . . . 8
|
2 | | nfcv 2764 |
. . . . . . . . . . . 12
|
3 | | nfv 1843 |
. . . . . . . . . . . . 13
|
4 | | nfcsb1v 3549 |
. . . . . . . . . . . . 13
|
5 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
6 | 3, 4, 5 | nfif 4115 |
. . . . . . . . . . . 12
|
7 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
8 | | csbeq1a 3542 |
. . . . . . . . . . . . 13
|
9 | 7, 8 | ifbieq1d 4109 |
. . . . . . . . . . . 12
|
10 | 2, 6, 9 | cbvmpt 4749 |
. . . . . . . . . . 11
|
11 | | simpll 790 |
. . . . . . . . . . . 12
|
12 | | zprod.6 |
. . . . . . . . . . . . . 14
|
13 | 12 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
14 | 4 | nfel1 2779 |
. . . . . . . . . . . . . 14
|
15 | 8 | eleq1d 2686 |
. . . . . . . . . . . . . 14
|
16 | 14, 15 | rspc 3303 |
. . . . . . . . . . . . 13
|
17 | 13, 16 | syl5 34 |
. . . . . . . . . . . 12
|
18 | 11, 17 | mpan9 486 |
. . . . . . . . . . 11
|
19 | | simplr 792 |
. . . . . . . . . . 11
|
20 | | zprod.2 |
. . . . . . . . . . . 12
|
21 | 20 | ad2antrr 762 |
. . . . . . . . . . 11
|
22 | | simpr 477 |
. . . . . . . . . . 11
|
23 | | zprod.4 |
. . . . . . . . . . . . 13
|
24 | | zprod.1 |
. . . . . . . . . . . . 13
|
25 | 23, 24 | syl6sseq 3651 |
. . . . . . . . . . . 12
|
26 | 25 | ad2antrr 762 |
. . . . . . . . . . 11
|
27 | 10, 18, 19, 21, 22, 26 | prodrb 14662 |
. . . . . . . . . 10
|
28 | 27 | biimpd 219 |
. . . . . . . . 9
|
29 | 28 | expimpd 629 |
. . . . . . . 8
|
30 | 1, 29 | syl5 34 |
. . . . . . 7
|
31 | 30 | rexlimdva 3031 |
. . . . . 6
|
32 | | uzssz 11707 |
. . . . . . . . . . . . . . . . 17
|
33 | | zssre 11384 |
. . . . . . . . . . . . . . . . 17
|
34 | 32, 33 | sstri 3612 |
. . . . . . . . . . . . . . . 16
|
35 | 24, 34 | eqsstri 3635 |
. . . . . . . . . . . . . . 15
|
36 | 23, 35 | syl6ss 3615 |
. . . . . . . . . . . . . 14
|
37 | 36 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
38 | | ltso 10118 |
. . . . . . . . . . . . 13
|
39 | | soss 5053 |
. . . . . . . . . . . . 13
|
40 | 37, 38, 39 | mpisyl 21 |
. . . . . . . . . . . 12
|
41 | | fzfi 12771 |
. . . . . . . . . . . . 13
|
42 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
43 | 42 | f1oen 7976 |
. . . . . . . . . . . . . . 15
|
44 | 43 | adantl 482 |
. . . . . . . . . . . . . 14
|
45 | 44 | ensymd 8007 |
. . . . . . . . . . . . 13
|
46 | | enfii 8177 |
. . . . . . . . . . . . 13
|
47 | 41, 45, 46 | sylancr 695 |
. . . . . . . . . . . 12
|
48 | | fz1iso 13246 |
. . . . . . . . . . . 12
|
49 | 40, 47, 48 | syl2anc 693 |
. . . . . . . . . . 11
|
50 | | simpll 790 |
. . . . . . . . . . . . . . 15
|
51 | 50, 17 | mpan9 486 |
. . . . . . . . . . . . . 14
|
52 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
53 | 52 | csbeq1d 3540 |
. . . . . . . . . . . . . . . 16
|
54 | | csbco 3543 |
. . . . . . . . . . . . . . . 16
|
55 | 53, 54 | syl6eqr 2674 |
. . . . . . . . . . . . . . 15
|
56 | 55 | cbvmptv 4750 |
. . . . . . . . . . . . . 14
|
57 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
58 | | simplr 792 |
. . . . . . . . . . . . . 14
|
59 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
60 | 25 | ad2antrr 762 |
. . . . . . . . . . . . . 14
|
61 | | simprl 794 |
. . . . . . . . . . . . . 14
|
62 | | simprr 796 |
. . . . . . . . . . . . . 14
|
63 | 10, 51, 56, 57, 58, 59, 60, 61, 62 | prodmolem2a 14664 |
. . . . . . . . . . . . 13
|
64 | 63 | expr 643 |
. . . . . . . . . . . 12
|
65 | 64 | exlimdv 1861 |
. . . . . . . . . . 11
|
66 | 49, 65 | mpd 15 |
. . . . . . . . . 10
|
67 | | breq2 4657 |
. . . . . . . . . 10
|
68 | 66, 67 | syl5ibrcom 237 |
. . . . . . . . 9
|
69 | 68 | expimpd 629 |
. . . . . . . 8
|
70 | 69 | exlimdv 1861 |
. . . . . . 7
|
71 | 70 | rexlimdva 3031 |
. . . . . 6
|
72 | 31, 71 | jaod 395 |
. . . . 5
|
73 | 20 | adantr 481 |
. . . . . . . 8
|
74 | 23 | adantr 481 |
. . . . . . . 8
|
75 | | zprod.3 |
. . . . . . . . . 10
|
76 | 24 | eleq2i 2693 |
. . . . . . . . . . . 12
|
77 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
79 | | uztrn 11704 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 79 | ancoms 469 |
. . . . . . . . . . . . . . . . . 18
|
81 | 24 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | | zprod.5 |
. . . . . . . . . . . . . . . . . . . . . 22
|
83 | 24, 32 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
84 | 83 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
85 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
86 | 85 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
87 | 86, 12 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
88 | 87 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
89 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
90 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
91 | 89, 90 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
92 | 88, 91 | pm2.61d1 171 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
93 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
94 | 93 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
95 | 84, 92, 94 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . 22
|
96 | 82, 95 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 81, 96 | sylan2br 493 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 97 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . 19
|
99 | | nffvmpt1 6199 |
. . . . . . . . . . . . . . . . . . . . 21
|
100 | 99 | nfeq2 2780 |
. . . . . . . . . . . . . . . . . . . 20
|
101 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
102 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | 101, 102 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | 100, 103 | rspc 3303 |
. . . . . . . . . . . . . . . . . . 19
|
105 | 98, 104 | mpan9 486 |
. . . . . . . . . . . . . . . . . 18
|
106 | 80, 105 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
|
107 | 106 | anassrs 680 |
. . . . . . . . . . . . . . . 16
|
108 | 78, 107 | seqfeq 12826 |
. . . . . . . . . . . . . . 15
|
109 | 108 | breq1d 4663 |
. . . . . . . . . . . . . 14
|
110 | 109 | anbi2d 740 |
. . . . . . . . . . . . 13
|
111 | 110 | exbidv 1850 |
. . . . . . . . . . . 12
|
112 | 76, 111 | sylan2b 492 |
. . . . . . . . . . 11
|
113 | 112 | rexbidva 3049 |
. . . . . . . . . 10
|
114 | 75, 113 | mpbid 222 |
. . . . . . . . 9
|
115 | 114 | adantr 481 |
. . . . . . . 8
|
116 | | simpr 477 |
. . . . . . . 8
|
117 | | fveq2 6191 |
. . . . . . . . . . . 12
|
118 | 117, 24 | syl6eqr 2674 |
. . . . . . . . . . 11
|
119 | 118 | sseq2d 3633 |
. . . . . . . . . 10
|
120 | 118 | rexeqdv 3145 |
. . . . . . . . . 10
|
121 | | seqeq1 12804 |
. . . . . . . . . . 11
|
122 | 121 | breq1d 4663 |
. . . . . . . . . 10
|
123 | 119, 120,
122 | 3anbi123d 1399 |
. . . . . . . . 9
|
124 | 123 | rspcev 3309 |
. . . . . . . 8
|
125 | 73, 74, 115, 116, 124 | syl13anc 1328 |
. . . . . . 7
|
126 | 125 | orcd 407 |
. . . . . 6
|
127 | 126 | ex 450 |
. . . . 5
|
128 | 72, 127 | impbid 202 |
. . . 4
|
129 | 95, 82 | eqtr4d 2659 |
. . . . . . . . 9
|
130 | 81, 129 | sylan2br 493 |
. . . . . . . 8
|
131 | 130 | ralrimiva 2966 |
. . . . . . 7
|
132 | 99 | nfeq1 2778 |
. . . . . . . 8
|
133 | 102, 101 | eqeq12d 2637 |
. . . . . . . 8
|
134 | 132, 133 | rspc 3303 |
. . . . . . 7
|
135 | 131, 134 | mpan9 486 |
. . . . . 6
|
136 | 20, 135 | seqfeq 12826 |
. . . . 5
|
137 | 136 | breq1d 4663 |
. . . 4
|
138 | 128, 137 | bitrd 268 |
. . 3
|
139 | 138 | iotabidv 5872 |
. 2
|
140 | | df-prod 14636 |
. 2
|
141 | | df-fv 5896 |
. 2
|
142 | 139, 140,
141 | 3eqtr4g 2681 |
1
|