Metamath Proof Explorer

Theorem efchtdvds

Description: The exponentiated Chebyshev function forms a divisibility chain between any two points. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion efchtdvds 
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` A ) ) || ( exp ` ( theta ` B ) ) )

Proof

Step Hyp Ref Expression
1 chtcl 
 |-  ( B e. RR -> ( theta ` B ) e. RR )
2 1 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` B ) e. RR )
3 2 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` B ) e. CC )
4 chtcl 
 |-  ( A e. RR -> ( theta ` A ) e. RR )
5 4 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` A ) e. RR )
6 5 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` A ) e. CC )
7 efsub 
 |-  ( ( ( theta ` B ) e. CC /\ ( theta ` A ) e. CC ) -> ( exp ` ( ( theta ` B ) - ( theta ` A ) ) ) = ( ( exp ` ( theta ` B ) ) / ( exp ` ( theta ` A ) ) ) )
8 3 6 7 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( ( theta ` B ) - ( theta ` A ) ) ) = ( ( exp ` ( theta ` B ) ) / ( exp ` ( theta ` A ) ) ) )
9 chtfl 
 |-  ( B e. RR -> ( theta ` ( |_ ` B ) ) = ( theta ` B ) )
10 9 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` ( |_ ` B ) ) = ( theta ` B ) )
11 chtfl 
 |-  ( A e. RR -> ( theta ` ( |_ ` A ) ) = ( theta ` A ) )
12 11 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( theta ` ( |_ ` A ) ) = ( theta ` A ) )
13 10 12 oveq12d 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( theta ` ( |_ ` B ) ) - ( theta ` ( |_ ` A ) ) ) = ( ( theta ` B ) - ( theta ` A ) ) )
14 flword2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) )
15 chtdif 
 |-  ( ( |_ ` B ) e. ( ZZ>= ` ( |_ ` A ) ) -> ( ( theta ` ( |_ ` B ) ) - ( theta ` ( |_ ` A ) ) ) = sum_ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ( log ` p ) )
16 14 15 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( theta ` ( |_ ` B ) ) - ( theta ` ( |_ ` A ) ) ) = sum_ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ( log ` p ) )
17 13 16 eqtr3d 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( theta ` B ) - ( theta ` A ) ) = sum_ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ( log ` p ) )
18 ssrab2 
 |-  { x e. RR | ( exp ` x ) e. NN } C_ RR
19 ax-resscn 
 |-  RR C_ CC
20 18 19 sstri 
 |-  { x e. RR | ( exp ` x ) e. NN } C_ CC
21 20 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> { x e. RR | ( exp ` x ) e. NN } C_ CC )
22 fveq2 
 |-  ( x = y -> ( exp ` x ) = ( exp ` y ) )
23 22 eleq1d 
 |-  ( x = y -> ( ( exp ` x ) e. NN <-> ( exp ` y ) e. NN ) )
24 23 elrab 
 |-  ( y e. { x e. RR | ( exp ` x ) e. NN } <-> ( y e. RR /\ ( exp ` y ) e. NN ) )
25 fveq2 
 |-  ( x = z -> ( exp ` x ) = ( exp ` z ) )
26 25 eleq1d 
 |-  ( x = z -> ( ( exp ` x ) e. NN <-> ( exp ` z ) e. NN ) )
27 26 elrab 
 |-  ( z e. { x e. RR | ( exp ` x ) e. NN } <-> ( z e. RR /\ ( exp ` z ) e. NN ) )
28 fveq2 
 |-  ( x = ( y + z ) -> ( exp ` x ) = ( exp ` ( y + z ) ) )
29 28 eleq1d 
 |-  ( x = ( y + z ) -> ( ( exp ` x ) e. NN <-> ( exp ` ( y + z ) ) e. NN ) )
30 simpll 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> y e. RR )
31 simprl 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> z e. RR )
32 30 31 readdcld 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( y + z ) e. RR )
33 30 recnd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> y e. CC )
34 31 recnd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> z e. CC )
35 efadd 
 |-  ( ( y e. CC /\ z e. CC ) -> ( exp ` ( y + z ) ) = ( ( exp ` y ) x. ( exp ` z ) ) )
36 33 34 35 syl2anc 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( exp ` ( y + z ) ) = ( ( exp ` y ) x. ( exp ` z ) ) )
37 nnmulcl 
 |-  ( ( ( exp ` y ) e. NN /\ ( exp ` z ) e. NN ) -> ( ( exp ` y ) x. ( exp ` z ) ) e. NN )
38 37 ad2ant2l 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( ( exp ` y ) x. ( exp ` z ) ) e. NN )
39 36 38 eqeltrd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( exp ` ( y + z ) ) e. NN )
40 29 32 39 elrabd 
 |-  ( ( ( y e. RR /\ ( exp ` y ) e. NN ) /\ ( z e. RR /\ ( exp ` z ) e. NN ) ) -> ( y + z ) e. { x e. RR | ( exp ` x ) e. NN } )
41 24 27 40 syl2anb 
 |-  ( ( y e. { x e. RR | ( exp ` x ) e. NN } /\ z e. { x e. RR | ( exp ` x ) e. NN } ) -> ( y + z ) e. { x e. RR | ( exp ` x ) e. NN } )
