Metamath Proof Explorer


Theorem logcnlem2

Description: Lemma for logcn . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Hypotheses logcn.d โŠข ๐ท = ( โ„‚ โˆ– ( -โˆž (,] 0 ) )
logcnlem.s โŠข ๐‘† = if ( ๐ด โˆˆ โ„+ , ๐ด , ( abs โ€˜ ( โ„‘ โ€˜ ๐ด ) ) )
logcnlem.t โŠข ๐‘‡ = ( ( abs โ€˜ ๐ด ) ยท ( ๐‘… / ( 1 + ๐‘… ) ) )
logcnlem.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ๐ท )
logcnlem.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ โ„+ )
Assertion logcnlem2 ( ๐œ‘ โ†’ if ( ๐‘† โ‰ค ๐‘‡ , ๐‘† , ๐‘‡ ) โˆˆ โ„+ )

Proof

Step Hyp Ref Expression
1 logcn.d โŠข ๐ท = ( โ„‚ โˆ– ( -โˆž (,] 0 ) )
2 logcnlem.s โŠข ๐‘† = if ( ๐ด โˆˆ โ„+ , ๐ด , ( abs โ€˜ ( โ„‘ โ€˜ ๐ด ) ) )
3 logcnlem.t โŠข ๐‘‡ = ( ( abs โ€˜ ๐ด ) ยท ( ๐‘… / ( 1 + ๐‘… ) ) )
4 logcnlem.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ๐ท )
5 logcnlem.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ โ„+ )
6 simpr โŠข ( ( ๐œ‘ โˆง ๐ด โˆˆ โ„+ ) โ†’ ๐ด โˆˆ โ„+ )
7 1 ellogdm โŠข ( ๐ด โˆˆ ๐ท โ†” ( ๐ด โˆˆ โ„‚ โˆง ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„+ ) ) )
8 7 simplbi โŠข ( ๐ด โˆˆ ๐ท โ†’ ๐ด โˆˆ โ„‚ )
9 4 8 syl โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
10 9 imcld โŠข ( ๐œ‘ โ†’ ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„ )
11 10 adantr โŠข ( ( ๐œ‘ โˆง ยฌ ๐ด โˆˆ โ„+ ) โ†’ ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„ )
12 11 recnd โŠข ( ( ๐œ‘ โˆง ยฌ ๐ด โˆˆ โ„+ ) โ†’ ( โ„‘ โ€˜ ๐ด ) โˆˆ โ„‚ )
13 reim0b โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด โˆˆ โ„ โ†” ( โ„‘ โ€˜ ๐ด ) = 0 ) )
14 9 13 syl โŠข ( ๐œ‘ โ†’ ( ๐ด โˆˆ โ„ โ†” ( โ„‘ โ€˜ ๐ด ) = 0 ) )
15 7 simprbi โŠข ( ๐ด โˆˆ ๐ท โ†’ ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„+ ) )
16 4 15 syl โŠข ( ๐œ‘ โ†’ ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„+ ) )
17 14 16 sylbird โŠข ( ๐œ‘ โ†’ ( ( โ„‘ โ€˜ ๐ด ) = 0 โ†’ ๐ด โˆˆ โ„+ ) )
18 17 necon3bd โŠข ( ๐œ‘ โ†’ ( ยฌ ๐ด โˆˆ โ„+ โ†’ ( โ„‘ โ€˜ ๐ด ) โ‰  0 ) )
19 18 imp โŠข ( ( ๐œ‘ โˆง ยฌ ๐ด โˆˆ โ„+ ) โ†’ ( โ„‘ โ€˜ ๐ด ) โ‰  0 )
20 12 19 absrpcld โŠข ( ( ๐œ‘ โˆง ยฌ ๐ด โˆˆ โ„+ ) โ†’ ( abs โ€˜ ( โ„‘ โ€˜ ๐ด ) ) โˆˆ โ„+ )
21 6 20 ifclda โŠข ( ๐œ‘ โ†’ if ( ๐ด โˆˆ โ„+ , ๐ด , ( abs โ€˜ ( โ„‘ โ€˜ ๐ด ) ) ) โˆˆ โ„+ )
22 2 21 eqeltrid โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ โ„+ )
23 1 logdmn0 โŠข ( ๐ด โˆˆ ๐ท โ†’ ๐ด โ‰  0 )
24 4 23 syl โŠข ( ๐œ‘ โ†’ ๐ด โ‰  0 )
25 9 24 absrpcld โŠข ( ๐œ‘ โ†’ ( abs โ€˜ ๐ด ) โˆˆ โ„+ )
26 1rp โŠข 1 โˆˆ โ„+
27 rpaddcl โŠข ( ( 1 โˆˆ โ„+ โˆง ๐‘… โˆˆ โ„+ ) โ†’ ( 1 + ๐‘… ) โˆˆ โ„+ )
28 26 5 27 sylancr โŠข ( ๐œ‘ โ†’ ( 1 + ๐‘… ) โˆˆ โ„+ )
29 5 28 rpdivcld โŠข ( ๐œ‘ โ†’ ( ๐‘… / ( 1 + ๐‘… ) ) โˆˆ โ„+ )
30 25 29 rpmulcld โŠข ( ๐œ‘ โ†’ ( ( abs โ€˜ ๐ด ) ยท ( ๐‘… / ( 1 + ๐‘… ) ) ) โˆˆ โ„+ )
31 3 30 eqeltrid โŠข ( ๐œ‘ โ†’ ๐‘‡ โˆˆ โ„+ )
32 22 31 ifcld โŠข ( ๐œ‘ โ†’ if ( ๐‘† โ‰ค ๐‘‡ , ๐‘† , ๐‘‡ ) โˆˆ โ„+ )