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	biimpi	$⊢ y \in ℕ \to y \in ℤ_{\geq 1}$
107	106	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 y \in ℤ_{\geq 1}$
108		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)$
109	107 108	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)$
110		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}}$
111	110	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)$
112		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}})$
113		oveq2	$⊢ k = y + 1 \to 2 k = 2 (y + 1)$
114	113	oveq1d	$⊢ k = y + 1 \to {2 k}^{4} = {2 (y + 1)}^{4}$
115	113	oveq1d	$⊢ k = y + 1 \to 2 k - 1 = 2 (y + 1) - 1$
116	113 115	oveq12d	$⊢ k = y + 1 \to 2 k (2 k - 1) = 2 (y + 1) (2 (y + 1) - 1)$
117	116	oveq1d	$⊢ k = y + 1 \to {2 k (2 k - 1)}^{2} = {2 (y + 1) (2 (y + 1) - 1)}^{2}$
118	114 117	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}}$
119	118	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}}$
120		peano2nn	$⊢ y \in ℕ \to y + 1 \in ℕ$
121		2cnd	$⊢ y \in ℕ \to 2 \in ℂ$
122		nncn	$⊢ y \in ℕ \to y \in ℂ$
123		1cnd	$⊢ y \in ℕ \to 1 \in ℂ$
124	122 123	addcld	$⊢ y \in ℕ \to y + 1 \in ℂ$
125	121 124	mulcld	$⊢ y \in ℕ \to 2 (y + 1) \in ℂ$
126		4nn0	$⊢ 4 \in ℕ_{0}$
127	126	a1i	$⊢ y \in ℕ \to 4 \in ℕ_{0}$
128	125 127	expcld	$⊢ y \in ℕ \to {2 (y + 1)}^{4} \in ℂ$
129	125 123	subcld	$⊢ y \in ℕ \to 2 (y + 1) - 1 \in ℂ$
130	125 129	mulcld	$⊢ y \in ℕ \to 2 (y + 1) (2 (y + 1) - 1) \in ℂ$
131	130	sqcld	$⊢ y \in ℕ \to {2 (y + 1) (2 (y + 1) - 1)}^{2} \in ℂ$
132		2pos	$⊢ 0 < 2$
133	132	a1i	$⊢ y \in ℕ \to 0 < 2$
134	133	gt0ne0d	$⊢ y \in ℕ \to 2 \neq 0$
135	120	nnne0d	$⊢ y \in ℕ \to y + 1 \neq 0$
136	121 124 134 135	mulne0d	$⊢ y \in ℕ \to 2 (y + 1) \neq 0$
137		1red	$⊢ y \in ℕ \to 1 \in ℝ$
138		2re	$⊢ 2 \in ℝ$
139	138	a1i	$⊢ y \in ℕ \to 2 \in ℝ$
140		nnre	$⊢ y \in ℕ \to y \in ℝ$
141	140 137	readdcld	$⊢ y \in ℕ \to y + 1 \in ℝ$
142		1lt2	$⊢ 1 < 2$
143	142	a1i	$⊢ y \in ℕ \to 1 < 2$
144		nnrp	$⊢ y \in ℕ \to y \in ℝ^{+}$
145	137 144	ltaddrp2d	$⊢ y \in ℕ \to 1 < y + 1$
146	139 141 143 145	mulgt1d	$⊢ y \in ℕ \to 1 < 2 (y + 1)$
147	137 146	gtned	$⊢ y \in ℕ \to 2 (y + 1) \neq 1$
148	125 123 147	subne0d	$⊢ y \in ℕ \to 2 (y + 1) - 1 \neq 0$
149	125 129 136 148	mulne0d	$⊢ y \in ℕ \to 2 (y + 1) (2 (y + 1) - 1) \neq 0$
150		2z	$⊢ 2 \in ℤ$
151	150	a1i	$⊢ y \in ℕ \to 2 \in ℤ$
152	130 149 151	expne0d	$⊢ y \in ℕ \to {2 (y + 1) (2 (y + 1) - 1)}^{2} \neq 0$
153	128 131 152	divcld	$⊢ y \in ℕ \to \frac{{2 (y + 1)}^{4}}{{2 (y + 1) (2 (y + 1) - 1)}^{2}} \in ℂ$
154	112 119 120 153	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}}$
155	154	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}})$
156		nnnn0	$⊢ y \in ℕ \to y \in ℕ_{0}$
157	127 156	nn0mulcld	$⊢ y \in ℕ \to 4 y \in ℕ_{0}$
158	121 157	expcld	$⊢ y \in ℕ \to 2^{4 y} \in ℂ$
159		faccl	$⊢ y \in ℕ_{0} \to y! \in ℕ$
160		nncn	$⊢ y! \in ℕ \to y! \in ℂ$
161	156 159 160	3syl	$⊢ y \in ℕ \to y! \in ℂ$
162	161 127	expcld	$⊢ y \in ℕ \to {y!}^{4} \in ℂ$
163	158 162	mulcld	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} \in ℂ$
164	75	a1i	$⊢ y \in ℕ \to 2 \in ℕ_{0}$
165	164 156	nn0mulcld	$⊢ y \in ℕ \to 2 y \in ℕ_{0}$
166		faccl	$⊢ 2 y \in ℕ_{0} \to 2 y! \in ℕ$
167		nncn	$⊢ 2 y! \in ℕ \to 2 y! \in ℂ$
168	165 166 167	3syl	$⊢ y \in ℕ \to 2 y! \in ℂ$
169	168	sqcld	$⊢ y \in ℕ \to {2 y!}^{2} \in ℂ$
170	165 166	syl	$⊢ y \in ℕ \to 2 y! \in ℕ$
171	170	nnne0d	$⊢ y \in ℕ \to 2 y! \neq 0$
172	168 171 151	expne0d	$⊢ y \in ℕ \to {2 y!}^{2} \neq 0$
173	163 169 128 131 172 152	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}}$
174	121 124 127	mulexpd	$⊢ y \in ℕ \to {2 (y + 1)}^{4} = 2^{4} {(y + 1)}^{4}$
175	174	oveq2d	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} {2 (y + 1)}^{4} = 2^{4 y} {y!}^{4} 2^{4} {(y + 1)}^{4}$
176	121 127	expcld	$⊢ y \in ℕ \to 2^{4} \in ℂ$
177	124 127	expcld	$⊢ y \in ℕ \to {(y + 1)}^{4} \in ℂ$
178	158 162 176 177	mul4d	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} 2^{4} {(y + 1)}^{4} = 2^{4 y} 2^{4} {y!}^{4} {(y + 1)}^{4}$
179	161 124 127	mulexpd	$⊢ y \in ℕ \to {y! (y + 1)}^{4} = {y!}^{4} {(y + 1)}^{4}$
180	179	eqcomd	$⊢ y \in ℕ \to {y!}^{4} {(y + 1)}^{4} = {y! (y + 1)}^{4}$
181	180	oveq2d	$⊢ y \in ℕ \to 2^{4 y} 2^{4} {y!}^{4} {(y + 1)}^{4} = 2^{4 y} 2^{4} {y! (y + 1)}^{4}$
182	175 178 181	3eqtrd	$⊢ y \in ℕ \to 2^{4 y} {y!}^{4} {2 (y + 1)}^{4} = 2^{4 y} 2^{4} {y! (y + 1)}^{4}$
183	121 122	mulcld	$⊢ y \in ℕ \to 2 y \in ℂ$
184	183 123	addcld	$⊢ y \in ℕ \to 2 y + 1 \in ℂ$
185	125 184	mulcomd	$⊢ y \in ℕ \to 2 (y + 1) (2 y + 1) = (2 y + 1) 2 (y + 1)$
186	185	oveq2d	$⊢ y \in ℕ \to 2 y! 2 (y + 1) (2 y + 1) = 2 y! (2 y + 1) 2 (y + 1)$
187	121 122 123	adddid	$⊢ y \in ℕ \to 2 (y + 1) = 2 y + 2 \cdot 1$
188	187	oveq1d	$⊢ y \in ℕ \to 2 (y + 1) - 1 = 2 y + 2 \cdot 1 - 1$
189	59 121	eqeltrid	$⊢ y \in ℕ \to 2 \cdot 1 \in ℂ$
190	183 189 123	addsubassd	$⊢ y \in ℕ \to 2 y + 2 \cdot 1 - 1 = 2 y + 2 \cdot 1 - 1$
191	59	a1i	$⊢ y \in ℕ \to 2 \cdot 1 = 2$
192	191	oveq1d	$⊢ y \in ℕ \to 2 \cdot 1 - 1 = 2 - 1$
193	192 92	eqtrdi	$⊢ y \in ℕ \to 2 \cdot 1 - 1 = 1$
194	193	oveq2d	$⊢ y \in ℕ \to 2 y + 2 \cdot 1 - 1 = 2 y + 1$
195	188 190 194	3eqtrd	$⊢ y \in ℕ \to 2 (y + 1) - 1 = 2 y + 1$
196	195	oveq2d	$⊢ y \in ℕ \to 2 (y + 1) (2 (y + 1) - 1) = 2 (y + 1) (2 y + 1)$
197	196	oveq2d	$⊢ y \in ℕ \to 2 y! 2 (y + 1) (2 (y + 1) - 1) = 2 y! 2 (y + 1) (2 y + 1)$
198	168 184 125	mulassd	$⊢ y \in ℕ \to 2 y! (2 y + 1) 2 (y + 1) = 2 y! (2 y + 1) 2 (y + 1)$
199	186 197 198	3eqtr4d	$⊢ y \in ℕ \to 2 y! 2 (y + 1) (2 (y + 1) - 1) = 2 y! (2 y + 1) 2 (y + 1)$
200	199	oveq1d	$⊢ y \in ℕ \to {2 y! 2 (y + 1) (2 (y + 1) - 1)}^{2} = {2 y! (2 y + 1) 2 (y + 1)}^{2}$
201	168 130 164	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}$
202		df-2	$⊢ 2 = 1 + 1$
203	202	a1i	$⊢ y \in ℕ \to 2 = 1 + 1$
204	203	oveq2d	$⊢ y \in ℕ \to 2 y + 2 = 2 y + 1 + 1$
205	183 123 123	addassd	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 y + 1 + 1$
206	204 205	eqtr4d	$⊢ y \in ℕ \to 2 y + 2 = 2 y + 1 + 1$
207	206	fveq2d	$⊢ y \in ℕ \to (2 y + 2)! = (2 y + 1 + 1)!$
208	62	a1i	$⊢ y \in ℕ \to 1 \in ℕ_{0}$
209	165 208	nn0addcld	$⊢ y \in ℕ \to 2 y + 1 \in ℕ_{0}$
210		facp1	$⊢ 2 y + 1 \in ℕ_{0} \to (2 y + 1 + 1)! = (2 y + 1)! (2 y + 1 + 1)$
211	209 210	syl	$⊢ y \in ℕ \to (2 y + 1 + 1)! = (2 y + 1)! (2 y + 1 + 1)$
212		facp1	$⊢ 2 y \in ℕ_{0} \to (2 y + 1)! = 2 y! (2 y + 1)$
213	165 212	syl	$⊢ y \in ℕ \to (2 y + 1)! = 2 y! (2 y + 1)$
214	203	eqcomd	$⊢ y \in ℕ \to 1 + 1 = 2$
215	214	oveq2d	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 y + 2$
216	214 202 59	3eqtr4g	$⊢ y \in ℕ \to 2 = 2 \cdot 1$
217	216	oveq2d	$⊢ y \in ℕ \to 2 y + 2 = 2 y + 2 \cdot 1$
218	217 187	eqtr4d	$⊢ y \in ℕ \to 2 y + 2 = 2 (y + 1)$
219	205 215 218	3eqtrd	$⊢ y \in ℕ \to 2 y + 1 + 1 = 2 (y + 1)$
220	213 219	oveq12d	$⊢ y \in ℕ \to (2 y + 1)! (2 y + 1 + 1) = 2 y! (2 y + 1) 2 (y + 1)$
221	207 211 220	3eqtrrd	$⊢ y \in ℕ \to 2 y! (2 y + 1) 2 (y + 1) = (2 y + 2)!$
222	221	oveq1d	$⊢ y \in ℕ \to {2 y! (2 y + 1) 2 (y + 1)}^{2} = {(2 y + 2)!}^{2}$
223	200 201 222	3eqtr3d	$⊢ y \in ℕ \to {2 y!}^{2} {2 (y + 1) (2 (y + 1) - 1)}^{2} = {(2 y + 2)!}^{2}$
224	182 223	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}}$
225	173 224	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}}$
226	83	a1i	$⊢ y \in ℕ \to 4 = 4 \cdot 1$
227	226	oveq2d	$⊢ y \in ℕ \to 4 y + 4 = 4 y + 4 \cdot 1$
228	227	oveq2d	$⊢ y \in ℕ \to 2^{4 y + 4} = 2^{4 y + 4 \cdot 1}$
229	121 127 157	expaddd	$⊢ y \in ℕ \to 2^{4 y + 4} = 2^{4 y} 2^{4}$
230	81	a1i	$⊢ y \in ℕ \to 4 \in ℂ$
231	230 122 123	adddid	$⊢ y \in ℕ \to 4 (y + 1) = 4 y + 4 \cdot 1$
232	231	eqcomd	$⊢ y \in ℕ \to 4 y + 4 \cdot 1 = 4 (y + 1)$
233	232	oveq2d	$⊢ y \in ℕ \to 2^{4 y + 4 \cdot 1} = 2^{4 (y + 1)}$
234	228 229 233	3eqtr3d	$⊢ y \in ℕ \to 2^{4 y} 2^{4} = 2^{4 (y + 1)}$
235		facp1	$⊢ y \in ℕ_{0} \to (y + 1)! = y! (y + 1)$
236	156 235	syl	$⊢ y \in ℕ \to (y + 1)! = y! (y + 1)$
237	236	eqcomd	$⊢ y \in ℕ \to y! (y + 1) = (y + 1)!$
238	237	oveq1d	$⊢ y \in ℕ \to {y! (y + 1)}^{4} = {(y + 1)!}^{4}$
239	234 238	oveq12d	$⊢ y \in ℕ \to 2^{4 y} 2^{4} {y! (y + 1)}^{4} = 2^{4 (y + 1)} {(y + 1)!}^{4}$
240	218	fveq2d	$⊢ y \in ℕ \to (2 y + 2)! = 2 (y + 1)!$
241	240	oveq1d	$⊢ y \in ℕ \to {(2 y + 2)!}^{2} = {2 (y + 1)!}^{2}$
242	239 241	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}}$
243	155 225 242	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}}$
244	243	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}}$
245	109 111 244	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}}$
246	245	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}})$
247	11 22 33 44 104 246	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