Step | Hyp | Ref
| Expression |
1 | | ere 11678 |
. . . . 5
โข e โ
โ |
2 | 1 | a1i 9 |
. . . 4
โข (๐ โ (0(,)e) โ e โ
โ) |
3 | | elioore 9912 |
. . . 4
โข (๐ โ (0(,)e) โ ๐ โ
โ) |
4 | | 0xr 8004 |
. . . . . . 7
โข 0 โ
โ* |
5 | 1 | rexri 8015 |
. . . . . . 7
โข e โ
โ* |
6 | | elioo2 9921 |
. . . . . . 7
โข ((0
โ โ* โง e โ โ*) โ (๐ โ (0(,)e) โ (๐ โ โ โง 0 <
๐ โง ๐ < e))) |
7 | 4, 5, 6 | mp2an 426 |
. . . . . 6
โข (๐ โ (0(,)e) โ (๐ โ โ โง 0 <
๐ โง ๐ < e)) |
8 | 7 | simp2bi 1013 |
. . . . 5
โข (๐ โ (0(,)e) โ 0 <
๐) |
9 | 3, 8 | gt0ap0d 8586 |
. . . 4
โข (๐ โ (0(,)e) โ ๐ # 0) |
10 | 2, 3, 9 | redivclapd 8792 |
. . 3
โข (๐ โ (0(,)e) โ (e /
๐) โ
โ) |
11 | 3 | recnd 7986 |
. . . . . 6
โข (๐ โ (0(,)e) โ ๐ โ
โ) |
12 | 11 | mulid2d 7976 |
. . . . 5
โข (๐ โ (0(,)e) โ (1
ยท ๐) = ๐) |
13 | 7 | simp3bi 1014 |
. . . . 5
โข (๐ โ (0(,)e) โ ๐ < e) |
14 | 12, 13 | eqbrtrd 4026 |
. . . 4
โข (๐ โ (0(,)e) โ (1
ยท ๐) <
e) |
15 | | 1red 7972 |
. . . . 5
โข (๐ โ (0(,)e) โ 1 โ
โ) |
16 | | ltmuldiv 8831 |
. . . . 5
โข ((1
โ โ โง e โ โ โง (๐ โ โ โง 0 < ๐)) โ ((1 ยท ๐) < e โ 1 < (e /
๐))) |
17 | 15, 2, 3, 8, 16 | syl112anc 1242 |
. . . 4
โข (๐ โ (0(,)e) โ ((1
ยท ๐) < e โ 1
< (e / ๐))) |
18 | 14, 17 | mpbid 147 |
. . 3
โข (๐ โ (0(,)e) โ 1 < (e
/ ๐)) |
19 | | reeff1olem 14195 |
. . 3
โข (((e /
๐) โ โ โง 1
< (e / ๐)) โ
โ๐ฆ โ โ
(expโ๐ฆ) = (e / ๐)) |
20 | 10, 18, 19 | syl2anc 411 |
. 2
โข (๐ โ (0(,)e) โ
โ๐ฆ โ โ
(expโ๐ฆ) = (e / ๐)) |
21 | | 1red 7972 |
. . . 4
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ 1 โ
โ) |
22 | | simprl 529 |
. . . 4
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ ๐ฆ โ โ) |
23 | 21, 22 | resubcld 8338 |
. . 3
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (1 โ ๐ฆ) โ
โ) |
24 | | 1cnd 7973 |
. . . . 5
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ 1 โ
โ) |
25 | 22 | recnd 7986 |
. . . . 5
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ ๐ฆ โ โ) |
26 | | efsub 11689 |
. . . . 5
โข ((1
โ โ โง ๐ฆ
โ โ) โ (expโ(1 โ ๐ฆ)) = ((expโ1) / (expโ๐ฆ))) |
27 | 24, 25, 26 | syl2anc 411 |
. . . 4
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ(1 โ
๐ฆ)) = ((expโ1) /
(expโ๐ฆ))) |
28 | | simprr 531 |
. . . . . . 7
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ๐ฆ) = (e / ๐)) |
29 | | df-e 11657 |
. . . . . . . 8
โข e =
(expโ1) |
30 | 29 | oveq1i 5885 |
. . . . . . 7
โข (e /
๐) = ((expโ1) / ๐) |
31 | 28, 30 | eqtr2di 2227 |
. . . . . 6
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ ((expโ1) /
๐) = (expโ๐ฆ)) |
32 | | efcl 11672 |
. . . . . . . 8
โข (1 โ
โ โ (expโ1) โ โ) |
33 | 24, 32 | syl 14 |
. . . . . . 7
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ1) โ
โ) |
34 | | efcl 11672 |
. . . . . . . 8
โข (๐ฆ โ โ โ
(expโ๐ฆ) โ
โ) |
35 | 25, 34 | syl 14 |
. . . . . . 7
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ๐ฆ) โ
โ) |
36 | 11 | adantr 276 |
. . . . . . 7
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ ๐ โ โ) |
37 | 9 | adantr 276 |
. . . . . . 7
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ ๐ # 0) |
38 | 33, 35, 36, 37 | divmulap2d 8781 |
. . . . . 6
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (((expโ1) /
๐) = (expโ๐ฆ) โ (expโ1) = (๐ ยท (expโ๐ฆ)))) |
39 | 31, 38 | mpbid 147 |
. . . . 5
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ1) =
(๐ ยท
(expโ๐ฆ))) |
40 | 22 | rpefcld 11694 |
. . . . . . 7
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ๐ฆ) โ
โ+) |
41 | 40 | rpap0d 9702 |
. . . . . 6
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ๐ฆ) # 0) |
42 | 33, 36, 35, 41 | divmulap3d 8782 |
. . . . 5
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (((expโ1) /
(expโ๐ฆ)) = ๐ โ (expโ1) = (๐ ยท (expโ๐ฆ)))) |
43 | 39, 42 | mpbird 167 |
. . . 4
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ ((expโ1) /
(expโ๐ฆ)) = ๐) |
44 | 27, 43 | eqtrd 2210 |
. . 3
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ (expโ(1 โ
๐ฆ)) = ๐) |
45 | | fveqeq2 5525 |
. . . 4
โข (๐ฅ = (1 โ ๐ฆ) โ ((expโ๐ฅ) = ๐ โ (expโ(1 โ ๐ฆ)) = ๐)) |
46 | 45 | rspcev 2842 |
. . 3
โข (((1
โ ๐ฆ) โ โ
โง (expโ(1 โ ๐ฆ)) = ๐) โ โ๐ฅ โ โ (expโ๐ฅ) = ๐) |
47 | 23, 44, 46 | syl2anc 411 |
. 2
โข ((๐ โ (0(,)e) โง (๐ฆ โ โ โง
(expโ๐ฆ) = (e / ๐))) โ โ๐ฅ โ โ (expโ๐ฅ) = ๐) |
48 | 20, 47 | rexlimddv 2599 |
1
โข (๐ โ (0(,)e) โ
โ๐ฅ โ โ
(expโ๐ฅ) = ๐) |