Step |
Hyp |
Ref |
Expression |
1 |
|
rpnnen1lem.1 |
โข ๐ = { ๐ โ โค โฃ ( ๐ / ๐ ) < ๐ฅ } |
2 |
|
rpnnen1lem.2 |
โข ๐น = ( ๐ฅ โ โ โฆ ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) ) |
3 |
|
rpnnen1lem.n |
โข โ โ V |
4 |
|
rpnnen1lem.q |
โข โ โ V |
5 |
3
|
mptex |
โข ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) โ V |
6 |
2
|
fvmpt2 |
โข ( ( ๐ฅ โ โ โง ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) โ V ) โ ( ๐น โ ๐ฅ ) = ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) ) |
7 |
5 6
|
mpan2 |
โข ( ๐ฅ โ โ โ ( ๐น โ ๐ฅ ) = ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) ) |
8 |
|
ssrab2 |
โข { ๐ โ โค โฃ ( ๐ / ๐ ) < ๐ฅ } โ โค |
9 |
1 8
|
eqsstri |
โข ๐ โ โค |
10 |
9
|
a1i |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ ๐ โ โค ) |
11 |
|
nnre |
โข ( ๐ โ โ โ ๐ โ โ ) |
12 |
|
remulcl |
โข ( ( ๐ โ โ โง ๐ฅ โ โ ) โ ( ๐ ยท ๐ฅ ) โ โ ) |
13 |
12
|
ancoms |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ฅ ) โ โ ) |
14 |
11 13
|
sylan2 |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ ( ๐ ยท ๐ฅ ) โ โ ) |
15 |
|
btwnz |
โข ( ( ๐ ยท ๐ฅ ) โ โ โ ( โ ๐ โ โค ๐ < ( ๐ ยท ๐ฅ ) โง โ ๐ โ โค ( ๐ ยท ๐ฅ ) < ๐ ) ) |
16 |
15
|
simpld |
โข ( ( ๐ ยท ๐ฅ ) โ โ โ โ ๐ โ โค ๐ < ( ๐ ยท ๐ฅ ) ) |
17 |
14 16
|
syl |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ โ ๐ โ โค ๐ < ( ๐ ยท ๐ฅ ) ) |
18 |
|
zre |
โข ( ๐ โ โค โ ๐ โ โ ) |
19 |
18
|
adantl |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ๐ โ โ ) |
20 |
|
simpll |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ๐ฅ โ โ ) |
21 |
|
nngt0 |
โข ( ๐ โ โ โ 0 < ๐ ) |
22 |
11 21
|
jca |
โข ( ๐ โ โ โ ( ๐ โ โ โง 0 < ๐ ) ) |
23 |
22
|
ad2antlr |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ( ๐ โ โ โง 0 < ๐ ) ) |
24 |
|
ltdivmul |
โข ( ( ๐ โ โ โง ๐ฅ โ โ โง ( ๐ โ โ โง 0 < ๐ ) ) โ ( ( ๐ / ๐ ) < ๐ฅ โ ๐ < ( ๐ ยท ๐ฅ ) ) ) |
25 |
19 20 23 24
|
syl3anc |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ( ( ๐ / ๐ ) < ๐ฅ โ ๐ < ( ๐ ยท ๐ฅ ) ) ) |
26 |
25
|
rexbidva |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ ( โ ๐ โ โค ( ๐ / ๐ ) < ๐ฅ โ โ ๐ โ โค ๐ < ( ๐ ยท ๐ฅ ) ) ) |
27 |
17 26
|
mpbird |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ โ ๐ โ โค ( ๐ / ๐ ) < ๐ฅ ) |
28 |
|
rabn0 |
โข ( { ๐ โ โค โฃ ( ๐ / ๐ ) < ๐ฅ } โ โ
โ โ ๐ โ โค ( ๐ / ๐ ) < ๐ฅ ) |
29 |
27 28
|
sylibr |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ { ๐ โ โค โฃ ( ๐ / ๐ ) < ๐ฅ } โ โ
) |
30 |
1
|
neeq1i |
โข ( ๐ โ โ
โ { ๐ โ โค โฃ ( ๐ / ๐ ) < ๐ฅ } โ โ
) |
31 |
29 30
|
sylibr |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ ๐ โ โ
) |
32 |
1
|
reqabi |
โข ( ๐ โ ๐ โ ( ๐ โ โค โง ( ๐ / ๐ ) < ๐ฅ ) ) |
33 |
11
|
ad2antlr |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ๐ โ โ ) |
34 |
33 20 12
|
syl2anc |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ( ๐ ยท ๐ฅ ) โ โ ) |
35 |
|
ltle |
โข ( ( ๐ โ โ โง ( ๐ ยท ๐ฅ ) โ โ ) โ ( ๐ < ( ๐ ยท ๐ฅ ) โ ๐ โค ( ๐ ยท ๐ฅ ) ) ) |
36 |
19 34 35
|
syl2anc |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ( ๐ < ( ๐ ยท ๐ฅ ) โ ๐ โค ( ๐ ยท ๐ฅ ) ) ) |
37 |
25 36
|
sylbid |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ โค ) โ ( ( ๐ / ๐ ) < ๐ฅ โ ๐ โค ( ๐ ยท ๐ฅ ) ) ) |
38 |
37
|
impr |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ( ๐ โ โค โง ( ๐ / ๐ ) < ๐ฅ ) ) โ ๐ โค ( ๐ ยท ๐ฅ ) ) |
39 |
32 38
|
sylan2b |
โข ( ( ( ๐ฅ โ โ โง ๐ โ โ ) โง ๐ โ ๐ ) โ ๐ โค ( ๐ ยท ๐ฅ ) ) |
40 |
39
|
ralrimiva |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ โ ๐ โ ๐ ๐ โค ( ๐ ยท ๐ฅ ) ) |
41 |
|
breq2 |
โข ( ๐ฆ = ( ๐ ยท ๐ฅ ) โ ( ๐ โค ๐ฆ โ ๐ โค ( ๐ ยท ๐ฅ ) ) ) |
42 |
41
|
ralbidv |
โข ( ๐ฆ = ( ๐ ยท ๐ฅ ) โ ( โ ๐ โ ๐ ๐ โค ๐ฆ โ โ ๐ โ ๐ ๐ โค ( ๐ ยท ๐ฅ ) ) ) |
43 |
42
|
rspcev |
โข ( ( ( ๐ ยท ๐ฅ ) โ โ โง โ ๐ โ ๐ ๐ โค ( ๐ ยท ๐ฅ ) ) โ โ ๐ฆ โ โ โ ๐ โ ๐ ๐ โค ๐ฆ ) |
44 |
14 40 43
|
syl2anc |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ โ ๐ฆ โ โ โ ๐ โ ๐ ๐ โค ๐ฆ ) |
45 |
|
suprzcl |
โข ( ( ๐ โ โค โง ๐ โ โ
โง โ ๐ฆ โ โ โ ๐ โ ๐ ๐ โค ๐ฆ ) โ sup ( ๐ , โ , < ) โ ๐ ) |
46 |
10 31 44 45
|
syl3anc |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ sup ( ๐ , โ , < ) โ ๐ ) |
47 |
9 46
|
sselid |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ sup ( ๐ , โ , < ) โ โค ) |
48 |
|
znq |
โข ( ( sup ( ๐ , โ , < ) โ โค โง ๐ โ โ ) โ ( sup ( ๐ , โ , < ) / ๐ ) โ โ ) |
49 |
47 48
|
sylancom |
โข ( ( ๐ฅ โ โ โง ๐ โ โ ) โ ( sup ( ๐ , โ , < ) / ๐ ) โ โ ) |
50 |
|
eqid |
โข ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) = ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) |
51 |
49 50
|
fmptd |
โข ( ๐ฅ โ โ โ ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) : โ โถ โ ) |
52 |
4 3
|
elmap |
โข ( ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) โ ( โ โm โ ) โ ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) : โ โถ โ ) |
53 |
51 52
|
sylibr |
โข ( ๐ฅ โ โ โ ( ๐ โ โ โฆ ( sup ( ๐ , โ , < ) / ๐ ) ) โ ( โ โm โ ) ) |
54 |
7 53
|
eqeltrd |
โข ( ๐ฅ โ โ โ ( ๐น โ ๐ฅ ) โ ( โ โm โ ) ) |