Step | Hyp | Ref
| Expression |
1 | | blocni.u |
. . . . . 6
|
2 | | blocnilem.1 |
. . . . . . 7
|
3 | | blocni.8 |
. . . . . . 7
|
4 | 2, 3 | imsxmet 27547 |
. . . . . 6
|
5 | 1, 4 | ax-mp 5 |
. . . . 5
|
6 | | blocni.w |
. . . . . 6
|
7 | | eqid 2622 |
. . . . . . 7
|
8 | | blocni.d |
. . . . . . 7
|
9 | 7, 8 | imsxmet 27547 |
. . . . . 6
|
10 | 6, 9 | ax-mp 5 |
. . . . 5
|
11 | | 1rp 11836 |
. . . . . 6
|
12 | | blocni.j |
. . . . . . 7
|
13 | | blocni.k |
. . . . . . 7
|
14 | 12, 13 | metcnpi3 22351 |
. . . . . 6
|
15 | 11, 14 | mpanr2 720 |
. . . . 5
|
16 | 5, 10, 15 | mpanl12 718 |
. . . 4
|
17 | | rpreccl 11857 |
. . . . . . . . 9
|
18 | 17 | rpred 11872 |
. . . . . . . 8
|
19 | 18 | ad2antlr 763 |
. . . . . . 7
|
20 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
21 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
CV CV |
22 | 2, 20, 21, 3 | imsdval 27541 |
. . . . . . . . . . . . . . 15
CV |
23 | 1, 22 | mp3an1 1411 |
. . . . . . . . . . . . . 14
CV |
24 | 23 | breq1d 4663 |
. . . . . . . . . . . . 13
CV |
25 | | blocni.l |
. . . . . . . . . . . . . . . . . 18
|
26 | | blocni.4 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 2, 7, 26 | lnof 27610 |
. . . . . . . . . . . . . . . . . 18
|
28 | 1, 6, 25, 27 | mp3an 1424 |
. . . . . . . . . . . . . . . . 17
|
29 | 28 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
|
30 | 28 | ffvelrni 6358 |
. . . . . . . . . . . . . . . 16
|
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
32 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
CV CV |
33 | 7, 31, 32, 8 | imsdval 27541 |
. . . . . . . . . . . . . . . . 17
CV |
34 | 6, 33 | mp3an1 1411 |
. . . . . . . . . . . . . . . 16
CV |
35 | 29, 30, 34 | syl2an 494 |
. . . . . . . . . . . . . . 15
CV |
36 | 1, 6, 25 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . 17
|
37 | 2, 20, 31, 26 | lnosub 27614 |
. . . . . . . . . . . . . . . . 17
|
38 | 36, 37 | mpan 706 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
CV CV |
40 | 35, 39 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
CV |
41 | 40 | breq1d 4663 |
. . . . . . . . . . . . 13
CV
|
42 | 24, 41 | imbi12d 334 |
. . . . . . . . . . . 12
CV CV |
43 | 42 | ancoms 469 |
. . . . . . . . . . 11
CV CV |
44 | 43 | adantlr 751 |
. . . . . . . . . 10
CV CV |
45 | 44 | ralbidva 2985 |
. . . . . . . . 9
CV CV |
46 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
47 | 46 | fveq2d 6195 |
. . . . . . . . . . . . 13
CV CV |
48 | | fveq2 6191 |
. . . . . . . . . . . . . 14
CV CV |
49 | 48 | oveq2d 6666 |
. . . . . . . . . . . . 13
CV CV |
50 | 47, 49 | breq12d 4666 |
. . . . . . . . . . . 12
CV
CV
CV CV |
51 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
54 | 2, 21 | nvcl 27516 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
CV |
55 | 1, 54 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
CV |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
CV |
57 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
58 | 2, 57, 21 | nvgt0 27529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
CV |
59 | 1, 58 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
CV |
60 | 59 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
CV |
61 | 56, 60 | elrpd 11869 |
. . . . . . . . . . . . . . . . . . . . . . . 24
CV |
62 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
CV CV |
63 | 53, 61, 62 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . 23
CV |
64 | 63 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . . 22
CV |
65 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | 2, 66 | nvscl 27481 |
. . . . . . . . . . . . . . . . . . . . . 22
CV CV |
68 | 51, 64, 65, 67 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . 21
CV |
69 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | 2, 69, 20 | nvpncan2 27508 |
. . . . . . . . . . . . . . . . . . . . 21
CV CV CV |
71 | 51, 52, 68, 70 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
CV CV |
72 | 71 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
CV CV CV CV |
73 | 63 | rprege0d 11879 |
. . . . . . . . . . . . . . . . . . . 20
CV CV |
74 | 2, 66, 21 | nvsge0 27519 |
. . . . . . . . . . . . . . . . . . . 20
CV CV
CV CV CV CV |
75 | 51, 73, 65, 74 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
CV CV CV CV |
76 | | rpcn 11841 |
. . . . . . . . . . . . . . . . . . . . 21
|
77 | 76 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
78 | 55 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . 21
CV |
79 | 78 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
CV |
80 | 2, 57, 21 | nvz 27524 |
. . . . . . . . . . . . . . . . . . . . . . . 24
CV
|
81 | 1, 80 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . 23
CV
|
82 | 81 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . . . 22
CV
|
83 | 82 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . 21
CV |
84 | 83 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
CV |
85 | 77, 79, 84 | divcan1d 10802 |
. . . . . . . . . . . . . . . . . . 19
CV CV |
86 | 72, 75, 85 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . 18
CV CV |
87 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 87 | leidd 10594 |
. . . . . . . . . . . . . . . . . . 19
|
89 | 88 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . 18
|
90 | 86, 89 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
CV CV |
91 | 2, 69 | nvgcl 27475 |
. . . . . . . . . . . . . . . . . . 19
CV CV |
92 | 51, 52, 68, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
CV |
93 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
CV
CV |
94 | 93 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
CV
CV CV CV |
95 | 94 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
CV
CV CV CV
|
96 | 93 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . 22
CV
CV |
97 | 96 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
CV
CV CV CV |
98 | 97 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . 20
CV
CV
CV CV
|
99 | 95, 98 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . 19
CV
CV CV
CV CV CV CV
|
100 | 99 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
CV
CV
CV
CV CV
CV CV
|
101 | 92, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
CV CV
CV CV
CV CV
|
102 | 90, 101 | mpid 44 |
. . . . . . . . . . . . . . . 16
CV CV
CV CV
|
103 | 28 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . . . . 20
|
104 | 7, 32 | nvcl 27516 |
. . . . . . . . . . . . . . . . . . . 20
CV |
105 | 6, 103, 104 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
CV |
106 | 105 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
CV |
107 | | 1red 10055 |
. . . . . . . . . . . . . . . . . 18
|
108 | 106, 107,
63 | lemuldiv2d 11922 |
. . . . . . . . . . . . . . . . 17
CV CV
CV
CV |
109 | 71 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
CV CV |
110 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
111 | 2, 66, 110, 26 | lnomul 27615 |
. . . . . . . . . . . . . . . . . . . . . . 23
CV CV CV |
112 | 36, 111 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . 22
CV CV CV |
113 | 64, 65, 112 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
CV CV |
114 | 109, 113 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
CV CV |
115 | 114 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
CV CV CV CV |
116 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
|
117 | 103 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . 20
|
118 | 7, 110, 32 | nvsge0 27519 |
. . . . . . . . . . . . . . . . . . . 20
CV CV CV CV CV CV |
119 | 116, 73, 117, 118 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . 19
CV CV CV CV |
120 | 115, 119 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
CV CV CV CV |
121 | 120 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
CV CV
CV CV |
122 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . . . . . . 21
|
123 | | rpcnne0 11850 |
. . . . . . . . . . . . . . . . . . . . 21
CV CV CV |
124 | | recdiv 10731 |
. . . . . . . . . . . . . . . . . . . . 21
CV CV CV CV |
125 | 122, 123,
124 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
CV CV CV |
126 | 53, 61, 125 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
CV CV |
127 | | rpne0 11848 |
. . . . . . . . . . . . . . . . . . . . 21
|
128 | 127 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | 79, 77, 128 | divrec2d 10805 |
. . . . . . . . . . . . . . . . . . 19
CV CV |
130 | 126, 129 | eqtr2d 2657 |
. . . . . . . . . . . . . . . . . 18
CV CV |
131 | 130 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
CV
CV
CV
CV |
132 | 108, 121,
131 | 3bitr4d 300 |
. . . . . . . . . . . . . . . 16
CV CV
CV
CV |
133 | 102, 132 | sylibd 229 |
. . . . . . . . . . . . . . 15
CV CV
CV
CV |
134 | 133 | anassrs 680 |
. . . . . . . . . . . . . 14
CV
CV
CV
CV |
135 | 134 | imp 445 |
. . . . . . . . . . . . 13
CV CV
CV
CV |
136 | 135 | an32s 846 |
. . . . . . . . . . . 12
CV CV
CV
CV |
137 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
|
138 | 2, 7, 57, 137, 26 | lno0 27611 |
. . . . . . . . . . . . . . . . . 18
|
139 | 1, 6, 25, 138 | mp3an 1424 |
. . . . . . . . . . . . . . . . 17
|
140 | 139 | fveq2i 6194 |
. . . . . . . . . . . . . . . 16
CV CV |
141 | 137, 32 | nvz0 27523 |
. . . . . . . . . . . . . . . . 17
CV |
142 | 6, 141 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
CV |
143 | 140, 142 | eqtri 2644 |
. . . . . . . . . . . . . . 15
CV |
144 | | 0le0 11110 |
. . . . . . . . . . . . . . 15
|
145 | 143, 144 | eqbrtri 4674 |
. . . . . . . . . . . . . 14
CV |
146 | 17 | rpcnd 11874 |
. . . . . . . . . . . . . . 15
|
147 | 57, 21 | nvz0 27523 |
. . . . . . . . . . . . . . . . . 18
CV |
148 | 1, 147 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
CV |
149 | 148 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
CV |
150 | | mul01 10215 |
. . . . . . . . . . . . . . . 16
|
151 | 149, 150 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
CV |
152 | 146, 151 | syl 17 |
. . . . . . . . . . . . . 14
CV |
153 | 145, 152 | syl5breqr 4691 |
. . . . . . . . . . . . 13
CV CV |
154 | 153 | ad3antlr 767 |
. . . . . . . . . . . 12
CV CV
CV CV |
155 | 50, 136, 154 | pm2.61ne 2879 |
. . . . . . . . . . 11
CV CV
CV
CV |
156 | 155 | ex 450 |
. . . . . . . . . 10
CV CV
CV
CV |
157 | 156 | ralrimdva 2969 |
. . . . . . . . 9
CV CV
CV
CV |
158 | 45, 157 | sylbid 230 |
. . . . . . . 8
CV
CV |
159 | 158 | imp 445 |
. . . . . . 7
CV
CV |
160 | | oveq1 6657 |
. . . . . . . . . 10
CV CV |
161 | 160 | breq2d 4665 |
. . . . . . . . 9
CV CV
CV
CV |
162 | 161 | ralbidv 2986 |
. . . . . . . 8
CV CV
CV
CV |
163 | 162 | rspcev 3309 |
. . . . . . 7
CV
CV
CV
CV |
164 | 19, 159, 163 | syl2anc 693 |
. . . . . 6
CV
CV |
165 | 164 | ex 450 |
. . . . 5
CV
CV |
166 | 165 | rexlimdva 3031 |
. . . 4
CV
CV |
167 | 16, 166 | syl5 34 |
. . 3
CV
CV |
168 | 167 | imp 445 |
. 2
CV
CV |
169 | | blocni.5 |
. . . 4
|
170 | 2, 21, 32, 26, 169, 1, 6 | isblo3i 27656 |
. . 3
CV
CV |
171 | 25, 170 | mpbiran 953 |
. 2
CV
CV |
172 | 168, 171 | sylibr 224 |
1
|