lgamgulmlem4 - Metamath Proof Explorer

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

Theorem lgamgulmlem4 27364

Description: Lemma for lgamgulm 27367. (Contributed by Mario Carneiro, 3-Jul-2017.)

**Hypotheses**
Ref	Expression
lgamgulm.r	⊢ (𝜑 → 𝑅 ∈ ℕ)
lgamgulm.u	⊢ 𝑈 = {𝑥 ∈ ℂ ∣ ((abs‘𝑥) ≤ 𝑅 ∧ ∀𝑘 ∈ ℕ₀ (1 / 𝑅) ≤ (abs‘(𝑥 + 𝑘)))}
lgamgulm.g	⊢ 𝐺 = (𝑚 ∈ ℕ ↦ (𝑧 ∈ 𝑈 ↦ ((𝑧 · (log‘((𝑚 + 1) / 𝑚))) − (log‘((𝑧 / 𝑚) + 1)))))
lgamgulm.t	⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))

**Assertion**
Ref	Expression
lgamgulmlem4	⊢ (𝜑 → seq1( + , 𝑇) ∈ dom ⇝ )

Distinct variable groups: 𝑘,𝑚,𝑥,𝑧,𝑅 𝑈,𝑚,𝑧 𝜑,𝑚,𝑥,𝑧 Allowed substitution hints: 𝜑(𝑘) 𝑇(𝑥, 𝑧, 𝑘, 𝑚) 𝑈(𝑥, 𝑘) 𝐺(𝑥, 𝑧, 𝑘, 𝑚)

