Step |
Hyp |
Ref |
Expression |
1 |
|
rrnequiv.y |
|
2 |
|
rrnequiv.d |
|
3 |
|
rrnequiv.1 |
|
4 |
|
rrnequiv.i |
|
5 |
|
ovex |
|
6 |
4
|
adantr |
|
7 |
|
reex |
|
8 |
|
eqid |
|
9 |
|
eqid |
|
10 |
8 9
|
resssca |
|
11 |
7 10
|
ax-mp |
|
12 |
1 11
|
pwsval |
|
13 |
5 6 12
|
sylancr |
|
14 |
13
|
fveq2d |
|
15 |
2 14
|
syl5eq |
|
16 |
15
|
oveqd |
|
17 |
|
fconstmpt |
|
18 |
17
|
oveq2i |
|
19 |
|
eqid |
|
20 |
|
fvexd |
|
21 |
5
|
a1i |
|
22 |
21
|
ralrimiva |
|
23 |
|
simprl |
|
24 |
|
ax-resscn |
|
25 |
|
cnfldbas |
|
26 |
8 25
|
ressbas2 |
|
27 |
24 26
|
ax-mp |
|
28 |
1 27
|
pwsbas |
|
29 |
5 6 28
|
sylancr |
|
30 |
13
|
fveq2d |
|
31 |
29 30
|
eqtrd |
|
32 |
3 31
|
syl5eq |
|
33 |
23 32
|
eleqtrd |
|
34 |
|
simprr |
|
35 |
34 32
|
eleqtrd |
|
36 |
|
cnfldds |
|
37 |
8 36
|
ressds |
|
38 |
7 37
|
ax-mp |
|
39 |
38
|
reseq1i |
|
40 |
|
eqid |
|
41 |
18 19 20 6 22 33 35 27 39 40
|
prdsdsval3 |
|
42 |
16 41
|
eqtrd |
|
43 |
|
eqid |
|
44 |
3 43
|
rrndstprj1 |
|
45 |
44
|
an32s |
|
46 |
4 45
|
sylanl1 |
|
47 |
46
|
ralrimiva |
|
48 |
|
ovex |
|
49 |
48
|
rgenw |
|
50 |
|
eqid |
|
51 |
|
breq1 |
|
52 |
50 51
|
ralrnmptw |
|
53 |
49 52
|
ax-mp |
|
54 |
47 53
|
sylibr |
|
55 |
3
|
rrnmet |
|
56 |
6 55
|
syl |
|
57 |
|
metge0 |
|
58 |
56 23 34 57
|
syl3anc |
|
59 |
|
elsni |
|
60 |
59
|
breq1d |
|
61 |
58 60
|
syl5ibrcom |
|
62 |
61
|
ralrimiv |
|
63 |
|
ralunb |
|
64 |
54 62 63
|
sylanbrc |
|
65 |
18 19 20 6 22 27 33
|
prdsbascl |
|
66 |
65
|
r19.21bi |
|
67 |
18 19 20 6 22 27 35
|
prdsbascl |
|
68 |
67
|
r19.21bi |
|
69 |
43
|
remet |
|
70 |
|
metcl |
|
71 |
69 70
|
mp3an1 |
|
72 |
66 68 71
|
syl2anc |
|
73 |
72
|
fmpttd |
|
74 |
73
|
frnd |
|
75 |
|
ressxr |
|
76 |
74 75
|
sstrdi |
|
77 |
|
0xr |
|
78 |
77
|
a1i |
|
79 |
78
|
snssd |
|
80 |
76 79
|
unssd |
|
81 |
|
metcl |
|
82 |
56 23 34 81
|
syl3anc |
|
83 |
75 82
|
sseldi |
|
84 |
|
supxrleub |
|
85 |
80 83 84
|
syl2anc |
|
86 |
64 85
|
mpbird |
|
87 |
42 86
|
eqbrtrd |
|
88 |
|
rzal |
|
89 |
23 3
|
eleqtrdi |
|
90 |
|
elmapi |
|
91 |
|
ffn |
|
92 |
89 90 91
|
3syl |
|
93 |
34 3
|
eleqtrdi |
|
94 |
|
elmapi |
|
95 |
|
ffn |
|
96 |
93 94 95
|
3syl |
|
97 |
|
eqfnfv |
|
98 |
92 96 97
|
syl2anc |
|
99 |
88 98
|
syl5ibr |
|
100 |
99
|
imp |
|
101 |
100
|
oveq1d |
|
102 |
|
met0 |
|
103 |
56 34 102
|
syl2anc |
|
104 |
|
hashcl |
|
105 |
6 104
|
syl |
|
106 |
105
|
nn0red |
|
107 |
105
|
nn0ge0d |
|
108 |
106 107
|
resqrtcld |
|
109 |
1 2 3
|
repwsmet |
|
110 |
6 109
|
syl |
|
111 |
|
metcl |
|
112 |
110 23 34 111
|
syl3anc |
|
113 |
106 107
|
sqrtge0d |
|
114 |
|
metge0 |
|
115 |
110 23 34 114
|
syl3anc |
|
116 |
108 112 113 115
|
mulge0d |
|
117 |
103 116
|
eqbrtrd |
|
118 |
117
|
adantr |
|
119 |
101 118
|
eqbrtrd |
|
120 |
82
|
adantr |
|
121 |
108 112
|
remulcld |
|
122 |
121
|
adantr |
|
123 |
|
rpre |
|
124 |
123
|
ad2antll |
|
125 |
122 124
|
readdcld |
|
126 |
6
|
adantr |
|
127 |
|
simprl |
|
128 |
|
eldifsn |
|
129 |
126 127 128
|
sylanbrc |
|
130 |
23
|
adantr |
|
131 |
34
|
adantr |
|
132 |
112
|
adantr |
|
133 |
|
simprr |
|
134 |
|
hashnncl |
|
135 |
126 134
|
syl |
|
136 |
127 135
|
mpbird |
|
137 |
136
|
nnrpd |
|
138 |
137
|
rpsqrtcld |
|
139 |
133 138
|
rpdivcld |
|
140 |
139
|
rpred |
|
141 |
132 140
|
readdcld |
|
142 |
|
0red |
|
143 |
115
|
adantr |
|
144 |
132 139
|
ltaddrpd |
|
145 |
142 132 141 143 144
|
lelttrd |
|
146 |
141 145
|
elrpd |
|
147 |
72
|
adantlr |
|
148 |
132
|
adantr |
|
149 |
141
|
adantr |
|
150 |
80
|
ad2antrr |
|
151 |
|
ssun1 |
|
152 |
|
simpr |
|
153 |
50
|
elrnmpt1 |
|
154 |
152 48 153
|
sylancl |
|
155 |
151 154
|
sseldi |
|
156 |
|
supxrub |
|
157 |
150 155 156
|
syl2anc |
|
158 |
42
|
ad2antrr |
|
159 |
157 158
|
breqtrrd |
|
160 |
144
|
adantr |
|
161 |
147 148 149 159 160
|
lelttrd |
|
162 |
161
|
ralrimiva |
|
163 |
3 43
|
rrndstprj2 |
|
164 |
129 130 131 146 162 163
|
syl32anc |
|
165 |
132
|
recnd |
|
166 |
140
|
recnd |
|
167 |
108
|
adantr |
|
168 |
167
|
recnd |
|
169 |
165 166 168
|
adddird |
|
170 |
165 168
|
mulcomd |
|
171 |
124
|
recnd |
|
172 |
138
|
rpne0d |
|
173 |
171 168 172
|
divcan1d |
|
174 |
170 173
|
oveq12d |
|
175 |
169 174
|
eqtrd |
|
176 |
164 175
|
breqtrd |
|
177 |
120 125 176
|
ltled |
|
178 |
177
|
anassrs |
|
179 |
178
|
ralrimiva |
|
180 |
|
alrple |
|
181 |
82 121 180
|
syl2anc |
|
182 |
181
|
adantr |
|
183 |
179 182
|
mpbird |
|
184 |
119 183
|
pm2.61dane |
|
185 |
87 184
|
jca |
|