Theorem leibpilem2

Description: The Leibniz formula for _pi . (Contributed by Mario Carneiro, 7-Apr-2015)

	Ref	Expression
Hypotheses	leibpi.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) )
	leibpilem2.2	⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ if ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) )
	leibpilem2.3	⊢ 𝐴 ∈ V
Assertion	leibpilem2	⊢ ( seq 0 ( + , 𝐹 ) ⇝ 𝐴 ↔ seq 0 ( + , 𝐺 ) ⇝ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		leibpi.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) )
2		leibpilem2.2	⊢ 𝐺 = ( 𝑘 ∈ ℕ0 ↦ if ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) )
3		leibpilem2.3	⊢ 𝐴 ∈ V
4		2cn	⊢ 2 ∈ ℂ
5		nn0cn	⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℂ )
6		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 2 · 𝑛 ) ∈ ℂ )
7	4 5 6	sylancr	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℂ )
8		ax-1cn	⊢ 1 ∈ ℂ
9		pncan	⊢ ( ( ( 2 · 𝑛 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
10	7 8 9	sylancl	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) = ( 2 · 𝑛 ) )
11	10	oveq1d	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) = ( ( 2 · 𝑛 ) / 2 ) )
12		2ne0	⊢ 2 ≠ 0
13		divcan3	⊢ ( ( 𝑛 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
14	4 12 13	mp3an23	⊢ ( 𝑛 ∈ ℂ → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
15	5 14	syl	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑛 ) / 2 ) = 𝑛 )
16	11 15	eqtrd	⊢ ( 𝑛 ∈ ℕ0 → ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) = 𝑛 )
17	16	oveq2d	⊢ ( 𝑛 ∈ ℕ0 → ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) = ( - 1 ↑ 𝑛 ) )
18	17	oveq1d	⊢ ( 𝑛 ∈ ℕ0 → ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) = ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) )
19	18	mpteq2ia	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) )
20	1 19	eqtr4i	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
21		seqeq3	⊢ ( 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) → seq 0 ( + , 𝐹 ) = seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) )
22	20 21	ax-mp	⊢ seq 0 ( + , 𝐹 ) = seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) )
23	22	breq1i	⊢ ( seq 0 ( + , 𝐹 ) ⇝ 𝐴 ↔ seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ⇝ 𝐴 )
24		neg1rr	⊢ - 1 ∈ ℝ
25		reexpcl	⊢ ( ( - 1 ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) → ( - 1 ↑ 𝑛 ) ∈ ℝ )
26	24 25	mpan	⊢ ( 𝑛 ∈ ℕ0 → ( - 1 ↑ 𝑛 ) ∈ ℝ )
27		2nn0	⊢ 2 ∈ ℕ0
28		nn0mulcl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
29	27 28	mpan	⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℕ0 )
30		nn0p1nn	⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
31	29 30	syl	⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
32	26 31	nndivred	⊢ ( 𝑛 ∈ ℕ0 → ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℝ )
33	32	recnd	⊢ ( 𝑛 ∈ ℕ0 → ( ( - 1 ↑ 𝑛 ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
34	18 33	eqeltrd	⊢ ( 𝑛 ∈ ℕ0 → ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
35	34	adantl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ0 ) → ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℂ )
36		oveq1	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( 𝑘 − 1 ) = ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) )
37	36	oveq1d	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( ( 𝑘 − 1 ) / 2 ) = ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) )
38	37	oveq2d	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) = ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) )
39		id	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → 𝑘 = ( ( 2 · 𝑛 ) + 1 ) )
40	38 39	oveq12d	⊢ ( 𝑘 = ( ( 2 · 𝑛 ) + 1 ) → ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) = ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) )
41	35 40	iserodd	⊢ ( ⊤ → ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ⇝ 𝐴 ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ) ⇝ 𝐴 ) )
42	41	mptru	⊢ ( seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( - 1 ↑ ( ( ( ( 2 · 𝑛 ) + 1 ) − 1 ) / 2 ) ) / ( ( 2 · 𝑛 ) + 1 ) ) ) ) ⇝ 𝐴 ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ) ⇝ 𝐴 )
43		addlid	⊢ ( 𝑛 ∈ ℂ → ( 0 + 𝑛 ) = 𝑛 )
44	43	adantl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ℂ ) → ( 0 + 𝑛 ) = 𝑛 )
45		0cnd	⊢ ( ⊤ → 0 ∈ ℂ )
46		1eluzge0	⊢ 1 ∈ ( ℤ≥ ‘ 0 )
47	46	a1i	⊢ ( ⊤ → 1 ∈ ( ℤ≥ ‘ 0 ) )
48		1nn0	⊢ 1 ∈ ℕ0
49		0cnd	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) ) → 0 ∈ ℂ )
50		ioran	⊢ ( ¬ ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) ↔ ( ¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘 ) )
51		leibpilem1	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘 ) ) → ( 𝑘 ∈ ℕ ∧ ( ( 𝑘 − 1 ) / 2 ) ∈ ℕ0 ) )
52	51	simprd	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘 ) ) → ( ( 𝑘 − 1 ) / 2 ) ∈ ℕ0 )
53		reexpcl	⊢ ( ( - 1 ∈ ℝ ∧ ( ( 𝑘 − 1 ) / 2 ) ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) ∈ ℝ )
54	24 52 53	sylancr	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘 ) ) → ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) ∈ ℝ )
55	51	simpld	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘 ) ) → 𝑘 ∈ ℕ )
56	54 55	nndivred	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘 ) ) → ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ∈ ℝ )
57	56	recnd	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ¬ 𝑘 = 0 ∧ ¬ 2 ∥ 𝑘 ) ) → ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ∈ ℂ )
58	50 57	sylan2b	⊢ ( ( 𝑘 ∈ ℕ0 ∧ ¬ ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) ) → ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ∈ ℂ )
59	49 58	ifclda	⊢ ( 𝑘 ∈ ℕ0 → if ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ∈ ℂ )
60	2 59	fmpti	⊢ 𝐺 : ℕ0 ⟶ ℂ
61	60	ffvelcdmi	⊢ ( 1 ∈ ℕ0 → ( 𝐺 ‘ 1 ) ∈ ℂ )
62	48 61	mp1i	⊢ ( ⊤ → ( 𝐺 ‘ 1 ) ∈ ℂ )
63		simpr	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) ) → 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) )
64		1m1e0	⊢ ( 1 − 1 ) = 0
65	64	oveq2i	⊢ ( 0 ... ( 1 − 1 ) ) = ( 0 ... 0 )
66	63 65	eleqtrdi	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) ) → 𝑛 ∈ ( 0 ... 0 ) )
67		elfz1eq	⊢ ( 𝑛 ∈ ( 0 ... 0 ) → 𝑛 = 0 )
68	66 67	syl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) ) → 𝑛 = 0 )
69	68	fveq2d	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 0 ) )
70		0nn0	⊢ 0 ∈ ℕ0
71		iftrue	⊢ ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) → if ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) = 0 )
72	71	orcs	⊢ ( 𝑘 = 0 → if ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) = 0 )
73		c0ex	⊢ 0 ∈ V
74	72 2 73	fvmpt	⊢ ( 0 ∈ ℕ0 → ( 𝐺 ‘ 0 ) = 0 )
75	70 74	ax-mp	⊢ ( 𝐺 ‘ 0 ) = 0
76	69 75	eqtrdi	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... ( 1 − 1 ) ) ) → ( 𝐺 ‘ 𝑛 ) = 0 )
77	44 45 47 62 76	seqid	⊢ ( ⊤ → ( seq 0 ( + , 𝐺 ) ↾ ( ℤ≥ ‘ 1 ) ) = seq 1 ( + , 𝐺 ) )
78		1zzd	⊢ ( ⊤ → 1 ∈ ℤ )
79		simpr	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
80		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
81	79 80	eleqtrrdi	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑛 ∈ ℕ )
82		nnne0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
83	82	neneqd	⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 )
84		biorf	⊢ ( ¬ 𝑛 = 0 → ( 2 ∥ 𝑛 ↔ ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) ) )
85	83 84	syl	⊢ ( 𝑛 ∈ ℕ → ( 2 ∥ 𝑛 ↔ ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) ) )
86	85	ifbid	⊢ ( 𝑛 ∈ ℕ → if ( 2 ∥ 𝑛 , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) = if ( ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) )
87		breq2	⊢ ( 𝑘 = 𝑛 → ( 2 ∥ 𝑘 ↔ 2 ∥ 𝑛 ) )
88		oveq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 − 1 ) = ( 𝑛 − 1 ) )
89	88	oveq1d	⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 − 1 ) / 2 ) = ( ( 𝑛 − 1 ) / 2 ) )
90	89	oveq2d	⊢ ( 𝑘 = 𝑛 → ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) = ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) )
91		id	⊢ ( 𝑘 = 𝑛 → 𝑘 = 𝑛 )
92	90 91	oveq12d	⊢ ( 𝑘 = 𝑛 → ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) = ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) )
93	87 92	ifbieq2d	⊢ ( 𝑘 = 𝑛 → if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) = if ( 2 ∥ 𝑛 , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) )
94		eqid	⊢ ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) = ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) )
95		ovex	⊢ ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ∈ V
96	73 95	ifex	⊢ if ( 2 ∥ 𝑛 , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) ∈ V
97	93 94 96	fvmpt	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ‘ 𝑛 ) = if ( 2 ∥ 𝑛 , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) )
98		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
99		eqeq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 = 0 ↔ 𝑛 = 0 ) )
100	99 87	orbi12d	⊢ ( 𝑘 = 𝑛 → ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) ↔ ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) ) )
101	100 92	ifbieq2d	⊢ ( 𝑘 = 𝑛 → if ( ( 𝑘 = 0 ∨ 2 ∥ 𝑘 ) , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) = if ( ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) )
102	73 95	ifex	⊢ if ( ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) ∈ V
103	101 2 102	fvmpt	⊢ ( 𝑛 ∈ ℕ0 → ( 𝐺 ‘ 𝑛 ) = if ( ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) )
104	98 103	syl	⊢ ( 𝑛 ∈ ℕ → ( 𝐺 ‘ 𝑛 ) = if ( ( 𝑛 = 0 ∨ 2 ∥ 𝑛 ) , 0 , ( ( - 1 ↑ ( ( 𝑛 − 1 ) / 2 ) ) / 𝑛 ) ) )
105	86 97 104	3eqtr4d	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
106	81 105	syl	⊢ ( ( ⊤ ∧ 𝑛 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝐺 ‘ 𝑛 ) )
107	78 106	seqfeq	⊢ ( ⊤ → seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ) = seq 1 ( + , 𝐺 ) )
108	77 107	eqtr4d	⊢ ( ⊤ → ( seq 0 ( + , 𝐺 ) ↾ ( ℤ≥ ‘ 1 ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ) )
109	108	mptru	⊢ ( seq 0 ( + , 𝐺 ) ↾ ( ℤ≥ ‘ 1 ) ) = seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) )
110	109	breq1i	⊢ ( ( seq 0 ( + , 𝐺 ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 𝐴 ↔ seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ) ⇝ 𝐴 )
111		1z	⊢ 1 ∈ ℤ
112		seqex	⊢ seq 0 ( + , 𝐺 ) ∈ V
113		climres	⊢ ( ( 1 ∈ ℤ ∧ seq 0 ( + , 𝐺 ) ∈ V ) → ( ( seq 0 ( + , 𝐺 ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 𝐴 ↔ seq 0 ( + , 𝐺 ) ⇝ 𝐴 ) )
114	111 112 113	mp2an	⊢ ( ( seq 0 ( + , 𝐺 ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 𝐴 ↔ seq 0 ( + , 𝐺 ) ⇝ 𝐴 )
115	110 114	bitr3i	⊢ ( seq 1 ( + , ( 𝑘 ∈ ℕ ↦ if ( 2 ∥ 𝑘 , 0 , ( ( - 1 ↑ ( ( 𝑘 − 1 ) / 2 ) ) / 𝑘 ) ) ) ) ⇝ 𝐴 ↔ seq 0 ( + , 𝐺 ) ⇝ 𝐴 )
116	23 42 115	3bitri	⊢ ( seq 0 ( + , 𝐹 ) ⇝ 𝐴 ↔ seq 0 ( + , 𝐺 ) ⇝ 𝐴 )