Metamath Proof Explorer


Theorem rpnnen1lem1

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-Aug-2021) (Proof modification is discouraged.)

Ref Expression
Hypotheses rpnnen1lem.1 โŠข ๐‘‡ = { ๐‘› โˆˆ โ„ค โˆฃ ( ๐‘› / ๐‘˜ ) < ๐‘ฅ }
rpnnen1lem.2 โŠข ๐น = ( ๐‘ฅ โˆˆ โ„ โ†ฆ ( ๐‘˜ โˆˆ โ„• โ†ฆ ( sup ( ๐‘‡ , โ„ , < ) / ๐‘˜ ) ) )
rpnnen1lem.n โŠข โ„• โˆˆ V
rpnnen1lem.q โŠข โ„š โˆˆ V
Assertion rpnnen1lem1 ( ๐‘ฅ โˆˆ โ„ โ†’ ( ๐น โ€˜ ๐‘ฅ ) โˆˆ ( โ„š โ†‘m โ„• ) )

Proof

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 โ„• ) )