![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > reeff1olem | GIF version |
Description: Lemma for reeff1o 14197. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
Ref | Expression |
---|---|
reeff1olem | ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioossicc 9959 | . . 3 ⊢ (0(,)𝑈) ⊆ (0[,]𝑈) | |
2 | 0re 7957 | . . . . 5 ⊢ 0 ∈ ℝ | |
3 | iccssre 9955 | . . . . 5 ⊢ ((0 ∈ ℝ ∧ 𝑈 ∈ ℝ) → (0[,]𝑈) ⊆ ℝ) | |
4 | 2, 3 | mpan 424 | . . . 4 ⊢ (𝑈 ∈ ℝ → (0[,]𝑈) ⊆ ℝ) |
5 | 4 | adantr 276 | . . 3 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (0[,]𝑈) ⊆ ℝ) |
6 | 1, 5 | sstrid 3167 | . 2 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (0(,)𝑈) ⊆ ℝ) |
7 | 2 | a1i 9 | . . 3 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 0 ∈ ℝ) |
8 | simpl 109 | . . 3 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 𝑈 ∈ ℝ) | |
9 | 0lt1 8084 | . . . . 5 ⊢ 0 < 1 | |
10 | 1re 7956 | . . . . . 6 ⊢ 1 ∈ ℝ | |
11 | lttr 8031 | . . . . . 6 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((0 < 1 ∧ 1 < 𝑈) → 0 < 𝑈)) | |
12 | 2, 10, 11 | mp3an12 1327 | . . . . 5 ⊢ (𝑈 ∈ ℝ → ((0 < 1 ∧ 1 < 𝑈) → 0 < 𝑈)) |
13 | 9, 12 | mpani 430 | . . . 4 ⊢ (𝑈 ∈ ℝ → (1 < 𝑈 → 0 < 𝑈)) |
14 | 13 | imp 124 | . . 3 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 0 < 𝑈) |
15 | ax-resscn 7903 | . . . 4 ⊢ ℝ ⊆ ℂ | |
16 | 5, 15 | sstrdi 3168 | . . 3 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (0[,]𝑈) ⊆ ℂ) |
17 | efcn 14192 | . . . 4 ⊢ exp ∈ (ℂ–cn→ℂ) | |
18 | 17 | a1i 9 | . . 3 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → exp ∈ (ℂ–cn→ℂ)) |
19 | ssel2 3151 | . . . . 5 ⊢ (((0[,]𝑈) ⊆ ℝ ∧ 𝑦 ∈ (0[,]𝑈)) → 𝑦 ∈ ℝ) | |
20 | 19 | reefcld 11677 | . . . 4 ⊢ (((0[,]𝑈) ⊆ ℝ ∧ 𝑦 ∈ (0[,]𝑈)) → (exp‘𝑦) ∈ ℝ) |
21 | 5, 20 | sylan 283 | . . 3 ⊢ (((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) → (exp‘𝑦) ∈ ℝ) |
22 | ef0 11680 | . . . . 5 ⊢ (exp‘0) = 1 | |
23 | simpr 110 | . . . . 5 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 1 < 𝑈) | |
24 | 22, 23 | eqbrtrid 4039 | . . . 4 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (exp‘0) < 𝑈) |
25 | peano2re 8093 | . . . . . 6 ⊢ (𝑈 ∈ ℝ → (𝑈 + 1) ∈ ℝ) | |
26 | 25 | adantr 276 | . . . . 5 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (𝑈 + 1) ∈ ℝ) |
27 | reefcl 11676 | . . . . . 6 ⊢ (𝑈 ∈ ℝ → (exp‘𝑈) ∈ ℝ) | |
28 | 27 | adantr 276 | . . . . 5 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (exp‘𝑈) ∈ ℝ) |
29 | ltp1 8801 | . . . . . 6 ⊢ (𝑈 ∈ ℝ → 𝑈 < (𝑈 + 1)) | |
30 | 29 | adantr 276 | . . . . 5 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 𝑈 < (𝑈 + 1)) |
31 | 8 | recnd 7986 | . . . . . . 7 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 𝑈 ∈ ℂ) |
32 | ax-1cn 7904 | . . . . . . 7 ⊢ 1 ∈ ℂ | |
33 | addcom 8094 | . . . . . . 7 ⊢ ((𝑈 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑈 + 1) = (1 + 𝑈)) | |
34 | 31, 32, 33 | sylancl 413 | . . . . . 6 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (𝑈 + 1) = (1 + 𝑈)) |
35 | 8, 14 | elrpd 9693 | . . . . . . 7 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 𝑈 ∈ ℝ+) |
36 | efgt1p 11704 | . . . . . . 7 ⊢ (𝑈 ∈ ℝ+ → (1 + 𝑈) < (exp‘𝑈)) | |
37 | 35, 36 | syl 14 | . . . . . 6 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (1 + 𝑈) < (exp‘𝑈)) |
38 | 34, 37 | eqbrtrd 4026 | . . . . 5 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → (𝑈 + 1) < (exp‘𝑈)) |
39 | 8, 26, 28, 30, 38 | lttrd 8083 | . . . 4 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → 𝑈 < (exp‘𝑈)) |
40 | 24, 39 | jca 306 | . . 3 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ((exp‘0) < 𝑈 ∧ 𝑈 < (exp‘𝑈))) |
41 | simplll 533 | . . . . . . 7 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → 𝑈 ∈ ℝ) | |
42 | 2, 41, 3 | sylancr 414 | . . . . . 6 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → (0[,]𝑈) ⊆ ℝ) |
43 | simplr 528 | . . . . . 6 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → 𝑦 ∈ (0[,]𝑈)) | |
44 | 42, 43 | sseldd 3157 | . . . . 5 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → 𝑦 ∈ ℝ) |
45 | simprl 529 | . . . . . 6 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → 𝑧 ∈ (0[,]𝑈)) | |
46 | 42, 45 | sseldd 3157 | . . . . 5 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → 𝑧 ∈ ℝ) |
47 | 44, 46 | jca 306 | . . . 4 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → (𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ)) |
48 | simprr 531 | . . . 4 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → 𝑦 < 𝑧) | |
49 | efltim 11706 | . . . 4 ⊢ ((𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑦 < 𝑧 → (exp‘𝑦) < (exp‘𝑧))) | |
50 | 47, 48, 49 | sylc 62 | . . 3 ⊢ ((((𝑈 ∈ ℝ ∧ 1 < 𝑈) ∧ 𝑦 ∈ (0[,]𝑈)) ∧ (𝑧 ∈ (0[,]𝑈) ∧ 𝑦 < 𝑧)) → (exp‘𝑦) < (exp‘𝑧)) |
51 | 7, 8, 8, 14, 16, 18, 21, 40, 50 | ivthinc 14124 | . 2 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ (0(,)𝑈)(exp‘𝑥) = 𝑈) |
52 | ssrexv 3221 | . 2 ⊢ ((0(,)𝑈) ⊆ ℝ → (∃𝑥 ∈ (0(,)𝑈)(exp‘𝑥) = 𝑈 → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈)) | |
53 | 6, 51, 52 | sylc 62 | 1 ⊢ ((𝑈 ∈ ℝ ∧ 1 < 𝑈) → ∃𝑥 ∈ ℝ (exp‘𝑥) = 𝑈) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1353 ∈ wcel 2148 ∃wrex 2456 ⊆ wss 3130 class class class wbr 4004 ‘cfv 5217 (class class class)co 5875 ℂcc 7809 ℝcr 7810 0cc0 7811 1c1 7812 + caddc 7814 < clt 7992 ℝ+crp 9653 (,)cioo 9888 [,]cicc 9891 expce 11650 –cn→ccncf 14060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4119 ax-sep 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-iinf 4588 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-mulrcl 7910 ax-addcom 7911 ax-mulcom 7912 ax-addass 7913 ax-mulass 7914 ax-distr 7915 ax-i2m1 7916 ax-0lt1 7917 ax-1rid 7918 ax-0id 7919 ax-rnegex 7920 ax-precex 7921 ax-cnre 7922 ax-pre-ltirr 7923 ax-pre-ltwlin 7924 ax-pre-lttrn 7925 ax-pre-apti 7926 ax-pre-ltadd 7927 ax-pre-mulgt0 7928 ax-pre-mulext 7929 ax-arch 7930 ax-caucvg 7931 ax-pre-suploc 7932 ax-addf 7933 ax-mulf 7934 |
This theorem depends on definitions: df-bi 117 df-stab 831 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-if 3536 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-disj 3982 df-br 4005 df-opab 4066 df-mpt 4067 df-tr 4103 df-id 4294 df-po 4297 df-iso 4298 df-iord 4367 df-on 4369 df-ilim 4370 df-suc 4372 df-iom 4591 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-f1 5222 df-fo 5223 df-f1o 5224 df-fv 5225 df-isom 5226 df-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-of 6083 df-1st 6141 df-2nd 6142 df-recs 6306 df-irdg 6371 df-frec 6392 df-1o 6417 df-oadd 6421 df-er 6535 df-map 6650 df-pm 6651 df-en 6741 df-dom 6742 df-fin 6743 df-sup 6983 df-inf 6984 df-pnf 7994 df-mnf 7995 df-xr 7996 df-ltxr 7997 df-le 7998 df-sub 8130 df-neg 8131 df-reap 8532 df-ap 8539 df-div 8630 df-inn 8920 df-2 8978 df-3 8979 df-4 8980 df-n0 9177 df-z 9254 df-uz 9529 df-q 9620 df-rp 9654 df-xneg 9772 df-xadd 9773 df-ioo 9892 df-ico 9894 df-icc 9895 df-fz 10009 df-fzo 10143 df-seqfrec 10446 df-exp 10520 df-fac 10706 df-bc 10728 df-ihash 10756 df-shft 10824 df-cj 10851 df-re 10852 df-im 10853 df-rsqrt 11007 df-abs 11008 df-clim 11287 df-sumdc 11362 df-ef 11656 df-rest 12690 df-topgen 12709 df-psmet 13450 df-xmet 13451 df-met 13452 df-bl 13453 df-mopn 13454 df-top 13501 df-topon 13514 df-bases 13546 df-ntr 13599 df-cn 13691 df-cnp 13692 df-tx 13756 df-cncf 14061 df-limced 14128 df-dvap 14129 |
This theorem is referenced by: reeff1oleme 14196 reeff1o 14197 |
Copyright terms: Public domain | W3C validator |