# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to {\mathrm{e}}^{\theta \left({A}\right)}\parallel {\mathrm{e}}^{\theta \left({B}\right)}$

### Proof

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