42 41 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ ( y e. { x e. RR | ( exp ` x ) e. NN } /\ z e. { x e. RR | ( exp ` x ) e. NN } ) ) -> ( y + z ) e. { x e. RR | ( exp ` x ) e. NN } )
43 fzfid 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) e. Fin )
44 inss1 
 |-  ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) C_ ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) )
45 ssfi 
 |-  ( ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) e. Fin /\ ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) C_ ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) ) -> ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) e. Fin )
46 43 44 45 sylancl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) e. Fin )
47 fveq2 
 |-  ( x = ( log ` p ) -> ( exp ` x ) = ( exp ` ( log ` p ) ) )
48 47 eleq1d 
 |-  ( x = ( log ` p ) -> ( ( exp ` x ) e. NN <-> ( exp ` ( log ` p ) ) e. NN ) )
49 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) )
50 49 elin2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> p e. Prime )
51 prmnn 
 |-  ( p e. Prime -> p e. NN )
52 50 51 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> p e. NN )
53 52 nnrpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> p e. RR+ )
54 53 relogcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> ( log ` p ) e. RR )
55 53 reeflogd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> ( exp ` ( log ` p ) ) = p )
56 55 52 eqeltrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> ( exp ` ( log ` p ) ) e. NN )
57 48 54 56 elrabd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A <_ B ) /\ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ) -> ( log ` p ) e. { x e. RR | ( exp ` x ) e. NN } )
58 0re 
 |-  0 e. RR
59 1nn 
 |-  1 e. NN
60 fveq2 
 |-  ( x = 0 -> ( exp ` x ) = ( exp ` 0 ) )
61 ef0 
 |-  ( exp ` 0 ) = 1
62 60 61 eqtrdi 
 |-  ( x = 0 -> ( exp ` x ) = 1 )
63 62 eleq1d 
 |-  ( x = 0 -> ( ( exp ` x ) e. NN <-> 1 e. NN ) )
64 63 elrab 
 |-  ( 0 e. { x e. RR | ( exp ` x ) e. NN } <-> ( 0 e. RR /\ 1 e. NN ) )
65 58 59 64 mpbir2an 
 |-  0 e. { x e. RR | ( exp ` x ) e. NN }
66 65 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> 0 e. { x e. RR | ( exp ` x ) e. NN } )
67 21 42 46 57 66 fsumcllem 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> sum_ p e. ( ( ( ( |_ ` A ) + 1 ) ... ( |_ ` B ) ) i^i Prime ) ( log ` p ) e. { x e. RR | ( exp ` x ) e. NN } )
68 17 67 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( theta ` B ) - ( theta ` A ) ) e. { x e. RR | ( exp ` x ) e. NN } )
69 fveq2 
 |-  ( x = ( ( theta ` B ) - ( theta ` A ) ) -> ( exp ` x ) = ( exp ` ( ( theta ` B ) - ( theta ` A ) ) ) )
70 69 eleq1d 
 |-  ( x = ( ( theta ` B ) - ( theta ` A ) ) -> ( ( exp ` x ) e. NN <-> ( exp ` ( ( theta ` B ) - ( theta ` A ) ) ) e. NN ) )
71 70 elrab 
 |-  ( ( ( theta ` B ) - ( theta ` A ) ) e. { x e. RR | ( exp ` x ) e. NN } <-> ( ( ( theta ` B ) - ( theta ` A ) ) e. RR /\ ( exp ` ( ( theta ` B ) - ( theta ` A ) ) ) e. NN ) )
72 71 simprbi 
 |-  ( ( ( theta ` B ) - ( theta ` A ) ) e. { x e. RR | ( exp ` x ) e. NN } -> ( exp ` ( ( theta ` B ) - ( theta ` A ) ) ) e. NN )
73 68 72 syl 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( ( theta ` B ) - ( theta ` A ) ) ) e. NN )
74 8 73 eqeltrrd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( exp ` ( theta ` B ) ) / ( exp ` ( theta ` A ) ) ) e. NN )
75 74 nnzd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( exp ` ( theta ` B ) ) / ( exp ` ( theta ` A ) ) ) e. ZZ )
76 efchtcl 
 |-  ( A e. RR -> ( exp ` ( theta ` A ) ) e. NN )
77 76 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` A ) ) e. NN )
78 77 nnzd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` A ) ) e. ZZ )
79 77 nnne0d 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` A ) ) =/= 0 )
80 efchtcl 
 |-  ( B e. RR -> ( exp ` ( theta ` B ) ) e. NN )
81 80 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` B ) ) e. NN )
82 81 nnzd 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` B ) ) e. ZZ )
83 dvdsval2 
 |-  ( ( ( exp ` ( theta ` A ) ) e. ZZ /\ ( exp ` ( theta ` A ) ) =/= 0 /\ ( exp ` ( theta ` B ) ) e. ZZ ) -> ( ( exp ` ( theta ` A ) ) || ( exp ` ( theta ` B ) ) <-> ( ( exp ` ( theta ` B ) ) / ( exp ` ( theta ` A ) ) ) e. ZZ ) )
84 78 79 82 83 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( ( exp ` ( theta ` A ) ) || ( exp ` ( theta ` B ) ) <-> ( ( exp ` ( theta ` B ) ) / ( exp ` ( theta ` A ) ) ) e. ZZ ) )
85 75 84 mpbird 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( exp ` ( theta ` A ) ) || ( exp ` ( theta ` B ) ) )