lgambdd

Description: The log-Gamma function is bounded on the region U . (Contributed by Mario Carneiro, 9-Jul-2017)

	Ref	Expression
Hypotheses	lgamgulm.r	$⊢ φ \to R \in ℕ$
	lgamgulm.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\}$
	lgamgulm.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
Assertion	lgambdd	$⊢ φ \to \exists r \in ℝ \forall z \in U \|\log Γ (z)\| \leq r$

Proof

Step	Hyp	Ref	Expression
1		lgamgulm.r	$⊢ φ \to R \in ℕ$
2		lgamgulm.u	$⊢ U = \{x \in ℂ \| (\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|)\}$
3		lgamgulm.g	$⊢ G = (m \in ℕ ⟼ (z \in U ⟼ z \log (\frac{m + 1}{m}) - \log ((\frac{z}{m}) + 1)))$
4	1 2 3	lgamgulm2	$⊢ φ \to (\forall z \in U \log Γ (z) \in ℂ \land seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z))$
5	4	simprd	$⊢ φ \to seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z)$
6		eqid	$⊢ (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π)) = (m \in ℕ ⟼ if (2 R \leq m, R (\frac{2 (R + 1)}{m^{2}}), R \log (\frac{m + 1}{m}) + \log (R + 1) m + π))$
7	1 2 3 6	lgamgulmlem6	$⊢ φ \to (seq 1 (\circ_{f} +, G) \in dom \underset{u}{⇝} (U) \land (seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z) \to \exists y \in ℝ \forall z \in U \|\log Γ (z) + \log z\| \leq y))$
8	7	simprd	$⊢ φ \to (seq 1 (\circ_{f} +, G) \underset{u}{⇝} (U) (z \in U ⟼ \log Γ (z) + \log z) \to \exists y \in ℝ \forall z \in U \|\log Γ (z) + \log z\| \leq y)$
9	5 8	mpd	$⊢ φ \to \exists y \in ℝ \forall z \in U \|\log Γ (z) + \log z\| \leq y$
10	1	nnrpd	$⊢ φ \to R \in ℝ^{+}$
11	10	adantr	$⊢ (φ \land y \in ℝ) \to R \in ℝ^{+}$
12	11	relogcld	$⊢ (φ \land y \in ℝ) \to \log R \in ℝ$
13		pire	$⊢ π \in ℝ$
14	13	a1i	$⊢ (φ \land y \in ℝ) \to π \in ℝ$
15	12 14	readdcld	$⊢ (φ \land y \in ℝ) \to \log R + π \in ℝ$
16		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
17	15 16	readdcld	$⊢ (φ \land y \in ℝ) \to \log R + π + y \in ℝ$
18	17	adantrr	$⊢ (φ \land (y \in ℝ \land \forall z \in U \|\log Γ (z) + \log z\| \leq y)) \to \log R + π + y \in ℝ$
19	4	simpld	$⊢ φ \to \forall z \in U \log Γ (z) \in ℂ$
20	19	adantr	$⊢ (φ \land y \in ℝ) \to \forall z \in U \log Γ (z) \in ℂ$
21	20	r19.21bi	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log Γ (z) \in ℂ$
22	21	abscld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z)\| \in ℝ$
23	22	adantr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \|\log Γ (z)\| \in ℝ$
24	11	adantr	$⊢ ((φ \land y \in ℝ) \land z \in U) \to R \in ℝ^{+}$
25	24	relogcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log R \in ℝ$
26	13	a1i	$⊢ ((φ \land y \in ℝ) \land z \in U) \to π \in ℝ$
27	25 26	readdcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log R + π \in ℝ$
28	1 2	lgamgulmlem1	$⊢ φ \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
29	28	adantr	$⊢ (φ \land y \in ℝ) \to U \subseteq ℂ ∖ (ℤ ∖ ℕ)$
30	29	sselda	$⊢ ((φ \land y \in ℝ) \land z \in U) \to z \in (ℂ ∖ (ℤ ∖ ℕ))$
31	30	eldifad	$⊢ ((φ \land y \in ℝ) \land z \in U) \to z \in ℂ$
32	30	dmgmn0	$⊢ ((φ \land y \in ℝ) \land z \in U) \to z \neq 0$
33	31 32	logcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log z \in ℂ$
34	21 33	addcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log Γ (z) + \log z \in ℂ$
35	34	abscld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z) + \log z\| \in ℝ$
36	27 35	readdcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log R + π + \|\log Γ (z) + \log z\| \in ℝ$
37	36	adantr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \log R + π + \|\log Γ (z) + \log z\| \in ℝ$
38	17	ad2antrr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \log R + π + y \in ℝ$
39	33	abscld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log z\| \in ℝ$
40	39 35	readdcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log z\| + \|\log Γ (z) + \log z\| \in ℝ$
41	33	negcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to - \log z \in ℂ$
42	21 41	abs2difd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z)\| - \|- \log z\| \leq \|\log Γ (z) - (- \log z)\|$
43	33	absnegd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|- \log z\| = \|\log z\|$
44	43	oveq2d	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z)\| - \|- \log z\| = \|\log Γ (z)\| - \|\log z\|$
45	21 33	subnegd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log Γ (z) - (- \log z) = \log Γ (z) + \log z$
46	45	fveq2d	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z) - (- \log z)\| = \|\log Γ (z) + \log z\|$
47	42 44 46	3brtr3d	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z)\| - \|\log z\| \leq \|\log Γ (z) + \log z\|$
48	22 39 35	lesubadd2d	$⊢ ((φ \land y \in ℝ) \land z \in U) \to (\|\log Γ (z)\| - \|\log z\| \leq \|\log Γ (z) + \log z\| \leftrightarrow \|\log Γ (z)\| \leq \|\log z\| + \|\log Γ (z) + \log z\|)$
49	47 48	mpbid	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z)\| \leq \|\log z\| + \|\log Γ (z) + \log z\|$
50	31 32	absrpcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|z\| \in ℝ^{+}$
51	50	relogcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log \|z\| \in ℝ$
52	51	recnd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log \|z\| \in ℂ$
53	52	abscld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log \|z\|\| \in ℝ$
54	53 26	readdcld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log \|z\|\| + π \in ℝ$
55		abslogle	$⊢ (z \in ℂ \land z \neq 0) \to \|\log z\| \leq \|\log \|z\|\| + π$
56	31 32 55	syl2anc	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log z\| \leq \|\log \|z\|\| + π$
57		df-neg	$⊢ - \log R = 0 - \log R$
58		log1	$⊢ \log 1 = 0$
59	58	oveq1i	$⊢ \log 1 - \log R = 0 - \log R$
60	57 59	eqtr4i	$⊢ - \log R = \log 1 - \log R$
61		1rp	$⊢ 1 \in ℝ^{+}$
62		relogdiv	$⊢ (1 \in ℝ^{+} \land R \in ℝ^{+}) \to \log (\frac{1}{R}) = \log 1 - \log R$
63	61 24 62	sylancr	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log (\frac{1}{R}) = \log 1 - \log R$
64	60 63	eqtr4id	$⊢ ((φ \land y \in ℝ) \land z \in U) \to - \log R = \log (\frac{1}{R})$
65		oveq2	$⊢ k = 0 \to z + k = z + 0$
66	65	fveq2d	$⊢ k = 0 \to \|z + k\| = \|z + 0\|$
67	66	breq2d	$⊢ k = 0 \to (\frac{1}{R} \leq \|z + k\| \leftrightarrow \frac{1}{R} \leq \|z + 0\|)$
68		fveq2	$⊢ x = z \to \|x\| = \|z\|$
69	68	breq1d	$⊢ x = z \to (\|x\| \leq R \leftrightarrow \|z\| \leq R)$
70		fvoveq1	$⊢ x = z \to \|x + k\| = \|z + k\|$
71	70	breq2d	$⊢ x = z \to (\frac{1}{R} \leq \|x + k\| \leftrightarrow \frac{1}{R} \leq \|z + k\|)$
72	71	ralbidv	$⊢ x = z \to (\forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\| \leftrightarrow \forall k \in ℕ_{0} \frac{1}{R} \leq \|z + k\|)$
73	69 72	anbi12d	$⊢ x = z \to ((\|x\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|x + k\|) \leftrightarrow (\|z\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|z + k\|))$
74	73 2	elrab2	$⊢ z \in U \leftrightarrow (z \in ℂ \land (\|z\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|z + k\|))$
75	74	simprbi	$⊢ z \in U \to (\|z\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|z + k\|)$
76	75	adantl	$⊢ ((φ \land y \in ℝ) \land z \in U) \to (\|z\| \leq R \land \forall k \in ℕ_{0} \frac{1}{R} \leq \|z + k\|)$
77	76	simprd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \forall k \in ℕ_{0} \frac{1}{R} \leq \|z + k\|$
78		0nn0	$⊢ 0 \in ℕ_{0}$
79	78	a1i	$⊢ ((φ \land y \in ℝ) \land z \in U) \to 0 \in ℕ_{0}$
80	67 77 79	rspcdva	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \frac{1}{R} \leq \|z + 0\|$
81	31	addid1d	$⊢ ((φ \land y \in ℝ) \land z \in U) \to z + 0 = z$
82	81	fveq2d	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|z + 0\| = \|z\|$
83	80 82	breqtrd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \frac{1}{R} \leq \|z\|$
84	24	rpreccld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \frac{1}{R} \in ℝ^{+}$
85	84 50	logled	$⊢ ((φ \land y \in ℝ) \land z \in U) \to (\frac{1}{R} \leq \|z\| \leftrightarrow \log (\frac{1}{R}) \leq \log \|z\|)$
86	83 85	mpbid	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log (\frac{1}{R}) \leq \log \|z\|$
87	64 86	eqbrtrd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to - \log R \leq \log \|z\|$
88	76	simpld	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|z\| \leq R$
89	50 24	logled	$⊢ ((φ \land y \in ℝ) \land z \in U) \to (\|z\| \leq R \leftrightarrow \log \|z\| \leq \log R)$
90	88 89	mpbid	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \log \|z\| \leq \log R$
91	51 25	absled	$⊢ ((φ \land y \in ℝ) \land z \in U) \to (\|\log \|z\|\| \leq \log R \leftrightarrow (- \log R \leq \log \|z\| \land \log \|z\| \leq \log R))$
92	87 90 91	mpbir2and	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log \|z\|\| \leq \log R$
93	53 25 26 92	leadd1dd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log \|z\|\| + π \leq \log R + π$
94	39 54 27 56 93	letrd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log z\| \leq \log R + π$
95	39 27 35 94	leadd1dd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log z\| + \|\log Γ (z) + \log z\| \leq \log R + π + \|\log Γ (z) + \log z\|$
96	22 40 36 49 95	letrd	$⊢ ((φ \land y \in ℝ) \land z \in U) \to \|\log Γ (z)\| \leq \log R + π + \|\log Γ (z) + \log z\|$
97	96	adantr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \|\log Γ (z)\| \leq \log R + π + \|\log Γ (z) + \log z\|$
98	35	adantr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \|\log Γ (z) + \log z\| \in ℝ$
99		simpllr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to y \in ℝ$
100	27	adantr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \log R + π \in ℝ$
101		simpr	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \|\log Γ (z) + \log z\| \leq y$
102	98 99 100 101	leadd2dd	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \log R + π + \|\log Γ (z) + \log z\| \leq \log R + π + y$
103	23 37 38 97 102	letrd	$⊢ (((φ \land y \in ℝ) \land z \in U) \land \|\log Γ (z) + \log z\| \leq y) \to \|\log Γ (z)\| \leq \log R + π + y$
104	103	ex	$⊢ ((φ \land y \in ℝ) \land z \in U) \to (\|\log Γ (z) + \log z\| \leq y \to \|\log Γ (z)\| \leq \log R + π + y)$
105	104	ralimdva	$⊢ (φ \land y \in ℝ) \to (\forall z \in U \|\log Γ (z) + \log z\| \leq y \to \forall z \in U \|\log Γ (z)\| \leq \log R + π + y)$
106	105	impr	$⊢ (φ \land (y \in ℝ \land \forall z \in U \|\log Γ (z) + \log z\| \leq y)) \to \forall z \in U \|\log Γ (z)\| \leq \log R + π + y$
107		brralrspcev	$⊢ (\log R + π + y \in ℝ \land \forall z \in U \|\log Γ (z)\| \leq \log R + π + y) \to \exists r \in ℝ \forall z \in U \|\log Γ (z)\| \leq r$
108	18 106 107	syl2anc	$⊢ (φ \land (y \in ℝ \land \forall z \in U \|\log Γ (z) + \log z\| \leq y)) \to \exists r \in ℝ \forall z \in U \|\log Γ (z)\| \leq r$
109	9 108	rexlimddv	$⊢ φ \to \exists r \in ℝ \forall z \in U \|\log Γ (z)\| \leq r$

Metamath Proof Explorer

Theorem lgambdd

Proof