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 B A B e θ A e θ B

Proof

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