etransc

Description: _e is transcendental. Section *5 of Juillerat p. 11 can be used as a reference for this proof. (Contributed by Glauco Siliprandi, 5-Apr-2020) (Proof shortened by AV, 28-Sep-2020)

		Ref	Expression
	Assertion	etransc	$⊢ e \in (ℂ ∖ 𝔸)$

Proof

Step	Hyp	Ref	Expression
1		1red	$⊢ (k \in ℤ \land k \neq 0) \to 1 \in ℝ$
2		nn0abscl	$⊢ k \in ℤ \to \|k\| \in ℕ_{0}$
3	2	nn0red	$⊢ k \in ℤ \to \|k\| \in ℝ$
4	3	adantr	$⊢ (k \in ℤ \land k \neq 0) \to \|k\| \in ℝ$
5		nnabscl	$⊢ (k \in ℤ \land k \neq 0) \to \|k\| \in ℕ$
6	5	nnge1d	$⊢ (k \in ℤ \land k \neq 0) \to 1 \leq \|k\|$
7	1 4 6	lensymd	$⊢ (k \in ℤ \land k \neq 0) \to \neg \|k\| < 1$
8		nan	$⊢ (k \in ℤ \to \neg (k \neq 0 \land \|k\| < 1)) \leftrightarrow ((k \in ℤ \land k \neq 0) \to \neg \|k\| < 1)$
9	7 8	mpbir	$⊢ k \in ℤ \to \neg (k \neq 0 \land \|k\| < 1)$
10	9	nrex	$⊢ \neg \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$
11		ere	$⊢ e \in ℝ$
12	11	recni	$⊢ e \in ℂ$
13		neldif	$⊢ (e \in ℂ \land \neg e \in (ℂ ∖ 𝔸)) \to e \in 𝔸$
14	12 13	mpan	$⊢ \neg e \in (ℂ ∖ 𝔸) \to e \in 𝔸$
15		ene0	$⊢ e \neq 0$
16		elsng	$⊢ e \in ℂ \to (e \in \{0\} \leftrightarrow e = 0)$
17	12 16	ax-mp	$⊢ e \in \{0\} \leftrightarrow e = 0$
18	15 17	nemtbir	$⊢ \neg e \in \{0\}$
19	18	a1i	$⊢ \neg e \in (ℂ ∖ 𝔸) \to \neg e \in \{0\}$
20	14 19	eldifd	$⊢ \neg e \in (ℂ ∖ 𝔸) \to e \in (𝔸 ∖ \{0\})$
21		elaa2	$⊢ e \in (𝔸 ∖ \{0\}) \leftrightarrow (e \in ℂ \land \exists q \in Poly (ℤ) (coeff (q) (0) \neq 0 \land q (e) = 0))$
22	20 21	sylib	$⊢ \neg e \in (ℂ ∖ 𝔸) \to (e \in ℂ \land \exists q \in Poly (ℤ) (coeff (q) (0) \neq 0 \land q (e) = 0))$
23	22	simprd	$⊢ \neg e \in (ℂ ∖ 𝔸) \to \exists q \in Poly (ℤ) (coeff (q) (0) \neq 0 \land q (e) = 0)$
24		simpl	$⊢ (q \in Poly (ℤ) \land coeff (q) (0) \neq 0) \to q \in Poly (ℤ)$
25		0nn0	$⊢ 0 \in ℕ_{0}$
26		n0p	$⊢ (q \in Poly (ℤ) \land 0 \in ℕ_{0} \land coeff (q) (0) \neq 0) \to q \neq 0_{𝑝}$
27	25 26	mp3an2	$⊢ (q \in Poly (ℤ) \land coeff (q) (0) \neq 0) \to q \neq 0_{𝑝}$
28		nelsn	$⊢ q \neq 0_{𝑝} \to \neg q \in \{0_{𝑝}\}$
29	27 28	syl	$⊢ (q \in Poly (ℤ) \land coeff (q) (0) \neq 0) \to \neg q \in \{0_{𝑝}\}$
30	24 29	eldifd	$⊢ (q \in Poly (ℤ) \land coeff (q) (0) \neq 0) \to q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
31	30	adantrr	$⊢ (q \in Poly (ℤ) \land (coeff (q) (0) \neq 0 \land q (e) = 0)) \to q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
32		simprr	$⊢ (q \in Poly (ℤ) \land (coeff (q) (0) \neq 0 \land q (e) = 0)) \to q (e) = 0$
33		eqid	$⊢ coeff (q) = coeff (q)$
34		simprl	$⊢ (q \in Poly (ℤ) \land (coeff (q) (0) \neq 0 \land q (e) = 0)) \to coeff (q) (0) \neq 0$
35		eqid	$⊢ \deg (q) = \deg (q)$
36		eqid	$⊢ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} = \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1}$
37		eqid	$⊢ (n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) = (n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!}))$
38		fveq2	$⊢ h = l \to coeff (q) (h) = coeff (q) (l)$
39		oveq2	$⊢ h = l \to e^{h} = e^{l}$
40	38 39	oveq12d	$⊢ h = l \to coeff (q) (h) e^{h} = coeff (q) (l) e^{l}$
41	40	fveq2d	$⊢ h = l \to \|coeff (q) (h) e^{h}\| = \|coeff (q) (l) e^{l}\|$
42	41	oveq1d	$⊢ h = l \to \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} = \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1}$
43	42	cbvsumv	$⊢ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} = \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1}$
44	43	a1i	$⊢ m = n \to \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} = \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1}$
45		oveq2	$⊢ m = n \to {({\deg (q)}^{\deg (q) + 1})}^{m} = {({\deg (q)}^{\deg (q) + 1})}^{n}$
46		fveq2	$⊢ m = n \to m! = n!$
47	45 46	oveq12d	$⊢ m = n \to \frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!} = \frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!}$
48	44 47	oveq12d	$⊢ m = n \to \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!}) = \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})$
49	48	cbvmptv	$⊢ (m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) = (n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!}))$
50	49	a1i	$⊢ m = n \to (m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) = (n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!}))$
51		id	$⊢ m = n \to m = n$
52	50 51	fveq12d	$⊢ m = n \to (m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m) = (n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)$
53	52	fveq2d	$⊢ m = n \to \|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| = \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\|$
54	53	breq1d	$⊢ m = n \to (\|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| < 1 \leftrightarrow \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\| < 1)$
55	54	cbvralvw	$⊢ \forall m \in ℤ_{\geq j} \|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| < 1 \leftrightarrow \forall n \in ℤ_{\geq j} \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\| < 1$
56		fveq2	$⊢ j = i \to ℤ_{\geq j} = ℤ_{\geq i}$
57	56	raleqdv	$⊢ j = i \to (\forall n \in ℤ_{\geq j} \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\| < 1 \leftrightarrow \forall n \in ℤ_{\geq i} \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\| < 1)$
58	55 57	bitrid	$⊢ j = i \to (\forall m \in ℤ_{\geq j} \|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| < 1 \leftrightarrow \forall n \in ℤ_{\geq i} \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\| < 1)$
59	58	cbvrabv	$⊢ \{j \in ℕ_{0} \| \forall m \in ℤ_{\geq j} \|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| < 1\} = \{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\| < 1\}$
60	59	infeq1i	$⊢ inf (\{j \in ℕ_{0} \| \forall m \in ℤ_{\geq j} \|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| < 1\} ℝ <) = inf (\{i \in ℕ_{0} \| \forall n \in ℤ_{\geq i} \|(n \in ℕ_{0} ⟼ \sum_{l = 0}^{\deg (q)} \|coeff (q) (l) e^{l}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{n}}{n!})) (n)\| < 1\} ℝ <)$
61		eqid	$⊢ sup (\{\|coeff (q) (0)\|, \deg (q)!, inf (\{j \in ℕ_{0} \| \forall m \in ℤ_{\geq j} \|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| < 1\} ℝ <)\} ℝ^{} <) = sup (\{\|coeff (q) (0)\|, \deg (q)!, inf (\{j \in ℕ_{0} \| \forall m \in ℤ_{\geq j} \|(m \in ℕ_{0} ⟼ \sum_{h = 0}^{\deg (q)} \|coeff (q) (h) e^{h}\| \deg (q) {\deg (q)}^{\deg (q) + 1} (\frac{{({\deg (q)}^{\deg (q) + 1})}^{m}}{m!})) (m)\| < 1\} ℝ <)\} ℝ^{} <)$
62	31 32 33 34 35 36 37 60 61	etransclem48	$⊢ (q \in Poly (ℤ) \land (coeff (q) (0) \neq 0 \land q (e) = 0)) \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$
63	62	rexlimiva	$⊢ \exists q \in Poly (ℤ) (coeff (q) (0) \neq 0 \land q (e) = 0) \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$
64	23 63	syl	$⊢ \neg e \in (ℂ ∖ 𝔸) \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$
65	10 64	mt3	$⊢ e \in (ℂ ∖ 𝔸)$

Metamath Proof Explorer

Theorem etransc

Proof