etransclem47

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)

	Ref	Expression
Hypotheses	etransclem47.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
	etransclem47.qe0	$⊢ φ \to Q (e) = 0$
	etransclem47.a	$⊢ A = coeff (Q)$
	etransclem47.a0	$⊢ φ \to A (0) \neq 0$
	etransclem47.m	$⊢ M = \deg (Q)$
	etransclem47.p	$⊢ φ \to P \in ℙ$
	etransclem47.ap	$⊢ φ \to \|A (0)\| < P$
	etransclem47.mp	$⊢ φ \to M! < P$
	etransclem47.9	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!}) < 1$
	etransclem47.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
	etransclem47.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
	etransclem47.k	$⊢ K = \frac{L}{(P - 1)!}$
Assertion	etransclem47	$⊢ φ \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$

Proof

Step	Hyp	Ref	Expression
1		etransclem47.q	$⊢ φ \to Q \in (Poly (ℤ) ∖ \{0_{𝑝}\})$
2		etransclem47.qe0	$⊢ φ \to Q (e) = 0$
3		etransclem47.a	$⊢ A = coeff (Q)$
4		etransclem47.a0	$⊢ φ \to A (0) \neq 0$
5		etransclem47.m	$⊢ M = \deg (Q)$
6		etransclem47.p	$⊢ φ \to P \in ℙ$
7		etransclem47.ap	$⊢ φ \to \|A (0)\| < P$
8		etransclem47.mp	$⊢ φ \to M! < P$
9		etransclem47.9	$⊢ φ \to \sum_{j = 0}^{M} \|A (j) e^{j}\| M M^{M + 1} (\frac{{(M^{M + 1})}^{P - 1}}{(P - 1)!}) < 1$
10		etransclem47.f	$⊢ F = (x \in ℝ ⟼ x^{P - 1} \prod_{j = 1}^{M} {(x - j)}^{P})$
11		etransclem47.l	$⊢ L = \sum_{j = 0}^{M} A (j) e^{j} \int_{(0, j)} e^{- x} F (x) d x$
12		etransclem47.k	$⊢ K = \frac{L}{(P - 1)!}$
13	12	a1i	$⊢ φ \to K = \frac{L}{(P - 1)!}$
14		ssid	$⊢ ℝ \subseteq ℝ$
15	14	a1i	$⊢ φ \to ℝ \subseteq ℝ$
16		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
17	16	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
18		reopn	$⊢ ℝ \in topGen (ran (.))$
19		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
20	18 19	eleqtri	$⊢ ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
21	20	a1i	$⊢ φ \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
22		prmnn	$⊢ P \in ℙ \to P \in ℕ$
23	6 22	syl	$⊢ φ \to P \in ℕ$
24		eqid	$⊢ M P + P - 1 = M P + P - 1$
25		fveq2	$⊢ y = x \to (ℝ D^{n} F) (i) (y) = (ℝ D^{n} F) (i) (x)$
26	25	sumeq2sdv	$⊢ y = x \to \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y) = \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (x)$
27	26	cbvmptv	$⊢ (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) = (x \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (x))$
28		negeq	$⊢ z = x \to - z = - x$
29	28	oveq2d	$⊢ z = x \to e^{- z} = e^{- x}$
30		fveq2	$⊢ z = x \to (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z) = (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x)$
31	29 30	oveq12d	$⊢ z = x \to e^{- z} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z) = e^{- x} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x)$
32	31	negeqd	$⊢ z = x \to - e^{- z} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z) = - e^{- x} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x)$
33	32	cbvmptv	$⊢ (z \in [0, j] ⟼ - e^{- z} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (z)) = (x \in [0, j] ⟼ - e^{- x} (y \in ℝ ⟼ \sum_{i = 0}^{M P + P - 1} (ℝ D^{n} F) (i) (y)) (x))$
34	1 2 3 5 15 17 21 23 10 11 24 27 33	etransclem46	$⊢ φ \to \frac{L}{(P - 1)!} = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
35		fzfid	$⊢ φ \to (0 \dots M) \in Fin$
36		fzfid	$⊢ φ \to (0 \dots M P + P - 1) \in Fin$
37		xpfi	$⊢ ((0 \dots M) \in Fin \land (0 \dots M P + P - 1) \in Fin) \to (0 \dots M) \times (0 \dots M P + P - 1) \in Fin$
38	35 36 37	syl2anc	$⊢ φ \to (0 \dots M) \times (0 \dots M P + P - 1) \in Fin$
39	1	eldifad	$⊢ φ \to Q \in Poly (ℤ)$
40		0zd	$⊢ φ \to 0 \in ℤ$
41	3	coef2	$⊢ (Q \in Poly (ℤ) \land 0 \in ℤ) \to A : ℕ_{0} ⟶ ℤ$
42	39 40 41	syl2anc	$⊢ φ \to A : ℕ_{0} ⟶ ℤ$
43	42	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A : ℕ_{0} ⟶ ℤ$
44		xp1st	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 1^{st} (k) \in (0 \dots M)$
45		elfznn0	$⊢ 1^{st} (k) \in (0 \dots M) \to 1^{st} (k) \in ℕ_{0}$
46	44 45	syl	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 1^{st} (k) \in ℕ_{0}$
47	46	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 1^{st} (k) \in ℕ_{0}$
48	43 47	ffvelcdmd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) \in ℤ$
49	48	zcnd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) \in ℂ$
50	16	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to ℝ \in \{ℝ, ℂ\}$
51	20	a1i	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to ℝ \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
52	23	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to P \in ℕ$
53		dgrcl	$⊢ Q \in Poly (ℤ) \to \deg (Q) \in ℕ_{0}$
54	39 53	syl	$⊢ φ \to \deg (Q) \in ℕ_{0}$
55	5 54	eqeltrid	$⊢ φ \to M \in ℕ_{0}$
56	55	adantr	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to M \in ℕ_{0}$
57		xp2nd	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 2^{nd} (k) \in (0 \dots M P + P - 1)$
58		elfznn0	$⊢ 2^{nd} (k) \in (0 \dots M P + P - 1) \to 2^{nd} (k) \in ℕ_{0}$
59	57 58	syl	$⊢ k \in ((0 \dots M) \times (0 \dots M P + P - 1)) \to 2^{nd} (k) \in ℕ_{0}$
60	59	adantl	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 2^{nd} (k) \in ℕ_{0}$
61	50 51 52 56 10 60	etransclem33	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to (ℝ D^{n} F) (2^{nd} (k)) : ℝ ⟶ ℂ$
62	47	nn0red	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to 1^{st} (k) \in ℝ$
63	61 62	ffvelcdmd	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
64	49 63	mulcld	$⊢ (φ \land k \in ((0 \dots M) \times (0 \dots M P + P - 1))) \to A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
65	38 64	fsumcl	$⊢ φ \to \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k)) \in ℂ$
66		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
67	23 66	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
68	67	faccld	$⊢ φ \to (P - 1)! \in ℕ$
69	68	nncnd	$⊢ φ \to (P - 1)! \in ℂ$
70	68	nnne0d	$⊢ φ \to (P - 1)! \neq 0$
71	65 69 70	divnegd	$⊢ φ \to - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
72	71	eqcomd	$⊢ φ \to \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
73	13 34 72	3eqtrd	$⊢ φ \to K = - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
74		eqid	$⊢ \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} = \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
75	23 55 10 42 74	etransclem45	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
76	75	znegcld	$⊢ φ \to - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℤ$
77	73 76	eqeltrd	$⊢ φ \to K \in ℤ$
78	12 34	eqtrid	$⊢ φ \to K = \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!}$
79	65 69 70	divcld	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \in ℂ$
80	42 4 55 6 7 8 10 74	etransclem44	$⊢ φ \to \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \neq 0$
81	79 80	negne0d	$⊢ φ \to - \frac{\sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \neq 0$
82	72 81	eqnetrd	$⊢ φ \to \frac{- \sum_{k \in (0 \dots M) \times (0 \dots M P + P - 1)} A (1^{st} (k)) (ℝ D^{n} F) (2^{nd} (k)) (1^{st} (k))}{(P - 1)!} \neq 0$
83	78 82	eqnetrd	$⊢ φ \to K \neq 0$
84		eldifsni	$⊢ Q \in (Poly (ℤ) ∖ \{0_{𝑝}\}) \to Q \neq 0_{𝑝}$
85	1 84	syl	$⊢ φ \to Q \neq 0_{𝑝}$
86		ere	$⊢ e \in ℝ$
87	86	recni	$⊢ e \in ℂ$
88	87	a1i	$⊢ φ \to e \in ℂ$
89		dgrnznn	$⊢ ((Q \in Poly (ℤ) \land Q \neq 0_{𝑝}) \land (e \in ℂ \land Q (e) = 0)) \to \deg (Q) \in ℕ$
90	39 85 88 2 89	syl22anc	$⊢ φ \to \deg (Q) \in ℕ$
91	5 90	eqeltrid	$⊢ φ \to M \in ℕ$
92	42 11 12 23 91 10 9	etransclem23	$⊢ φ \to \|K\| < 1$
93		neeq1	$⊢ k = K \to (k \neq 0 \leftrightarrow K \neq 0)$
94		fveq2	$⊢ k = K \to \|k\| = \|K\|$
95	94	breq1d	$⊢ k = K \to (\|k\| < 1 \leftrightarrow \|K\| < 1)$
96	93 95	anbi12d	$⊢ k = K \to ((k \neq 0 \land \|k\| < 1) \leftrightarrow (K \neq 0 \land \|K\| < 1))$
97	96	rspcev	$⊢ (K \in ℤ \land (K \neq 0 \land \|K\| < 1)) \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$
98	77 83 92 97	syl12anc	$⊢ φ \to \exists k \in ℤ (k \neq 0 \land \|k\| < 1)$

Metamath Proof Explorer

Theorem etransclem47

Proof