Theorem regamcl

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

	Ref	Expression
Assertion	regamcl	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eldifi	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → 𝐴 ∈ ℝ )
2	1	recnd	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → 𝐴 ∈ ℂ )
3		eldifn	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ¬ 𝐴 ∈ ( ℤ ∖ ℕ ) )
4	2 3	eldifd	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
5		gamcl	⊢ ( 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℂ )
6	4 5	syl	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℂ )
7	4	dmgmn0	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → 𝐴 ≠ 0 )
8	6 2 7	divcan4d	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ( ( ( Γ ‘ 𝐴 ) · 𝐴 ) / 𝐴 ) = ( Γ ‘ 𝐴 ) )
9		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
10		1zzd	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → 1 ∈ ℤ )
11		eqid	⊢ ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) )
12	11 4	gamcvg2	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → seq 1 ( · , ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ⇝ ( ( Γ ‘ 𝐴 ) · 𝐴 ) )
13		simpr	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ )
14	13	peano2nnd	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℕ )
15	14	nnrpd	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 + 1 ) ∈ ℝ+ )
16	13	nnrpd	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ+ )
17	15 16	rpdivcld	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) / 𝑚 ) ∈ ℝ+ )
18	17	rpred	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 + 1 ) / 𝑚 ) ∈ ℝ )
19	17	rpge0d	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → 0 ≤ ( ( 𝑚 + 1 ) / 𝑚 ) )
20	1	adantr	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → 𝐴 ∈ ℝ )
21	18 19 20	recxpcld	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) ∈ ℝ )
22	20 13	nndivred	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝐴 / 𝑚 ) ∈ ℝ )
23		1red	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℝ )
24	22 23	readdcld	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 / 𝑚 ) + 1 ) ∈ ℝ )
25	4	adantr	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → 𝐴 ∈ ( ℂ ∖ ( ℤ ∖ ℕ ) ) )
26	25 13	dmgmdivn0	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐴 / 𝑚 ) + 1 ) ≠ 0 )
27	21 24 26	redivcld	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) ∈ ℝ )
28	27	fmpttd	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) ) : ℕ ⟶ ℝ )
29	28	ffvelcdmda	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ‘ 𝑛 ) ∈ ℝ )
30		remulcl	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑛 · 𝑥 ) ∈ ℝ )
31	30	adantl	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) → ( 𝑛 · 𝑥 ) ∈ ℝ )
32	9 10 29 31	seqf	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → seq 1 ( · , ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) : ℕ ⟶ ℝ )
33	32	ffvelcdmda	⊢ ( ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) ∧ 𝑛 ∈ ℕ ) → ( seq 1 ( · , ( 𝑚 ∈ ℕ ↦ ( ( ( ( 𝑚 + 1 ) / 𝑚 ) ↑𝑐 𝐴 ) / ( ( 𝐴 / 𝑚 ) + 1 ) ) ) ) ‘ 𝑛 ) ∈ ℝ )
34	9 10 12 33	climrecl	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ( ( Γ ‘ 𝐴 ) · 𝐴 ) ∈ ℝ )
35	34 1 7	redivcld	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ( ( ( Γ ‘ 𝐴 ) · 𝐴 ) / 𝐴 ) ∈ ℝ )
36	8 35	eqeltrrd	⊢ ( 𝐴 ∈ ( ℝ ∖ ( ℤ ∖ ℕ ) ) → ( Γ ‘ 𝐴 ) ∈ ℝ )