Step | Hyp | Ref
| Expression |
1 | | eliun 4524 |
. . . . . . . . 9
|
2 | 1 | biimpi 206 |
. . . . . . . 8
|
3 | 2 | adantl 482 |
. . . . . . 7
|
4 | | iundjiun.nph |
. . . . . . . . 9
|
5 | | nfcv 2764 |
. . . . . . . . . 10
|
6 | | nfiu1 4550 |
. . . . . . . . . 10
|
7 | 5, 6 | nfel 2777 |
. . . . . . . . 9
|
8 | | simp2 1062 |
. . . . . . . . . . . 12
|
9 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
10 | | elfzuz 12338 |
. . . . . . . . . . . . . . . . 17
|
11 | | iundjiun.z |
. . . . . . . . . . . . . . . . . 18
|
12 | 11 | eqcomi 2631 |
. . . . . . . . . . . . . . . . 17
|
13 | 10, 12 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
|
14 | 13 | adantl 482 |
. . . . . . . . . . . . . . 15
|
15 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
16 | | iundjiun.e |
. . . . . . . . . . . . . . . . . . 19
|
17 | 16 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
|
18 | | difexg 4808 |
. . . . . . . . . . . . . . . . . 18
..^ |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
20 | | iundjiun.f |
. . . . . . . . . . . . . . . . . 18
..^ |
21 | 20 | fvmpt2 6291 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
22 | 15, 19, 21 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
..^ |
23 | | difssd 3738 |
. . . . . . . . . . . . . . . 16
..^ |
24 | 22, 23 | eqsstrd 3639 |
. . . . . . . . . . . . . . 15
|
25 | 9, 14, 24 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
26 | 25 | 3adant3 1081 |
. . . . . . . . . . . . 13
|
27 | | simp3 1063 |
. . . . . . . . . . . . 13
|
28 | 26, 27 | sseldd 3604 |
. . . . . . . . . . . 12
|
29 | | rspe 3003 |
. . . . . . . . . . . 12
|
30 | 8, 28, 29 | syl2anc 693 |
. . . . . . . . . . 11
|
31 | | eliun 4524 |
. . . . . . . . . . 11
|
32 | 30, 31 | sylibr 224 |
. . . . . . . . . 10
|
33 | 32 | 3exp 1264 |
. . . . . . . . 9
|
34 | 4, 7, 33 | rexlimd 3026 |
. . . . . . . 8
|
35 | 34 | adantr 481 |
. . . . . . 7
|
36 | 3, 35 | mpd 15 |
. . . . . 6
|
37 | 36 | ralrimiva 2966 |
. . . . 5
|
38 | | dfss3 3592 |
. . . . 5
|
39 | 37, 38 | sylibr 224 |
. . . 4
|
40 | | fzssuz 12382 |
. . . . . . . . . . 11
|
41 | 40 | a1i 11 |
. . . . . . . . . 10
|
42 | 31 | biimpi 206 |
. . . . . . . . . 10
|
43 | | nfv 1843 |
. . . . . . . . . . 11
|
44 | | fveq2 6191 |
. . . . . . . . . . . 12
|
45 | 44 | eleq2d 2687 |
. . . . . . . . . . 11
|
46 | 43, 45 | uzwo4 39221 |
. . . . . . . . . 10
|
47 | 41, 42, 46 | syl2anc 693 |
. . . . . . . . 9
|
48 | 47 | adantl 482 |
. . . . . . . 8
|
49 | | simprl 794 |
. . . . . . . . . . . . . 14
|
50 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . 19
|
51 | | nfra1 2941 |
. . . . . . . . . . . . . . . . . . 19
|
52 | 50, 51 | nfan 1828 |
. . . . . . . . . . . . . . . . . 18
|
53 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
|
54 | 53 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
56 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
57 | 56 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
59 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
60 | 58, 59 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
61 | | elfzolem1 39537 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
|
62 | 61 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
63 | 58 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
64 | 55, 60, 58, 62, 63 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . 21
..^
|
65 | 64 | ad4ant24 1298 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
66 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
67 | | elfzel1 12341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
69 | | elfzel2 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
70 | 69 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
71 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^ |
72 | 68, 70, 71 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
73 | | elfzole1 12478 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
74 | 73 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^ |
75 | 70 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
76 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
77 | 57, 76 | resubcld 10458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
78 | 69 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
79 | 57 | ltm1d 10956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
80 | | elfzle2 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
81 | 77, 57, 78, 79, 80 | ltletrd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
..^ |
83 | 55, 60, 75, 62, 82 | lelttrd 10195 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
..^
|
84 | 55, 75, 83 | ltled 10185 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
..^
|
85 | 72, 74, 84 | jca32 558 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ |
86 | | elfz2 12333 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
87 | 85, 86 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
88 | 87 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
89 | | rspa 2930 |
. . . . . . . . . . . . . . . . . . . . . 22
|
90 | 66, 88, 89 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
91 | 90 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
92 | 65, 91 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
..^
|
93 | 92 | ex 450 |
. . . . . . . . . . . . . . . . . 18
..^
|
94 | 52, 93 | ralrimi 2957 |
. . . . . . . . . . . . . . . . 17
..^ |
95 | | ralnex 2992 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
96 | 94, 95 | sylib 208 |
. . . . . . . . . . . . . . . 16
..^ |
97 | | eliun 4524 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
98 | 96, 97 | sylnibr 319 |
. . . . . . . . . . . . . . 15
..^ |
99 | 98 | adantrl 752 |
. . . . . . . . . . . . . 14
..^ |
100 | 49, 99 | eldifd 3585 |
. . . . . . . . . . . . 13
..^ |
101 | 14, 22 | syldan 487 |
. . . . . . . . . . . . . . 15
..^ |
102 | 101 | eqcomd 2628 |
. . . . . . . . . . . . . 14
..^ |
103 | 102 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
104 | 100, 103 | eleqtrd 2703 |
. . . . . . . . . . . 12
|
105 | 104 | ex 450 |
. . . . . . . . . . 11
|
106 | 105 | ex 450 |
. . . . . . . . . 10
|
107 | 4, 106 | reximdai 3012 |
. . . . . . . . 9
|
108 | 107 | adantr 481 |
. . . . . . . 8
|
109 | 48, 108 | mpd 15 |
. . . . . . 7
|
110 | 109, 1 | sylibr 224 |
. . . . . 6
|
111 | 110 | ralrimiva 2966 |
. . . . 5
|
112 | | dfss3 3592 |
. . . . 5
|
113 | 111, 112 | sylibr 224 |
. . . 4
|
114 | 39, 113 | eqssd 3620 |
. . 3
|
115 | 114 | ralrimivw 2967 |
. 2
|
116 | 11 | iuneqfzuz 39551 |
. . 3
|
117 | 115, 116 | syl 17 |
. 2
|
118 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
119 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
..^ ..^ |
120 | 119 | iuneq1d 4545 |
. . . . . . . . . . . . . 14
..^ ..^ |
121 | 118, 120 | difeq12d 3729 |
. . . . . . . . . . . . 13
..^
..^ |
122 | 121 | cbvmptv 4750 |
. . . . . . . . . . . 12
..^
..^ |
123 | 20, 122 | eqtri 2644 |
. . . . . . . . . . 11
..^ |
124 | | simpllr 799 |
. . . . . . . . . . 11
|
125 | | simplr 792 |
. . . . . . . . . . 11
|
126 | | simpr 477 |
. . . . . . . . . . 11
|
127 | 11, 123, 124, 125, 126 | iundjiunlem 40676 |
. . . . . . . . . 10
|
128 | 127 | adantlr 751 |
. . . . . . . . 9
|
129 | | simpll 790 |
. . . . . . . . . 10
|
130 | | neqne 2802 |
. . . . . . . . . . . 12
|
131 | | id 22 |
. . . . . . . . . . . . . . . . . 18
|
132 | 131, 11 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
|
133 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . 17
|
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . 16
|
135 | 134 | zred 11482 |
. . . . . . . . . . . . . . 15
|
136 | 135 | adantl 482 |
. . . . . . . . . . . . . 14
|
137 | 136 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
138 | | id 22 |
. . . . . . . . . . . . . . . . 17
|
139 | 138, 11 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
|
140 | | eluzelz 11697 |
. . . . . . . . . . . . . . . 16
|
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . 15
|
142 | 141 | zred 11482 |
. . . . . . . . . . . . . 14
|
143 | 142 | ad3antrrr 766 |
. . . . . . . . . . . . 13
|
144 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
145 | 136 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
146 | 142 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
|
147 | 145, 146 | lenltd 10183 |
. . . . . . . . . . . . . . 15
|
148 | 144, 147 | mpbird 247 |
. . . . . . . . . . . . . 14
|
149 | 148 | adantlr 751 |
. . . . . . . . . . . . 13
|
150 | | simplr 792 |
. . . . . . . . . . . . 13
|
151 | 137, 143,
149, 150 | leneltd 10191 |
. . . . . . . . . . . 12
|
152 | 130, 151 | sylanl2 683 |
. . . . . . . . . . 11
|
153 | 152 | ad5ant2345 1317 |
. . . . . . . . . 10
|
154 | | anass 681 |
. . . . . . . . . . 11
|
155 | | incom 3805 |
. . . . . . . . . . . . 13
|
156 | 155 | a1i 11 |
. . . . . . . . . . . 12
|
157 | | simplrr 801 |
. . . . . . . . . . . . 13
|
158 | | simplrl 800 |
. . . . . . . . . . . . 13
|
159 | | simpr 477 |
. . . . . . . . . . . . 13
|
160 | 11, 123, 157, 158, 159 | iundjiunlem 40676 |
. . . . . . . . . . . 12
|
161 | 156, 160 | eqtrd 2656 |
. . . . . . . . . . 11
|
162 | 154, 161 | sylanb 489 |
. . . . . . . . . 10
|
163 | 129, 153,
162 | syl2anc 693 |
. . . . . . . . 9
|
164 | 128, 163 | pm2.61dan 832 |
. . . . . . . 8
|
165 | 164 | ex 450 |
. . . . . . 7
|
166 | | df-or 385 |
. . . . . . 7
|
167 | 165, 166 | sylibr 224 |
. . . . . 6
|
168 | 167 | ralrimiva 2966 |
. . . . 5
|
169 | 168 | ex 450 |
. . . 4
|
170 | 4, 169 | ralrimi 2957 |
. . 3
|
171 | | nfcv 2764 |
. . . . 5
|
172 | | nfmpt1 4747 |
. . . . . . 7
..^ |
173 | 20, 172 | nfcxfr 2762 |
. . . . . 6
|
174 | | nfcv 2764 |
. . . . . 6
|
175 | 173, 174 | nffv 6198 |
. . . . 5
|
176 | | fveq2 6191 |
. . . . 5
|
177 | 171, 175,
176 | cbvdisj 4630 |
. . . 4
Disj
Disj |
178 | | fveq2 6191 |
. . . . 5
|
179 | 178 | disjor 4634 |
. . . 4
Disj
|
180 | | nfcv 2764 |
. . . . . 6
|
181 | | nfv 1843 |
. . . . . . 7
|
182 | | nfcv 2764 |
. . . . . . . . . 10
|
183 | 173, 182 | nffv 6198 |
. . . . . . . . 9
|
184 | 175, 183 | nfin 3820 |
. . . . . . . 8
|
185 | | nfcv 2764 |
. . . . . . . 8
|
186 | 184, 185 | nfeq 2776 |
. . . . . . 7
|
187 | 181, 186 | nfor 1834 |
. . . . . 6
|
188 | 180, 187 | nfral 2945 |
. . . . 5
|
189 | | nfv 1843 |
. . . . 5
|
190 | | equequ1 1952 |
. . . . . . 7
|
191 | | fveq2 6191 |
. . . . . . . . 9
|
192 | 191 | ineq1d 3813 |
. . . . . . . 8
|
193 | 192 | eqeq1d 2624 |
. . . . . . 7
|
194 | 190, 193 | orbi12d 746 |
. . . . . 6
|
195 | 194 | ralbidv 2986 |
. . . . 5
|
196 | 188, 189,
195 | cbvral 3167 |
. . . 4
|
197 | 177, 179,
196 | 3bitri 286 |
. . 3
Disj
|
198 | 170, 197 | sylibr 224 |
. 2
Disj
|
199 | 115, 117,
198 | jca31 557 |
1
Disj |