Metamath Proof Explorer

Theorem logtayl

Description: The Taylor series for -u log ( 1 - A ) . (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion logtayl ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) ⇝ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 nn0uz ⊒ β„•0 = ( β„€β‰₯ β€˜ 0 )
2 0zd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ 0 ∈ β„€ )
3 eqeq1 ⊒ ( π‘˜ = 𝑛 β†’ ( π‘˜ = 0 ↔ 𝑛 = 0 ) )
4 oveq2 ⊒ ( π‘˜ = 𝑛 β†’ ( 1 / π‘˜ ) = ( 1 / 𝑛 ) )
5 3 4 ifbieq2d ⊒ ( π‘˜ = 𝑛 β†’ if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
6 oveq2 ⊒ ( π‘˜ = 𝑛 β†’ ( 𝐴 ↑ π‘˜ ) = ( 𝐴 ↑ 𝑛 ) )
7 5 6 oveq12d ⊒ ( π‘˜ = 𝑛 β†’ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
8 eqid ⊒ ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) = ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) )
9 ovex ⊒ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) ∈ V
10 7 8 9 fvmpt ⊒ ( 𝑛 ∈ β„•0 β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
11 10 adantl ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
12 0cnd ⊒ ( ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = 0 ) β†’ 0 ∈ β„‚ )
13 simpr ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ 𝑛 ∈ β„•0 )
14 elnn0 ⊒ ( 𝑛 ∈ β„•0 ↔ ( 𝑛 ∈ β„• ∨ 𝑛 = 0 ) )
15 13 14 sylib ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝑛 ∈ β„• ∨ 𝑛 = 0 ) )
16 15 ord ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( Β¬ 𝑛 ∈ β„• β†’ 𝑛 = 0 ) )
17 16 con1d ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( Β¬ 𝑛 = 0 β†’ 𝑛 ∈ β„• ) )
18 17 imp ⊒ ( ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ 𝑛 ∈ β„• )
19 18 nnrecred ⊒ ( ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( 1 / 𝑛 ) ∈ ℝ )
20 19 recnd ⊒ ( ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( 1 / 𝑛 ) ∈ β„‚ )
21 12 20 ifclda ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) ∈ β„‚ )
22 expcl ⊒ ( ( 𝐴 ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝐴 ↑ 𝑛 ) ∈ β„‚ )
23 22 adantlr ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝐴 ↑ 𝑛 ) ∈ β„‚ )
24 21 23 mulcld ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„•0 ) β†’ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) ∈ β„‚ )
25 logtayllem ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) ∈ dom ⇝ )
26 1 2 11 24 25 isumclim2 ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) ⇝ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
27 simpl ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ 𝐴 ∈ β„‚ )
28 0cn ⊒ 0 ∈ β„‚
29 eqid ⊒ ( abs ∘ βˆ’ ) = ( abs ∘ βˆ’ )
30 29 cnmetdval ⊒ ( ( 𝐴 ∈ β„‚ ∧ 0 ∈ β„‚ ) β†’ ( 𝐴 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ ( 𝐴 βˆ’ 0 ) ) )
31 27 28 30 sylancl ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( 𝐴 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ ( 𝐴 βˆ’ 0 ) ) )
32 subid1 ⊒ ( 𝐴 ∈ β„‚ β†’ ( 𝐴 βˆ’ 0 ) = 𝐴 )
33 32 adantr ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( 𝐴 βˆ’ 0 ) = 𝐴 )
34 33 fveq2d ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( abs β€˜ ( 𝐴 βˆ’ 0 ) ) = ( abs β€˜ 𝐴 ) )
35 31 34 eqtrd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( 𝐴 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ 𝐴 ) )
36 simpr ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( abs β€˜ 𝐴 ) < 1 )
37 35 36 eqbrtrd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( 𝐴 ( abs ∘ βˆ’ ) 0 ) < 1 )
38 cnxmet ⊒ ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ )
39 1xr ⊒ 1 ∈ ℝ*
40 elbl3 ⊒ ( ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ) ) β†’ ( 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝐴 ( abs ∘ βˆ’ ) 0 ) < 1 ) )
41 38 39 40 mpanl12 ⊒ ( ( 0 ∈ β„‚ ∧ 𝐴 ∈ β„‚ ) β†’ ( 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝐴 ( abs ∘ βˆ’ ) 0 ) < 1 ) )
42 28 27 41 sylancr ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝐴 ( abs ∘ βˆ’ ) 0 ) < 1 ) )
43 37 42 mpbird ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
44 tru ⊒ ⊀
45 eqid ⊒ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 )
46 0cnd ⊒ ( ⊀ β†’ 0 ∈ β„‚ )
47 39 a1i ⊒ ( ⊀ β†’ 1 ∈ ℝ* )
48 ax-1cn ⊒ 1 ∈ β„‚
49 blssm ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 0 ∈ β„‚ ∧ 1 ∈ ℝ* ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† β„‚ )
50 38 28 39 49 mp3an ⊒ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† β„‚
51 50 sseli ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 𝑦 ∈ β„‚ )
52 subcl ⊒ ( ( 1 ∈ β„‚ ∧ 𝑦 ∈ β„‚ ) β†’ ( 1 βˆ’ 𝑦 ) ∈ β„‚ )
53 48 51 52 sylancr ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 βˆ’ 𝑦 ) ∈ β„‚ )
54 51 abscld ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ 𝑦 ) ∈ ℝ )
55 29 cnmetdval ⊒ ( ( 𝑦 ∈ β„‚ ∧ 0 ∈ β„‚ ) β†’ ( 𝑦 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ ( 𝑦 βˆ’ 0 ) ) )
56 51 28 55 sylancl ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 𝑦 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ ( 𝑦 βˆ’ 0 ) ) )
57 51 subid1d ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 𝑦 βˆ’ 0 ) = 𝑦 )
58 57 fveq2d ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ ( 𝑦 βˆ’ 0 ) ) = ( abs β€˜ 𝑦 ) )
59 56 58 eqtrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 𝑦 ( abs ∘ βˆ’ ) 0 ) = ( abs β€˜ 𝑦 ) )
60 elbl3 ⊒ ( ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ β„‚ ∧ 𝑦 ∈ β„‚ ) ) β†’ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝑦 ( abs ∘ βˆ’ ) 0 ) < 1 ) )
61 38 39 60 mpanl12 ⊒ ( ( 0 ∈ β„‚ ∧ 𝑦 ∈ β„‚ ) β†’ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝑦 ( abs ∘ βˆ’ ) 0 ) < 1 ) )
62 28 51 61 sylancr ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( 𝑦 ( abs ∘ βˆ’ ) 0 ) < 1 ) )
63 62 ibi ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 𝑦 ( abs ∘ βˆ’ ) 0 ) < 1 )
64 59 63 eqbrtrrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ 𝑦 ) < 1 )
65 54 64 gtned ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 1 β‰  ( abs β€˜ 𝑦 ) )
66 abs1 ⊒ ( abs β€˜ 1 ) = 1
67 fveq2 ⊒ ( 1 = 𝑦 β†’ ( abs β€˜ 1 ) = ( abs β€˜ 𝑦 ) )
68 66 67 eqtr3id ⊒ ( 1 = 𝑦 β†’ 1 = ( abs β€˜ 𝑦 ) )
69 68 necon3i ⊒ ( 1 β‰  ( abs β€˜ 𝑦 ) β†’ 1 β‰  𝑦 )
70 65 69 syl ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 1 β‰  𝑦 )
71 subeq0 ⊒ ( ( 1 ∈ β„‚ ∧ 𝑦 ∈ β„‚ ) β†’ ( ( 1 βˆ’ 𝑦 ) = 0 ↔ 1 = 𝑦 ) )
72 71 necon3bid ⊒ ( ( 1 ∈ β„‚ ∧ 𝑦 ∈ β„‚ ) β†’ ( ( 1 βˆ’ 𝑦 ) β‰  0 ↔ 1 β‰  𝑦 ) )
73 48 51 72 sylancr ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 1 βˆ’ 𝑦 ) β‰  0 ↔ 1 β‰  𝑦 ) )
74 70 73 mpbird ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 βˆ’ 𝑦 ) β‰  0 )
75 53 74 logcld ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ∈ β„‚ )
76 75 negcld ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ∈ β„‚ )
77 76 adantl ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ∈ β„‚ )
78 77 fmpttd ⊒ ( ⊀ β†’ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) : ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ⟢ β„‚ )
79 51 absge0d ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 0 ≀ ( abs β€˜ 𝑦 ) )
80 54 rexrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ 𝑦 ) ∈ ℝ* )
81 peano2re ⊒ ( ( abs β€˜ 𝑦 ) ∈ ℝ β†’ ( ( abs β€˜ 𝑦 ) + 1 ) ∈ ℝ )
82 54 81 syl ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( abs β€˜ 𝑦 ) + 1 ) ∈ ℝ )
83 82 rehalfcld ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ∈ ℝ )
84 83 rexrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ∈ ℝ* )
85 iccssxr ⊒ ( 0 [,] +∞ ) βŠ† ℝ*
86 eqeq1 ⊒ ( π‘š = 𝑗 β†’ ( π‘š = 0 ↔ 𝑗 = 0 ) )
87 oveq2 ⊒ ( π‘š = 𝑗 β†’ ( 1 / π‘š ) = ( 1 / 𝑗 ) )
88 86 87 ifbieq2d ⊒ ( π‘š = 𝑗 β†’ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) = if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) )
89 eqid ⊒ ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) = ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) )
90 c0ex ⊒ 0 ∈ V
91 ovex ⊒ ( 1 / 𝑗 ) ∈ V
92 90 91 ifex ⊒ if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) ∈ V
93 88 89 92 fvmpt ⊒ ( 𝑗 ∈ β„•0 β†’ ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑗 ) = if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) )
94 93 eqcomd ⊒ ( 𝑗 ∈ β„•0 β†’ if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) = ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑗 ) )
95 94 oveq1d ⊒ ( 𝑗 ∈ β„•0 β†’ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) = ( ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑗 ) Β· ( π‘₯ ↑ 𝑗 ) ) )
96 95 mpteq2ia ⊒ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) = ( 𝑗 ∈ β„•0 ↦ ( ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑗 ) Β· ( π‘₯ ↑ 𝑗 ) ) )
97 96 mpteq2i ⊒ ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) = ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑗 ) Β· ( π‘₯ ↑ 𝑗 ) ) ) )
98 0cnd ⊒ ( ( ( ⊀ ∧ π‘š ∈ β„•0 ) ∧ π‘š = 0 ) β†’ 0 ∈ β„‚ )
99 nn0cn ⊒ ( π‘š ∈ β„•0 β†’ π‘š ∈ β„‚ )
100 99 adantl ⊒ ( ( ⊀ ∧ π‘š ∈ β„•0 ) β†’ π‘š ∈ β„‚ )
101 neqne ⊒ ( Β¬ π‘š = 0 β†’ π‘š β‰  0 )
102 reccl ⊒ ( ( π‘š ∈ β„‚ ∧ π‘š β‰  0 ) β†’ ( 1 / π‘š ) ∈ β„‚ )
103 100 101 102 syl2an ⊒ ( ( ( ⊀ ∧ π‘š ∈ β„•0 ) ∧ Β¬ π‘š = 0 ) β†’ ( 1 / π‘š ) ∈ β„‚ )
104 98 103 ifclda ⊒ ( ( ⊀ ∧ π‘š ∈ β„•0 ) β†’ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ∈ β„‚ )
105 104 fmpttd ⊒ ( ⊀ β†’ ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) : β„•0 ⟢ β„‚ )
106 recn ⊒ ( π‘Ÿ ∈ ℝ β†’ π‘Ÿ ∈ β„‚ )
107 oveq1 ⊒ ( π‘₯ = π‘Ÿ β†’ ( π‘₯ ↑ 𝑗 ) = ( π‘Ÿ ↑ 𝑗 ) )
108 107 oveq2d ⊒ ( π‘₯ = π‘Ÿ β†’ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) = ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) )
109 108 mpteq2dv ⊒ ( π‘₯ = π‘Ÿ β†’ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) )
110 eqid ⊒ ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) = ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) )
111 nn0ex ⊒ β„•0 ∈ V
112 111 mptex ⊒ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ∈ V
113 109 110 112 fvmpt ⊒ ( π‘Ÿ ∈ β„‚ β†’ ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ π‘Ÿ ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) )
114 106 113 syl ⊒ ( π‘Ÿ ∈ ℝ β†’ ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ π‘Ÿ ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) )
115 114 eqcomd ⊒ ( π‘Ÿ ∈ ℝ β†’ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) = ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ π‘Ÿ ) )
116 115 seqeq3d ⊒ ( π‘Ÿ ∈ ℝ β†’ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) = seq 0 ( + , ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ π‘Ÿ ) ) )
117 116 eleq1d ⊒ ( π‘Ÿ ∈ ℝ β†’ ( seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ ↔ seq 0 ( + , ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ ) )
118 117 rabbiia ⊒ { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } = { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ }
119 118 supeq1i ⊒ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ π‘Ÿ ) ) ∈ dom ⇝ } , ℝ* , < )
120 97 105 119 radcnvcl ⊒ ( ⊀ β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
121 85 120 sselid ⊒ ( ⊀ β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
122 44 121 mp1i ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
123 1re ⊒ 1 ∈ ℝ
124 avglt1 ⊒ ( ( ( abs β€˜ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ) β†’ ( ( abs β€˜ 𝑦 ) < 1 ↔ ( abs β€˜ 𝑦 ) < ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) )
125 54 123 124 sylancl ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( abs β€˜ 𝑦 ) < 1 ↔ ( abs β€˜ 𝑦 ) < ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) )
126 64 125 mpbid ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ 𝑦 ) < ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) )
127 0red ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 0 ∈ ℝ )
128 127 54 83 79 126 lelttrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 0 < ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) )
129 127 83 128 ltled ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 0 ≀ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) )
130 83 129 absidd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) = ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) )
131 44 105 mp1i ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) : β„•0 ⟢ β„‚ )
132 83 recnd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ∈ β„‚ )
133 oveq1 ⊒ ( π‘₯ = ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) β†’ ( π‘₯ ↑ 𝑗 ) = ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) )
134 133 oveq2d ⊒ ( π‘₯ = ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) β†’ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) = ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) )
135 134 mpteq2dv ⊒ ( π‘₯ = ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) β†’ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) )
136 111 mptex ⊒ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ∈ V
137 135 110 136 fvmpt ⊒ ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ∈ β„‚ β†’ ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) )
138 132 137 syl ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) )
139 138 seqeq3d ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ seq 0 ( + , ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) ) = seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ) )
140 avglt2 ⊒ ( ( ( abs β€˜ 𝑦 ) ∈ ℝ ∧ 1 ∈ ℝ ) β†’ ( ( abs β€˜ 𝑦 ) < 1 ↔ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) < 1 ) )
141 54 123 140 sylancl ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( abs β€˜ 𝑦 ) < 1 ↔ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) < 1 ) )
142 64 141 mpbid ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) < 1 )
143 130 142 eqbrtrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) < 1 )
144 logtayllem ⊒ ( ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ∈ β„‚ ∧ ( abs β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) < 1 ) β†’ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ) ∈ dom ⇝ )
145 132 143 144 syl2anc ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ↑ 𝑗 ) ) ) ) ∈ dom ⇝ )
146 139 145 eqeltrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ seq 0 ( + , ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) ) ∈ dom ⇝ )
147 97 131 119 132 146 radcnvle ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ) ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) )
148 130 147 eqbrtrrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( ( abs β€˜ 𝑦 ) + 1 ) / 2 ) ≀ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) )
149 80 84 122 126 148 xrltletrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ 𝑦 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) )
150 0re ⊒ 0 ∈ ℝ
151 elico2 ⊒ ( ( 0 ∈ ℝ ∧ sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* ) β†’ ( ( abs β€˜ 𝑦 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs β€˜ 𝑦 ) ∈ ℝ ∧ 0 ≀ ( abs β€˜ 𝑦 ) ∧ ( abs β€˜ 𝑦 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
152 150 122 151 sylancr ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( abs β€˜ 𝑦 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs β€˜ 𝑦 ) ∈ ℝ ∧ 0 ≀ ( abs β€˜ 𝑦 ) ∧ ( abs β€˜ 𝑦 ) < sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
153 54 79 149 152 mpbir3and ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ 𝑦 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
154 absf ⊒ abs : β„‚ ⟢ ℝ
155 ffn ⊒ ( abs : β„‚ ⟢ ℝ β†’ abs Fn β„‚ )
156 elpreima ⊒ ( abs Fn β„‚ β†’ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑦 ∈ β„‚ ∧ ( abs β€˜ 𝑦 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
157 154 155 156 mp2b ⊒ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑦 ∈ β„‚ ∧ ( abs β€˜ 𝑦 ) ∈ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
158 51 153 157 sylanbrc ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
159 cnvimass ⊒ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) βŠ† dom abs
160 154 fdmi ⊒ dom abs = β„‚
161 159 160 sseqtri ⊒ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) βŠ† β„‚
162 161 sseli ⊒ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) β†’ 𝑦 ∈ β„‚ )
163 oveq1 ⊒ ( π‘₯ = 𝑦 β†’ ( π‘₯ ↑ 𝑗 ) = ( 𝑦 ↑ 𝑗 ) )
164 163 oveq2d ⊒ ( π‘₯ = 𝑦 β†’ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) = ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) )
165 164 mpteq2dv ⊒ ( π‘₯ = 𝑦 β†’ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) )
166 111 mptex ⊒ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) ∈ V
167 165 110 166 fvmpt ⊒ ( 𝑦 ∈ β„‚ β†’ ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) )
168 167 adantr ⊒ ( ( 𝑦 ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) )
169 168 fveq1d ⊒ ( ( 𝑦 ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ 𝑛 ) = ( ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) β€˜ 𝑛 ) )
170 eqeq1 ⊒ ( 𝑗 = 𝑛 β†’ ( 𝑗 = 0 ↔ 𝑛 = 0 ) )
171 oveq2 ⊒ ( 𝑗 = 𝑛 β†’ ( 1 / 𝑗 ) = ( 1 / 𝑛 ) )
172 170 171 ifbieq2d ⊒ ( 𝑗 = 𝑛 β†’ if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
173 oveq2 ⊒ ( 𝑗 = 𝑛 β†’ ( 𝑦 ↑ 𝑗 ) = ( 𝑦 ↑ 𝑛 ) )
174 172 173 oveq12d ⊒ ( 𝑗 = 𝑛 β†’ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) )
175 eqid ⊒ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) = ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) )
176 ovex ⊒ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ∈ V
177 174 175 176 fvmpt ⊒ ( 𝑛 ∈ β„•0 β†’ ( ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) β€˜ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) )
178 177 adantl ⊒ ( ( 𝑦 ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( 𝑦 ↑ 𝑗 ) ) ) β€˜ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) )
179 169 178 eqtr2d ⊒ ( ( 𝑦 ∈ β„‚ ∧ 𝑛 ∈ β„•0 ) β†’ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ 𝑛 ) )
180 179 sumeq2dv ⊒ ( 𝑦 ∈ β„‚ β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = Ξ£ 𝑛 ∈ β„•0 ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ 𝑛 ) )
181 162 180 syl ⊒ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = Ξ£ 𝑛 ∈ β„•0 ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ 𝑛 ) )
182 181 mpteq2ia ⊒ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) = ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ 𝑛 ) )
183 eqid ⊒ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) = ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
184 eqid ⊒ if ( sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs β€˜ 𝑧 ) + sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs β€˜ 𝑧 ) + 1 ) ) = if ( sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs β€˜ 𝑧 ) + sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs β€˜ 𝑧 ) + 1 ) )
185 97 182 105 119 183 184 psercn ⊒ ( ⊀ β†’ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) ∈ ( ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cnβ†’ β„‚ ) )
186 cncff ⊒ ( ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) ∈ ( ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cnβ†’ β„‚ ) β†’ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) : ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⟢ β„‚ )
187 185 186 syl ⊒ ( ⊀ β†’ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) : ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⟢ β„‚ )
188 187 fvmptelcdm ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ∈ β„‚ )
189 158 188 sylan2 ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ∈ β„‚ )
190 189 fmpttd ⊒ ( ⊀ β†’ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) : ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ⟢ β„‚ )
191 cnelprrecn ⊒ β„‚ ∈ { ℝ , β„‚ }
192 191 a1i ⊒ ( ⊀ β†’ β„‚ ∈ { ℝ , β„‚ } )
193 75 adantl ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ∈ β„‚ )
194 ovexd ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) ∈ V )
195 29 cnmetdval ⊒ ( ( 1 ∈ β„‚ ∧ ( 1 βˆ’ 𝑦 ) ∈ β„‚ ) β†’ ( 1 ( abs ∘ βˆ’ ) ( 1 βˆ’ 𝑦 ) ) = ( abs β€˜ ( 1 βˆ’ ( 1 βˆ’ 𝑦 ) ) ) )
196 48 53 195 sylancr ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 ( abs ∘ βˆ’ ) ( 1 βˆ’ 𝑦 ) ) = ( abs β€˜ ( 1 βˆ’ ( 1 βˆ’ 𝑦 ) ) ) )
197 nncan ⊒ ( ( 1 ∈ β„‚ ∧ 𝑦 ∈ β„‚ ) β†’ ( 1 βˆ’ ( 1 βˆ’ 𝑦 ) ) = 𝑦 )
198 48 51 197 sylancr ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 βˆ’ ( 1 βˆ’ 𝑦 ) ) = 𝑦 )
199 198 fveq2d ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( abs β€˜ ( 1 βˆ’ ( 1 βˆ’ 𝑦 ) ) ) = ( abs β€˜ 𝑦 ) )
200 196 199 eqtrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 ( abs ∘ βˆ’ ) ( 1 βˆ’ 𝑦 ) ) = ( abs β€˜ 𝑦 ) )
201 200 64 eqbrtrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 ( abs ∘ βˆ’ ) ( 1 βˆ’ 𝑦 ) ) < 1 )
202 elbl ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 1 ∈ β„‚ ∧ 1 ∈ ℝ* ) β†’ ( ( 1 βˆ’ 𝑦 ) ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( ( 1 βˆ’ 𝑦 ) ∈ β„‚ ∧ ( 1 ( abs ∘ βˆ’ ) ( 1 βˆ’ 𝑦 ) ) < 1 ) ) )
203 38 48 39 202 mp3an ⊒ ( ( 1 βˆ’ 𝑦 ) ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↔ ( ( 1 βˆ’ 𝑦 ) ∈ β„‚ ∧ ( 1 ( abs ∘ βˆ’ ) ( 1 βˆ’ 𝑦 ) ) < 1 ) )
204 53 201 203 sylanbrc ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 βˆ’ 𝑦 ) ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
205 204 adantl ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ ( 1 βˆ’ 𝑦 ) ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
206 neg1cn ⊒ - 1 ∈ β„‚
207 206 a1i ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ - 1 ∈ β„‚ )
208 eqid ⊒ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) = ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 )
209 208 dvlog2lem ⊒ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† ( β„‚ βˆ– ( -∞ (,] 0 ) )
210 209 sseli ⊒ ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ π‘₯ ∈ ( β„‚ βˆ– ( -∞ (,] 0 ) ) )
211 210 eldifad ⊒ ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ π‘₯ ∈ β„‚ )
212 eqid ⊒ ( β„‚ βˆ– ( -∞ (,] 0 ) ) = ( β„‚ βˆ– ( -∞ (,] 0 ) )
213 212 logdmn0 ⊒ ( π‘₯ ∈ ( β„‚ βˆ– ( -∞ (,] 0 ) ) β†’ π‘₯ β‰  0 )
214 210 213 syl ⊒ ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ π‘₯ β‰  0 )
215 211 214 logcld ⊒ ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( log β€˜ π‘₯ ) ∈ β„‚ )
216 215 adantl ⊒ ( ( ⊀ ∧ π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ ( log β€˜ π‘₯ ) ∈ β„‚ )
217 ovexd ⊒ ( ( ⊀ ∧ π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β†’ ( 1 / π‘₯ ) ∈ V )
218 simpr ⊒ ( ( ⊀ ∧ 𝑦 ∈ β„‚ ) β†’ 𝑦 ∈ β„‚ )
219 48 218 52 sylancr ⊒ ( ( ⊀ ∧ 𝑦 ∈ β„‚ ) β†’ ( 1 βˆ’ 𝑦 ) ∈ β„‚ )
220 206 a1i ⊒ ( ( ⊀ ∧ 𝑦 ∈ β„‚ ) β†’ - 1 ∈ β„‚ )
221 1cnd ⊒ ( ( ⊀ ∧ 𝑦 ∈ β„‚ ) β†’ 1 ∈ β„‚ )
222 0cnd ⊒ ( ( ⊀ ∧ 𝑦 ∈ β„‚ ) β†’ 0 ∈ β„‚ )
223 1cnd ⊒ ( ⊀ β†’ 1 ∈ β„‚ )
224 192 223 dvmptc ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ β„‚ ↦ 1 ) ) = ( 𝑦 ∈ β„‚ ↦ 0 ) )
225 192 dvmptid ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ β„‚ ↦ 𝑦 ) ) = ( 𝑦 ∈ β„‚ ↦ 1 ) )
226 192 221 222 224 218 221 225 dvmptsub ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ β„‚ ↦ ( 1 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ β„‚ ↦ ( 0 βˆ’ 1 ) ) )
227 df-neg ⊒ - 1 = ( 0 βˆ’ 1 )
228 227 mpteq2i ⊒ ( 𝑦 ∈ β„‚ ↦ - 1 ) = ( 𝑦 ∈ β„‚ ↦ ( 0 βˆ’ 1 ) )
229 226 228 eqtr4di ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ β„‚ ↦ ( 1 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ β„‚ ↦ - 1 ) )
230 50 a1i ⊒ ( ⊀ β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† β„‚ )
231 eqid ⊒ ( TopOpen β€˜ β„‚fld ) = ( TopOpen β€˜ β„‚fld )
232 231 cnfldtopon ⊒ ( TopOpen β€˜ β„‚fld ) ∈ ( TopOn β€˜ β„‚ )
233 232 toponrestid ⊒ ( TopOpen β€˜ β„‚fld ) = ( ( TopOpen β€˜ β„‚fld ) β†Ύt β„‚ )
234 231 cnfldtopn ⊒ ( TopOpen β€˜ β„‚fld ) = ( MetOpen β€˜ ( abs ∘ βˆ’ ) )
235 234 blopn ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 0 ∈ β„‚ ∧ 1 ∈ ℝ* ) β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∈ ( TopOpen β€˜ β„‚fld ) )
236 38 28 39 235 mp3an ⊒ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∈ ( TopOpen β€˜ β„‚fld )
237 236 a1i ⊒ ( ⊀ β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∈ ( TopOpen β€˜ β„‚fld ) )
238 192 219 220 229 230 233 231 237 dvmptres ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - 1 ) )
239 logf1o ⊒ log : ( β„‚ βˆ– { 0 } ) –1-1-ontoβ†’ ran log
240 f1of ⊒ ( log : ( β„‚ βˆ– { 0 } ) –1-1-ontoβ†’ ran log β†’ log : ( β„‚ βˆ– { 0 } ) ⟢ ran log )
241 239 240 ax-mp ⊒ log : ( β„‚ βˆ– { 0 } ) ⟢ ran log
242 212 logdmss ⊒ ( β„‚ βˆ– ( -∞ (,] 0 ) ) βŠ† ( β„‚ βˆ– { 0 } )
243 209 242 sstri ⊒ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† ( β„‚ βˆ– { 0 } )
244 fssres ⊒ ( ( log : ( β„‚ βˆ– { 0 } ) ⟢ ran log ∧ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† ( β„‚ βˆ– { 0 } ) ) β†’ ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) : ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ⟢ ran log )
245 241 243 244 mp2an ⊒ ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) : ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ⟢ ran log
246 245 a1i ⊒ ( ⊀ β†’ ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) : ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ⟢ ran log )
247 246 feqmptd ⊒ ( ⊀ β†’ ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) = ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β€˜ π‘₯ ) ) )
248 fvres ⊒ ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β€˜ π‘₯ ) = ( log β€˜ π‘₯ ) )
249 248 mpteq2ia ⊒ ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) β€˜ π‘₯ ) ) = ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( log β€˜ π‘₯ ) )
250 247 249 eqtrdi ⊒ ( ⊀ β†’ ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) = ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( log β€˜ π‘₯ ) ) )
251 250 oveq2d ⊒ ( ⊀ β†’ ( β„‚ D ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) ) = ( β„‚ D ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( log β€˜ π‘₯ ) ) ) )
252 208 dvlog2 ⊒ ( β„‚ D ( log β†Ύ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ) ) = ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / π‘₯ ) )
253 251 252 eqtr3di ⊒ ( ⊀ β†’ ( β„‚ D ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( log β€˜ π‘₯ ) ) ) = ( π‘₯ ∈ ( 1 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / π‘₯ ) ) )
254 fveq2 ⊒ ( π‘₯ = ( 1 βˆ’ 𝑦 ) β†’ ( log β€˜ π‘₯ ) = ( log β€˜ ( 1 βˆ’ 𝑦 ) ) )
255 oveq2 ⊒ ( π‘₯ = ( 1 βˆ’ 𝑦 ) β†’ ( 1 / π‘₯ ) = ( 1 / ( 1 βˆ’ 𝑦 ) ) )
256 192 192 205 207 216 217 238 253 254 255 dvmptco ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) ) )
257 192 193 194 256 dvmptneg ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) ) )
258 53 74 reccld ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 / ( 1 βˆ’ 𝑦 ) ) ∈ β„‚ )
259 mulcom ⊒ ( ( ( 1 / ( 1 βˆ’ 𝑦 ) ) ∈ β„‚ ∧ - 1 ∈ β„‚ ) β†’ ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) = ( - 1 Β· ( 1 / ( 1 βˆ’ 𝑦 ) ) ) )
260 258 206 259 sylancl ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) = ( - 1 Β· ( 1 / ( 1 βˆ’ 𝑦 ) ) ) )
261 258 mulm1d ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( - 1 Β· ( 1 / ( 1 βˆ’ 𝑦 ) ) ) = - ( 1 / ( 1 βˆ’ 𝑦 ) ) )
262 260 261 eqtrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) = - ( 1 / ( 1 βˆ’ 𝑦 ) ) )
263 262 negeqd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ - ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) = - - ( 1 / ( 1 βˆ’ 𝑦 ) ) )
264 258 negnegd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ - - ( 1 / ( 1 βˆ’ 𝑦 ) ) = ( 1 / ( 1 βˆ’ 𝑦 ) ) )
265 263 264 eqtrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ - ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) = ( 1 / ( 1 βˆ’ 𝑦 ) ) )
266 265 mpteq2ia ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( ( 1 / ( 1 βˆ’ 𝑦 ) ) Β· - 1 ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / ( 1 βˆ’ 𝑦 ) ) )
267 257 266 eqtrdi ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / ( 1 βˆ’ 𝑦 ) ) ) )
268 267 dmeqd ⊒ ( ⊀ β†’ dom ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) ) = dom ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / ( 1 βˆ’ 𝑦 ) ) ) )
269 dmmptg ⊒ ( βˆ€ 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ( 1 / ( 1 βˆ’ 𝑦 ) ) ∈ V β†’ dom ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / ( 1 βˆ’ 𝑦 ) ) ) = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
270 ovexd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( 1 / ( 1 βˆ’ 𝑦 ) ) ∈ V )
271 269 270 mprg ⊒ dom ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / ( 1 βˆ’ 𝑦 ) ) ) = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 )
272 268 271 eqtrdi ⊒ ( ⊀ β†’ dom ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) ) = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
273 sumex ⊒ Ξ£ 𝑛 ∈ β„• ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) ∈ V
274 273 a1i ⊒ ( ( ⊀ ∧ 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) β†’ Ξ£ 𝑛 ∈ β„• ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) ∈ V )
275 fveq2 ⊒ ( 𝑛 = π‘˜ β†’ ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ 𝑛 ) = ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) )
276 275 cbvsumv ⊒ Ξ£ 𝑛 ∈ β„•0 ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ 𝑛 ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ )
277 181 276 eqtrdi ⊒ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) )
278 277 mpteq2ia ⊒ ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) = ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ π‘˜ ∈ β„•0 ( ( ( π‘₯ ∈ β„‚ ↦ ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘₯ ↑ 𝑗 ) ) ) ) β€˜ 𝑦 ) β€˜ π‘˜ ) )
279 eqid ⊒ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ 𝑧 ) + if ( sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs β€˜ 𝑧 ) + sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs β€˜ 𝑧 ) + 1 ) ) ) / 2 ) ) = ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) ( ( ( abs β€˜ 𝑧 ) + if ( sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs β€˜ 𝑧 ) + sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs β€˜ 𝑧 ) + 1 ) ) ) / 2 ) )
280 97 278 105 119 183 184 279 pserdv2 ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) ) = ( 𝑦 ∈ ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Ξ£ 𝑛 ∈ β„• ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) ) )
281 158 ssriv ⊒ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
282 281 a1i ⊒ ( ⊀ β†’ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) βŠ† ( β—‘ abs β€œ ( 0 [,) sup ( { π‘Ÿ ∈ ℝ ∣ seq 0 ( + , ( 𝑗 ∈ β„•0 ↦ ( if ( 𝑗 = 0 , 0 , ( 1 / 𝑗 ) ) Β· ( π‘Ÿ ↑ 𝑗 ) ) ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
283 192 188 274 280 282 233 231 237 dvmptres ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„• ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) ) )
284 nnnn0 ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 ∈ β„•0 )
285 284 adantl ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ 𝑛 ∈ β„•0 )
286 eqeq1 ⊒ ( π‘š = 𝑛 β†’ ( π‘š = 0 ↔ 𝑛 = 0 ) )
287 oveq2 ⊒ ( π‘š = 𝑛 β†’ ( 1 / π‘š ) = ( 1 / 𝑛 ) )
288 286 287 ifbieq2d ⊒ ( π‘š = 𝑛 β†’ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
289 ovex ⊒ ( 1 / 𝑛 ) ∈ V
290 90 289 ifex ⊒ if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) ∈ V
291 288 89 290 fvmpt ⊒ ( 𝑛 ∈ β„•0 β†’ ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
292 285 291 syl ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) )
293 nnne0 ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 β‰  0 )
294 293 adantl ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ 𝑛 β‰  0 )
295 294 neneqd ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ Β¬ 𝑛 = 0 )
296 295 iffalsed ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) = ( 1 / 𝑛 ) )
297 292 296 eqtrd ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) = ( 1 / 𝑛 ) )
298 297 oveq2d ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) = ( 𝑛 Β· ( 1 / 𝑛 ) ) )
299 nncn ⊒ ( 𝑛 ∈ β„• β†’ 𝑛 ∈ β„‚ )
300 299 adantl ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ 𝑛 ∈ β„‚ )
301 300 294 recidd ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( 𝑛 Β· ( 1 / 𝑛 ) ) = 1 )
302 298 301 eqtrd ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) = 1 )
303 302 oveq1d ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) = ( 1 Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) )
304 nnm1nn0 ⊒ ( 𝑛 ∈ β„• β†’ ( 𝑛 βˆ’ 1 ) ∈ β„•0 )
305 expcl ⊒ ( ( 𝑦 ∈ β„‚ ∧ ( 𝑛 βˆ’ 1 ) ∈ β„•0 ) β†’ ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ∈ β„‚ )
306 51 304 305 syl2an ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ∈ β„‚ )
307 306 mullidd ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( 1 Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) = ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) )
308 303 307 eqtrd ⊒ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) = ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) )
309 308 sumeq2dv ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ Ξ£ 𝑛 ∈ β„• ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) = Ξ£ 𝑛 ∈ β„• ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) )
310 nnuz ⊒ β„• = ( β„€β‰₯ β€˜ 1 )
311 1e0p1 ⊒ 1 = ( 0 + 1 )
312 311 fveq2i ⊒ ( β„€β‰₯ β€˜ 1 ) = ( β„€β‰₯ β€˜ ( 0 + 1 ) )
313 310 312 eqtri ⊒ β„• = ( β„€β‰₯ β€˜ ( 0 + 1 ) )
314 oveq1 ⊒ ( 𝑛 = ( 1 + π‘š ) β†’ ( 𝑛 βˆ’ 1 ) = ( ( 1 + π‘š ) βˆ’ 1 ) )
315 314 oveq2d ⊒ ( 𝑛 = ( 1 + π‘š ) β†’ ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) = ( 𝑦 ↑ ( ( 1 + π‘š ) βˆ’ 1 ) ) )
316 1zzd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 1 ∈ β„€ )
317 0zd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ 0 ∈ β„€ )
318 1 313 315 316 317 306 isumshft ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ Ξ£ 𝑛 ∈ β„• ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) = Ξ£ π‘š ∈ β„•0 ( 𝑦 ↑ ( ( 1 + π‘š ) βˆ’ 1 ) ) )
319 pncan2 ⊒ ( ( 1 ∈ β„‚ ∧ π‘š ∈ β„‚ ) β†’ ( ( 1 + π‘š ) βˆ’ 1 ) = π‘š )
320 48 99 319 sylancr ⊒ ( π‘š ∈ β„•0 β†’ ( ( 1 + π‘š ) βˆ’ 1 ) = π‘š )
321 320 oveq2d ⊒ ( π‘š ∈ β„•0 β†’ ( 𝑦 ↑ ( ( 1 + π‘š ) βˆ’ 1 ) ) = ( 𝑦 ↑ π‘š ) )
322 321 sumeq2i ⊒ Ξ£ π‘š ∈ β„•0 ( 𝑦 ↑ ( ( 1 + π‘š ) βˆ’ 1 ) ) = Ξ£ π‘š ∈ β„•0 ( 𝑦 ↑ π‘š )
323 318 322 eqtrdi ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ Ξ£ 𝑛 ∈ β„• ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) = Ξ£ π‘š ∈ β„•0 ( 𝑦 ↑ π‘š ) )
324 geoisum ⊒ ( ( 𝑦 ∈ β„‚ ∧ ( abs β€˜ 𝑦 ) < 1 ) β†’ Ξ£ π‘š ∈ β„•0 ( 𝑦 ↑ π‘š ) = ( 1 / ( 1 βˆ’ 𝑦 ) ) )
325 51 64 324 syl2anc ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ Ξ£ π‘š ∈ β„•0 ( 𝑦 ↑ π‘š ) = ( 1 / ( 1 βˆ’ 𝑦 ) ) )
326 309 323 325 3eqtrd ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ Ξ£ 𝑛 ∈ β„• ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) = ( 1 / ( 1 βˆ’ 𝑦 ) ) )
327 326 mpteq2ia ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„• ( ( 𝑛 Β· ( ( π‘š ∈ β„•0 ↦ if ( π‘š = 0 , 0 , ( 1 / π‘š ) ) ) β€˜ 𝑛 ) ) Β· ( 𝑦 ↑ ( 𝑛 βˆ’ 1 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / ( 1 βˆ’ 𝑦 ) ) )
328 283 327 eqtrdi ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ ( 1 / ( 1 βˆ’ 𝑦 ) ) ) )
329 267 328 eqtr4d ⊒ ( ⊀ β†’ ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) ) = ( β„‚ D ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) ) )
330 1rp ⊒ 1 ∈ ℝ+
331 blcntr ⊒ ( ( ( abs ∘ βˆ’ ) ∈ ( ∞Met β€˜ β„‚ ) ∧ 0 ∈ β„‚ ∧ 1 ∈ ℝ+ ) β†’ 0 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
332 38 28 330 331 mp3an ⊒ 0 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 )
333 332 a1i ⊒ ( ⊀ β†’ 0 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) )
334 oveq2 ⊒ ( 𝑦 = 0 β†’ ( 1 βˆ’ 𝑦 ) = ( 1 βˆ’ 0 ) )
335 1m0e1 ⊒ ( 1 βˆ’ 0 ) = 1
336 334 335 eqtrdi ⊒ ( 𝑦 = 0 β†’ ( 1 βˆ’ 𝑦 ) = 1 )
337 336 fveq2d ⊒ ( 𝑦 = 0 β†’ ( log β€˜ ( 1 βˆ’ 𝑦 ) ) = ( log β€˜ 1 ) )
338 log1 ⊒ ( log β€˜ 1 ) = 0
339 337 338 eqtrdi ⊒ ( 𝑦 = 0 β†’ ( log β€˜ ( 1 βˆ’ 𝑦 ) ) = 0 )
340 339 negeqd ⊒ ( 𝑦 = 0 β†’ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) = - 0 )
341 neg0 ⊒ - 0 = 0
342 340 341 eqtrdi ⊒ ( 𝑦 = 0 β†’ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) = 0 )
343 eqid ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) )
344 342 343 90 fvmpt ⊒ ( 0 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) β€˜ 0 ) = 0 )
345 332 344 mp1i ⊒ ( ⊀ β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) β€˜ 0 ) = 0 )
346 oveq1 ⊒ ( 0 = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) β†’ ( 0 Β· ( 𝑦 ↑ 𝑛 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) )
347 346 eqeq1d ⊒ ( 0 = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) β†’ ( ( 0 Β· ( 𝑦 ↑ 𝑛 ) ) = 0 ↔ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = 0 ) )
348 oveq1 ⊒ ( ( 1 / 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) β†’ ( ( 1 / 𝑛 ) Β· ( 𝑦 ↑ 𝑛 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) )
349 348 eqeq1d ⊒ ( ( 1 / 𝑛 ) = if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) β†’ ( ( ( 1 / 𝑛 ) Β· ( 𝑦 ↑ 𝑛 ) ) = 0 ↔ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = 0 ) )
350 simpll ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = 0 ) β†’ 𝑦 = 0 )
351 350 28 eqeltrdi ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = 0 ) β†’ 𝑦 ∈ β„‚ )
352 simplr ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = 0 ) β†’ 𝑛 ∈ β„•0 )
353 351 352 expcld ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = 0 ) β†’ ( 𝑦 ↑ 𝑛 ) ∈ β„‚ )
354 353 mul02d ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ 𝑛 = 0 ) β†’ ( 0 Β· ( 𝑦 ↑ 𝑛 ) ) = 0 )
355 simpll ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ 𝑦 = 0 )
356 355 oveq1d ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( 𝑦 ↑ 𝑛 ) = ( 0 ↑ 𝑛 ) )
357 simpr ⊒ ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) β†’ 𝑛 ∈ β„•0 )
358 357 14 sylib ⊒ ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) β†’ ( 𝑛 ∈ β„• ∨ 𝑛 = 0 ) )
359 358 ord ⊒ ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) β†’ ( Β¬ 𝑛 ∈ β„• β†’ 𝑛 = 0 ) )
360 359 con1d ⊒ ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) β†’ ( Β¬ 𝑛 = 0 β†’ 𝑛 ∈ β„• ) )
361 360 imp ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ 𝑛 ∈ β„• )
362 361 0expd ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( 0 ↑ 𝑛 ) = 0 )
363 356 362 eqtrd ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( 𝑦 ↑ 𝑛 ) = 0 )
364 363 oveq2d ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( ( 1 / 𝑛 ) Β· ( 𝑦 ↑ 𝑛 ) ) = ( ( 1 / 𝑛 ) Β· 0 ) )
365 361 nnrecred ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( 1 / 𝑛 ) ∈ ℝ )
366 365 recnd ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( 1 / 𝑛 ) ∈ β„‚ )
367 366 mul01d ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( ( 1 / 𝑛 ) Β· 0 ) = 0 )
368 364 367 eqtrd ⊒ ( ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) ∧ Β¬ 𝑛 = 0 ) β†’ ( ( 1 / 𝑛 ) Β· ( 𝑦 ↑ 𝑛 ) ) = 0 )
369 347 349 354 368 ifbothda ⊒ ( ( 𝑦 = 0 ∧ 𝑛 ∈ β„•0 ) β†’ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = 0 )
370 369 sumeq2dv ⊒ ( 𝑦 = 0 β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = Ξ£ 𝑛 ∈ β„•0 0 )
371 1 eqimssi ⊒ β„•0 βŠ† ( β„€β‰₯ β€˜ 0 )
372 371 orci ⊒ ( β„•0 βŠ† ( β„€β‰₯ β€˜ 0 ) ∨ β„•0 ∈ Fin )
373 sumz ⊒ ( ( β„•0 βŠ† ( β„€β‰₯ β€˜ 0 ) ∨ β„•0 ∈ Fin ) β†’ Ξ£ 𝑛 ∈ β„•0 0 = 0 )
374 372 373 ax-mp ⊒ Ξ£ 𝑛 ∈ β„•0 0 = 0
375 370 374 eqtrdi ⊒ ( 𝑦 = 0 β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = 0 )
376 eqid ⊒ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) )
377 375 376 90 fvmpt ⊒ ( 0 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) β€˜ 0 ) = 0 )
378 332 377 mp1i ⊒ ( ⊀ β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) β€˜ 0 ) = 0 )
379 345 378 eqtr4d ⊒ ( ⊀ β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) β€˜ 0 ) = ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) β€˜ 0 ) )
380 45 46 47 78 190 272 329 333 379 dv11cn ⊒ ( ⊀ β†’ ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) )
381 380 fveq1d ⊒ ( ⊀ β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) β€˜ 𝐴 ) = ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) β€˜ 𝐴 ) )
382 44 381 mp1i ⊒ ( 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) β€˜ 𝐴 ) = ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) β€˜ 𝐴 ) )
383 oveq2 ⊒ ( 𝑦 = 𝐴 β†’ ( 1 βˆ’ 𝑦 ) = ( 1 βˆ’ 𝐴 ) )
384 383 fveq2d ⊒ ( 𝑦 = 𝐴 β†’ ( log β€˜ ( 1 βˆ’ 𝑦 ) ) = ( log β€˜ ( 1 βˆ’ 𝐴 ) ) )
385 384 negeqd ⊒ ( 𝑦 = 𝐴 β†’ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) = - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) )
386 negex ⊒ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) ∈ V
387 385 343 386 fvmpt ⊒ ( 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ - ( log β€˜ ( 1 βˆ’ 𝑦 ) ) ) β€˜ 𝐴 ) = - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) )
388 oveq1 ⊒ ( 𝑦 = 𝐴 β†’ ( 𝑦 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑛 ) )
389 388 oveq2d ⊒ ( 𝑦 = 𝐴 β†’ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
390 389 sumeq2sdv ⊒ ( 𝑦 = 𝐴 β†’ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) = Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
391 sumex ⊒ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) ∈ V
392 390 376 391 fvmpt ⊒ ( 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ ( ( 𝑦 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) ↦ Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝑦 ↑ 𝑛 ) ) ) β€˜ 𝐴 ) = Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
393 382 387 392 3eqtr3d ⊒ ( 𝐴 ∈ ( 0 ( ball β€˜ ( abs ∘ βˆ’ ) ) 1 ) β†’ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) = Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
394 43 393 syl ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) = Ξ£ 𝑛 ∈ β„•0 ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
395 26 394 breqtrrd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) ⇝ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) )
396 seqex ⊒ seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) ∈ V
397 396 a1i ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) ∈ V )
398 seqex ⊒ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) ∈ V
399 398 a1i ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) ∈ V )
400 1zzd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ 1 ∈ β„€ )
401 elnnuz ⊒ ( 𝑛 ∈ β„• ↔ 𝑛 ∈ ( β„€β‰₯ β€˜ 1 ) )
402 fvres ⊒ ( 𝑛 ∈ ( β„€β‰₯ β€˜ 1 ) β†’ ( ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β†Ύ ( β„€β‰₯ β€˜ 1 ) ) β€˜ 𝑛 ) = ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β€˜ 𝑛 ) )
403 401 402 sylbi ⊒ ( 𝑛 ∈ β„• β†’ ( ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β†Ύ ( β„€β‰₯ β€˜ 1 ) ) β€˜ 𝑛 ) = ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β€˜ 𝑛 ) )
404 403 eqcomd ⊒ ( 𝑛 ∈ β„• β†’ ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β€˜ 𝑛 ) = ( ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β†Ύ ( β„€β‰₯ β€˜ 1 ) ) β€˜ 𝑛 ) )
405 addlid ⊒ ( 𝑛 ∈ β„‚ β†’ ( 0 + 𝑛 ) = 𝑛 )
406 405 adantl ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„‚ ) β†’ ( 0 + 𝑛 ) = 𝑛 )
407 0cnd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ 0 ∈ β„‚ )
408 1eluzge0 ⊒ 1 ∈ ( β„€β‰₯ β€˜ 0 )
409 408 a1i ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ 1 ∈ ( β„€β‰₯ β€˜ 0 ) )
410 0cnd ⊒ ( ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ π‘˜ ∈ β„•0 ) ∧ π‘˜ = 0 ) β†’ 0 ∈ β„‚ )
411 nn0cn ⊒ ( π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚ )
412 411 adantl ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ π‘˜ ∈ β„•0 ) β†’ π‘˜ ∈ β„‚ )
413 neqne ⊒ ( Β¬ π‘˜ = 0 β†’ π‘˜ β‰  0 )
414 reccl ⊒ ( ( π‘˜ ∈ β„‚ ∧ π‘˜ β‰  0 ) β†’ ( 1 / π‘˜ ) ∈ β„‚ )
415 412 413 414 syl2an ⊒ ( ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ π‘˜ ∈ β„•0 ) ∧ Β¬ π‘˜ = 0 ) β†’ ( 1 / π‘˜ ) ∈ β„‚ )
416 410 415 ifclda ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ π‘˜ ∈ β„•0 ) β†’ if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) ∈ β„‚ )
417 expcl ⊒ ( ( 𝐴 ∈ β„‚ ∧ π‘˜ ∈ β„•0 ) β†’ ( 𝐴 ↑ π‘˜ ) ∈ β„‚ )
418 417 adantlr ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( 𝐴 ↑ π‘˜ ) ∈ β„‚ )
419 416 418 mulcld ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ π‘˜ ∈ β„•0 ) β†’ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ∈ β„‚ )
420 419 fmpttd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) : β„•0 ⟢ β„‚ )
421 1nn0 ⊒ 1 ∈ β„•0
422 ffvelcdm ⊒ ( ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) : β„•0 ⟢ β„‚ ∧ 1 ∈ β„•0 ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 1 ) ∈ β„‚ )
423 420 421 422 sylancl ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 1 ) ∈ β„‚ )
424 elfz1eq ⊒ ( 𝑛 ∈ ( 0 ... 0 ) β†’ 𝑛 = 0 )
425 1m1e0 ⊒ ( 1 βˆ’ 1 ) = 0
426 425 oveq2i ⊒ ( 0 ... ( 1 βˆ’ 1 ) ) = ( 0 ... 0 )
427 424 426 eleq2s ⊒ ( 𝑛 ∈ ( 0 ... ( 1 βˆ’ 1 ) ) β†’ 𝑛 = 0 )
428 427 fveq2d ⊒ ( 𝑛 ∈ ( 0 ... ( 1 βˆ’ 1 ) ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 0 ) )
429 0nn0 ⊒ 0 ∈ β„•0
430 iftrue ⊒ ( π‘˜ = 0 β†’ if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) = 0 )
431 oveq2 ⊒ ( π‘˜ = 0 β†’ ( 𝐴 ↑ π‘˜ ) = ( 𝐴 ↑ 0 ) )
432 430 431 oveq12d ⊒ ( π‘˜ = 0 β†’ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) = ( 0 Β· ( 𝐴 ↑ 0 ) ) )
433 ovex ⊒ ( 0 Β· ( 𝐴 ↑ 0 ) ) ∈ V
434 432 8 433 fvmpt ⊒ ( 0 ∈ β„•0 β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 0 ) = ( 0 Β· ( 𝐴 ↑ 0 ) ) )
435 429 434 ax-mp ⊒ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 0 ) = ( 0 Β· ( 𝐴 ↑ 0 ) )
436 expcl ⊒ ( ( 𝐴 ∈ β„‚ ∧ 0 ∈ β„•0 ) β†’ ( 𝐴 ↑ 0 ) ∈ β„‚ )
437 27 429 436 sylancl ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( 𝐴 ↑ 0 ) ∈ β„‚ )
438 437 mul02d ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( 0 Β· ( 𝐴 ↑ 0 ) ) = 0 )
439 435 438 eqtrid ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 0 ) = 0 )
440 428 439 sylan9eqr ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ( 0 ... ( 1 βˆ’ 1 ) ) ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = 0 )
441 406 407 409 423 440 seqid ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β†Ύ ( β„€β‰₯ β€˜ 1 ) ) = seq 1 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) )
442 293 adantl ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ 𝑛 β‰  0 )
443 442 neneqd ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ Β¬ 𝑛 = 0 )
444 443 iffalsed ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) = ( 1 / 𝑛 ) )
445 444 oveq1d ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) = ( ( 1 / 𝑛 ) Β· ( 𝐴 ↑ 𝑛 ) ) )
446 284 23 sylan2 ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( 𝐴 ↑ 𝑛 ) ∈ β„‚ )
447 299 adantl ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ 𝑛 ∈ β„‚ )
448 446 447 442 divrec2d ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) = ( ( 1 / 𝑛 ) Β· ( 𝐴 ↑ 𝑛 ) ) )
449 445 448 eqtr4d ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) = ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) )
450 284 11 sylan2 ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( if ( 𝑛 = 0 , 0 , ( 1 / 𝑛 ) ) Β· ( 𝐴 ↑ 𝑛 ) ) )
451 id ⊒ ( π‘˜ = 𝑛 β†’ π‘˜ = 𝑛 )
452 6 451 oveq12d ⊒ ( π‘˜ = 𝑛 β†’ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) = ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) )
453 eqid ⊒ ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) = ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) )
454 ovex ⊒ ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) ∈ V
455 452 453 454 fvmpt ⊒ ( 𝑛 ∈ β„• β†’ ( ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) = ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) )
456 455 adantl ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) = ( ( 𝐴 ↑ 𝑛 ) / 𝑛 ) )
457 449 450 456 3eqtr4d ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) )
458 401 457 sylan2br ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ ( β„€β‰₯ β€˜ 1 ) ) β†’ ( ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) β€˜ 𝑛 ) = ( ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) β€˜ 𝑛 ) )
459 400 458 seqfeq ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 1 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) = seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) )
460 441 459 eqtrd ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β†Ύ ( β„€β‰₯ β€˜ 1 ) ) = seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) )
461 460 fveq1d ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β†Ύ ( β„€β‰₯ β€˜ 1 ) ) β€˜ 𝑛 ) = ( seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) β€˜ 𝑛 ) )
462 404 461 sylan9eqr ⊒ ( ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) ∧ 𝑛 ∈ β„• ) β†’ ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) β€˜ 𝑛 ) = ( seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) β€˜ 𝑛 ) )
463 310 397 399 400 462 climeq ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ ( seq 0 ( + , ( π‘˜ ∈ β„•0 ↦ ( if ( π‘˜ = 0 , 0 , ( 1 / π‘˜ ) ) Β· ( 𝐴 ↑ π‘˜ ) ) ) ) ⇝ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) ↔ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) ⇝ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) ) )
464 395 463 mpbid ⊒ ( ( 𝐴 ∈ β„‚ ∧ ( abs β€˜ 𝐴 ) < 1 ) β†’ seq 1 ( + , ( π‘˜ ∈ β„• ↦ ( ( 𝐴 ↑ π‘˜ ) / π‘˜ ) ) ) ⇝ - ( log β€˜ ( 1 βˆ’ 𝐴 ) ) )