Theorem faclimlem1 36235

Description: Lemma for faclim 36238. Closed form for a particular sequence. (Contributed by Scott Fenton, 15-Dec-2017.)

Assertion

Ref	Expression
faclimlem1	⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))))

Distinct variable groups:   𝑛,𝑀   𝑥,𝑀

Proof of Theorem faclimlem1

Dummy variables 𝑎 𝑏 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6881	. . . . . . . . 9 ⊢ (𝑎 = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1))
2		1z 12619	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
3		seq1 14046	. . . . . . . . . 10 ⊢ (1 ∈ ℤ → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1))
4	2, 3	ax-mp 5	. . . . . . . . 9 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1)
5	1, 4	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑎 = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1))
6		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = 1 → (𝑎 + 1) = (1 + 1))
7		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = 1 → (𝑎 + (𝑀 + 1)) = (1 + (𝑀 + 1)))
8	6, 7	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑎 = 1 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((1 + 1) / (1 + (𝑀 + 1))))
9	8	oveq2d 7426	. . . . . . . 8 ⊢ (𝑎 = 1 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
10	5, 9	eqeq12d 2779	. . . . . . 7 ⊢ (𝑎 = 1 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1))))))
11	10	imbi2d 343	. . . . . 6 ⊢ (𝑎 = 1 → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))))
12		fveq2 6881	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘))
13		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (𝑎 + 1) = (𝑘 + 1))
14		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (𝑎 + (𝑀 + 1)) = (𝑘 + (𝑀 + 1)))
15	13, 14	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))
16	15	oveq2d 7426	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))))
17	12, 16	eqeq12d 2779	. . . . . . 7 ⊢ (𝑎 = 𝑘 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))))
18	17	imbi2d 343	. . . . . 6 ⊢ (𝑎 = 𝑘 → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))))))
19		fveq2 6881	. . . . . . . 8 ⊢ (𝑎 = (𝑘 + 1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)))
20		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 + 1) → (𝑎 + 1) = ((𝑘 + 1) + 1))
21		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 + 1) → (𝑎 + (𝑀 + 1)) = ((𝑘 + 1) + (𝑀 + 1)))
22	20, 21	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 + 1) → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
23	22	oveq2d 7426	. . . . . . . 8 ⊢ (𝑎 = (𝑘 + 1) → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
24	19, 23	eqeq12d 2779	. . . . . . 7 ⊢ (𝑎 = (𝑘 + 1) → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))))
25	24	imbi2d 343	. . . . . 6 ⊢ (𝑎 = (𝑘 + 1) → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))))
26		fveq2 6881	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏))
27		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝑎 + 1) = (𝑏 + 1))
28		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝑎 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1)))
29	27, 28	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))
30	29	oveq2d 7426	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
31	26, 30	eqeq12d 2779	. . . . . . 7 ⊢ (𝑎 = 𝑏 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))))
32	31	imbi2d 343	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))))
33		1nn 12239	. . . . . . . 8 ⊢ 1 ∈ ℕ
34		oveq2 7418	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝑀 / 𝑛) = (𝑀 / 1))
35	34	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / 1)))
36		oveq2 7418	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1))
37	36	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → (1 + (1 / 𝑛)) = (1 + (1 / 1)))
38	35, 37	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / 1)) · (1 + (1 / 1))))
39		oveq2 7418	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / 1))
40	39	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / 1)))
41	38, 40	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑛 = 1 → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))))
42		eqid 2763	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))
43		ovex 7443	. . . . . . . . 9 ⊢ (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) ∈ V
44	41, 42, 43	fvmpt 6989	. . . . . . . 8 ⊢ (1 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))))
45	33, 44	ax-mp 5	. . . . . . 7 ⊢ ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1)))
46		nn0cn 12509	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ)
47	46	div1d 11978	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → (𝑀 / 1) = 𝑀)
48	47	oveq2d 7426	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 / 1)) = (1 + 𝑀))
49		1div1e1 11900	. . . . . . . . . . . 12 ⊢ (1 / 1) = 1
50	49	oveq2i 7421	. . . . . . . . . . 11 ⊢ (1 + (1 / 1)) = (1 + 1)
51	50	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (1 / 1)) = (1 + 1))
52	48, 51	oveq12d 7428	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → ((1 + (𝑀 / 1)) · (1 + (1 / 1))) = ((1 + 𝑀) · (1 + 1)))
53		nn0p1nn 12538	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
54	53	nncnd 12244	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℂ)
55	54	div1d 11978	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → ((𝑀 + 1) / 1) = (𝑀 + 1))
56	55	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + ((𝑀 + 1) / 1)) = (1 + (𝑀 + 1)))
57	52, 56	oveq12d 7428	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = (((1 + 𝑀) · (1 + 1)) / (1 + (𝑀 + 1))))
58		1cnd 11197	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → 1 ∈ ℂ)
59	58, 46	addcomd 11407	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + 𝑀) = (𝑀 + 1))
60	59	oveq1d 7425	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → ((1 + 𝑀) · (1 + 1)) = ((𝑀 + 1) · (1 + 1)))
61	60	oveq1d 7425	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((1 + 𝑀) · (1 + 1)) / (1 + (𝑀 + 1))) = (((𝑀 + 1) · (1 + 1)) / (1 + (𝑀 + 1))))
62		ax-1cn 11153	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
63	62, 62	addcli 11210	. . . . . . . . . 10 ⊢ (1 + 1) ∈ ℂ
64	63	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + 1) ∈ ℂ)
65	33	a1i 11	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → 1 ∈ ℕ)
66	65, 53	nnaddcld 12283	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ∈ ℕ)
67	66	nncnd 12244	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ∈ ℂ)
68	66	nnne0d 12281	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ≠ 0)
69	54, 64, 67, 68	divassd 12021	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((𝑀 + 1) · (1 + 1)) / (1 + (𝑀 + 1))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
70	57, 61, 69	3eqtrd 2802	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
71	45, 70	eqtrid 2810	. . . . . 6 ⊢ (𝑀 ∈ ℕ0 → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
72		seqp1 14048	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
73		nnuz 12896	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
74	72, 73	eleq2s 2881	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
75	74	adantr 485	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
76	75	adantr 485	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) ∧ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
77		oveq1 7417	. . . . . . . . . 10 ⊢ ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
78	77	adantl 486	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) ∧ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
79		peano2nn 12240	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
80		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑘 + 1) → (𝑀 / 𝑛) = (𝑀 / (𝑘 + 1)))
81	80	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / (𝑘 + 1))))
82		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1)))
83	82	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → (1 + (1 / 𝑛)) = (1 + (1 / (𝑘 + 1))))
84	81, 83	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 + 1) → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))
85		oveq2 7418	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / (𝑘 + 1)))
86	85	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 + 1) → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / (𝑘 + 1))))
87	84, 86	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑘 + 1) → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
88		ovex 7443	. . . . . . . . . . . . . . 15 ⊢ (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ V
89	87, 42, 88	fvmpt 6989	. . . . . . . . . . . . . 14 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
90	79, 89	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
91	90	oveq2d 7426	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))))
92	91	adantr 485	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))))
93	53	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ)
94	93	nncnd 12244	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℂ)
95	79	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ)
96	95	nnrpd 13053	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ+)
97		simpl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℕ)
98	97	nnrpd 13053	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℝ+)
99	93	nnrpd 13053	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℝ+)
100	98, 99	rpaddcld 13070	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ∈ ℝ+)
101	96, 100	rpdivcld 13072	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ ℝ+)
102	101	rpcnd 13057	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ ℂ)
103		1cnd 11197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℂ)
104		nn0re 12508	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
105	104	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℝ)
106	105, 95	nndivred 12285	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 / (𝑘 + 1)) ∈ ℝ)
107	106	recnd 11232	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 / (𝑘 + 1)) ∈ ℂ)
108	103, 107	addcomd 11407	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) = ((𝑀 / (𝑘 + 1)) + 1))
109		nn0ge0 12524	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
110	109	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 0 ≤ 𝑀)
111	105, 96, 110	divge0d 13095	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑀 / (𝑘 + 1)))
112	106, 111	ge0p1rpd 13085	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 / (𝑘 + 1)) + 1) ∈ ℝ+)
113	108, 112	eqeltrd 2863	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) ∈ ℝ+)
114		1rp 13015	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ+
115	114	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℝ+)
116	96	rpreccld 13065	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 / (𝑘 + 1)) ∈ ℝ+)
117	115, 116	rpaddcld 13070	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (1 / (𝑘 + 1))) ∈ ℝ+)
118	113, 117	rpmulcld 13071	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) ∈ ℝ+)
119	99, 96	rpdivcld 13072	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) / (𝑘 + 1)) ∈ ℝ+)
120	115, 119	rpaddcld 13070	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ∈ ℝ+)
121	118, 120	rpdivcld 13072	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ ℝ+)
122	121	rpcnd 13057	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ ℂ)
123	94, 102, 122	mulassd 11227	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) = ((𝑀 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))))
124	101, 118	rpmulcld 13071	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈ ℝ+)
125	124	rpcnd 13057	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈ ℂ)
126	120	rpcnd 13057	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ∈ ℂ)
127	95	nncnd 12244	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℂ)
128	120	rpne0d 13060	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ≠ 0)
129	95	nnne0d 12281	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ≠ 0)
130	125, 126, 127, 128, 129	divcan5d 12012	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) / ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1))))) = ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
131	118	rpcnd 13057	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) ∈ ℂ)
132	127, 102, 131	mul12d 11414	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))))
133	113	rpcnd 13057	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) ∈ ℂ)
134	117	rpcnd 13057	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (1 / (𝑘 + 1))) ∈ ℂ)
135	127, 133, 134	mulassd 11227	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))))
136	127, 103, 107	adddid 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · (𝑀 / (𝑘 + 1)))))
137	127	mulridd 11221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · 1) = (𝑘 + 1))
138		simpr 489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
139	138	nn0cnd 12562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℂ)
140	139, 127, 129	divcan2d 11988	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (𝑀 / (𝑘 + 1))) = 𝑀)
141	137, 140	oveq12d 7428	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · (𝑀 / (𝑘 + 1)))) = ((𝑘 + 1) + 𝑀))
142	97	nncnd 12244	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℂ)
143	142, 103, 139	addassd 11226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) + 𝑀) = (𝑘 + (1 + 𝑀)))
144	103, 139	addcomd 11407	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + 𝑀) = (𝑀 + 1))
145	144	oveq2d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (1 + 𝑀)) = (𝑘 + (𝑀 + 1)))
146	143, 145	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) + 𝑀) = (𝑘 + (𝑀 + 1)))
147	136, 141, 146	3eqtrd 2802	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) = (𝑘 + (𝑀 + 1)))
148	147	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))
149	135, 148	eqtr3d 2800	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))
150	149	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))))
151	100	rpcnd 13057	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ∈ ℂ)
152	102, 151, 134	mulassd 11227	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))))
153	100	rpne0d 13060	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ≠ 0)
154	127, 151, 153	divcan1d 11987	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) = (𝑘 + 1))
155	154	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) · (1 + (1 / (𝑘 + 1)))))
156	116	rpcnd 13057	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 / (𝑘 + 1)) ∈ ℂ)
157	127, 103, 156	adddid 11228	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (1 / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · (1 / (𝑘 + 1)))))
158	103, 127, 129	divcan2d 11988	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 / (𝑘 + 1))) = 1)
159	137, 158	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · (1 / (𝑘 + 1)))) = ((𝑘 + 1) + 1))
160	155, 157, 159	3eqtrd 2802	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) + 1))
161	152, 160	eqtr3d 2800	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))) = ((𝑘 + 1) + 1))
162	132, 150, 161	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = ((𝑘 + 1) + 1))
163	119	rpcnd 13057	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) / (𝑘 + 1)) ∈ ℂ)
164	127, 103, 163	adddid 11228	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1)))))
165	94, 127, 129	divcan2d 11988	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1))) = (𝑀 + 1))
166	137, 165	oveq12d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1)))
167	164, 166	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1)))
168	162, 167	oveq12d 7428	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) / ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
169	102, 131, 126, 128	divassd 12021	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))))
170	130, 168, 169	3eqtr3rd 2807	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
171	170	oveq2d 7426	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
172	92, 123, 171	3eqtrd 2802	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
173	172	adantr 485	. . . . . . . . 9 ⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) ∧ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
174	76, 78, 173	3eqtrd 2802	. . . . . . . 8 ⊢ (((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) ∧ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
175	174	exp31 424	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝑀 ∈ ℕ0 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))))
176	175	a2d 30	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))) → (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))))
177	11, 18, 25, 32, 71, 176	nnind 12246	. . . . 5 ⊢ (𝑏 ∈ ℕ → (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))))
178	177	impcom 412	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
179		oveq1 7417	. . . . . . . 8 ⊢ (𝑥 = 𝑏 → (𝑥 + 1) = (𝑏 + 1))
180		oveq1 7417	. . . . . . . 8 ⊢ (𝑥 = 𝑏 → (𝑥 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1)))
181	179, 180	oveq12d 7428	. . . . . . 7 ⊢ (𝑥 = 𝑏 → ((𝑥 + 1) / (𝑥 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))
182	181	oveq2d 7426	. . . . . 6 ⊢ (𝑥 = 𝑏 → ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
183		eqid 2763	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))
184		ovex 7443	. . . . . 6 ⊢ ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))) ∈ V
185	182, 183, 184	fvmpt 6989	. . . . 5 ⊢ (𝑏 ∈ ℕ → ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
186	185	adantl 486	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
187	178, 186	eqtr4d 2801	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
188	187	ralrimiva 3157	. 2 ⊢ (𝑀 ∈ ℕ0 → ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
189		seqfn 14045	. . . . 5 ⊢ (1 ∈ ℤ → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn (ℤ≥‘1))
190	2, 189	ax-mp 5	. . . 4 ⊢ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn (ℤ≥‘1)
191	73	fneq2i 6633	. . . 4 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ ↔ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn (ℤ≥‘1))
192	190, 191	mpbir 234	. . 3 ⊢ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ
193		ovex 7443	. . . 4 ⊢ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) ∈ V
194	193, 183	fnmpti 6678	. . 3 ⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) Fn ℕ
195		eqfnfv 7025	. . 3 ⊢ ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ ∧ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) Fn ℕ) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) ↔ ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏)))
196	192, 194, 195	mp2an 704	. 2 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) ↔ ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
197	188, 196	sylibr 237	1 ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079   class class class wbr 5109   ↦ cmpt 5192   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410  ℂcc 11093  ℝcr 11094  0cc0 11095  1c1 11096   + caddc 11098   · cmul 11100   ≤ cle 11239   / cdiv 11866  ℕcn 12228  ℕ₀cn0 12499  ℤcz 12586  ℤ_≥cuz 12857  ℝ⁺crp 13011  seqcseq 14033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-n0 12500  df-z 12587  df-uz 12858  df-rp 13012  df-seq 14034

This theorem is referenced by:  faclimlem2  36236