regamcl

Description: The Gamma function is real for real input. (Contributed by Mario Carneiro, 9-Jul-2017)

		Ref	Expression
	Assertion	regamcl	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to Γ (A) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to A \in ℝ$
2	1	recnd	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to A \in ℂ$
3		eldifn	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to \neg A \in (ℤ ∖ ℕ)$
4	2 3	eldifd	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
5		gamcl	$⊢ A \in (ℂ ∖ (ℤ ∖ ℕ)) \to Γ (A) \in ℂ$
6	4 5	syl	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to Γ (A) \in ℂ$
7	4	dmgmn0	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to A \neq 0$
8	6 2 7	divcan4d	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to \frac{Γ (A) A}{A} = Γ (A)$
9		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
10		1zzd	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to 1 \in ℤ$
11		eqid	$⊢ (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1}) = (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1})$
12	11 4	gamcvg2	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to seq 1 (\times (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1})) ⇝ Γ (A) A$
13		simpr	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to m \in ℕ$
14	13	peano2nnd	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to m + 1 \in ℕ$
15	14	nnrpd	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to m + 1 \in ℝ^{+}$
16	13	nnrpd	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to m \in ℝ^{+}$
17	15 16	rpdivcld	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to \frac{m + 1}{m} \in ℝ^{+}$
18	17	rpred	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to \frac{m + 1}{m} \in ℝ$
19	17	rpge0d	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to 0 \leq \frac{m + 1}{m}$
20	1	adantr	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to A \in ℝ$
21	18 19 20	recxpcld	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to {(\frac{m + 1}{m})}^{A} \in ℝ$
22	20 13	nndivred	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to \frac{A}{m} \in ℝ$
23		1red	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to 1 \in ℝ$
24	22 23	readdcld	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to (\frac{A}{m}) + 1 \in ℝ$
25	4	adantr	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to A \in (ℂ ∖ (ℤ ∖ ℕ))$
26	25 13	dmgmdivn0	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to (\frac{A}{m}) + 1 \neq 0$
27	21 24 26	redivcld	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land m \in ℕ) \to \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1} \in ℝ$
28	27	fmpttd	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1}) : ℕ ⟶ ℝ$
29	28	ffvelcdmda	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land n \in ℕ) \to (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1}) (n) \in ℝ$
30		remulcl	$⊢ (n \in ℝ \land x \in ℝ) \to n x \in ℝ$
31	30	adantl	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land (n \in ℝ \land x \in ℝ)) \to n x \in ℝ$
32	9 10 29 31	seqf	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to seq 1 (\times (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1})) : ℕ ⟶ ℝ$
33	32	ffvelcdmda	$⊢ (A \in (ℝ ∖ (ℤ ∖ ℕ)) \land n \in ℕ) \to seq 1 (\times (m \in ℕ ⟼ \frac{{(\frac{m + 1}{m})}^{A}}{(\frac{A}{m}) + 1})) (n) \in ℝ$
34	9 10 12 33	climrecl	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to Γ (A) A \in ℝ$
35	34 1 7	redivcld	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to \frac{Γ (A) A}{A} \in ℝ$
36	8 35	eqeltrrd	$⊢ A \in (ℝ ∖ (ℤ ∖ ℕ)) \to Γ (A) \in ℝ$

Metamath Proof Explorer

Theorem regamcl

Proof