Metamath Proof Explorer


Theorem pntlemq

Description: Lemma for pntlemj . (Contributed by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses pntlem1.r โŠข ๐‘… = ( ๐‘Ž โˆˆ โ„+ โ†ฆ ( ( ฯˆ โ€˜ ๐‘Ž ) โˆ’ ๐‘Ž ) )
pntlem1.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„+ )
pntlem1.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„+ )
pntlem1.l โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ( 0 (,) 1 ) )
pntlem1.d โŠข ๐ท = ( ๐ด + 1 )
pntlem1.f โŠข ๐น = ( ( 1 โˆ’ ( 1 / ๐ท ) ) ยท ( ( ๐ฟ / ( 3 2 ยท ๐ต ) ) / ( ๐ท โ†‘ 2 ) ) )
pntlem1.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„+ )
pntlem1.u2 โŠข ( ๐œ‘ โ†’ ๐‘ˆ โ‰ค ๐ด )
pntlem1.e โŠข ๐ธ = ( ๐‘ˆ / ๐ท )
pntlem1.k โŠข ๐พ = ( exp โ€˜ ( ๐ต / ๐ธ ) )
pntlem1.y โŠข ( ๐œ‘ โ†’ ( ๐‘Œ โˆˆ โ„+ โˆง 1 โ‰ค ๐‘Œ ) )
pntlem1.x โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ โ„+ โˆง ๐‘Œ < ๐‘‹ ) )
pntlem1.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
pntlem1.w โŠข ๐‘Š = ( ( ( ๐‘Œ + ( 4 / ( ๐ฟ ยท ๐ธ ) ) ) โ†‘ 2 ) + ( ( ( ๐‘‹ ยท ( ๐พ โ†‘ 2 ) ) โ†‘ 4 ) + ( exp โ€˜ ( ( ( 3 2 ยท ๐ต ) / ( ( ๐‘ˆ โˆ’ ๐ธ ) ยท ( ๐ฟ ยท ( ๐ธ โ†‘ 2 ) ) ) ) ยท ( ( ๐‘ˆ ยท 3 ) + ๐ถ ) ) ) ) )
pntlem1.z โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( ๐‘Š [,) +โˆž ) )
pntlem1.m โŠข ๐‘€ = ( ( โŒŠ โ€˜ ( ( log โ€˜ ๐‘‹ ) / ( log โ€˜ ๐พ ) ) ) + 1 )
pntlem1.n โŠข ๐‘ = ( โŒŠ โ€˜ ( ( ( log โ€˜ ๐‘ ) / ( log โ€˜ ๐พ ) ) / 2 ) )
pntlem1.U โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ง โˆˆ ( ๐‘Œ [,) +โˆž ) ( abs โ€˜ ( ( ๐‘… โ€˜ ๐‘ง ) / ๐‘ง ) ) โ‰ค ๐‘ˆ )
pntlem1.K โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฆ โˆˆ ( ๐‘‹ (,) +โˆž ) โˆƒ ๐‘ง โˆˆ โ„+ ( ( ๐‘ฆ < ๐‘ง โˆง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘ง ) < ( ๐พ ยท ๐‘ฆ ) ) โˆง โˆ€ ๐‘ข โˆˆ ( ๐‘ง [,] ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘ง ) ) ( abs โ€˜ ( ( ๐‘… โ€˜ ๐‘ข ) / ๐‘ข ) ) โ‰ค ๐ธ ) )
pntlem1.o โŠข ๐‘‚ = ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) )
pntlem1.v โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ โ„+ )
pntlem1.V โŠข ( ๐œ‘ โ†’ ( ( ( ๐พ โ†‘ ๐ฝ ) < ๐‘‰ โˆง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) < ( ๐พ ยท ( ๐พ โ†‘ ๐ฝ ) ) ) โˆง โˆ€ ๐‘ข โˆˆ ( ๐‘‰ [,] ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ( abs โ€˜ ( ( ๐‘… โ€˜ ๐‘ข ) / ๐‘ข ) ) โ‰ค ๐ธ ) )
pntlem1.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ ( ๐‘€ ..^ ๐‘ ) )
pntlem1.i โŠข ๐ผ = ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) )
Assertion pntlemq ( ๐œ‘ โ†’ ๐ผ โŠ† ๐‘‚ )

Proof

