wallispi2lem2

Description: Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017)

		Ref	Expression
	Assertion	wallispi2lem2	$⊢ N \in ℕ \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (N) = \frac{2^{4 \cdot N} {N!}^{4}}{{2 \cdot N!}^{2}}$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = 1 \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (1)$
2		oveq2	$⊢ x = 1 \to 4 x = 4 \cdot 1$
3	2	oveq2d	$⊢ x = 1 \to 2^{4 x} = 2^{4 \cdot 1}$
4		fveq2	$⊢ x = 1 \to x! = 1!$
5	4	oveq1d	$⊢ x = 1 \to {x!}^{4} = {1!}^{4}$
6	3 5	oveq12d	$⊢ x = 1 \to 2^{4 x} {x!}^{4} = 2^{4 \cdot 1} {1!}^{4}$
7		oveq2	$⊢ x = 1 \to 2 x = 2 \cdot 1$
8	7	fveq2d	$⊢ x = 1 \to 2 x! = 2 \cdot 1!$
9	8	oveq1d	$⊢ x = 1 \to {2 x!}^{2} = {2 \cdot 1!}^{2}$
10	6 9	oveq12d	$⊢ x = 1 \to \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} = \frac{2^{4 \cdot 1} {1!}^{4}}{{2 \cdot 1!}^{2}}$
11	1 10	eqeq12d	$⊢ x = 1 \to (seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} \leftrightarrow seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (1) = \frac{2^{4 \cdot 1} {1!}^{4}}{{2 \cdot 1!}^{2}})$
12		fveq2	$⊢ x = y \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y)$
13		oveq2	$⊢ x = y \to 4 x = 4 y$
14	13	oveq2d	$⊢ x = y \to 2^{4 x} = 2^{4 y}$
15		fveq2	$⊢ x = y \to x! = y!$
16	15	oveq1d	$⊢ x = y \to {x!}^{4} = {y!}^{4}$
17	14 16	oveq12d	$⊢ x = y \to 2^{4 x} {x!}^{4} = 2^{4 y} {y!}^{4}$
18		oveq2	$⊢ x = y \to 2 x = 2 y$
19	18	fveq2d	$⊢ x = y \to 2 x! = 2 y!$
20	19	oveq1d	$⊢ x = y \to {2 x!}^{2} = {2 y!}^{2}$
21	17 20	oveq12d	$⊢ x = y \to \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}$
22	12 21	eqeq12d	$⊢ x = y \to (seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} \leftrightarrow seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}})$
23		fveq2	$⊢ x = y + 1 \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y + 1)$
24		oveq2	$⊢ x = y + 1 \to 4 x = 4 (y + 1)$
25	24	oveq2d	$⊢ x = y + 1 \to 2^{4 x} = 2^{4 (y + 1)}$
26		fveq2	$⊢ x = y + 1 \to x! = (y + 1)!$
27	26	oveq1d	$⊢ x = y + 1 \to {x!}^{4} = {(y + 1)!}^{4}$
28	25 27	oveq12d	$⊢ x = y + 1 \to 2^{4 x} {x!}^{4} = 2^{4 (y + 1)} {(y + 1)!}^{4}$
29		oveq2	$⊢ x = y + 1 \to 2 x = 2 (y + 1)$
30	29	fveq2d	$⊢ x = y + 1 \to 2 x! = 2 (y + 1)!$
31	30	oveq1d	$⊢ x = y + 1 \to {2 x!}^{2} = {2 (y + 1)!}^{2}$
32	28 31	oveq12d	$⊢ x = y + 1 \to \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} = \frac{2^{4 (y + 1)} {(y + 1)!}^{4}}{{2 (y + 1)!}^{2}}$
33	23 32	eqeq12d	$⊢ x = y + 1 \to (seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} \leftrightarrow seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y + 1) = \frac{2^{4 (y + 1)} {(y + 1)!}^{4}}{{2 (y + 1)!}^{2}})$
34		fveq2	$⊢ x = N \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (N)$
35		oveq2	$⊢ x = N \to 4 x = 4 \cdot N$
36	35	oveq2d	$⊢ x = N \to 2^{4 x} = 2^{4 \cdot N}$
37		fveq2	$⊢ x = N \to x! = N!$
38	37	oveq1d	$⊢ x = N \to {x!}^{4} = {N!}^{4}$
39	36 38	oveq12d	$⊢ x = N \to 2^{4 x} {x!}^{4} = 2^{4 \cdot N} {N!}^{4}$
40		oveq2	$⊢ x = N \to 2 x = 2 \cdot N$
41	40	fveq2d	$⊢ x = N \to 2 x! = 2 \cdot N!$
42	41	oveq1d	$⊢ x = N \to {2 x!}^{2} = {2 \cdot N!}^{2}$
43	39 42	oveq12d	$⊢ x = N \to \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} = \frac{2^{4 \cdot N} {N!}^{4}}{{2 \cdot N!}^{2}}$
44	34 43	eqeq12d	$⊢ x = N \to (seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (x) = \frac{2^{4 x} {x!}^{4}}{{2 x!}^{2}} \leftrightarrow seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (N) = \frac{2^{4 \cdot N} {N!}^{4}}{{2 \cdot N!}^{2}})$
45		1z	$⊢ 1 \in ℤ$
46		seq1	$⊢ 1 \in ℤ \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (1) = (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (1)$
47	45 46	ax-mp	$⊢ seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (1) = (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (1)$
48		1nn	$⊢ 1 \in ℕ$
49		oveq2	$⊢ k = 1 \to 2 k = 2 \cdot 1$
50	49	oveq1d	$⊢ k = 1 \to {2 k}^{4} = {2 \cdot 1}^{4}$
51	49	oveq1d	$⊢ k = 1 \to 2 k - 1 = 2 \cdot 1 - 1$
52	49 51	oveq12d	$⊢ k = 1 \to 2 k (2 k - 1) = 2 \cdot 1 (2 \cdot 1 - 1)$
53	52	oveq1d	$⊢ k = 1 \to {2 k (2 k - 1)}^{2} = {2 \cdot 1 (2 \cdot 1 - 1)}^{2}$
54	50 53	oveq12d	$⊢ k = 1 \to \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}} = \frac{{2 \cdot 1}^{4}}{{2 \cdot 1 (2 \cdot 1 - 1)}^{2}}$
55		eqid	$⊢ (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) = (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})$
56		ovex	$⊢ \frac{{2 \cdot 1}^{4}}{{2 \cdot 1 (2 \cdot 1 - 1)}^{2}} \in V$
57	54 55 56	fvmpt	$⊢ 1 \in ℕ \to (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (1) = \frac{{2 \cdot 1}^{4}}{{2 \cdot 1 (2 \cdot 1 - 1)}^{2}}$
58	48 57	ax-mp	$⊢ (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (1) = \frac{{2 \cdot 1}^{4}}{{2 \cdot 1 (2 \cdot 1 - 1)}^{2}}$
59		2t1e2	$⊢ 2 \cdot 1 = 2$
60	59	oveq1i	$⊢ {2 \cdot 1}^{4} = 2^{4}$
61		2exp4	$⊢ 2^{4} = 16$
62		1nn0	$⊢ 1 \in ℕ_{0}$
63		6nn0	$⊢ 6 \in ℕ_{0}$
64		0nn0	$⊢ 0 \in ℕ_{0}$
65		1t1e1	$⊢ 1 \cdot 1 = 1$
66	65	oveq1i	$⊢ 1 \cdot 1 + 0 = 1 + 0$
67		1p0e1	$⊢ 1 + 0 = 1$
68	66 67	eqtri	$⊢ 1 \cdot 1 + 0 = 1$
69		6cn	$⊢ 6 \in ℂ$
70	69	mulridi	$⊢ 6 \cdot 1 = 6$
71	63	dec0h	$⊢ 6 = 06$
72	70 71	eqtri	$⊢ 6 \cdot 1 = 06$
73	62 62 63 61 63 64 68 72	decmul1c	$⊢ 2^{4} \cdot 1 = 16$
74	61 73	eqtr4i	$⊢ 2^{4} = 2^{4} \cdot 1$
75		2nn0	$⊢ 2 \in ℕ_{0}$
76		2t2e4	$⊢ 2 \cdot 2 = 4$
77		sq1	$⊢ 1^{2} = 1$
78	62 75 76 77 65	numexp2x	$⊢ 1^{4} = 1$
79	78	eqcomi	$⊢ 1 = 1^{4}$
80	79	oveq2i	$⊢ 2^{4} \cdot 1 = 2^{4} 1^{4}$
81		4cn	$⊢ 4 \in ℂ$
82	81	mulridi	$⊢ 4 \cdot 1 = 4$
83	82	eqcomi	$⊢ 4 = 4 \cdot 1$
84	83	oveq2i	$⊢ 2^{4} = 2^{4 \cdot 1}$
85		fac1	$⊢ 1! = 1$
86	85	eqcomi	$⊢ 1 = 1!$
87	86	oveq1i	$⊢ 1^{4} = {1!}^{4}$
88	84 87	oveq12i	$⊢ 2^{4} 1^{4} = 2^{4 \cdot 1} {1!}^{4}$
89	74 80 88	3eqtri	$⊢ 2^{4} = 2^{4 \cdot 1} {1!}^{4}$
90	60 89	eqtri	$⊢ {2 \cdot 1}^{4} = 2^{4 \cdot 1} {1!}^{4}$
91	59	oveq1i	$⊢ 2 \cdot 1 - 1 = 2 - 1$
92		2m1e1	$⊢ 2 - 1 = 1$
93	91 92	eqtri	$⊢ 2 \cdot 1 - 1 = 1$
94	93	oveq2i	$⊢ 2 \cdot 1 (2 \cdot 1 - 1) = 2 \cdot 1 \cdot 1$
95	59	oveq1i	$⊢ 2 \cdot 1 \cdot 1 = 2 \cdot 1$
96	95 59	eqtri	$⊢ 2 \cdot 1 \cdot 1 = 2$
97	59	fveq2i	$⊢ 2 \cdot 1! = 2!$
98		fac2	$⊢ 2! = 2$
99	97 98	eqtri	$⊢ 2 \cdot 1! = 2$
100	99	eqcomi	$⊢ 2 = 2 \cdot 1!$
101	94 96 100	3eqtri	$⊢ 2 \cdot 1 (2 \cdot 1 - 1) = 2 \cdot 1!$
102	101	oveq1i	$⊢ {2 \cdot 1 (2 \cdot 1 - 1)}^{2} = {2 \cdot 1!}^{2}$
103	90 102	oveq12i	$⊢ \frac{{2 \cdot 1}^{4}}{{2 \cdot 1 (2 \cdot 1 - 1)}^{2}} = \frac{2^{4 \cdot 1} {1!}^{4}}{{2 \cdot 1!}^{2}}$
104	47 58 103	3eqtri	$⊢ seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (1) = \frac{2^{4 \cdot 1} {1!}^{4}}{{2 \cdot 1!}^{2}}$
105		elnnuz	$⊢ y \in ℕ \leftrightarrow y \in ℤ_{\geq 1}$
106	105	birani	$⊢ (y \in ℕ \land seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) \to y \in ℤ_{\geq 1}$
107		seqp1	$⊢ y \in ℤ_{\geq 1} \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y + 1) = seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1)$
108	106 107	syl	$⊢ (y \in ℕ \land seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y + 1) = seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1)$
109		simpr	$⊢ (y \in ℕ \land seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}$
110	109	oveq1d	$⊢ (y \in ℕ \land seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1) = (\frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1)$
111		eqidd	$⊢ y \in ℕ \to (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) = (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})$
112		oveq2	$⊢ k = y + 1 \to 2 k = 2 (y + 1)$
113	112	oveq1d	$⊢ k = y + 1 \to {2 k}^{4} = {2 (y + 1)}^{4}$
114	112	oveq1d	$⊢ k = y + 1 \to 2 k - 1 = 2 (y + 1) - 1$
115	112 114	oveq12d	$⊢ k = y + 1 \to 2 k (2 k - 1) = 2 (y + 1) (2 (y + 1) - 1)$
116	115	oveq1d	$⊢ k = y + 1 \to {2 k (2 k - 1)}^{2} = {2 (y + 1) (2 (y + 1) - 1)}^{2}$
117	113 116	oveq12d	$⊢ k = y + 1 \to \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}} = \frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}}$
118	117	adantl	$⊢ (y \in ℕ \land k = y + 1) \to \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}} = \frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}}$
119		peano2nn	$⊢ y \in ℕ \to y + 1 \in ℕ$
120		2cnd	$⊢ y \in ℕ \to 2 \in ℂ$
121		nncn	$⊢ y \in ℕ \to y \in ℂ$
122		1cnd	$⊢ y \in ℕ \to 1 \in ℂ$
123	121 122	addcld	$⊢ y \in ℕ \to y + 1 \in ℂ$
124	120 123	mulcld	$⊢ y \in ℕ \to 2 (y + 1) \in ℂ$
125		4nn0	$⊢ 4 \in ℕ_{0}$
126	125	a1i	$⊢ y \in ℕ \to 4 \in ℕ_{0}$
127	124 126	expcld	$⊢ y \in ℕ \to {2 (y + 1)}^{4} \in ℂ$
128	124 122	subcld	$⊢ y \in ℕ \to 2 (y + 1) - 1 \in ℂ$
129	124 128	mulcld	$⊢ y \in ℕ \to 2 (y + 1) (2 (y + 1) - 1) \in ℂ$
130	129	sqcld	$⊢ y \in ℕ \to {2 (y + 1) (2 (y + 1) - 1)}^{2} \in ℂ$
131		2pos	$⊢ 0 < 2$
132	131	a1i	$⊢ y \in ℕ \to 0 < 2$
133	132	gt0ne0d	$⊢ y \in ℕ \to 2 \neq 0$
134	119	nnne0d	$⊢ y \in ℕ \to y + 1 \neq 0$
135	120 123 133 134	mulne0d	$⊢ y \in ℕ \to 2 (y + 1) \neq 0$
136		1red	$⊢ y \in ℕ \to 1 \in ℝ$
137		2re	$⊢ 2 \in ℝ$
138	137	a1i	$⊢ y \in ℕ \to 2 \in ℝ$
139		nnre	$⊢ y \in ℕ \to y \in ℝ$
140	139 136	readdcld	$⊢ y \in ℕ \to y + 1 \in ℝ$
141		1lt2	$⊢ 1 < 2$
142	141	a1i	$⊢ y \in ℕ \to 1 < 2$
143		nnrp	$⊢ y \in ℕ \to y \in ℝ^{+}$
144	136 143	ltaddrp2d	$⊢ y \in ℕ \to 1 < y + 1$
145	138 140 142 144	mulgt1d	$⊢ y \in ℕ \to 1 < 2 (y + 1)$
146	136 145	gtned	$⊢ y \in ℕ \to 2 (y + 1) \neq 1$
147	124 122 146	subne0d	$⊢ y \in ℕ \to 2 (y + 1) - 1 \neq 0$
148	124 128 135 147	mulne0d	$⊢ y \in ℕ \to 2 (y + 1) (2 (y + 1) - 1) \neq 0$
149		2z	$⊢ 2 \in ℤ$
150	149	a1i	$⊢ y \in ℕ \to 2 \in ℤ$
151	129 148 150	expne0d	$⊢ y \in ℕ \to {2 (y + 1) (2 (y + 1) - 1)}^{2} \neq 0$
152	127 130 151	divcld	$⊢ y \in ℕ \to \frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}} \in ℂ$
153	111 118 119 152	fvmptd	$⊢ y \in ℕ \to (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1) = \frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}}$
154	153	oveq2d	$⊢ y \in ℕ \to (\frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1) = (\frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) (\frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}})$
155		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
156	126 155	nn0mulcld	$⊢ y \in ℕ \to 4 y \in ℕ_{0}$
157	120 156	expcld	$⊢ y \in ℕ \to 2^{4 y} \in ℂ$
158		faccl	$⊢ y \in ℕ_{0} \to y! \in ℕ$
159		nncn	$⊢ y! \in ℕ \to y! \in ℂ$
160	155 158 159	3syl	$⊢ y \in ℕ \to y! \in ℂ$
161	160 126	expcld	$⊢ y \in ℕ \to {y!}^{4} \in ℂ$
162	157 161	mulcld	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} \in ℂ$
163	75	a1i	$⊢ y \in ℕ \to 2 \in ℕ_{0}$
164	163 155	nn0mulcld	$⊢ y \in ℕ \to 2 y \in ℕ_{0}$
165		faccl	$⊢ 2 y \in ℕ_{0} \to 2 y! \in ℕ$
166		nncn	$⊢ 2 y! \in ℕ \to 2 y! \in ℂ$
167	164 165 166	3syl	$⊢ y \in ℕ \to 2 y! \in ℂ$
168	167	sqcld	$⊢ y \in ℕ \to {2 y!}^{2} \in ℂ$
169	164 165	syl	$⊢ y \in ℕ \to 2 y! \in ℕ$
170	169	nnne0d	$⊢ y \in ℕ \to 2 y! \neq 0$
171	167 170 150	expne0d	$⊢ y \in ℕ \to {2 y!}^{2} \neq 0$
172	162 168 127 130 171 151	divmuldivd	$⊢ y \in ℕ \to (\frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) (\frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}}) = \frac{2^{4 y} {y!}^{4} {2 (y + 1)}^{4}}{{2 y!}^{2} {2 (y + 1) (2 (y + 1) - 1)}^{2}}$
173	120 123 126	mulexpd	$⊢ y \in ℕ \to {2 (y + 1)}^{4} = 2^{4} {(y + 1)}^{4}$
174	173	oveq2d	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} {2 (y + 1)}^{4} = 2^{4 y} {y!}^{4} 2^{4} {(y + 1)}^{4}$
175	120 126	expcld	$⊢ y \in ℕ \to 2^{4} \in ℂ$
176	123 126	expcld	$⊢ y \in ℕ \to {(y + 1)}^{4} \in ℂ$
177	157 161 175 176	mul4d	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} 2^{4} {(y + 1)}^{4} = 2^{4 y} 2^{4} {y!}^{4} {(y + 1)}^{4}$
178	160 123 126	mulexpd	$⊢ y \in ℕ \to {y! (y + 1)}^{4} = {y!}^{4} {(y + 1)}^{4}$
179	178	eqcomd	$⊢ y \in ℕ \to {y!}^{4} {(y + 1)}^{4} = {y! (y + 1)}^{4}$
180	179	oveq2d	$⊢ y \in ℕ \to 2^{4 y} 2^{4} {y!}^{4} {(y + 1)}^{4} = 2^{4 y} 2^{4} {y! (y + 1)}^{4}$
181	174 177 180	3eqtrd	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} {2 (y + 1)}^{4} = 2^{4 y} 2^{4} {y! (y + 1)}^{4}$
182	120 121	mulcld	$⊢ y \in ℕ \to 2 y \in ℂ$
183	182 122	addcld	$⊢ y \in ℕ \to 2 y + 1 \in ℂ$
184	124 183	mulcomd	$⊢ y \in ℕ \to 2 (y + 1) (2 y + 1) = (2 y + 1) 2 (y + 1)$
185	184	oveq2d	$⊢ y \in ℕ \to 2 y! 2 (y + 1) (2 y + 1) = 2 y! (2 y + 1) 2 (y + 1)$
186	120 121 122	adddid	$⊢ y \in ℕ \to 2 (y + 1) = 2 y + 2 \cdot 1$
187	186	oveq1d	$⊢ y \in ℕ \to 2 (y + 1) - 1 = 2 y + 2 \cdot 1 - 1$
188	59 120	eqeltrid	$⊢ y \in ℕ \to 2 \cdot 1 \in ℂ$
189	182 188 122	addsubassd	$⊢ y \in ℕ \to 2 y + 2 \cdot 1 - 1 = 2 y + 2 \cdot 1 - 1$
190	59	a1i	$⊢ y \in ℕ \to 2 \cdot 1 = 2$
191	190	oveq1d	$⊢ y \in ℕ \to 2 \cdot 1 - 1 = 2 - 1$
192	191 92	eqtrdi	$⊢ y \in ℕ \to 2 \cdot 1 - 1 = 1$
193	192	oveq2d	$⊢ y \in ℕ \to 2 y + 2 \cdot 1 - 1 = 2 y + 1$
194	187 189 193	3eqtrd	$⊢ y \in ℕ \to 2 (y + 1) - 1 = 2 y + 1$
195	194	oveq2d	$⊢ y \in ℕ \to 2 (y + 1) (2 (y + 1) - 1) = 2 (y + 1) (2 y + 1)$
196	195	oveq2d	$⊢ y \in ℕ \to 2 y! 2 (y + 1) (2 (y + 1) - 1) = 2 y! 2 (y + 1) (2 y + 1)$
197	167 183 124	mulassd	$⊢ y \in ℕ \to 2 y! (2 y + 1) 2 (y + 1) = 2 y! (2 y + 1) 2 (y + 1)$
198	185 196 197	3eqtr4d	$⊢ y \in ℕ \to 2 y! 2 (y + 1) (2 (y + 1) - 1) = 2 y! (2 y + 1) 2 (y + 1)$
199	198	oveq1d	$⊢ y \in ℕ \to {2 y! 2 (y + 1) (2 (y + 1) - 1)}^{2} = {2 y! (2 y + 1) 2 (y + 1)}^{2}$
200	167 129 163	mulexpd	$⊢ y \in ℕ \to {2 y! 2 (y + 1) (2 (y + 1) - 1)}^{2} = {2 y!}^{2} {2 (y + 1) (2 (y + 1) - 1)}^{2}$
201		df-2	$⊢ 2 = 1 + 1$
202	201	a1i	$⊢ y \in ℕ \to 2 = 1 + 1$
203	202	oveq2d	$⊢ y \in ℕ \to 2 y + 2 = 2 y + 1 + 1$
204	182 122 122	addassd	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 y + 1 + 1$
205	203 204	eqtr4d	$⊢ y \in ℕ \to 2 y + 2 = 2 y + 1 + 1$
206	205	fveq2d	$⊢ y \in ℕ \to (2 y + 2)! = (2 y + 1 + 1)!$
207	62	a1i	$⊢ y \in ℕ \to 1 \in ℕ_{0}$
208	164 207	nn0addcld	$⊢ y \in ℕ \to 2 y + 1 \in ℕ_{0}$
209		facp1	$⊢ 2 y + 1 \in ℕ_{0} \to (2 y + 1 + 1)! = (2 y + 1)! (2 y + 1 + 1)$
210	208 209	syl	$⊢ y \in ℕ \to (2 y + 1 + 1)! = (2 y + 1)! (2 y + 1 + 1)$
211		facp1	$⊢ 2 y \in ℕ_{0} \to (2 y + 1)! = 2 y! (2 y + 1)$
212	164 211	syl	$⊢ y \in ℕ \to (2 y + 1)! = 2 y! (2 y + 1)$
213	202	eqcomd	$⊢ y \in ℕ \to 1 + 1 = 2$
214	213	oveq2d	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 y + 2$
215	213 201 59	3eqtr4g	$⊢ y \in ℕ \to 2 = 2 \cdot 1$
216	215	oveq2d	$⊢ y \in ℕ \to 2 y + 2 = 2 y + 2 \cdot 1$
217	216 186	eqtr4d	$⊢ y \in ℕ \to 2 y + 2 = 2 (y + 1)$
218	204 214 217	3eqtrd	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 (y + 1)$
219	212 218	oveq12d	$⊢ y \in ℕ \to (2 y + 1)! (2 y + 1 + 1) = 2 y! (2 y + 1) 2 (y + 1)$
220	206 210 219	3eqtrrd	$⊢ y \in ℕ \to 2 y! (2 y + 1) 2 (y + 1) = (2 y + 2)!$
221	220	oveq1d	$⊢ y \in ℕ \to {2 y! (2 y + 1) 2 (y + 1)}^{2} = {(2 y + 2)!}^{2}$
222	199 200 221	3eqtr3d	$⊢ y \in ℕ \to {2 y!}^{2} {2 (y + 1) (2 (y + 1) - 1)}^{2} = {(2 y + 2)!}^{2}$
223	181 222	oveq12d	$⊢ y \in ℕ \to \frac{2^{4 y} {y!}^{4} {2 (y + 1)}^{4}}{{2 y!}^{2} {2 (y + 1) (2 (y + 1) - 1)}^{2}} = \frac{2^{4 y} 2^{4} {y! (y + 1)}^{4}}{{(2 y + 2)!}^{2}}$
224	172 223	eqtrd	$⊢ y \in ℕ \to (\frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) (\frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}}) = \frac{2^{4 y} 2^{4} {y! (y + 1)}^{4}}{{(2 y + 2)!}^{2}}$
225	83	a1i	$⊢ y \in ℕ \to 4 = 4 \cdot 1$
226	225	oveq2d	$⊢ y \in ℕ \to 4 y + 4 = 4 y + 4 \cdot 1$
227	226	oveq2d	$⊢ y \in ℕ \to 2^{4 y + 4} = 2^{4 y + 4 \cdot 1}$
228	120 126 156	expaddd	$⊢ y \in ℕ \to 2^{4 y + 4} = 2^{4 y} 2^{4}$
229	81	a1i	$⊢ y \in ℕ \to 4 \in ℂ$
230	229 121 122	adddid	$⊢ y \in ℕ \to 4 (y + 1) = 4 y + 4 \cdot 1$
231	230	eqcomd	$⊢ y \in ℕ \to 4 y + 4 \cdot 1 = 4 (y + 1)$
232	231	oveq2d	$⊢ y \in ℕ \to 2^{4 y + 4 \cdot 1} = 2^{4 (y + 1)}$
233	227 228 232	3eqtr3d	$⊢ y \in ℕ \to 2^{4 y} 2^{4} = 2^{4 (y + 1)}$
234		facp1	$⊢ y \in ℕ_{0} \to (y + 1)! = y! (y + 1)$
235	155 234	syl	$⊢ y \in ℕ \to (y + 1)! = y! (y + 1)$
236	235	eqcomd	$⊢ y \in ℕ \to y! (y + 1) = (y + 1)!$
237	236	oveq1d	$⊢ y \in ℕ \to {y! (y + 1)}^{4} = {(y + 1)!}^{4}$
238	233 237	oveq12d	$⊢ y \in ℕ \to 2^{4 y} 2^{4} {y! (y + 1)}^{4} = 2^{4 (y + 1)} {(y + 1)!}^{4}$
239	217	fveq2d	$⊢ y \in ℕ \to (2 y + 2)! = 2 (y + 1)!$
240	239	oveq1d	$⊢ y \in ℕ \to {(2 y + 2)!}^{2} = {2 (y + 1)!}^{2}$
241	238 240	oveq12d	$⊢ y \in ℕ \to \frac{2^{4 y} 2^{4} {y! (y + 1)}^{4}}{{(2 y + 2)!}^{2}} = \frac{2^{4 (y + 1)} {(y + 1)!}^{4}}{{2 (y + 1)!}^{2}}$
242	154 224 241	3eqtrd	$⊢ y \in ℕ \to (\frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1) = \frac{2^{4 (y + 1)} {(y + 1)!}^{4}}{{2 (y + 1)!}^{2}}$
243	242	adantr	$⊢ (y \in ℕ \land seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) \to (\frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}}) (y + 1) = \frac{2^{4 (y + 1)} {(y + 1)!}^{4}}{{2 (y + 1)!}^{2}}$
244	108 110 243	3eqtrd	$⊢ (y \in ℕ \land seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}}) \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y + 1) = \frac{2^{4 (y + 1)} {(y + 1)!}^{4}}{{2 (y + 1)!}^{2}}$
245	244	ex	$⊢ y \in ℕ \to (seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y) = \frac{2^{4 y} {y!}^{4}}{{2 y!}^{2}} \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (y + 1) = \frac{2^{4 (y + 1)} {(y + 1)!}^{4}}{{2 (y + 1)!}^{2}})$
246	11 22 33 44 104 245	nnind	$⊢ N \in ℕ \to seq 1 (\times (k \in ℕ ⟼ \frac{{2 k}^{4}}{{2 k (2 k - 1)}^{2}})) (N) = \frac{2^{4 \cdot N} {N!}^{4}}{{2 \cdot N!}^{2}}$

Metamath Proof Explorer

Theorem wallispi2lem2

Proof