Metamath Proof Explorer

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 ( + , 𝐺 ) ⇝ 𝐴 )