lgamcvglem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lgamcvglem		Structured version Visualization version GIF version

Theorem lgamcvglem 27101

Description: Lemma for lgamf 27103 and lgamcvg 27115. (Contributed by Mario Carneiro, 8-Jul-2017.)

**Hypotheses**
Ref	Expression
lgamucov.u	⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
lgamucov.a	⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
lgamcvglem.g	⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))

**Assertion**
Ref	Expression
lgamcvglem	⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))))

Distinct variable groups: 𝑘,𝑚,𝑟,𝑥,𝐴 𝐺,𝑟 𝜑,𝑘,𝑚,𝑟,𝑥 𝑈,𝑚 Allowed substitution hints: 𝑈(𝑥,𝑘,𝑟) 𝐺(𝑥,𝑘,𝑚)

Proof of Theorem lgamcvglem Dummy variables 𝑛 𝑡 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lgamucov.u	. . 3 ⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))}
2		lgamucov.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ (ℂ ∖ (ℤ ∖ ℕ)))
3	1, 2	lgamucov2 27100	. 2 ⊢ (𝜑 → ∃𝑟 ∈ ℕ 𝐴 ∈ 𝑈)
4		fveq2 6867	. . . . 5 ⊢ (𝑧 = 𝐴 → (log Γ‘𝑧) = (log Γ‘𝐴))
5	4	eleq1d 2847	. . . 4 ⊢ (𝑧 = 𝐴 → ((log Γ‘𝑧) ∈ ℂ ↔ (log Γ‘𝐴) ∈ ℂ))
6		simprl 780	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 𝑟 ∈ ℕ)
7		fveq2 6867	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → (abs‘𝑥) = (abs‘𝑡))
8	7	breq1d 5110	. . . . . . . . 9 ⊢ (𝑥 = 𝑡 → ((abs‘𝑥) ≤ 𝑟 ↔ (abs‘𝑡) ≤ 𝑟))
9		fvoveq1 7419	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → (abs‘(𝑥 + 𝑘)) = (abs‘(𝑡 + 𝑘)))
10	9	breq2d 5112	. . . . . . . . . 10 ⊢ (𝑥 = 𝑡 → ((1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)) ↔ (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘))))
11	10	ralbidv 3185	. . . . . . . . 9 ⊢ (𝑥 = 𝑡 → (∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)) ↔ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘))))
12	8, 11	anbi12d 641	. . . . . . . 8 ⊢ (𝑥 = 𝑡 → (((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘))) ↔ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))))
13	12	cbvrabv 3424	. . . . . . 7 ⊢ {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑥 + 𝑘)))} = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))}
14	1, 13	eqtri 2785	. . . . . 6 ⊢ 𝑈 = {𝑡 ∈ ℂ ∣ ((abs‘𝑡) ≤ 𝑟 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑟) ≤ (abs‘(𝑡 + 𝑘)))}
15		eqid 2762	. . . . . 6 ⊢ (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))
16	6, 14, 15	lgamgulm2 27097	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → (∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ ∧ seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))(⇝_𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))))
17	16	simpld 498	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ∀𝑧 ∈ 𝑈 (log Γ‘𝑧) ∈ ℂ)
18		simprr 782	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 𝐴 ∈ 𝑈)
19	5, 17, 18	rspcdva 3582	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → (log Γ‘𝐴) ∈ ℂ)
20		nnuz 12878	. . . . 5 ⊢ ℕ = (ℤ_≥‘1)
21		1zzd 12602	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → 1 ∈ ℤ)
22		1z 12601	. . . . . . . 8 ⊢ 1 ∈ ℤ
23		seqfn 14026	. . . . . . . 8 ⊢ (1 ∈ ℤ → seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn (ℤ_≥‘1))
24	22, 23	ax-mp 5	. . . . . . 7 ⊢ seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn (ℤ_≥‘1)
25	20	fneq2i 6619	. . . . . . 7 ⊢ (seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ ↔ seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn (ℤ_≥‘1))
26	24, 25	mpbir 233	. . . . . 6 ⊢ seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ
27	16	simprd 499	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))(⇝_𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))))
28		ulmf2 26444	. . . . . 6 ⊢ ((seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))) Fn ℕ ∧ seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))(⇝_𝑢‘𝑈)(𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))) → seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))):ℕ⟶(ℂ ↑_m 𝑈))
29	26, 27, 28	sylancr 596	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))):ℕ⟶(ℂ ↑_m 𝑈))
30		seqex 14016	. . . . . 6 ⊢ seq1( + , 𝐺) ∈ V
31	30	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ∈ V)
32		cnex 11154	. . . . . . . . 9 ⊢ ℂ ∈ V
33	1, 32	rabex2 5297	. . . . . . . 8 ⊢ 𝑈 ∈ V
34	33	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑈 ∈ V)
35		simpr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
36	35, 20	eleqtrdi 2872	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ (ℤ_≥‘1))
37		fz1ssnn 13560	. . . . . . . 8 ⊢ (1...𝑛) ⊆ ℕ
38	37	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (1...𝑛) ⊆ ℕ)
39		ovexd 7431	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ (𝑚 ∈ ℕ ∧ 𝑧 ∈ 𝑈)) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) ∈ V)
40	34, 36, 38, 39	seqof2 14073	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛) = (𝑧 ∈ 𝑈 ↦ (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛)))
41		simplr 778	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → 𝑧 = 𝐴)
42	41	oveq1d 7411	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 · (log‘((𝑚 + 1) / 𝑚))) = (𝐴 · (log‘((𝑚 + 1) / 𝑚))))
43	41	oveq1d 7411	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (𝑧 / 𝑚) = (𝐴 / 𝑚))
44	43	fvoveq1d 7418	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → (log‘((𝑧 / 𝑚) + 1)) = (log‘((𝐴 / 𝑚) + 1)))
45	42, 44	oveq12d 7414	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) ∧ 𝑚 ∈ ℕ) → ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))) = ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
46	45	mpteq2dva 5193	. . . . . . . . 9 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1)))))
47		lgamcvglem.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑚 ∈ ℕ ↦ ((𝐴 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝐴 / 𝑚) + 1))))
48	46, 47	eqtr4di 2815	. . . . . . . 8 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))) = 𝐺)
49	48	seqeq3d 14022	. . . . . . 7 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))) = seq1( + , 𝐺))
50	49	fveq1d 6869	. . . . . 6 ⊢ ((((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) ∧ 𝑧 = 𝐴) → (seq1( + , (𝑚 ∈ ℕ ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))‘𝑛) = (seq1( + , 𝐺)‘𝑛))
51		simplrr 787	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → 𝐴 ∈ 𝑈)
52		fvexd 6882	. . . . . 6 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → (seq1( + , 𝐺)‘𝑛) ∈ V)
53	40, 50, 51, 52	fvmptd 6983	. . . . 5 ⊢ (((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) ∧ 𝑛 ∈ ℕ) → ((seq1( ∘_f + , (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1))))))‘𝑛)‘𝐴) = (seq1( + , 𝐺)‘𝑛))
54	20, 21, 29, 18, 31, 53, 27	ulmclm 26447	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ⇝ ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴))
55		fveq2 6867	. . . . . . 7 ⊢ (𝑧 = 𝐴 → (log‘𝑧) = (log‘𝐴))
56	4, 55	oveq12d 7414	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((log Γ‘𝑧) + (log‘𝑧)) = ((log Γ‘𝐴) + (log‘𝐴)))
57		eqid 2762	. . . . . 6 ⊢ (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧))) = (𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))
58		ovex 7429	. . . . . 6 ⊢ ((log Γ‘𝐴) + (log‘𝐴)) ∈ V
59	56, 57, 58	fvmpt 6975	. . . . 5 ⊢ (𝐴 ∈ 𝑈 → ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴) = ((log Γ‘𝐴) + (log‘𝐴)))
60	18, 59	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ((𝑧 ∈ 𝑈 ↦ ((log Γ‘𝑧) + (log‘𝑧)))‘𝐴) = ((log Γ‘𝐴) + (log‘𝐴)))
61	54, 60	breqtrd 5126	. . 3 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴)))
62	19, 61	jca 519	. 2 ⊢ ((𝜑 ∧ (𝑟 ∈ ℕ ∧ 𝐴 ∈ 𝑈)) → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))))
63	3, 62	rexlimddv 3169	1 ⊢ (𝜑 → ((log Γ‘𝐴) ∈ ℂ ∧ seq1( + , 𝐺) ⇝ ((log Γ‘𝐴) + (log‘𝐴))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 = wceq 1560 ∈ wcel 2142 ∀wral 3076 {crab 3414 Vcvv 3454 ∖ cdif 3901 ⊆ wss 3904 class class class wbr 5100 ↦ cmpt 5181 Fn wfn 6516 ⟶wf 6517 ‘cfv 6521 (class class class)co 7396 ∘_f cof 7658 ↑_m cmap 8808 ℂcc 11071 1c1 11074 + caddc 11076 · cmul 11078 ≤ cle 11217 − cmin 11414 / cdiv 11844 ℕcn 12210 ℕ₀cn0 12481 ℤcz 12568 ℤ_≥cuz 12839 ...cfz 13512 seqcseq 14014 abscabs 15261 ⇝ cli 15511 ⇝_𝑢culm 26436 logclog 26616 log Γclgam 27077

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-inf2 9596 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151 ax-addf 11152

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8678 df-map 8810 df-pm 8811 df-ixp 8880 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-fi 9357 df-sup 9388 df-inf 9389 df-oi 9458 df-dju 9859 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-q 12950 df-rp 12994 df-xneg 13114 df-xadd 13115 df-xmul 13116 df-ioo 13353 df-ioc 13354 df-ico 13355 df-icc 13356 df-fz 13513 df-fzo 13660 df-fl 13802 df-mod 13880 df-seq 14015 df-exp 14075 df-fac 14287 df-bc 14316 df-hash 14344 df-shft 15080 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-limsup 15498 df-clim 15515 df-rlim 15516 df-sum 15714 df-ef 16097 df-sin 16099 df-cos 16100 df-tan 16101 df-pi 16102 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-starv 17301 df-sca 17302 df-vsca 17303 df-ip 17304 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-hom 17310 df-cco 17311 df-rest 17451 df-topn 17452 df-0g 17470 df-gsum 17471 df-topgen 17472 df-pt 17473 df-prds 17476 df-xrs 17532 df-qtop 17537 df-imas 17538 df-xps 17540 df-mre 17614 df-mrc 17615 df-acs 17617 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-submnd 18818 df-mulg 19110 df-cntz 19357 df-cmn 19822 df-psmet 21413 df-xmet 21414 df-met 21415 df-bl 21416 df-mopn 21417 df-fbas 21418 df-fg 21419 df-cnfld 21422 df-top 22951 df-topon 22968 df-topsp 22990 df-bases 23003 df-cld 23076 df-ntr 23077 df-cls 23078 df-nei 23155 df-lp 23193 df-perf 23194 df-cn 23284 df-cnp 23285 df-haus 23372 df-cmp 23444 df-tx 23619 df-hmeo 23812 df-fil 23903 df-fm 23995 df-flim 23996 df-flf 23997 df-xms 24377 df-ms 24378 df-tms 24379 df-cncf 24937 df-limc 25925 df-dv 25926 df-ulm 26437 df-log 26618 df-cxp 26619 df-lgam 27080

This theorem is referenced by: lgamcl 27102 lgamcvg 27115

W3C validator