Proof of Theorem stoweidlem51
Step | Hyp | Ref
| Expression |
1 | | stoweidlem51.5 |
. . . 4
|
2 | | ssrab2 3687 |
. . . 4
|
3 | 1, 2 | eqsstri 3635 |
. . 3
|
4 | | stoweidlem51.6 |
. . . 4
|
5 | | stoweidlem51.7 |
. . . 4
|
6 | | 1zzd 11408 |
. . . . . 6
|
7 | | stoweidlem51.10 |
. . . . . . 7
|
8 | 7 | nnzd 11481 |
. . . . . 6
|
9 | 6, 8, 8 | 3jca 1242 |
. . . . 5
|
10 | 7 | nnge1d 11063 |
. . . . . 6
|
11 | 7 | nnred 11035 |
. . . . . . 7
|
12 | 11 | leidd 10594 |
. . . . . 6
|
13 | 10, 12 | jca 554 |
. . . . 5
|
14 | | elfz2 12333 |
. . . . 5
|
15 | 9, 13, 14 | sylanbrc 698 |
. . . 4
|
16 | | stoweidlem51.12 |
. . . 4
|
17 | | stoweidlem51.2 |
. . . . 5
|
18 | | eqid 2622 |
. . . . 5
|
19 | | stoweidlem51.20 |
. . . . 5
|
20 | | stoweidlem51.19 |
. . . . 5
|
21 | 17, 1, 18, 19, 20 | stoweidlem16 40233 |
. . . 4
|
22 | | stoweidlem51.21 |
. . . 4
|
23 | 4, 5, 15, 16, 21, 22 | fmulcl 39813 |
. . 3
|
24 | 3, 23 | sseldi 3601 |
. 2
|
25 | 1 | eleq2i 2693 |
. . . . . . 7
|
26 | | nfcv 2764 |
. . . . . . . . . . 11
|
27 | | nfrab1 3122 |
. . . . . . . . . . . . . 14
|
28 | 1, 27 | nfcxfr 2762 |
. . . . . . . . . . . . 13
|
29 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
30 | 28, 28, 29 | nfmpt2 6724 |
. . . . . . . . . . . 12
|
31 | 4, 30 | nfcxfr 2762 |
. . . . . . . . . . 11
|
32 | | nfcv 2764 |
. . . . . . . . . . 11
|
33 | 26, 31, 32 | nfseq 12811 |
. . . . . . . . . 10
|
34 | | nfcv 2764 |
. . . . . . . . . 10
|
35 | 33, 34 | nffv 6198 |
. . . . . . . . 9
|
36 | 5, 35 | nfcxfr 2762 |
. . . . . . . 8
|
37 | | nfcv 2764 |
. . . . . . . 8
|
38 | | nfcv 2764 |
. . . . . . . . 9
|
39 | | nfcv 2764 |
. . . . . . . . . . 11
|
40 | | nfcv 2764 |
. . . . . . . . . . 11
|
41 | | nfcv 2764 |
. . . . . . . . . . . 12
|
42 | 36, 41 | nffv 6198 |
. . . . . . . . . . 11
|
43 | 39, 40, 42 | nfbr 4699 |
. . . . . . . . . 10
|
44 | 42, 40, 26 | nfbr 4699 |
. . . . . . . . . 10
|
45 | 43, 44 | nfan 1828 |
. . . . . . . . 9
|
46 | 38, 45 | nfral 2945 |
. . . . . . . 8
|
47 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
48 | | nfra1 2941 |
. . . . . . . . . . . . . . . . 17
|
49 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
|
50 | 48, 49 | nfrab 3123 |
. . . . . . . . . . . . . . . 16
|
51 | 1, 50 | nfcxfr 2762 |
. . . . . . . . . . . . . . 15
|
52 | | nfmpt1 4747 |
. . . . . . . . . . . . . . 15
|
53 | 51, 51, 52 | nfmpt2 6724 |
. . . . . . . . . . . . . 14
|
54 | 4, 53 | nfcxfr 2762 |
. . . . . . . . . . . . 13
|
55 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
56 | 47, 54, 55 | nfseq 12811 |
. . . . . . . . . . . 12
|
57 | | nfcv 2764 |
. . . . . . . . . . . 12
|
58 | 56, 57 | nffv 6198 |
. . . . . . . . . . 11
|
59 | 5, 58 | nfcxfr 2762 |
. . . . . . . . . 10
|
60 | 59 | nfeq2 2780 |
. . . . . . . . 9
|
61 | | fveq1 6190 |
. . . . . . . . . . 11
|
62 | 61 | breq2d 4665 |
. . . . . . . . . 10
|
63 | 61 | breq1d 4663 |
. . . . . . . . . 10
|
64 | 62, 63 | anbi12d 747 |
. . . . . . . . 9
|
65 | 60, 64 | ralbid 2983 |
. . . . . . . 8
|
66 | 36, 37, 46, 65 | elrabf 3360 |
. . . . . . 7
|
67 | 25, 66 | bitri 264 |
. . . . . 6
|
68 | 23, 67 | sylib 208 |
. . . . 5
|
69 | 68 | simprd 479 |
. . . 4
|
70 | | stoweidlem51.1 |
. . . . 5
|
71 | | stoweidlem51.8 |
. . . . 5
|
72 | | stoweidlem51.9 |
. . . . 5
|
73 | | stoweidlem51.11 |
. . . . 5
|
74 | | stoweidlem51.14 |
. . . . 5
|
75 | | stoweidlem51.15 |
. . . . 5
|
76 | | nfv 1843 |
. . . . . . 7
|
77 | 17, 76 | nfan 1828 |
. . . . . 6
|
78 | 16 | ffvelrnda 6359 |
. . . . . . . . . . . 12
|
79 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
80 | 79 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
|
81 | 79 | breq1d 4663 |
. . . . . . . . . . . . . . . 16
|
82 | 80, 81 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
83 | 82 | ralbidv 2986 |
. . . . . . . . . . . . . 14
|
84 | 83, 1 | elrab2 3366 |
. . . . . . . . . . . . 13
|
85 | 84 | simplbi 476 |
. . . . . . . . . . . 12
|
86 | 78, 85 | syl 17 |
. . . . . . . . . . 11
|
87 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
88 | 87 | anbi2d 740 |
. . . . . . . . . . . . . 14
|
89 | | feq1 6026 |
. . . . . . . . . . . . . 14
|
90 | 88, 89 | imbi12d 334 |
. . . . . . . . . . . . 13
|
91 | 19 | a1i 11 |
. . . . . . . . . . . . 13
|
92 | 90, 91 | vtoclga 3272 |
. . . . . . . . . . . 12
|
93 | 92 | anabsi7 860 |
. . . . . . . . . . 11
|
94 | 86, 93 | syldan 487 |
. . . . . . . . . 10
|
95 | 94 | adantr 481 |
. . . . . . . . 9
|
96 | 73 | ffvelrnda 6359 |
. . . . . . . . . . 11
|
97 | | simpl 473 |
. . . . . . . . . . . 12
|
98 | 97, 96 | jca 554 |
. . . . . . . . . . 11
|
99 | | stoweidlem51.3 |
. . . . . . . . . . . . . 14
|
100 | | stoweidlem51.4 |
. . . . . . . . . . . . . . 15
|
101 | 100 | nfel2 2781 |
. . . . . . . . . . . . . 14
|
102 | 99, 101 | nfan 1828 |
. . . . . . . . . . . . 13
|
103 | | nfv 1843 |
. . . . . . . . . . . . 13
|
104 | 102, 103 | nfim 1825 |
. . . . . . . . . . . 12
|
105 | | eleq1 2689 |
. . . . . . . . . . . . . 14
|
106 | 105 | anbi2d 740 |
. . . . . . . . . . . . 13
|
107 | | sseq1 3626 |
. . . . . . . . . . . . 13
|
108 | 106, 107 | imbi12d 334 |
. . . . . . . . . . . 12
|
109 | | stoweidlem51.13 |
. . . . . . . . . . . 12
|
110 | 104, 108,
109 | vtoclg1f 3265 |
. . . . . . . . . . 11
|
111 | 96, 98, 110 | sylc 65 |
. . . . . . . . . 10
|
112 | 111 | sselda 3603 |
. . . . . . . . 9
|
113 | 95, 112 | ffvelrnd 6360 |
. . . . . . . 8
|
114 | | stoweidlem51.22 |
. . . . . . . . . . 11
|
115 | 114 | rpred 11872 |
. . . . . . . . . 10
|
116 | 115 | ad2antrr 762 |
. . . . . . . . 9
|
117 | 11 | ad2antrr 762 |
. . . . . . . . 9
|
118 | 7 | nnne0d 11065 |
. . . . . . . . . 10
|
119 | 118 | ad2antrr 762 |
. . . . . . . . 9
|
120 | 116, 117,
119 | redivcld 10853 |
. . . . . . . 8
|
121 | | stoweidlem51.17 |
. . . . . . . . 9
|
122 | 121 | r19.21bi 2932 |
. . . . . . . 8
|
123 | | 1red 10055 |
. . . . . . . . . . . 12
|
124 | | 0lt1 10550 |
. . . . . . . . . . . . 13
|
125 | 124 | a1i 11 |
. . . . . . . . . . . 12
|
126 | 7 | nngt0d 11064 |
. . . . . . . . . . . 12
|
127 | 114 | rpregt0d 11878 |
. . . . . . . . . . . 12
|
128 | | lediv2 10913 |
. . . . . . . . . . . 12
|
129 | 123, 125,
11, 126, 127, 128 | syl221anc 1337 |
. . . . . . . . . . 11
|
130 | 10, 129 | mpbid 222 |
. . . . . . . . . 10
|
131 | 114 | rpcnd 11874 |
. . . . . . . . . . 11
|
132 | 131 | div1d 10793 |
. . . . . . . . . 10
|
133 | 130, 132 | breqtrd 4679 |
. . . . . . . . 9
|
134 | 133 | ad2antrr 762 |
. . . . . . . 8
|
135 | 113, 120,
116, 122, 134 | ltletrd 10197 |
. . . . . . 7
|
136 | 135 | ex 450 |
. . . . . 6
|
137 | 77, 136 | ralrimi 2957 |
. . . . 5
|
138 | 70, 17, 1, 4, 5, 71,
72, 7, 73, 16, 74, 75, 137, 22, 19, 20, 114 | stoweidlem48 40265 |
. . . 4
|
139 | | stoweidlem51.18 |
. . . . 5
|
140 | | stoweidlem51.23 |
. . . . 5
|
141 | 3 | sseli 3599 |
. . . . . 6
|
142 | 141, 19 | sylan2 491 |
. . . . 5
|
143 | | stoweidlem51.16 |
. . . . 5
|
144 | 70, 17, 51, 4, 5, 71, 72, 7, 16, 139, 114, 140, 142, 21, 22, 143 | stoweidlem42 40259 |
. . . 4
|
145 | 69, 138, 144 | 3jca 1242 |
. . 3
|
146 | 24, 145 | jca 554 |
. 2
|
147 | | eleq1 2689 |
. . . 4
|
148 | 59 | nfeq2 2780 |
. . . . . 6
|
149 | | fveq1 6190 |
. . . . . . . 8
|
150 | 149 | breq2d 4665 |
. . . . . . 7
|
151 | 149 | breq1d 4663 |
. . . . . . 7
|
152 | 150, 151 | anbi12d 747 |
. . . . . 6
|
153 | 148, 152 | ralbid 2983 |
. . . . 5
|
154 | 149 | breq1d 4663 |
. . . . . 6
|
155 | 148, 154 | ralbid 2983 |
. . . . 5
|
156 | 149 | breq2d 4665 |
. . . . . 6
|
157 | 148, 156 | ralbid 2983 |
. . . . 5
|
158 | 153, 155,
157 | 3anbi123d 1399 |
. . . 4
|
159 | 147, 158 | anbi12d 747 |
. . 3
|
160 | 159 | spcegv 3294 |
. 2
|
161 | 24, 146, 160 | sylc 65 |
1
|