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 \in ℝ \land B \in ℝ \land A \leq B) \to e^{θ (A)} ∥ e^{θ (B)}$

Proof

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

Metamath Proof Explorer

Theorem efchtdvds

Proof