Theorem faclimlem1 35971

Description: Lemma for faclim 35974. 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 6827	. . . . . . . . 9 ⊢ (𝑎 = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘1))
2		1z 12548	. . . . . . . . . 10 ⊢ 1 ∈ ℤ
3		seq1 13967	. . . . . . . . . 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 2790	. . . . . . . 8 ⊢ (𝑎 = 1 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1))
6		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = 1 → (𝑎 + 1) = (1 + 1))
7		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = 1 → (𝑎 + (𝑀 + 1)) = (1 + (𝑀 + 1)))
8	6, 7	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑎 = 1 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((1 + 1) / (1 + (𝑀 + 1))))
9	8	oveq2d 7372	. . . . . . . 8 ⊢ (𝑎 = 1 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
10	5, 9	eqeq12d 2755	. . . . . . 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 341	. . . . . 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 6827	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘))
13		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (𝑎 + 1) = (𝑘 + 1))
14		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = 𝑘 → (𝑎 + (𝑀 + 1)) = (𝑘 + (𝑀 + 1)))
15	13, 14	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑎 = 𝑘 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))
16	15	oveq2d 7372	. . . . . . . 8 ⊢ (𝑎 = 𝑘 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))))
17	12, 16	eqeq12d 2755	. . . . . . 7 ⊢ (𝑎 = 𝑘 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1))))))
18	17	imbi2d 341	. . . . . 6 ⊢ (𝑎 = 𝑘 → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) = ((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))))))
19		fveq2 6827	. . . . . . . 8 ⊢ (𝑎 = (𝑘 + 1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)))
20		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 + 1) → (𝑎 + 1) = ((𝑘 + 1) + 1))
21		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = (𝑘 + 1) → (𝑎 + (𝑀 + 1)) = ((𝑘 + 1) + (𝑀 + 1)))
22	20, 21	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑎 = (𝑘 + 1) → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
23	22	oveq2d 7372	. . . . . . . 8 ⊢ (𝑎 = (𝑘 + 1) → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
24	19, 23	eqeq12d 2755	. . . . . . 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 341	. . . . . 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 6827	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏))
27		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝑎 + 1) = (𝑏 + 1))
28		oveq1 7363	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝑎 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1)))
29	27, 28	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝑎 + 1) / (𝑎 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))
30	29	oveq2d 7372	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
31	26, 30	eqeq12d 2755	. . . . . . 7 ⊢ (𝑎 = 𝑏 → ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1)))) ↔ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))))
32	31	imbi2d 341	. . . . . 6 ⊢ (𝑎 = 𝑏 → ((𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑎) = ((𝑀 + 1) · ((𝑎 + 1) / (𝑎 + (𝑀 + 1))))) ↔ (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))))
33		1nn 12176	. . . . . . . 8 ⊢ 1 ∈ ℕ
34		oveq2 7364	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (𝑀 / 𝑛) = (𝑀 / 1))
35	34	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / 1)))
36		oveq2 7364	. . . . . . . . . . . 12 ⊢ (𝑛 = 1 → (1 / 𝑛) = (1 / 1))
37	36	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → (1 + (1 / 𝑛)) = (1 + (1 / 1)))
38	35, 37	oveq12d 7374	. . . . . . . . . 10 ⊢ (𝑛 = 1 → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / 1)) · (1 + (1 / 1))))
39		oveq2 7364	. . . . . . . . . . 11 ⊢ (𝑛 = 1 → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / 1))
40	39	oveq2d 7372	. . . . . . . . . 10 ⊢ (𝑛 = 1 → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / 1)))
41	38, 40	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑛 = 1 → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))))
42		eqid 2739	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))) = (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))
43		ovex 7389	. . . . . . . . 9 ⊢ (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) ∈ V
44	41, 42, 43	fvmpt 6935	. . . . . . . 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 12438	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ)
47	46	div1d 11914	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → (𝑀 / 1) = 𝑀)
48	47	oveq2d 7372	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 / 1)) = (1 + 𝑀))
49		1div1e1 11836	. . . . . . . . . . . 12 ⊢ (1 / 1) = 1
50	49	oveq2i 7367	. . . . . . . . . . 11 ⊢ (1 + (1 / 1)) = (1 + 1)
51	50	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (1 / 1)) = (1 + 1))
52	48, 51	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → ((1 + (𝑀 / 1)) · (1 + (1 / 1))) = ((1 + 𝑀) · (1 + 1)))
53		nn0p1nn 12467	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
54	53	nncnd 12181	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℂ)
55	54	div1d 11914	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → ((𝑀 + 1) / 1) = (𝑀 + 1))
56	55	oveq2d 7372	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + ((𝑀 + 1) / 1)) = (1 + (𝑀 + 1)))
57	52, 56	oveq12d 7374	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = (((1 + 𝑀) · (1 + 1)) / (1 + (𝑀 + 1))))
58		1cnd 11130	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → 1 ∈ ℂ)
59	58, 46	addcomd 11339	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + 𝑀) = (𝑀 + 1))
60	59	oveq1d 7371	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → ((1 + 𝑀) · (1 + 1)) = ((𝑀 + 1) · (1 + 1)))
61	60	oveq1d 7371	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((1 + 𝑀) · (1 + 1)) / (1 + (𝑀 + 1))) = (((𝑀 + 1) · (1 + 1)) / (1 + (𝑀 + 1))))
62		ax-1cn 11087	. . . . . . . . . . 11 ⊢ 1 ∈ ℂ
63	62, 62	addcli 11142	. . . . . . . . . 10 ⊢ (1 + 1) ∈ ℂ
64	63	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + 1) ∈ ℂ)
65	33	a1i 11	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → 1 ∈ ℕ)
66	65, 53	nnaddcld 12220	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ∈ ℕ)
67	66	nncnd 12181	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ∈ ℂ)
68	66	nnne0d 12218	. . . . . . . . 9 ⊢ (𝑀 ∈ ℕ0 → (1 + (𝑀 + 1)) ≠ 0)
69	54, 64, 67, 68	divassd 11957	. . . . . . . 8 ⊢ (𝑀 ∈ ℕ0 → (((𝑀 + 1) · (1 + 1)) / (1 + (𝑀 + 1))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
70	57, 61, 69	3eqtrd 2778	. . . . . . 7 ⊢ (𝑀 ∈ ℕ0 → (((1 + (𝑀 / 1)) · (1 + (1 / 1))) / (1 + ((𝑀 + 1) / 1))) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
71	45, 70	eqtrid 2786	. . . . . 6 ⊢ (𝑀 ∈ ℕ0 → ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘1) = ((𝑀 + 1) · ((1 + 1) / (1 + (𝑀 + 1)))))
72		seqp1 13969	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (ℤ≥‘1) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
73		nnuz 12818	. . . . . . . . . . . 12 ⊢ ℕ = (ℤ≥‘1)
74	72, 73	eleq2s 2857	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
75	74	adantr 481	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘(𝑘 + 1)) = ((seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑘) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))))
76	75	adantr 481	. . . . . . . . 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 7363	. . . . . . . . . 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 482	. . . . . . . . 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 12177	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
80		oveq2 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑘 + 1) → (𝑀 / 𝑛) = (𝑀 / (𝑘 + 1)))
81	80	oveq2d 7372	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → (1 + (𝑀 / 𝑛)) = (1 + (𝑀 / (𝑘 + 1))))
82		oveq2 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = (𝑘 + 1) → (1 / 𝑛) = (1 / (𝑘 + 1)))
83	82	oveq2d 7372	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → (1 + (1 / 𝑛)) = (1 + (1 / (𝑘 + 1))))
84	81, 83	oveq12d 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 + 1) → ((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) = ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))
85		oveq2 7364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = (𝑘 + 1) → ((𝑀 + 1) / 𝑛) = ((𝑀 + 1) / (𝑘 + 1)))
86	85	oveq2d 7372	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = (𝑘 + 1) → (1 + ((𝑀 + 1) / 𝑛)) = (1 + ((𝑀 + 1) / (𝑘 + 1))))
87	84, 86	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = (𝑘 + 1) → (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))) = (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))
88		ovex 7389	. . . . . . . . . . . . . . 15 ⊢ (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ V
89	87, 42, 88	fvmpt 6935	. . . . . . . . . . . . . 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 7372	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))))
92	91	adantr 481	. . . . . . . . . . 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 482	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℕ)
94	93	nncnd 12181	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℂ)
95	79	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℕ)
96	95	nnrpd 12975	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℝ+)
97		simpl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℕ)
98	97	nnrpd 12975	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℝ+)
99	93	nnrpd 12975	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 + 1) ∈ ℝ+)
100	98, 99	rpaddcld 12992	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ∈ ℝ+)
101	96, 100	rpdivcld 12994	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ ℝ+)
102	101	rpcnd 12979	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) / (𝑘 + (𝑀 + 1))) ∈ ℂ)
103		1cnd 11130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℂ)
104		nn0re 12437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ)
105	104	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℝ)
106	105, 95	nndivred 12222	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 / (𝑘 + 1)) ∈ ℝ)
107	106	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑀 / (𝑘 + 1)) ∈ ℂ)
108	103, 107	addcomd 11339	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) = ((𝑀 / (𝑘 + 1)) + 1))
109		nn0ge0 12453	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℕ0 → 0 ≤ 𝑀)
110	109	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 0 ≤ 𝑀)
111	105, 96, 110	divge0d 13017	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 0 ≤ (𝑀 / (𝑘 + 1)))
112	106, 111	ge0p1rpd 13007	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 / (𝑘 + 1)) + 1) ∈ ℝ+)
113	108, 112	eqeltrd 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) ∈ ℝ+)
114		1rp 12937	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℝ+
115	114	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 1 ∈ ℝ+)
116	96	rpreccld 12987	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 / (𝑘 + 1)) ∈ ℝ+)
117	115, 116	rpaddcld 12992	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (1 / (𝑘 + 1))) ∈ ℝ+)
118	113, 117	rpmulcld 12993	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) ∈ ℝ+)
119	99, 96	rpdivcld 12994	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) / (𝑘 + 1)) ∈ ℝ+)
120	115, 119	rpaddcld 12992	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ∈ ℝ+)
121	118, 120	rpdivcld 12994	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ ℝ+)
122	121	rpcnd 12979	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))) ∈ ℂ)
123	94, 102, 122	mulassd 11159	. . . . . . . . . . 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 12993	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈ ℝ+)
125	124	rpcnd 12979	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) ∈ ℂ)
126	120	rpcnd 12979	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ∈ ℂ)
127	95	nncnd 12181	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ∈ ℂ)
128	120	rpne0d 12982	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + ((𝑀 + 1) / (𝑘 + 1))) ≠ 0)
129	95	nnne0d 12218	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + 1) ≠ 0)
130	125, 126, 127, 128, 129	divcan5d 11948	. . . . . . . . . . . . 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 12979	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) ∈ ℂ)
132	127, 102, 131	mul12d 11346	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))))
133	113	rpcnd 12979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (𝑀 / (𝑘 + 1))) ∈ ℂ)
134	117	rpcnd 12979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + (1 / (𝑘 + 1))) ∈ ℂ)
135	127, 133, 134	mulassd 11159	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))))
136	127, 103, 107	adddid 11160	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · (𝑀 / (𝑘 + 1)))))
137	127	mulridd 11153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · 1) = (𝑘 + 1))
138		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℕ0)
139	138	nn0cnd 12491	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑀 ∈ ℂ)
140	139, 127, 129	divcan2d 11924	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (𝑀 / (𝑘 + 1))) = 𝑀)
141	137, 140	oveq12d 7374	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · (𝑀 / (𝑘 + 1)))) = ((𝑘 + 1) + 𝑀))
142	97	nncnd 12181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → 𝑘 ∈ ℂ)
143	142, 103, 139	addassd 11158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) + 𝑀) = (𝑘 + (1 + 𝑀)))
144	103, 139	addcomd 11339	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 + 𝑀) = (𝑀 + 1))
145	144	oveq2d 7372	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (1 + 𝑀)) = (𝑘 + (𝑀 + 1)))
146	143, 145	eqtrd 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) + 𝑀) = (𝑘 + (𝑀 + 1)))
147	136, 141, 146	3eqtrd 2778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) = (𝑘 + (𝑀 + 1)))
148	147	oveq1d 7371	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (1 + (𝑀 / (𝑘 + 1)))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))
149	135, 148	eqtr3d 2776	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1))))) = ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1)))))
150	149	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + 1) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))))
151	100	rpcnd 12979	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ∈ ℂ)
152	102, 151, 134	mulassd 11159	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))))
153	100	rpne0d 12982	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (𝑘 + (𝑀 + 1)) ≠ 0)
154	127, 151, 153	divcan1d 11923	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) = (𝑘 + 1))
155	154	oveq1d 7371	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) · (1 + (1 / (𝑘 + 1)))))
156	116	rpcnd 12979	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (1 / (𝑘 + 1)) ∈ ℂ)
157	127, 103, 156	adddid 11160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + (1 / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · (1 / (𝑘 + 1)))))
158	103, 127, 129	divcan2d 11924	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 / (𝑘 + 1))) = 1)
159	137, 158	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · (1 / (𝑘 + 1)))) = ((𝑘 + 1) + 1))
160	155, 157, 159	3eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (𝑘 + (𝑀 + 1))) · (1 + (1 / (𝑘 + 1)))) = ((𝑘 + 1) + 1))
161	152, 160	eqtr3d 2776	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((𝑘 + (𝑀 + 1)) · (1 + (1 / (𝑘 + 1))))) = ((𝑘 + 1) + 1))
162	132, 150, 161	3eqtrd 2778	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) = ((𝑘 + 1) + 1))
163	119	rpcnd 12979	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) / (𝑘 + 1)) ∈ ℂ)
164	127, 103, 163	adddid 11160	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1)))) = (((𝑘 + 1) · 1) + ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1)))))
165	94, 127, 129	divcan2d 11924	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1))) = (𝑀 + 1))
166	137, 165	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · 1) + ((𝑘 + 1) · ((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1)))
167	164, 166	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1)))) = ((𝑘 + 1) + (𝑀 + 1)))
168	162, 167	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · ((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))))) / ((𝑘 + 1) · (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
169	102, 131, 126, 128	divassd 11957	. . . . . . . . . . . . 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 2783	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1))))) = (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1))))
171	170	oveq2d 7372	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 1) · (((𝑘 + 1) / (𝑘 + (𝑀 + 1))) · (((1 + (𝑀 / (𝑘 + 1))) · (1 + (1 / (𝑘 + 1)))) / (1 + ((𝑀 + 1) / (𝑘 + 1)))))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
172	92, 123, 171	3eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (((𝑀 + 1) · ((𝑘 + 1) / (𝑘 + (𝑀 + 1)))) · ((𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))‘(𝑘 + 1))) = ((𝑀 + 1) · (((𝑘 + 1) + 1) / ((𝑘 + 1) + (𝑀 + 1)))))
173	172	adantr 481	. . . . . . . . 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 2778	. . . . . . . 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 420	. . . . . . 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 12183	. . . . 5 ⊢ (𝑏 ∈ ℕ → (𝑀 ∈ ℕ0 → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))))
178	177	impcom 408	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
179		oveq1 7363	. . . . . . . 8 ⊢ (𝑥 = 𝑏 → (𝑥 + 1) = (𝑏 + 1))
180		oveq1 7363	. . . . . . . 8 ⊢ (𝑥 = 𝑏 → (𝑥 + (𝑀 + 1)) = (𝑏 + (𝑀 + 1)))
181	179, 180	oveq12d 7374	. . . . . . 7 ⊢ (𝑥 = 𝑏 → ((𝑥 + 1) / (𝑥 + (𝑀 + 1))) = ((𝑏 + 1) / (𝑏 + (𝑀 + 1))))
182	181	oveq2d 7372	. . . . . 6 ⊢ (𝑥 = 𝑏 → ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
183		eqid 2739	. . . . . 6 ⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))
184		ovex 7389	. . . . . 6 ⊢ ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))) ∈ V
185	182, 183, 184	fvmpt 6935	. . . . 5 ⊢ (𝑏 ∈ ℕ → ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
186	185	adantl 482	. . . 4 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏) = ((𝑀 + 1) · ((𝑏 + 1) / (𝑏 + (𝑀 + 1)))))
187	178, 186	eqtr4d 2777	. . 3 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑏 ∈ ℕ) → (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
188	187	ralrimiva 3131	. 2 ⊢ (𝑀 ∈ ℕ0 → ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
189		seqfn 13966	. . . . 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 6583	. . . 4 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ ↔ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn (ℤ≥‘1))
192	190, 191	mpbir 232	. . 3 ⊢ seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) Fn ℕ
193		ovex 7389	. . . 4 ⊢ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))) ∈ V
194	193, 183	fnmpti 6628	. . 3 ⊢ (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) Fn ℕ
195		eqfnfv 6971	. . 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 698	. 2 ⊢ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))) ↔ ∀𝑏 ∈ ℕ (seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛)))))‘𝑏) = ((𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1)))))‘𝑏))
197	188, 196	sylibr 235	1 ⊢ (𝑀 ∈ ℕ0 → seq1( · , (𝑛 ∈ ℕ ↦ (((1 + (𝑀 / 𝑛)) · (1 + (1 / 𝑛))) / (1 + ((𝑀 + 1) / 𝑛))))) = (𝑥 ∈ ℕ ↦ ((𝑀 + 1) · ((𝑥 + 1) / (𝑥 + (𝑀 + 1))))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053   class class class wbr 5072   ↦ cmpt 5153   Fn wfn 6480  ‘cfv 6485  (class class class)co 7356  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030   + caddc 11032   · cmul 11034   ≤ cle 11171   / cdiv 11798  ℕcn 12165  ℕ₀cn0 12428  ℤcz 12515  ℤ_≥cuz 12779  ℝ⁺crp 12933  seqcseq 13954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-n0 12429  df-z 12516  df-uz 12780  df-rp 12934  df-seq 13955

This theorem is referenced by:  faclimlem2  35972