Metamath Proof Explorer

Theorem regamcl

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

Ref Expression
Assertion regamcl ⊢A∈ℝ∖ℤ∖ℕ→Γ⁡A∈ℝ

Proof

Step Hyp Ref Expression
1 eldifi ⊢A∈ℝ∖ℤ∖ℕ→A∈ℝ
2 1 recnd ⊢A∈ℝ∖ℤ∖ℕ→A∈ℂ
3 eldifn ⊢A∈ℝ∖ℤ∖ℕ→¬A∈ℤ∖ℕ
4 2 3 eldifd ⊢A∈ℝ∖ℤ∖ℕ→A∈ℂ∖ℤ∖ℕ
5 gamcl ⊢A∈ℂ∖ℤ∖ℕ→Γ⁡A∈ℂ
6 4 5 syl ⊢A∈ℝ∖ℤ∖ℕ→Γ⁡A∈ℂ
7 4 dmgmn0 ⊢A∈ℝ∖ℤ∖ℕ→A≠0
8 6 2 7 divcan4d ⊢A∈ℝ∖ℤ∖ℕ→Γ⁡A⁢AA=Γ⁡A
9 nnuz ⊢ℕ=ℤ≥1
10 1zzd ⊢A∈ℝ∖ℤ∖ℕ→1∈ℤ
11 eqid ⊢m∈ℕ⟼m+1mAAm+1=m∈ℕ⟼m+1mAAm+1
12 11 4 gamcvg2 ⊢A∈ℝ∖ℤ∖ℕ→seq1×m∈ℕ⟼m+1mAAm+1⇝Γ⁡A⁢A
13 simpr ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m∈ℕ
14 13 peano2nnd ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m+1∈ℕ
15 14 nnrpd ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m+1∈ℝ+
16 13 nnrpd ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m∈ℝ+
17 15 16 rpdivcld ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m+1m∈ℝ+
18 17 rpred ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m+1m∈ℝ
19 17 rpge0d ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→0≤m+1m
20 1 adantr ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→A∈ℝ
21 18 19 20 recxpcld ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m+1mA∈ℝ
22 20 13 nndivred ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→Am∈ℝ
23 1red ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→1∈ℝ
24 22 23 readdcld ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→Am+1∈ℝ
25 4 adantr ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→A∈ℂ∖ℤ∖ℕ
26 25 13 dmgmdivn0 ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→Am+1≠0
27 21 24 26 redivcld ⊢A∈ℝ∖ℤ∖ℕ∧m∈ℕ→m+1mAAm+1∈ℝ
28 27 fmpttd ⊢A∈ℝ∖ℤ∖ℕ→m∈ℕ⟼m+1mAAm+1:ℕ⟶ℝ
29 28 ffvelcdmda ⊢A∈ℝ∖ℤ∖ℕ∧n∈ℕ→m∈ℕ⟼m+1mAAm+1⁡n∈ℝ
30 remulcl ⊢n∈ℝ∧x∈ℝ→n⁢x∈ℝ
31 30 adantl ⊢A∈ℝ∖ℤ∖ℕ∧n∈ℝ∧x∈ℝ→n⁢x∈ℝ
32 9 10 29 31 seqf ⊢A∈ℝ∖ℤ∖ℕ→seq1×m∈ℕ⟼m+1mAAm+1:ℕ⟶ℝ
33 32 ffvelcdmda ⊢A∈ℝ∖ℤ∖ℕ∧n∈ℕ→seq1×m∈ℕ⟼m+1mAAm+1⁡n∈ℝ
34 9 10 12 33 climrecl ⊢A∈ℝ∖ℤ∖ℕ→Γ⁡A⁢A∈ℝ
35 34 1 7 redivcld ⊢A∈ℝ∖ℤ∖ℕ→Γ⁡A⁢AA∈ℝ
36 8 35 eqeltrrd ⊢A∈ℝ∖ℤ∖ℕ→Γ⁡A∈ℝ