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 addid2 ( 𝑛 ∈ ℂ → ( 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 ffvelrni ( 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 ( + , 𝐺 ) ⇝ 𝐴 )