| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The positive real number 'one'. |
| Ref | Expression |
|---|---|
| 1pr |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elnp 6244 |
. 2
| |
| 2 | 1lt2pq 6230 |
. . . . . . 7
| |
| 3 | 1q 6209 |
. . . . . . . . . 10
| |
| 4 | 3 | elisseti 2301 |
. . . . . . . . 9
|
| 5 | oprex 4907 |
. . . . . . . . 9
| |
| 6 | 4, 5 | ltrpq 6237 |
. . . . . . . 8
|
| 7 | fvex 4689 |
. . . . . . . . . 10
| |
| 8 | 7, 4 | mulcompq 6216 |
. . . . . . . . 9
|
| 9 | recclpq 6224 |
. . . . . . . . . . 11
| |
| 10 | 3, 9 | ax-mp 7 |
. . . . . . . . . 10
|
| 11 | mulidpq 6221 |
. . . . . . . . . 10
| |
| 12 | 10, 11 | ax-mp 7 |
. . . . . . . . 9
|
| 13 | recidpq 6223 |
. . . . . . . . . 10
| |
| 14 | 3, 13 | ax-mp 7 |
. . . . . . . . 9
|
| 15 | 8, 12, 14 | 3eqtr3i 1918 |
. . . . . . . 8
|
| 16 | 6, 15 | syl6breq 3376 |
. . . . . . 7
|
| 17 | 2, 16 | ax-mp 7 |
. . . . . 6
|
| 18 | fvex 4689 |
. . . . . . 7
| |
| 19 | breq1 3341 |
. . . . . . 7
| |
| 20 | df-1p 6239 |
. . . . . . 7
| |
| 21 | 18, 19, 20 | elab2 2407 |
. . . . . 6
|
| 22 | 17, 21 | mpbir 207 |
. . . . 5
|
| 23 | ne0i 2881 |
. . . . 5
| |
| 24 | 22, 23 | ax-mp 7 |
. . . 4
|
| 25 | 0pss 2910 |
. . . 4
| |
| 26 | 24, 25 | mpbir 207 |
. . 3
|
| 27 | dfpss2 2694 |
. . . 4
| |
| 28 | 20 | abeq2i 2001 |
. . . . . 6
|
| 29 | ltrelpq 6203 |
. . . . . . . 8
| |
| 30 | 4, 29 | brel 4048 |
. . . . . . 7
|
| 31 | 30 | simplld 348 |
. . . . . 6
|
| 32 | 28, 31 | sylbi 216 |
. . . . 5
|
| 33 | 32 | ssriv 2621 |
. . . 4
|
| 34 | ltsopq 6227 |
. . . . . . 7
| |
| 35 | 4, 34, 29 | soirri 4314 |
. . . . . 6
|
| 36 | breq1 3341 |
. . . . . . 7
| |
| 37 | 4, 36, 20 | elab2 2407 |
. . . . . 6
|
| 38 | 35, 37 | mtbir 209 |
. . . . 5
|
| 39 | eleq2 1958 |
. . . . . 6
| |
| 40 | 3, 39 | mpbiri 211 |
. . . . 5
|
| 41 | 38, 40 | mto 121 |
. . . 4
|
| 42 | 27, 33, 41 | mpbir2an 800 |
. . 3
|
| 43 | 26, 42 | pm3.2i 307 |
. 2
|
| 44 | visset 2295 |
. . . . . . . . 9
| |
| 45 | visset 2295 |
. . . . . . . . 9
| |
| 46 | 44, 34, 29, 45, 4 | sotri 4315 |
. . . . . . . 8
|
| 47 | 46 | ex 402 |
. . . . . . 7
|
| 48 | df-1p 6239 |
. . . . . . . 8
| |
| 49 | 48 | abeq2i 2001 |
. . . . . . 7
|
| 50 | 47, 28, 49 | 3imtr4g 612 |
. . . . . 6
|
| 51 | 50 | com12 14 |
. . . . 5
|
| 52 | 51 | 19.21aiv 1664 |
. . . 4
|
| 53 | 45, 4 | ltbtwnpq 6236 |
. . . . . 6
|
| 54 | 49 | anbi1i 539 |
. . . . . . . 8
|
| 55 | ancom 482 |
. . . . . . . 8
| |
| 56 | 54, 55 | bitri 190 |
. . . . . . 7
|
| 57 | 56 | exbii 1398 |
. . . . . 6
|
| 58 | 53, 28, 57 | 3imtr4i 236 |
. . . . 5
|
| 59 | df-rex 2110 |
. . . . 5
| |
| 60 | 58, 59 | sylibr 217 |
. . . 4
|
| 61 | 52, 60 | jca 310 |
. . 3
|
| 62 | 61 | rgen 2159 |
. 2
|
| 63 | 1, 43, 62 | mpbir2an 800 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: 1idpr 6285 recexpr 6312 gt0srpr 6339 0r 6341 1r 6342 m1r 6343 m1p1sr 6353 m1m1sr 6354 0lt1sr 6356 0idsr 6358 1idsr 6359 00sr 6360 recexsrlem 6364 mappsrpr 6370 ltpsrpr 6371 map2psrpr 6372 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-fv 4014 df-opr 4886 df-oprab 4887 df-1st 5020 df-2nd 5021 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 |