Step | Hyp | Ref
| Expression |
1 | | limsupre3uzlem.1 |
. . 3
|
2 | | limsupre3uzlem.3 |
. . . . 5
|
3 | | uzssre 39620 |
. . . . 5
|
4 | 2, 3 | eqsstri 3635 |
. . . 4
|
5 | 4 | a1i 11 |
. . 3
|
6 | | limsupre3uzlem.4 |
. . 3
|
7 | 1, 5, 6 | limsupre3 39965 |
. 2
|
8 | | breq1 4656 |
. . . . . . . . . . 11
|
9 | 8 | anbi1d 741 |
. . . . . . . . . 10
|
10 | 9 | rexbidv 3052 |
. . . . . . . . 9
|
11 | 10 | cbvralv 3171 |
. . . . . . . 8
|
12 | 11 | biimpi 206 |
. . . . . . 7
|
13 | | nfra1 2941 |
. . . . . . . 8
|
14 | | simpr 477 |
. . . . . . . . 9
|
15 | 4, 14 | sseldi 3601 |
. . . . . . . . . 10
|
16 | | rspa 2930 |
. . . . . . . . . 10
|
17 | 15, 16 | syldan 487 |
. . . . . . . . 9
|
18 | | nfv 1843 |
. . . . . . . . . . 11
|
19 | | nfre1 3005 |
. . . . . . . . . . 11
|
20 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
21 | 2 | eluzelz2 39627 |
. . . . . . . . . . . . . . . 16
|
22 | 21 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
23 | 2 | eluzelz2 39627 |
. . . . . . . . . . . . . . . 16
|
24 | 23 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . 15
|
25 | | simp3 1063 |
. . . . . . . . . . . . . . 15
|
26 | 20, 22, 24, 25 | eluzd 39635 |
. . . . . . . . . . . . . 14
|
27 | 26 | 3adant3r 1323 |
. . . . . . . . . . . . 13
|
28 | | simp3r 1090 |
. . . . . . . . . . . . 13
|
29 | | rspe 3003 |
. . . . . . . . . . . . 13
|
30 | 27, 28, 29 | syl2anc 693 |
. . . . . . . . . . . 12
|
31 | 30 | 3exp 1264 |
. . . . . . . . . . 11
|
32 | 18, 19, 31 | rexlimd 3026 |
. . . . . . . . . 10
|
33 | 32 | imp 445 |
. . . . . . . . 9
|
34 | 14, 17, 33 | syl2anc 693 |
. . . . . . . 8
|
35 | 13, 34 | ralrimia 39315 |
. . . . . . 7
|
36 | 12, 35 | syl 17 |
. . . . . 6
|
37 | 36 | a1i 11 |
. . . . 5
|
38 | | iftrue 4092 |
. . . . . . . . . . . . 13
⌈ ⌈ ⌈ ⌈ |
39 | 38 | adantl 482 |
. . . . . . . . . . . 12
⌈
⌈ ⌈ ⌈ |
40 | | limsupre3uzlem.2 |
. . . . . . . . . . . . . 14
|
41 | 40 | ad2antrr 762 |
. . . . . . . . . . . . 13
⌈
|
42 | | ceilcl 12643 |
. . . . . . . . . . . . . 14
⌈ |
43 | 42 | ad2antlr 763 |
. . . . . . . . . . . . 13
⌈
⌈ |
44 | | simpr 477 |
. . . . . . . . . . . . 13
⌈
⌈ |
45 | 2, 41, 43, 44 | eluzd 39635 |
. . . . . . . . . . . 12
⌈
⌈ |
46 | 39, 45 | eqeltrd 2701 |
. . . . . . . . . . 11
⌈
⌈ ⌈ |
47 | | iffalse 4095 |
. . . . . . . . . . . . . 14
⌈
⌈ ⌈ |
48 | 47 | adantl 482 |
. . . . . . . . . . . . 13
⌈
⌈ ⌈ |
49 | 40, 2 | uzidd2 39643 |
. . . . . . . . . . . . . 14
|
50 | 49 | adantr 481 |
. . . . . . . . . . . . 13
⌈
|
51 | 48, 50 | eqeltrd 2701 |
. . . . . . . . . . . 12
⌈
⌈ ⌈ |
52 | 51 | adantlr 751 |
. . . . . . . . . . 11
⌈
⌈ ⌈ |
53 | 46, 52 | pm2.61dan 832 |
. . . . . . . . . 10
⌈ ⌈ |
54 | 53 | adantlr 751 |
. . . . . . . . 9
⌈ ⌈ |
55 | | simplr 792 |
. . . . . . . . 9
|
56 | | fveq2 6191 |
. . . . . . . . . . 11
⌈ ⌈ ⌈ ⌈ |
57 | 56 | rexeqdv 3145 |
. . . . . . . . . 10
⌈ ⌈
⌈ ⌈ |
58 | 57 | rspcva 3307 |
. . . . . . . . 9
⌈ ⌈
⌈ ⌈ |
59 | 54, 55, 58 | syl2anc 693 |
. . . . . . . 8
⌈ ⌈ |
60 | | nfv 1843 |
. . . . . . . . . . 11
|
61 | 18 | nfci 2754 |
. . . . . . . . . . . 12
|
62 | 61, 19 | nfral 2945 |
. . . . . . . . . . 11
|
63 | 60, 62 | nfan 1828 |
. . . . . . . . . 10
|
64 | | nfv 1843 |
. . . . . . . . . 10
|
65 | 63, 64 | nfan 1828 |
. . . . . . . . 9
|
66 | | nfre1 3005 |
. . . . . . . . 9
|
67 | 40 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⌈ ⌈ |
68 | | eluzelz 11697 |
. . . . . . . . . . . . . . 15
⌈ ⌈
|
69 | 68 | adantl 482 |
. . . . . . . . . . . . . 14
⌈ ⌈ |
70 | 67 | zred 11482 |
. . . . . . . . . . . . . . 15
⌈ ⌈ |
71 | 4, 53 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⌈ ⌈ |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . 15
⌈ ⌈ ⌈ ⌈ |
73 | 69 | zred 11482 |
. . . . . . . . . . . . . . 15
⌈ ⌈ |
74 | 4, 49 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . . . . . 17
|
76 | 42 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⌈ |
77 | 76 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⌈ |
78 | | max1 12016 |
. . . . . . . . . . . . . . . . 17
⌈ ⌈ ⌈ |
79 | 75, 77, 78 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⌈ ⌈ |
80 | 79 | adantr 481 |
. . . . . . . . . . . . . . 15
⌈ ⌈
⌈ ⌈ |
81 | | eluzle 11700 |
. . . . . . . . . . . . . . . 16
⌈ ⌈
⌈ ⌈ |
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . 15
⌈ ⌈ ⌈ ⌈ |
83 | 70, 72, 73, 80, 82 | letrd 10194 |
. . . . . . . . . . . . . 14
⌈ ⌈ |
84 | 2, 67, 69, 83 | eluzd 39635 |
. . . . . . . . . . . . 13
⌈ ⌈ |
85 | 84 | 3adant3 1081 |
. . . . . . . . . . . 12
⌈ ⌈ |
86 | | simplr 792 |
. . . . . . . . . . . . . . 15
⌈ ⌈ |
87 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
88 | | ceilge 12645 |
. . . . . . . . . . . . . . . . . 18
⌈ |
89 | 88 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⌈ |
90 | | max2 12018 |
. . . . . . . . . . . . . . . . . 18
⌈ ⌈
⌈ ⌈ |
91 | 75, 77, 90 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⌈
⌈ ⌈ |
92 | 87, 77, 71, 89, 91 | letrd 10194 |
. . . . . . . . . . . . . . . 16
⌈ ⌈ |
93 | 92 | adantr 481 |
. . . . . . . . . . . . . . 15
⌈ ⌈
⌈ ⌈ |
94 | 86, 72, 73, 93, 82 | letrd 10194 |
. . . . . . . . . . . . . 14
⌈ ⌈ |
95 | 94 | 3adant3 1081 |
. . . . . . . . . . . . 13
⌈ ⌈
|
96 | | simp3 1063 |
. . . . . . . . . . . . 13
⌈ ⌈ |
97 | 95, 96 | jca 554 |
. . . . . . . . . . . 12
⌈ ⌈
|
98 | | rspe 3003 |
. . . . . . . . . . . 12
|
99 | 85, 97, 98 | syl2anc 693 |
. . . . . . . . . . 11
⌈ ⌈
|
100 | 99 | 3exp 1264 |
. . . . . . . . . 10
⌈ ⌈
|
101 | 100 | adantlr 751 |
. . . . . . . . 9
⌈ ⌈
|
102 | 65, 66, 101 | rexlimd 3026 |
. . . . . . . 8
⌈ ⌈
|
103 | 59, 102 | mpd 15 |
. . . . . . 7
|
104 | 103 | ralrimiva 2966 |
. . . . . 6
|
105 | 104 | ex 450 |
. . . . 5
|
106 | 37, 105 | impbid 202 |
. . . 4
|
107 | 106 | rexbidv 3052 |
. . 3
|
108 | 53 | adantr 481 |
. . . . . . . 8
⌈ ⌈ |
109 | 60, 64 | nfan 1828 |
. . . . . . . . . 10
|
110 | | nfra1 2941 |
. . . . . . . . . 10
|
111 | 109, 110 | nfan 1828 |
. . . . . . . . 9
|
112 | 94 | adantlr 751 |
. . . . . . . . . . 11
⌈ ⌈ |
113 | | simplr 792 |
. . . . . . . . . . . 12
⌈ ⌈
|
114 | 84 | adantlr 751 |
. . . . . . . . . . . 12
⌈ ⌈ |
115 | | rspa 2930 |
. . . . . . . . . . . 12
|
116 | 113, 114,
115 | syl2anc 693 |
. . . . . . . . . . 11
⌈ ⌈
|
117 | 112, 116 | mpd 15 |
. . . . . . . . . 10
⌈ ⌈ |
118 | 117 | ex 450 |
. . . . . . . . 9
⌈ ⌈
|
119 | 111, 118 | ralrimi 2957 |
. . . . . . . 8
⌈ ⌈ |
120 | 56 | raleqdv 3144 |
. . . . . . . . 9
⌈ ⌈
⌈ ⌈ |
121 | 120 | rspcev 3309 |
. . . . . . . 8
⌈ ⌈ ⌈ ⌈
|
122 | 108, 119,
121 | syl2anc 693 |
. . . . . . 7
|
123 | 122 | ex 450 |
. . . . . 6
|
124 | 123 | rexlimdva 3031 |
. . . . 5
|
125 | 4 | sseli 3599 |
. . . . . . . . 9
|
126 | 125 | ad2antlr 763 |
. . . . . . . 8
|
127 | | nfra1 2941 |
. . . . . . . . . . 11
|
128 | 18, 127 | nfan 1828 |
. . . . . . . . . 10
|
129 | | simp1r 1086 |
. . . . . . . . . . . 12
|
130 | 26 | 3adant1r 1319 |
. . . . . . . . . . . 12
|
131 | | rspa 2930 |
. . . . . . . . . . . 12
|
132 | 129, 130,
131 | syl2anc 693 |
. . . . . . . . . . 11
|
133 | 132 | 3exp 1264 |
. . . . . . . . . 10
|
134 | 128, 133 | ralrimi 2957 |
. . . . . . . . 9
|
135 | 134 | adantll 750 |
. . . . . . . 8
|
136 | 8 | imbi1d 331 |
. . . . . . . . . 10
|
137 | 136 | ralbidv 2986 |
. . . . . . . . 9
|
138 | 137 | rspcev 3309 |
. . . . . . . 8
|
139 | 126, 135,
138 | syl2anc 693 |
. . . . . . 7
|
140 | 139 | ex 450 |
. . . . . 6
|
141 | 140 | rexlimdva 3031 |
. . . . 5
|
142 | 124, 141 | impbid 202 |
. . . 4
|
143 | 142 | rexbidv 3052 |
. . 3
|
144 | 107, 143 | anbi12d 747 |
. 2
|
145 | 7, 144 | bitrd 268 |
1
|