Step Hyp Ref Expression
1 pntlem1.r โŠข ๐‘… = ( ๐‘Ž โˆˆ โ„+ โ†ฆ ( ( ฯˆ โ€˜ ๐‘Ž ) โˆ’ ๐‘Ž ) )
2 pntlem1.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„+ )
3 pntlem1.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„+ )
4 pntlem1.l โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ ( 0 (,) 1 ) )
5 pntlem1.d โŠข ๐ท = ( ๐ด + 1 )
6 pntlem1.f โŠข ๐น = ( ( 1 โˆ’ ( 1 / ๐ท ) ) ยท ( ( ๐ฟ / ( 3 2 ยท ๐ต ) ) / ( ๐ท โ†‘ 2 ) ) )
7 pntlem1.u โŠข ( ๐œ‘ โ†’ ๐‘ˆ โˆˆ โ„+ )
8 pntlem1.u2 โŠข ( ๐œ‘ โ†’ ๐‘ˆ โ‰ค ๐ด )
9 pntlem1.e โŠข ๐ธ = ( ๐‘ˆ / ๐ท )
10 pntlem1.k โŠข ๐พ = ( exp โ€˜ ( ๐ต / ๐ธ ) )
11 pntlem1.y โŠข ( ๐œ‘ โ†’ ( ๐‘Œ โˆˆ โ„+ โˆง 1 โ‰ค ๐‘Œ ) )
12 pntlem1.x โŠข ( ๐œ‘ โ†’ ( ๐‘‹ โˆˆ โ„+ โˆง ๐‘Œ < ๐‘‹ ) )
13 pntlem1.c โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
14 pntlem1.w โŠข ๐‘Š = ( ( ( ๐‘Œ + ( 4 / ( ๐ฟ ยท ๐ธ ) ) ) โ†‘ 2 ) + ( ( ( ๐‘‹ ยท ( ๐พ โ†‘ 2 ) ) โ†‘ 4 ) + ( exp โ€˜ ( ( ( 3 2 ยท ๐ต ) / ( ( ๐‘ˆ โˆ’ ๐ธ ) ยท ( ๐ฟ ยท ( ๐ธ โ†‘ 2 ) ) ) ) ยท ( ( ๐‘ˆ ยท 3 ) + ๐ถ ) ) ) ) )
15 pntlem1.z โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( ๐‘Š [,) +โˆž ) )
16 pntlem1.m โŠข ๐‘€ = ( ( โŒŠ โ€˜ ( ( log โ€˜ ๐‘‹ ) / ( log โ€˜ ๐พ ) ) ) + 1 )
17 pntlem1.n โŠข ๐‘ = ( โŒŠ โ€˜ ( ( ( log โ€˜ ๐‘ ) / ( log โ€˜ ๐พ ) ) / 2 ) )
18 pntlem1.U โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ง โˆˆ ( ๐‘Œ [,) +โˆž ) ( abs โ€˜ ( ( ๐‘… โ€˜ ๐‘ง ) / ๐‘ง ) ) โ‰ค ๐‘ˆ )
19 pntlem1.K โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฆ โˆˆ ( ๐‘‹ (,) +โˆž ) โˆƒ ๐‘ง โˆˆ โ„+ ( ( ๐‘ฆ < ๐‘ง โˆง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘ง ) < ( ๐พ ยท ๐‘ฆ ) ) โˆง โˆ€ ๐‘ข โˆˆ ( ๐‘ง [,] ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘ง ) ) ( abs โ€˜ ( ( ๐‘… โ€˜ ๐‘ข ) / ๐‘ข ) ) โ‰ค ๐ธ ) )
20 pntlem1.o โŠข ๐‘‚ = ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) )
21 pntlem1.v โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ โ„+ )
22 pntlem1.V โŠข ( ๐œ‘ โ†’ ( ( ( ๐พ โ†‘ ๐ฝ ) < ๐‘‰ โˆง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) < ( ๐พ ยท ( ๐พ โ†‘ ๐ฝ ) ) ) โˆง โˆ€ ๐‘ข โˆˆ ( ๐‘‰ [,] ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ( abs โ€˜ ( ( ๐‘… โ€˜ ๐‘ข ) / ๐‘ข ) ) โ‰ค ๐ธ ) )
23 pntlem1.j โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ ( ๐‘€ ..^ ๐‘ ) )
24 pntlem1.i โŠข ๐ผ = ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) )
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb โŠข ( ๐œ‘ โ†’ ( ๐‘ โˆˆ โ„+ โˆง ( 1 < ๐‘ โˆง e โ‰ค ( โˆš โ€˜ ๐‘ ) โˆง ( โˆš โ€˜ ๐‘ ) โ‰ค ( ๐‘ / ๐‘Œ ) ) โˆง ( ( 4 / ( ๐ฟ ยท ๐ธ ) ) โ‰ค ( โˆš โ€˜ ๐‘ ) โˆง ( ( ( log โ€˜ ๐‘‹ ) / ( log โ€˜ ๐พ ) ) + 2 ) โ‰ค ( ( ( log โ€˜ ๐‘ ) / ( log โ€˜ ๐พ ) ) / 4 ) โˆง ( ( ๐‘ˆ ยท 3 ) + ๐ถ ) โ‰ค ( ( ( ๐‘ˆ โˆ’ ๐ธ ) ยท ( ( ๐ฟ ยท ( ๐ธ โ†‘ 2 ) ) / ( 3 2 ยท ๐ต ) ) ) ยท ( log โ€˜ ๐‘ ) ) ) ) )
26 25 simp1d โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„+ )
27 1 2 3 4 5 6 7 8 9 10 pntlemc โŠข ( ๐œ‘ โ†’ ( ๐ธ โˆˆ โ„+ โˆง ๐พ โˆˆ โ„+ โˆง ( ๐ธ โˆˆ ( 0 (,) 1 ) โˆง 1 < ๐พ โˆง ( ๐‘ˆ โˆ’ ๐ธ ) โˆˆ โ„+ ) ) )
28 27 simp2d โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ โ„+ )
29 elfzoelz โŠข ( ๐ฝ โˆˆ ( ๐‘€ ..^ ๐‘ ) โ†’ ๐ฝ โˆˆ โ„ค )
30 23 29 syl โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„ค )
31 30 peano2zd โŠข ( ๐œ‘ โ†’ ( ๐ฝ + 1 ) โˆˆ โ„ค )
32 28 31 rpexpcld โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) โˆˆ โ„+ )
33 26 32 rpdivcld โŠข ( ๐œ‘ โ†’ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) โˆˆ โ„+ )
34 33 rpred โŠข ( ๐œ‘ โ†’ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) โˆˆ โ„ )
35 34 flcld โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) โˆˆ โ„ค )
36 1rp โŠข 1 โˆˆ โ„+
37 1 2 3 4 5 6 pntlemd โŠข ( ๐œ‘ โ†’ ( ๐ฟ โˆˆ โ„+ โˆง ๐ท โˆˆ โ„+ โˆง ๐น โˆˆ โ„+ ) )
38 37 simp1d โŠข ( ๐œ‘ โ†’ ๐ฟ โˆˆ โ„+ )
39 27 simp1d โŠข ( ๐œ‘ โ†’ ๐ธ โˆˆ โ„+ )
40 38 39 rpmulcld โŠข ( ๐œ‘ โ†’ ( ๐ฟ ยท ๐ธ ) โˆˆ โ„+ )
41 rpaddcl โŠข ( ( 1 โˆˆ โ„+ โˆง ( ๐ฟ ยท ๐ธ ) โˆˆ โ„+ ) โ†’ ( 1 + ( ๐ฟ ยท ๐ธ ) ) โˆˆ โ„+ )
42 36 40 41 sylancr โŠข ( ๐œ‘ โ†’ ( 1 + ( ๐ฟ ยท ๐ธ ) ) โˆˆ โ„+ )
43 42 21 rpmulcld โŠข ( ๐œ‘ โ†’ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) โˆˆ โ„+ )
44 26 43 rpdivcld โŠข ( ๐œ‘ โ†’ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) โˆˆ โ„+ )
45 44 rpred โŠข ( ๐œ‘ โ†’ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) โˆˆ โ„ )
46 45 flcld โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) โˆˆ โ„ค )
47 43 rpred โŠข ( ๐œ‘ โ†’ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) โˆˆ โ„ )
48 32 rpred โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) โˆˆ โ„ )
49 22 simpld โŠข ( ๐œ‘ โ†’ ( ( ๐พ โ†‘ ๐ฝ ) < ๐‘‰ โˆง ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) < ( ๐พ ยท ( ๐พ โ†‘ ๐ฝ ) ) ) )
50 49 simprd โŠข ( ๐œ‘ โ†’ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) < ( ๐พ ยท ( ๐พ โ†‘ ๐ฝ ) ) )
51 28 rpcnd โŠข ( ๐œ‘ โ†’ ๐พ โˆˆ โ„‚ )
52 28 30 rpexpcld โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ๐ฝ ) โˆˆ โ„+ )
53 52 rpcnd โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ๐ฝ ) โˆˆ โ„‚ )
54 51 53 mulcomd โŠข ( ๐œ‘ โ†’ ( ๐พ ยท ( ๐พ โ†‘ ๐ฝ ) ) = ( ( ๐พ โ†‘ ๐ฝ ) ยท ๐พ ) )
55 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemg โŠข ( ๐œ‘ โ†’ ( ๐‘€ โˆˆ โ„• โˆง ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) โˆง ( ( ( log โ€˜ ๐‘ ) / ( log โ€˜ ๐พ ) ) / 4 ) โ‰ค ( ๐‘ โˆ’ ๐‘€ ) ) )
56 55 simp1d โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„• )
57 elfzouz โŠข ( ๐ฝ โˆˆ ( ๐‘€ ..^ ๐‘ ) โ†’ ๐ฝ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) )
58 23 57 syl โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) )
59 eluznn โŠข ( ( ๐‘€ โˆˆ โ„• โˆง ๐ฝ โˆˆ ( โ„คโ‰ฅ โ€˜ ๐‘€ ) ) โ†’ ๐ฝ โˆˆ โ„• )
60 56 58 59 syl2anc โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„• )
61 60 nnnn0d โŠข ( ๐œ‘ โ†’ ๐ฝ โˆˆ โ„•0 )
62 51 61 expp1d โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) = ( ( ๐พ โ†‘ ๐ฝ ) ยท ๐พ ) )
63 54 62 eqtr4d โŠข ( ๐œ‘ โ†’ ( ๐พ ยท ( ๐พ โ†‘ ๐ฝ ) ) = ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) )
64 50 63 breqtrd โŠข ( ๐œ‘ โ†’ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) < ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) )
65 47 48 64 ltled โŠข ( ๐œ‘ โ†’ ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) โ‰ค ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) )
66 43 32 26 lediv2d โŠข ( ๐œ‘ โ†’ ( ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) โ‰ค ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) โ†” ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) โ‰ค ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) )
67 65 66 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) โ‰ค ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) )
68 flwordi โŠข ( ( ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) โˆˆ โ„ โˆง ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) โˆˆ โ„ โˆง ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) โ‰ค ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) โ‰ค ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) )
69 34 45 67 68 syl3anc โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) โ‰ค ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) )
70 eluz2 โŠข ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) ) โ†” ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) โˆˆ โ„ค โˆง ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) โˆˆ โ„ค โˆง ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) โ‰ค ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) ) )
71 35 46 69 70 syl3anbrc โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) ) )
72 eluzp1p1 โŠข ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) ) โ†’ ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) + 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ) )
73 fzss1 โŠข ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) + 1 ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ) โ†’ ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) โŠ† ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) )
74 71 72 73 3syl โŠข ( ๐œ‘ โ†’ ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) โŠ† ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) )
75 26 21 rpdivcld โŠข ( ๐œ‘ โ†’ ( ๐‘ / ๐‘‰ ) โˆˆ โ„+ )
76 75 rpred โŠข ( ๐œ‘ โ†’ ( ๐‘ / ๐‘‰ ) โˆˆ โ„ )
77 76 flcld โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) โˆˆ โ„ค )
78 26 52 rpdivcld โŠข ( ๐œ‘ โ†’ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) โˆˆ โ„+ )
79 78 rpred โŠข ( ๐œ‘ โ†’ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) โˆˆ โ„ )
80 79 flcld โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) โˆˆ โ„ค )
81 52 rpred โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ๐ฝ ) โˆˆ โ„ )
82 21 rpred โŠข ( ๐œ‘ โ†’ ๐‘‰ โˆˆ โ„ )
83 49 simpld โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ๐ฝ ) < ๐‘‰ )
84 81 82 83 ltled โŠข ( ๐œ‘ โ†’ ( ๐พ โ†‘ ๐ฝ ) โ‰ค ๐‘‰ )
85 52 21 26 lediv2d โŠข ( ๐œ‘ โ†’ ( ( ๐พ โ†‘ ๐ฝ ) โ‰ค ๐‘‰ โ†” ( ๐‘ / ๐‘‰ ) โ‰ค ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) )
86 84 85 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘ / ๐‘‰ ) โ‰ค ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) )
87 flwordi โŠข ( ( ( ๐‘ / ๐‘‰ ) โˆˆ โ„ โˆง ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) โˆˆ โ„ โˆง ( ๐‘ / ๐‘‰ ) โ‰ค ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) โ†’ ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) โ‰ค ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) )
88 76 79 86 87 syl3anc โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) โ‰ค ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) )
89 eluz2 โŠข ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) โ†” ( ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) โˆˆ โ„ค โˆง ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) โˆˆ โ„ค โˆง ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) โ‰ค ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) ) )
90 77 80 88 89 syl3anbrc โŠข ( ๐œ‘ โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) )
91 fzss2 โŠข ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) โˆˆ ( โ„คโ‰ฅ โ€˜ ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) โ†’ ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) โŠ† ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) ) )
92 90 91 syl โŠข ( ๐œ‘ โ†’ ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) โŠ† ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) ) )
93 74 92 sstrd โŠข ( ๐œ‘ โ†’ ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ( 1 + ( ๐ฟ ยท ๐ธ ) ) ยท ๐‘‰ ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ๐‘‰ ) ) ) โŠ† ( ( ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ( ๐ฝ + 1 ) ) ) ) + 1 ) ... ( โŒŠ โ€˜ ( ๐‘ / ( ๐พ โ†‘ ๐ฝ ) ) ) ) )
94 93 24 20 3sstr4g โŠข ( ๐œ‘ โ†’ ๐ผ โŠ† ๐‘‚ )