Theorem faclimlem1 35959

Description: Lemma for faclim 35962. 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 6842	. . . . . . . . 9 ⊢ (𝑎 = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1))
2		1z 12533	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
3		seq1 13949	. . . . . . . . . 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 2788	. . . . . . . 8 ⊢ (𝑎 = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1))
6		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = 1 → (𝑎 + 1) = (1 + 1))
7		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = 1 → (𝑎 + (𝑀 + 1)) = (1 + (𝑀 + 1)))
8	6, 7	oveq12d 7386	. . . . . . . . 9 ⊢ (𝑎 = 1 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((1 + 1) / (1 + (𝑀 + 1))))
9	8	oveq2d 7384	. . . . . . . 8 ⊢ (𝑎 = 1 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
10	5, 9	eqeq12d 2753	. . . . . . 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 340	. . . . . 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 6842	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘))
13		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (𝑎 + 1) = (𝑘 + 1))
14		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (𝑎 + (𝑀 + 1)) = (𝑘 + (𝑀 + 1)))
15	13, 14	oveq12d 7386	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))
16	15	oveq2d 7384	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))))
17	12, 16	eqeq12d 2753	. . . . . . 7 ⊢ (𝑎 = 𝑘 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))))
18	17	imbi2d 340	. . . . . 6 ⊢ (𝑎 = 𝑘 → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))))))
19		fveq2 6842	. . . . . . . 8 ⊢ (𝑎 = (𝑘 + 1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)))
20		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 + 1) → (𝑎 + 1) = ((𝑘 + 1) + 1))
21		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 + 1) → (𝑎 + (𝑀 + 1)) = ((𝑘 + 1) + (𝑀 + 1)))
22	20, 21	oveq12d 7386	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 + 1) → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
23	22	oveq2d 7384	. . . . . . . 8 ⊢ (𝑎 = (𝑘 + 1) → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
24	19, 23	eqeq12d 2753	. . . . . . 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 340	. . . . . 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 6842	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏))
27		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝑎 + 1) = (𝑏 + 1))
28		oveq1 7375	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝑎 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1)))
29	27, 28	oveq12d 7386	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))
30	29	oveq2d 7384	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
31	26, 30	eqeq12d 2753	. . . . . . 7 ⊢ (𝑎 = 𝑏 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))))
32	31	imbi2d 340	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))))
33		1nn 12168	. . . . . . . 8 ⊢ 1 ∈ ℕ
34		oveq2 7376	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝑀 / 𝑛) = (𝑀 / 1))
35	34	oveq2d 7384	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / 1)))
36		oveq2 7376	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1))
37	36	oveq2d 7384	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → (1 + (1 / 𝑛)) = (1 + (1 / 1)))
38	35, 37	oveq12d 7386	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / 1)) · (1 + (1 / 1))))
39		oveq2 7376	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / 1))
40	39	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / 1)))
41	38, 40	oveq12d 7386	. . . . . . . . 9 ⊢ (𝑛 = 1 → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))))
42		eqid 2737	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))
43		ovex 7401	. . . . . . . . 9 ⊢ (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) ∈ V
44	41, 42, 43	fvmpt 6949	. . . . . . . 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 12423	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ)
47	46	div1d 11921	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → (𝑀 / 1) = 𝑀)
48	47	oveq2d 7384	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 / 1)) = (1 + 𝑀))
49		1div1e1 11844	. . . . . . . . . . . 12 ⊢ (1 / 1) = 1
50	49	oveq2i 7379	. . . . . . . . . . 11 ⊢ (1 + (1 / 1)) = (1 + 1)
51	50	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (1 / 1)) = (1 + 1))
52	48, 51	oveq12d 7386	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → ((1 + (𝑀 / 1)) · (1 + (1 / 1))) = ((1 + 𝑀) · (1 + 1)))
53		nn0p1nn 12452	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
54	53	nncnd 12173	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℂ)
55	54	div1d 11921	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → ((𝑀 + 1) / 1) = (𝑀 + 1))
56	55	oveq2d 7384	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + ((𝑀 + 1) / 1)) = (1 + (𝑀 + 1)))
57	52, 56	oveq12d 7386	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = (((1 + 𝑀) · (1 + 1)) / (1 + (𝑀 + 1))))
58		1cnd 11139	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → 1 ∈ ℂ)
59	58, 46	addcomd 11347	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + 𝑀) = (𝑀 + 1))
60	59	oveq1d 7383	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → ((1 + 𝑀) · (1 + 1)) = ((𝑀 + 1) · (1 + 1)))
61	60	oveq1d 7383	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((1 + 𝑀) · (1 + 1)) / (1 + (𝑀 + 1))) = (((𝑀 + 1) · (1 + 1)) / (1 + (𝑀 + 1))))
62		ax-1cn 11096	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
63	62, 62	addcli 11150	. . . . . . . . . 10 ⊢ (1 + 1) ∈ ℂ
64	63	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + 1) ∈ ℂ)
65	33	a1i 11	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → 1 ∈ ℕ)
66	65, 53	nnaddcld 12209	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ∈ ℕ)
67	66	nncnd 12173	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ∈ ℂ)
68	66	nnne0d 12207	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ≠ 0)
69	54, 64, 67, 68	divassd 11964	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((𝑀 + 1) · (1 + 1)) / (1 + (𝑀 + 1))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
70	57, 61, 69	3eqtrd 2776	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
71	45, 70	eqtrid 2784	. . . . . 6 ⊢ (𝑀 ∈ ℕ0 → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
72		seqp1 13951	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
73		nnuz 12802	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
74	72, 73	eleq2s 2855	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
75	74	adantr 480	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
76	75	adantr 480	. . . . . . . . 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 7375	. . . . . . . . . 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 481	. . . . . . . . 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 12169	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
80		oveq2 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑘 + 1) → (𝑀 / 𝑛) = (𝑀 / (𝑘 + 1)))
81	80	oveq2d 7384	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / (𝑘 + 1))))
82		oveq2 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1)))
83	82	oveq2d 7384	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → (1 + (1 / 𝑛)) = (1 + (1 / (𝑘 + 1))))
84	81, 83	oveq12d 7386	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 + 1) → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))
85		oveq2 7376	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / (𝑘 + 1)))
86	85	oveq2d 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 + 1) → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / (𝑘 + 1))))
87	84, 86	oveq12d 7386	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑘 + 1) → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
88		ovex 7401	. . . . . . . . . . . . . . 15 ⊢ (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ V
89	87, 42, 88	fvmpt 6949	. . . . . . . . . . . . . 14 ⊢ ((𝑘 + 1) ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
90	79, 89	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1)) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
91	90	oveq2d 7384	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))))
92	91	adantr 480	. . . . . . . . . . 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 481	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ)
94	93	nncnd 12173	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℂ)
95	79	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ)
96	95	nnrpd 12959	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ+)
97		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℕ)
98	97	nnrpd 12959	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℝ+)
99	93	nnrpd 12959	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℝ+)
100	98, 99	rpaddcld 12976	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ∈ ℝ+)
101	96, 100	rpdivcld 12978	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ ℝ+)
102	101	rpcnd 12963	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ ℂ)
103		1cnd 11139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℂ)
104		nn0re 12422	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
105	104	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℝ)
106	105, 95	nndivred 12211	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 / (𝑘 + 1)) ∈ ℝ)
107	106	recnd 11172	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 / (𝑘 + 1)) ∈ ℂ)
108	103, 107	addcomd 11347	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) = ((𝑀 / (𝑘 + 1)) + 1))
109		nn0ge0 12438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
110	109	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 0 ≤ 𝑀)
111	105, 96, 110	divge0d 13001	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑀 / (𝑘 + 1)))
112	106, 111	ge0p1rpd 12991	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 / (𝑘 + 1)) + 1) ∈ ℝ+)
113	108, 112	eqeltrd 2837	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) ∈ ℝ+)
114		1rp 12921	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ+
115	114	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℝ+)
116	96	rpreccld 12971	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 / (𝑘 + 1)) ∈ ℝ+)
117	115, 116	rpaddcld 12976	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (1 / (𝑘 + 1))) ∈ ℝ+)
118	113, 117	rpmulcld 12977	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) ∈ ℝ+)
119	99, 96	rpdivcld 12978	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) / (𝑘 + 1)) ∈ ℝ+)
120	115, 119	rpaddcld 12976	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ∈ ℝ+)
121	118, 120	rpdivcld 12978	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ ℝ+)
122	121	rpcnd 12963	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ ℂ)
123	94, 102, 122	mulassd 11167	. . . . . . . . . . 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 12977	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈ ℝ+)
125	124	rpcnd 12963	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈ ℂ)
126	120	rpcnd 12963	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ∈ ℂ)
127	95	nncnd 12173	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℂ)
128	120	rpne0d 12966	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ≠ 0)
129	95	nnne0d 12207	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ≠ 0)
130	125, 126, 127, 128, 129	divcan5d 11955	. . . . . . . . . . . . 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 12963	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) ∈ ℂ)
132	127, 102, 131	mul12d 11354	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))))
133	113	rpcnd 12963	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) ∈ ℂ)
134	117	rpcnd 12963	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (1 / (𝑘 + 1))) ∈ ℂ)
135	127, 133, 134	mulassd 11167	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))))
136	127, 103, 107	adddid 11168	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · (𝑀 / (𝑘 + 1)))))
137	127	mulridd 11161	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · 1) = (𝑘 + 1))
138		simpr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
139	138	nn0cnd 12476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℂ)
140	139, 127, 129	divcan2d 11931	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (𝑀 / (𝑘 + 1))) = 𝑀)
141	137, 140	oveq12d 7386	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · (𝑀 / (𝑘 + 1)))) = ((𝑘 + 1) + 𝑀))
142	97	nncnd 12173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℂ)
143	142, 103, 139	addassd 11166	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) + 𝑀) = (𝑘 + (1 + 𝑀)))
144	103, 139	addcomd 11347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + 𝑀) = (𝑀 + 1))
145	144	oveq2d 7384	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (1 + 𝑀)) = (𝑘 + (𝑀 + 1)))
146	143, 145	eqtrd 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) + 𝑀) = (𝑘 + (𝑀 + 1)))
147	136, 141, 146	3eqtrd 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) = (𝑘 + (𝑀 + 1)))
148	147	oveq1d 7383	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))
149	135, 148	eqtr3d 2774	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))
150	149	oveq2d 7384	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))))
151	100	rpcnd 12963	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ∈ ℂ)
152	102, 151, 134	mulassd 11167	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))))
153	100	rpne0d 12966	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ≠ 0)
154	127, 151, 153	divcan1d 11930	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) = (𝑘 + 1))
155	154	oveq1d 7383	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) · (1 + (1 / (𝑘 + 1)))))
156	116	rpcnd 12963	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 / (𝑘 + 1)) ∈ ℂ)
157	127, 103, 156	adddid 11168	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (1 / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · (1 / (𝑘 + 1)))))
158	103, 127, 129	divcan2d 11931	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 / (𝑘 + 1))) = 1)
159	137, 158	oveq12d 7386	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · (1 / (𝑘 + 1)))) = ((𝑘 + 1) + 1))
160	155, 157, 159	3eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) + 1))
161	152, 160	eqtr3d 2774	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))) = ((𝑘 + 1) + 1))
162	132, 150, 161	3eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = ((𝑘 + 1) + 1))
163	119	rpcnd 12963	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) / (𝑘 + 1)) ∈ ℂ)
164	127, 103, 163	adddid 11168	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1)))))
165	94, 127, 129	divcan2d 11931	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1))) = (𝑀 + 1))
166	137, 165	oveq12d 7386	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1)))
167	164, 166	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1)))
168	162, 167	oveq12d 7386	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) / ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
169	102, 131, 126, 128	divassd 11964	. . . . . . . . . . . . 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 2781	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
171	170	oveq2d 7384	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
172	92, 123, 171	3eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
173	172	adantr 480	. . . . . . . . 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 2776	. . . . . . . 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 419	. . . . . . 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 29	. . . . . 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 12175	. . . . 5 ⊢ (𝑏 ∈ ℕ → (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))))
178	177	impcom 407	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
179		oveq1 7375	. . . . . . . 8 ⊢ (𝑥 = 𝑏 → (𝑥 + 1) = (𝑏 + 1))
180		oveq1 7375	. . . . . . . 8 ⊢ (𝑥 = 𝑏 → (𝑥 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1)))
181	179, 180	oveq12d 7386	. . . . . . 7 ⊢ (𝑥 = 𝑏 → ((𝑥 + 1) / (𝑥 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))
182	181	oveq2d 7384	. . . . . 6 ⊢ (𝑥 = 𝑏 → ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
183		eqid 2737	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))
184		ovex 7401	. . . . . 6 ⊢ ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))) ∈ V
185	182, 183, 184	fvmpt 6949	. . . . 5 ⊢ (𝑏 ∈ ℕ → ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
186	185	adantl 481	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
187	178, 186	eqtr4d 2775	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
188	187	ralrimiva 3130	. 2 ⊢ (𝑀 ∈ ℕ0 → ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
189		seqfn 13948	. . . . 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 6598	. . . 4 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ ↔ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn (ℤ≥‘1))
192	190, 191	mpbir 231	. . 3 ⊢ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ
193		ovex 7401	. . . 4 ⊢ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) ∈ V
194	193, 183	fnmpti 6643	. . 3 ⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) Fn ℕ
195		eqfnfv 6985	. . 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 693	. 2 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) ↔ ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
197	188, 196	sylibr 234	1 ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052   class class class wbr 5100   ↦ cmpt 5181   Fn wfn 6495  ‘cfv 6500  (class class class)co 7368  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043   ≤ cle 11179   / cdiv 11806  ℕcn 12157  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763  ℝ⁺crp 12917  seqcseq 13936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-n0 12414  df-z 12501  df-uz 12764  df-rp 12918  df-seq 13937

This theorem is referenced by:  faclimlem2  35960