1re - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 1re		Structured version Visualization version Unicode version

Theorem 1re 10039

Description:

is a real number. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 9994, by exploiting properties of the imaginary unit

. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)

**Assertion**
Ref	Expression
1re

Proof of Theorem 1re Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1ne0 10005	. . 3
2		ax-1cn 9994	. . . . 5
3		cnre 10036	. . . . 5
4	2, 3	ax-mp 5	. . . 4
5		neeq1 2856	. . . . . . . 8
6	5	biimpcd 239	. . . . . . 7
7		0cn 10032	. . . . . . . 8
8		cnre 10036	. . . . . . . 8
9	7, 8	ax-mp 5	. . . . . . 7
10		neeq2 2857	. . . . . . . . . 10
11	10	biimpcd 239	. . . . . . . . 9
12	11	reximdv 3016	. . . . . . . 8
13	12	reximdv 3016	. . . . . . 7
14	6, 9, 13	syl6mpi 67	. . . . . 6
15	14	reximdv 3016	. . . . 5
16	15	reximdv 3016	. . . 4
17	4, 16	mpi 20	. . 3
18		ioran 511	. . . . . . . . 9 $\/$ $/\$
19		df-ne 2795	. . . . . . . . . . 11
20	19	con2bii 347	. . . . . . . . . 10
21		df-ne 2795	. . . . . . . . . . 11
22	21	con2bii 347	. . . . . . . . . 10
23	20, 22	anbi12i 733	. . . . . . . . 9 $/\$ $/\$
24	18, 23	bitr4i 267	. . . . . . . 8 $\/$ $/\$
25		id 22	. . . . . . . . 9
26		oveq2 6658	. . . . . . . . 9
27	25, 26	oveqan12d 6669	. . . . . . . 8 $/\$
28	24, 27	sylbi 207	. . . . . . 7 $\/$
29	28	necon1ai 2821	. . . . . 6 $\/$
30		neeq1 2856	. . . . . . . . . 10
31		neeq2 2857	. . . . . . . . . 10
32	30, 31	rspc2ev 3324	. . . . . . . . 9 $/\$ $/\$
33	32	3expia 1267	. . . . . . . 8 $/\$
34	33	ad2ant2r 783	. . . . . . 7 $/\$ $/\$ $/\$
35		neeq1 2856	. . . . . . . . . 10
36		neeq2 2857	. . . . . . . . . 10
37	35, 36	rspc2ev 3324	. . . . . . . . 9 $/\$ $/\$
38	37	3expia 1267	. . . . . . . 8 $/\$
39	38	ad2ant2l 782	. . . . . . 7 $/\$ $/\$ $/\$
40	34, 39	jaod 395	. . . . . 6 $/\$ $/\$ $/\$ $\/$
41	29, 40	syl5 34	. . . . 5 $/\$ $/\$ $/\$
42	41	rexlimdvva 3038	. . . 4 $/\$
43	42	rexlimivv 3036	. . 3
44	1, 17, 43	mp2b 10	. 2
45		eqtr3 2643	. . . . . . . . 9 $/\$
46	45	ex 450	. . . . . . . 8
47	46	necon3d 2815	. . . . . . 7
48		neeq1 2856	. . . . . . . . 9
49	48	rspcev 3309	. . . . . . . 8 $/\$
50	49	expcom 451	. . . . . . 7
51	47, 50	syl6 35	. . . . . 6
52	51	com23 86	. . . . 5
53	52	adantld 483	. . . 4 $/\$
54		neeq1 2856	. . . . . . . 8
55	54	rspcev 3309	. . . . . . 7 $/\$
56	55	expcom 451	. . . . . 6
57	56	adantrd 484	. . . . 5 $/\$
58	57	a1dd 50	. . . 4 $/\$
59	53, 58	pm2.61ine 2877	. . 3 $/\$
60	59	rexlimivv 3036	. 2
61		ax-rrecex 10008	. . . 4 $/\$
62		remulcl 10021	. . . . . . 7 $/\$
63	62	adantlr 751	. . . . . 6 $/\$ $/\$
64		eleq1 2689	. . . . . 6
65	63, 64	syl5ibcom 235	. . . . 5 $/\$ $/\$
66	65	rexlimdva 3031	. . . 4 $/\$
67	61, 66	mpd 15	. . 3 $/\$
68	67	rexlimiva 3028	. 2
69	44, 60, 68	mp2b 10	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

wne 2794

wrex 2913 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

ci 9938

caddc 9939