Proof of Theorem lgamgulmlem4 Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn 12419	. . . . . . 7 ⊢ 2 ∈ ℕ
2	1	a1i 11	. . . . . 6 ⊢ (𝜑 → 2 ∈ ℕ)
3		lgamgulm.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ ℕ)
4	2, 3	nnmulcld 12394	. . . . 5 ⊢ (𝜑 → (2 · 𝑅) ∈ ℕ)
5	4	nnzd 12722	. . . 4 ⊢ (𝜑 → (2 · 𝑅) ∈ ℤ)
6		eluzle 12981	. . . . . . 7 ⊢ (𝑛 ∈ (ℤ_≥‘(2 · 𝑅)) → (2 · 𝑅) ≤ 𝑛)
7	6	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(2 · 𝑅))) → (2 · 𝑅) ≤ 𝑛)
8	7	iftrued 4489	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(2 · 𝑅))) → if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))))
9		eluznn 13048	. . . . . . 7 ⊢ (((2 · 𝑅) ∈ ℕ ∧ 𝑛 ∈ (ℤ_≥‘(2 · 𝑅))) → 𝑛 ∈ ℕ)
10	4, 9	sylan 592	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(2 · 𝑅))) → 𝑛 ∈ ℕ)
11		breq2 5106	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((2 · 𝑅) ≤ 𝑚 ↔ (2 · 𝑅) ≤ 𝑛))
12		oveq1 7427	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2))
13	12	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → ((2 · (𝑅 + 1)) / (𝑚↑2)) = ((2 · (𝑅 + 1)) / (𝑛↑2)))
14	13	oveq2d 7436	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))))
15		oveq1 7427	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1))
16		id 23	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛)
17	15, 16	oveq12d 7438	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛))
18	17	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛)))
19	18	oveq2d 7436	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → (𝑅 · (log‘((𝑚 + 1) / 𝑚))) = (𝑅 · (log‘((𝑛 + 1) / 𝑛))))
20		oveq2 7428	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑛 → ((𝑅 + 1) · 𝑚) = ((𝑅 + 1) · 𝑛))
21	20	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (log‘((𝑅 + 1) · 𝑚)) = (log‘((𝑅 + 1) · 𝑛)))
22	21	oveq1d 7435	. . . . . . . . 9 ⊢ (𝑚 = 𝑛 → ((log‘((𝑅 + 1) · 𝑚)) + π) = ((log‘((𝑅 + 1) · 𝑛)) + π))
23	19, 22	oveq12d 7438	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)) = ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))
24	11, 14, 23	ifbieq12d 4510	. . . . . . 7 ⊢ (𝑚 = 𝑛 → if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))
25		lgamgulm.t	. . . . . . 7 ⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))))
26		ovex 7453	. . . . . . . 8 ⊢ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ V
27		ovex 7453	. . . . . . . 8 ⊢ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ V
28	26, 27	ifex 4532	. . . . . . 7 ⊢ if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) ∈ V
29	24, 25, 28	fvmpt 6993	. . . . . 6 ⊢ (𝑛 ∈ ℕ → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))
30	10, 29	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(2 · 𝑅))) → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))
31		eqid 2760	. . . . . . 7 ⊢ (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2)))) = (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))
32	14, 31, 26	fvmpt 6993	. . . . . 6 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))))
33	10, 32	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(2 · 𝑅))) → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))))
34	8, 30, 33	3eqtr4d 2805	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘(2 · 𝑅))) → (𝑇‘𝑛) = ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛))
35	5, 34	seqfeq 14173	. . 3 ⊢ (𝜑 → seq(2 · 𝑅)( + , 𝑇) = seq(2 · 𝑅)( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))))
36		nnuz 13007	. . . . . 6 ⊢ ℕ = (ℤ_≥‘1)
37		1zzd 12730	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℤ)
38	3	nncnd 12354	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ ℂ)
39		2cnd 12424	. . . . . . . 8 ⊢ (𝜑 → 2 ∈ ℂ)
40		1cnd 11305	. . . . . . . . 9 ⊢ (𝜑 → 1 ∈ ℂ)
41	38, 40	addcld 11331	. . . . . . . 8 ⊢ (𝜑 → (𝑅 + 1) ∈ ℂ)
42	39, 41	mulcld 11332	. . . . . . 7 ⊢ (𝜑 → (2 · (𝑅 + 1)) ∈ ℂ)
43	38, 42	mulcld 11332	. . . . . 6 ⊢ (𝜑 → (𝑅 · (2 · (𝑅 + 1))) ∈ ℂ)
44		1lt2 12518	. . . . . . . . . 10 ⊢ 1 < 2
45		2re 12420	. . . . . . . . . . 11 ⊢ 2 ∈ ℝ
46		rere 15294	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ → (ℜ‘2) = 2)
47	45, 46	ax-mp 5	. . . . . . . . . 10 ⊢ (ℜ‘2) = 2
48	44, 47	breqtrri 5131	. . . . . . . . 9 ⊢ 1 < (ℜ‘2)
49	48	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 1 < (ℜ‘2))
50		oveq1 7427	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 → (𝑚↑_𝑐 -2) = (𝑛↑_𝑐 -2))
51		eqid 2760	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2)) = (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))
52		ovex 7453	. . . . . . . . . 10 ⊢ (𝑛↑_𝑐 -2) ∈ V
53	50, 51, 52	fvmpt 6993	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))‘𝑛) = (𝑛↑_𝑐 -2))
54	53	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))‘𝑛) = (𝑛↑_𝑐 -2))
55	39, 49, 54	zetacvg 27347	. . . . . . 7 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))) ∈ dom ⇝ )
56		climdm 15726	. . . . . . 7 ⊢ (seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))) ∈ dom ⇝ ↔ seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))) ⇝ ( ⇝ ‘seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2)))))
57	55, 56	sylib 221	. . . . . 6 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))) ⇝ ( ⇝ ‘seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2)))))
58		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
59	58	nncnd 12354	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ)
60		2cnd 12424	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 2 ∈ ℂ)
61	60	negcld 11659	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -2 ∈ ℂ)
62	59, 61	cxpcld 27041	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑_𝑐 -2) ∈ ℂ)
63	54, 62	eqeltrd 2860	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))‘𝑛) ∈ ℂ)
64	38	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ∈ ℂ)
65		1cnd 11305	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈ ℂ)
66	64, 65	addcld 11331	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈ ℂ)
67	60, 66	mulcld 11332	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2 · (𝑅 + 1)) ∈ ℂ)
68	64, 67	mulcld 11332	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · (2 · (𝑅 + 1))) ∈ ℂ)
69	59	sqcld 14290	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑2) ∈ ℂ)
70	58	nnne0d 12391	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0)
71		2z 12731	. . . . . . . . . . 11 ⊢ 2 ∈ ℤ
72	71	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 2 ∈ ℤ)
73	59, 70, 72	expne0d 14298	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑2) ≠ 0)
74	68, 69, 73	divrecd 12099	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) / (𝑛↑2)) = ((𝑅 · (2 · (𝑅 + 1))) · (1 / (𝑛↑2))))
75	64, 67, 69, 73	divassd 12131	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) / (𝑛↑2)) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))))
76	59, 70, 60	cxpnegd 27048	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑_𝑐 -2) = (1 / (𝑛↑_𝑐2)))
77	59, 70, 72	cxpexpzd 27044	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑_𝑐2) = (𝑛↑2))
78	77	oveq2d 7436	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / (𝑛↑_𝑐2)) = (1 / (𝑛↑2)))
79	76, 78	eqtr2d 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / (𝑛↑2)) = (𝑛↑_𝑐 -2))
80	79	oveq2d 7436	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) · (1 / (𝑛↑2))) = ((𝑅 · (2 · (𝑅 + 1))) · (𝑛↑_𝑐 -2)))
81	74, 75, 80	3eqtr3d 2803	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) = ((𝑅 · (2 · (𝑅 + 1))) · (𝑛↑_𝑐 -2)))
82	32	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))))
83	54	oveq2d 7436	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) · ((𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))‘𝑛)) = ((𝑅 · (2 · (𝑅 + 1))) · (𝑛↑_𝑐 -2)))
84	81, 82, 83	3eqtr4d 2805	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) = ((𝑅 · (2 · (𝑅 + 1))) · ((𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))‘𝑛)))
85	36, 37, 43, 57, 63, 84	isermulc2 15830	. . . . 5 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ⇝ ((𝑅 · (2 · (𝑅 + 1))) · ( ⇝ ‘seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))))))
86		climrel 15664	. . . . . 6 ⊢ Rel ⇝
87	86	releldmi 5929	. . . . 5 ⊢ (seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ⇝ ((𝑅 · (2 · (𝑅 + 1))) · ( ⇝ ‘seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑_𝑐 -2))))) → seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝ )
88	85, 87	syl 18	. . . 4 ⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝ )
89	67, 69, 73	divcld 12096	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2 · (𝑅 + 1)) / (𝑛↑2)) ∈ ℂ)
90	64, 89	mulcld 11332	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ ℂ)
91	82, 90	eqeltrd 2860	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) ∈ ℂ)
92	36, 4, 91	iserex 15829	. . . 4 ⊢ (𝜑 → (seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝ ↔ seq(2 · 𝑅)( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝ ))
93	88, 92	mpbid 235	. . 3 ⊢ (𝜑 → seq(2 · 𝑅)( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝ )
94	35, 93	eqeltrd 2860	. 2 ⊢ (𝜑 → seq(2 · 𝑅)( + , 𝑇) ∈ dom ⇝ )
95	29	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))))
96	3	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ∈ ℕ)
97	96	nnred 12353	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ∈ ℝ)
98	45	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 2 ∈ ℝ)
99		1red 11312	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈ ℝ)
100	97, 99	readdcld 11341	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈ ℝ)
101	98, 100	remulcld 11342	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2 · (𝑅 + 1)) ∈ ℝ)
102	58	nnsqcld 14391	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑2) ∈ ℕ)
103	101, 102	nndivred 12395	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2 · (𝑅 + 1)) / (𝑛↑2)) ∈ ℝ)
104	97, 103	remulcld 11342	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ ℝ)
105	58	peano2nnd 12355	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ)
106	105	nnrpd 13165	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℝ⁺)
107	58	nnrpd 13165	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ⁺)
108	106, 107	rpdivcld 13184	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) / 𝑛) ∈ ℝ⁺)
109	108	relogcld 26956	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ)
110	97, 109	remulcld 11342	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℝ)
111	96	peano2nnd 12355	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈ ℕ)
112	111	nnrpd 13165	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈ ℝ⁺)
113	112, 107	rpmulcld 13183	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 + 1) · 𝑛) ∈ ℝ⁺)
114	113	relogcld 26956	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝑅 + 1) · 𝑛)) ∈ ℝ)
115		pire 26788	. . . . . . . . 9 ⊢ π ∈ ℝ
116	115	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈ ℝ)
117	114, 116	readdcld 11341	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘((𝑅 + 1) · 𝑛)) + π) ∈ ℝ)
118	110, 117	readdcld 11341	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ ℝ)
119	104, 118	ifcld 4528	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) ∈ ℝ)
120	95, 119	eqeltrd 2860	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑛) ∈ ℝ)
121	120	recnd 11340	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑛) ∈ ℂ)
122	36, 4, 121	iserex 15829	. 2 ⊢ (𝜑 → (seq1( + , 𝑇) ∈ dom ⇝ ↔ seq(2 · 𝑅)( + , 𝑇) ∈ dom ⇝ ))
123	94, 122	mpbird 260	1 ⊢ (𝜑 → seq1( + , 𝑇) ∈ dom ⇝ )

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∀wral 3076 {crab 3412 ifcif 4481 class class class wbr 5102 ↦ cmpt 5185 dom cdm 5650 ‘cfv 6538 (class class class)co 7420 ℂcc 11201 ℝcr 11202 1c1 11204 + caddc 11206 · cmul 11208 < clt 11346 ≤ cle 11347 − cmin 11544 -cneg 11545 / cdiv 11976 ℕcn 12338 2c2 12400 ℕ₀cn0 12609 ℤcz 12696 ℤ_≥cuz 12968 seqcseq 14147 ↑cexp 14207 ℜcre 15269 abscabs 15406 ⇝ cli 15656 πcpi 16237 logclog 26887 ↑_𝑐ccxp 26888

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9645 ax-cnex 11259 ax-resscn 11260 ax-1cn 11261 ax-icn 11262 ax-addcl 11263 ax-addrcl 11264 ax-mulcl 11265 ax-mulrcl 11266 ax-mulcom 11267 ax-addass 11268 ax-mulass 11269 ax-distr 11270 ax-i2m1 11271 ax-1ne0 11272 ax-1rid 11273 ax-rnegex 11274 ax-rrecex 11275 ax-cnre 11276 ax-pre-lttri 11277 ax-pre-lttrn 11278 ax-pre-ltadd 11279 ax-pre-mulgt0 11280 ax-pre-sup 11281 ax-addf 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8180 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-rdg 8421 df-1o 8479 df-2o 8480 df-oadd 8483 df-er 8720 df-map 8852 df-pm 8853 df-ixp 8929 df-en 8977 df-dom 8978 df-sdom 8979 df-fin 8980 df-fsupp 9357 df-fi 9406 df-sup 9437 df-inf 9438 df-oi 9507 df-dju 9985 df-card 10023 df-pnf 11348 df-mnf 11349 df-xr 11350 df-ltxr 11351 df-le 11352 df-sub 11546 df-neg 11547 df-div 11977 df-nn 12339 df-2 12408 df-3 12409 df-4 12410 df-5 12411 df-6 12412 df-7 12413 df-8 12414 df-9 12415 df-n0 12610 df-z 12697 df-dec 12818 df-uz 12969 df-q 13079 df-rp 13124 df-xneg 13244 df-xadd 13245 df-xmul 13246 df-ioo 13483 df-ioc 13484 df-ico 13485 df-icc 13486 df-fz 13643 df-fzo 13792 df-fl 13935 df-mod 14013 df-seq 14148 df-exp 14208 df-fac 14421 df-bc 14450 df-hash 14478 df-shft 15225 df-cj 15271 df-re 15272 df-im 15273 df-sqrt 15407 df-abs 15408 df-limsup 15643 df-clim 15660 df-rlim 15661 df-sum 15859 df-ef 16238 df-sin 16240 df-cos 16241 df-pi 16243 df-struct 17330 df-sets 17347 df-slot 17365 df-ndx 17377 df-base 17393 df-ress 17414 df-plusg 17446 df-mulr 17447 df-starv 17448 df-sca 17449 df-vsca 17450 df-ip 17451 df-tset 17452 df-ple 17453 df-ds 17455 df-unif 17456 df-hom 17457 df-cco 17458 df-rest 17598 df-topn 17599 df-0g 17617 df-gsum 17618 df-topgen 17619 df-pt 17620 df-prds 17623 df-xrs 17679 df-qtop 17684 df-imas 17685 df-xps 17687 df-mre 17761 df-mrc 17762 df-acs 17764 df-mgm 18821 df-sgrp 18913 df-mnd 18929 df-submnd 18984 df-mulg 19283 df-cntz 19536 df-cmn 20001 df-psmet 21675 df-xmet 21676 df-met 21677 df-bl 21678 df-mopn 21679 df-fbas 21680 df-fg 21681 df-cnfld 21684 df-top 23217 df-topon 23234 df-topsp 23256 df-bases 23269 df-cld 23342 df-ntr 23343 df-cls 23344 df-nei 23421 df-lp 23459 df-perf 23460 df-cn 23550 df-cnp 23551 df-haus 23638 df-tx 23886 df-hmeo 24079 df-fil 24170 df-fm 24262 df-flim 24263 df-flf 24264 df-xms 24644 df-ms 24645 df-tms 24646 df-cncf 25204 df-limc 26191 df-dv 26192 df-log 26889 df-cxp 26890

This theorem is used by: lgamgulmlem6 27366

W3C validator