cmul 9941

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-mulcl 9998 ax-mulrcl 9999 ax-i2m1 10004 ax-1ne0 10005 ax-rrecex 10008 ax-cnre 10009

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653

This theorem is referenced by: 0re 10040 1red 10055 dedekind 10200 peano2re 10209 mul02lem2 10213 addid1 10216 renegcl 10344 peano2rem 10348 0reALT 10378 0lt1 10550 0le1 10551 relin01 10552 1le1 10655 eqneg 10745 ltp1 10861 ltm1 10863 recgt0 10867 mulgt1 10882 ltmulgt11 10883 lemulge11 10885 reclt1 10918 recgt1 10919 recgt1i 10920 recp1lt1 10921 recreclt 10922 recgt0ii 10929 ledivp1i 10949 ltdivp1i 10950 inelr 11010 cju 11016 nnssre 11024 nnge1 11046 nngt1ne1 11047 nnle1eq1 11048 nngt0 11049 nnnlt1 11050 nnrecre 11057 nnrecgt0 11058 nnsub 11059 2re 11090 3re 11094 4re 11097 5re 11099 6re 11101 7re 11103 8re 11105 9re 11107 10reOLD 11109 0le2 11111 2pos 11112 3pos 11114 4pos 11116 5pos 11118 6pos 11119 7pos 11120 8pos 11121 9pos 11122 10posOLD 11123 neg1rr 11125 neg1lt0 11127 1lt2 11194 1lt3 11196 1lt4 11199 1lt5 11203 1lt6 11208 1lt7 11214 1lt8 11221 1lt9 11229 1lt10OLD 11238 1ne2 11240 1le2 11241 1le3 11244 halflt1 11250 addltmul 11268 nnunb 11288 elnnnn0c 11338 nn0ge2m1nn 11360 elnnz1 11403 znnnlt1 11404 zltp1le 11427 zleltp1 11428 nn0lt2 11440 recnz 11452 gtndiv 11454 3halfnz 11456 1lt10 11681 eluzp1m1 11711 eluzp1p1 11713 eluz2b2 11761 zbtwnre 11786 rebtwnz 11787 1rp 11836 divlt1lt 11899 divle1le 11900 nnledivrp 11940 qbtwnxr 12031 xmulid1 12109 xmulid2 12110 xmulm1 12111 x2times 12129 xrub 12142 0elunit 12290 1elunit 12291 divelunit 12314 lincmb01cmp 12315 iccf1o 12316 xov1plusxeqvd 12318 unitssre 12319 0nelfz1 12360 fzpreddisj 12390 fznatpl1 12395 fztpval 12402 fraclt1 12603 fracle1 12604 flbi2 12618 ico01fl0 12620 fldiv4p1lem1div2 12636 fldiv4lem1div2 12638 fldiv 12659 modid 12695 1mod 12702 m1modnnsub1 12716 modm1p1mod0 12721 seqf1olem1 12840 reexpcl 12877 reexpclz 12880 expge0 12896 expge1 12897 expgt1 12898 bernneq 12990 bernneq2 12991 expnbnd 12993 expnlbnd 12994 expnlbnd2 12995 expmulnbnd 12996 discr1 13000 facwordi 13076 faclbnd3 13079 faclbnd4lem1 13080 faclbnd4lem4 13083 faclbnd6 13086 facavg 13088 hashv01gt1 13133 hashge1 13178 hashnn0n0nn 13180 hash1snb 13207 hashgt12el 13210 hashgt12el2 13211 hashfun 13224 hashge2el2dif 13262 brfi1indALT 13282 brfi1indALTOLD 13288 lsw0 13352 f1oun2prg 13662 sgn1 13832 cjexp 13890 re1 13894 im1 13895 rei 13896 imi 13897 sqrlem1 13983 sqrlem2 13984 sqrlem3 13985 sqrlem4 13986 sqrlem7 13989 resqrex 13991 sqrt1 14012 sqrt2gt1lt2 14015 sqrtm1 14016 abs1 14037 absrdbnd 14081 caubnd2 14097 mulcn2 14326 reccn2 14327 rlimno1 14384 o1fsum 14545 expcnv 14596 geolim 14601 geolim2 14602 georeclim 14603 geomulcvg 14607 geoisumr 14609 geoisum1c 14611 geoihalfsum 14614 fprodreclf 14689 fprodge0 14724 fprodge1 14726 rerisefaccl 14748 refallfaccl 14749 ere 14819 ege2le3 14820 efgt1 14846 resin4p 14868 recos4p 14869 tanhbnd 14891 sinbnd 14910 cosbnd 14911 sinbnd2 14912 cosbnd2 14913 ef01bndlem 14914 sin01bnd 14915 cos01bnd 14916 cos1bnd 14917 cos2bnd 14918 sinltx 14919 sin01gt0 14920 cos01gt0 14921 sin02gt0 14922 sincos1sgn 14923 ene1 14938 rpnnen2lem2 14944 rpnnen2lem3 14945 rpnnen2lem4 14946 rpnnen2lem9 14951 rpnnen2lem12 14954 ruclem6 14964 ruclem11 14969 ruclem12 14970 3dvds 15052 3dvdsOLD 15053 halfleoddlt 15086 n2dvds1 15104 flodddiv4 15137 sadcadd 15180 isprm3 15396 sqnprm 15414 coprm 15423 phibndlem 15475 pythagtriplem3 15523 pcmpt 15596 fldivp1 15601 pockthi 15611 infpn2 15617 resslem 15933 basendxnmulrndx 15999 slotsbhcdif 16080 oppcbas 16378 rescbas 16489 rescabs 16493 odubas 17133 lt6abl 18296 srgbinomlem4 18543 abvneg 18834 abvtrivd 18840 rmodislmod 18931 isnzr2hash 19264 0ringnnzr 19269 cnfldfun 19758 xrsmcmn 19769 xrsnsgrp 19782 gzrngunitlem 19811 gzrngunit 19812 rge0srg 19817 psgnodpmr 19936 remulg 19953 resubdrg 19954 thlbas 20040 matbas 20219 leordtval2 21016 tuslem 22071 setsmsbas 22280 dscmet 22377 dscopn 22378 nrginvrcnlem 22495 nmoid 22546 idnghm 22547 tgioo 22599 blcvx 22601 metnrmlem1a 22661 metnrmlem1 22662 iicmp 22689 iiconn 22690 iirev 22728 iihalf1 22730 iihalf2 22732 iihalf2cn 22733 elii1 22734 elii2 22735 iimulcl 22736 icopnfcnv 22741 icopnfhmeo 22742 iccpnfcnv 22743 iccpnfhmeo 22744 xrhmeo 22745 xrhmph 22746 evth 22758 xlebnum 22764 lebnumii 22765 htpycc 22779 reparphti 22797 pcoval1 22813 pco1 22815 pcoval2 22816 pcocn 22817 pcohtpylem 22819 pcopt 22822 pcopt2 22823 pcoass 22824 pcorevlem 22826 nmhmcn 22920 ncvs1 22957 ovolunlem1a 23264 vitalilem2 23378 vitalilem4 23380 vitalilem5 23381 vitali 23382 i1f1 23457 itg11 23458 itg2const 23507 itg2monolem1 23517 itg2monolem3 23519 dveflem 23742 dvlipcn 23757 dvcvx 23783 ply1remlem 23922 fta1blem 23928 vieta1lem2 24066 aalioulem3 24089 aalioulem5 24091 aaliou3lem2 24098 ulmbdd 24152 iblulm 24161 radcnvlem1 24167 dvradcnv 24175 abelthlem2 24186 abelthlem3 24187 abelthlem5 24189 abelthlem7 24192 abelth 24195 abelth2 24196 reeff1olem 24200 reeff1o 24201 sinhalfpilem 24215 tangtx 24257 sincos4thpi 24265 pige3 24269 coskpi 24272 recosf1o 24281 tanregt0 24285 efif1olem3 24290 efif1olem4 24291 loge 24333 logdivlti 24366 logcnlem4 24391 logf1o2 24396 dvlog2lem 24398 logtayl 24406 logccv 24409 recxpcl 24421 cxplea 24442 cxpcn3lem 24488 cxpaddlelem 24492 loglesqrt 24499 logblog 24530 ang180lem2 24540 angpined 24557 chordthmlem4 24562 acosrecl 24630 atancj 24637 atanlogaddlem 24640 atantan 24650 atans2 24658 ressatans 24661 leibpi 24669 log2le1 24677 birthdaylem3 24680 cxp2lim 24703 cxploglim 24704 cxploglim2 24705 divsqrtsumlem 24706 cvxcl 24711 scvxcvx 24712 jensenlem2 24714 amgmlem 24716 emcllem2 24723 emcllem4 24725 emcllem6 24727 emcllem7 24728 emre 24732 emgt0 24733 harmonicbnd3 24734 harmonicubnd 24736 harmonicbnd4 24737 zetacvg 24741 lgamgulmlem2 24756 ftalem1 24799 ftalem2 24800 ftalem5 24803 issqf 24862 cht1 24891 chp1 24893 ppiltx 24903 mumullem2 24906 ppiublem1 24927 ppiub 24929 chtublem 24936 chtub 24937 logfacbnd3 24948 logexprlim 24950 perfectlem2 24955 dchrinv 24986 dchr1re 24988 efexple 25006 bposlem1 25009 bposlem2 25010 bposlem5 25013 bposlem8 25016 lgsdir2lem1 25050 lgsdir2lem5 25054 lgsdir 25057 lgsne0 25060 lgsabs1 25061 lgsdinn0 25070 gausslemma2dlem0i 25089 lgseisen 25104 m1lgs 25113 2lgslem3 25129 chebbnd1lem3 25160 chebbnd1 25161 chtppilimlem1 25162 chtppilimlem2 25163 chtppilim 25164 chpchtlim 25168 vmadivsumb 25172 rplogsumlem2 25174 rpvmasumlem 25176 dchrmusumlema 25182 dchrmusum2 25183 dchrvmasumlem2 25187 dchrvmasumiflem1 25190 dchrisum0flblem1 25197 dchrisum0flblem2 25198 dchrisum0fno1 25200 rpvmasum2 25201 dchrisum0re 25202 dchrisum0lema 25203 dchrisum0lem1b 25204 dchrisum0lem1 25205 dchrisum0lem2a 25206 dchrisum0lem2 25207 logdivsum 25222 mulog2sumlem2 25224 2vmadivsumlem 25229 log2sumbnd 25233 selbergb 25238 selberg2b 25241 chpdifbndlem1 25242 selberg3lem1 25246 selberg3lem2 25247 selberg4lem1 25249 pntrmax 25253 pntrsumo1 25254 selbergsb 25264 pntrlog2bndlem3 25268 pntrlog2bndlem5 25270 pntpbnd1a 25274 pntpbnd2 25276 pntibndlem1 25278 pntibndlem2 25280 pntibndlem3 25281 pntibnd 25282 pntlemd 25283 pntlemc 25284 pntlemb 25286 pntlemr 25291 pntlemf 25294 pntlemk 25295 pntlemo 25296 pntlem3 25298 pntleml 25300 pnt 25303 abvcxp 25304 ostth2lem1 25307 padicabvf 25320 padicabvcxp 25321 ostth1 25322 ostth2lem2 25323 ostth2lem3 25324 ostth2lem4 25325 ostth2 25326 ostth3 25327 ostth 25328 trgcgrg 25410 ttgcontlem1 25765 brbtwn2 25785 colinearalglem4 25789 ax5seglem1 25808 ax5seglem2 25809 ax5seglem3 25811 ax5seglem5 25813 ax5seglem6 25814 ax5seglem9 25817 ax5seg 25818 axbtwnid 25819 axpaschlem 25820 axpasch 25821 axlowdimlem6 25827 axlowdimlem10 25831 axlowdimlem16 25837 axlowdim1 25839 axlowdim2 25840 axlowdim 25841 axcontlem2 25845 axcontlem4 25847 axcontlem7 25850 lfgrnloop 26020 lfuhgr1v0e 26146 usgrexmpldifpr 26150 usgrexmplef 26151 1loopgrvd2 26399 vdegp1bi 26433 lfgrwlkprop 26584 pthdlem1 26662 pthdlem2 26664 upgr4cycl4dv4e 27045 konigsberglem2 27115 konigsberglem3 27116 konigsberglem5 27118 frgrreg 27252 ex-dif 27280 ex-in 27282 ex-pss 27285 ex-res 27298 ex-fl 27304 nv1 27530 smcnlem 27552 ipidsq 27565 nmlno0lem 27648 norm-ii-i 27994 bcs2 28039 norm1 28106 nmopub2tALT 28768 nmfnleub2 28785 nmlnop0iALT 28854 nmopun 28873 unopbd 28874 nmopadjlem 28948 nmopcoadji 28960 pjnmopi 29007 pjbdlni 29008 stge0 29083 stle1 29084 hstle1 29085 hstle 29089 hstles 29090 stge1i 29097 stlesi 29100 staddi 29105 stadd3i 29107 strlem1 29109 strlem3a 29111 strlem5 29114 jplem1 29127 cdj1i 29292 addltmulALT 29305 xlt2addrd 29523 pr01ssre 29570 dp2lt10 29591 dp2ltsuc 29593 dp2ltc 29594 dplti 29613 dpmul4 29622 xdivrec 29635 xrsmulgzz 29678 xrnarchi 29738 resvbas 29832 rearchi 29842 xrge0slmod 29844 submateqlem1 29873 elunitrn 29943 elunitge0 29945 unitssxrge0 29946 unitdivcld 29947 xrge0iifcnv 29979 xrge0iifcv 29980 xrge0iifiso 29981 xrge0iifhom 29983 zrhre 30063 indf 30077 indfval 30078 esumcst 30125 hasheuni 30147 cntnevol 30291 ddemeas 30299 omssubadd 30362 iwrdsplit 30449 prob01 30475 dstfrvclim1 30539 coinfliprv 30544 ballotlem2 30550 ballotlem4 30560 ballotlemi1 30564 ballotlemic 30568 sgnclre 30601 sgnnbi 30607 sgnpbi 30608 sgnmulsgp 30612 plymulx0 30624 plymulx 30625 signswch 30638 signstf 30643 signsvfn 30659 itgexpif 30684 hgt750lemd 30726 logdivsqrle 30728 hgt750lem 30729 hgt750lem2 30730 hgt750leme 30736 tgoldbachgnn 30737 subfacp1lem1 31161 subfacp1lem5 31166 resconn 31228 iisconn 31234 iillysconn 31235 snmlff 31311 problem2 31559 problem2OLD 31560 problem3 31561 sinccvglem 31566 fz0n 31616 dnizeq0 32465 dnibndlem12 32479 knoppcnlem4 32486 knoppndvlem13 32515 cnndvlem1 32528 relowlpssretop 33212 sin2h 33399 cos2h 33400 tan2h 33401 poimirlem7 33416 poimirlem16 33425 poimirlem17 33426 poimirlem19 33428 poimirlem20 33429 poimirlem22 33431 poimirlem23 33432 poimirlem29 33438 poimirlem30 33439 poimirlem31 33440 poimirlem32 33441 broucube 33443 itg2addnclem3 33463 asindmre 33495 dvasin 33496 dvacos 33497 dvreasin 33498 dvreacos 33499 areacirclem1 33500 fdc 33541 geomcau 33555 cntotbnd 33595 heiborlem8 33617 bfplem2 33622 bfp 33623 rabren3dioph 37379 pellexlem5 37397 pellexlem6 37398 pell1qrgaplem 37437 pell14qrgap 37439 pellqrex 37443 pellfundre 37445 pellfundlb 37448 pellfund14gap 37451 rmspecsqrtnqOLD 37471 jm2.17a 37527 acongeq 37550 jm2.23 37563 jm3.1lem2 37585 relexp01min 38005 imo72b2 38475 cvgdvgrat 38512 lhe4.4ex1a 38528 binomcxplemnotnn0 38555 isosctrlem1ALT 39170 supxrgelem 39553 xrlexaddrp 39568 infxr 39583 infleinflem2 39587 1xr 39686 sumnnodd 39862 limsup10exlem 40004 limsup10ex 40005 liminf10ex 40006 dvnprodlem3 40163 stoweidlem1 40218 stoweidlem18 40235 stoweidlem19 40236 stoweidlem26 40243 stoweidlem34 40251 stoweidlem40 40257 stoweidlem41 40258 stoweidlem59 40276 stoweid 40280 stirlinglem10 40300 stirlinglem11 40301 dirkercncflem1 40320 fourierdlem16 40340 fourierdlem21 40345 fourierdlem22 40346 fourierdlem42 40366 fourierdlem68 40391 fourierdlem83 40406 fourierdlem103 40426 sqwvfourb 40446 fouriersw 40448 etransclem23 40474 salexct2 40557 salgencntex 40561 ovn0lem 40779 smfmullem3 41000 smfmullem4 41001 zm1nn 41316 m1mod0mod1 41339 fmtnosqrt 41451 perfectALTVlem2 41631 nnsum3primesprm 41678 nnsum4primesodd 41684 nnsum4primesoddALTV 41685 nnsum4primeseven 41688 nnsum4primesevenALTV 41689 tgblthelfgott 41703 tgoldbach 41705 tgblthelfgottOLD 41709 tgoldbachOLD 41712 expnegico01 42308 regt1loggt0 42330 rege1logbrege0 42352 rege1logbzge0 42353 blennnelnn 42370 dignnld 42397 nn0sumshdiglemA 42413 nn0sumshdiglem1 42415

W3C validator