Step | Hyp | Ref
| Expression |
1 | | 1cnd 7972 |
. . 3
β’ (((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ π = 0) β 1 β
β) |
2 | | simp1 997 |
. . . . . . 7
β’ ((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β π΄ β β) |
3 | | nnuz 9562 |
. . . . . . . 8
β’ β =
(β€β₯β1) |
4 | | 1zzd 9279 |
. . . . . . . 8
β’ (π΄ β β β 1 β
β€) |
5 | | fvconst2g 5730 |
. . . . . . . . 9
β’ ((π΄ β β β§ π₯ β β) β
((β Γ {π΄})βπ₯) = π΄) |
6 | | simpl 109 |
. . . . . . . . 9
β’ ((π΄ β β β§ π₯ β β) β π΄ β
β) |
7 | 5, 6 | eqeltrd 2254 |
. . . . . . . 8
β’ ((π΄ β β β§ π₯ β β) β
((β Γ {π΄})βπ₯) β β) |
8 | | mulcl 7937 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯ Β· π¦) β β) |
9 | 8 | adantl 277 |
. . . . . . . 8
β’ ((π΄ β β β§ (π₯ β β β§ π¦ β β)) β (π₯ Β· π¦) β β) |
10 | 3, 4, 7, 9 | seqf 10460 |
. . . . . . 7
β’ (π΄ β β β seq1(
Β· , (β Γ {π΄})):ββΆβ) |
11 | 2, 10 | syl 14 |
. . . . . 6
β’ ((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β seq1( Β· ,
(β Γ {π΄})):ββΆβ) |
12 | 11 | ad2antrr 488 |
. . . . 5
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ 0 < π) β seq1( Β· , (β Γ
{π΄})):ββΆβ) |
13 | | simp2 998 |
. . . . . . 7
β’ ((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β π β β€) |
14 | 13 | ad2antrr 488 |
. . . . . 6
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ 0 < π) β π β β€) |
15 | | simpr 110 |
. . . . . 6
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ 0 < π) β 0 < π) |
16 | | elnnz 9262 |
. . . . . 6
β’ (π β β β (π β β€ β§ 0 <
π)) |
17 | 14, 15, 16 | sylanbrc 417 |
. . . . 5
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ 0 < π) β π β β) |
18 | 12, 17 | ffvelcdmd 5652 |
. . . 4
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ 0 < π) β (seq1( Β· , (β Γ
{π΄}))βπ) β
β) |
19 | 11 | ad2antrr 488 |
. . . . . 6
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β seq1( Β· , (β Γ
{π΄})):ββΆβ) |
20 | 13 | ad2antrr 488 |
. . . . . . . 8
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β π β β€) |
21 | 20 | znegcld 9376 |
. . . . . . 7
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β -π β β€) |
22 | | simpr 110 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β Β¬ 0 < π) |
23 | | simplr 528 |
. . . . . . . . . . . 12
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β Β¬ π = 0) |
24 | | eqcom 2179 |
. . . . . . . . . . . 12
β’ (π = 0 β 0 = π) |
25 | 23, 24 | sylnib 676 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β Β¬ 0 = π) |
26 | | ioran 752 |
. . . . . . . . . . 11
β’ (Β¬ (0
< π β¨ 0 = π) β (Β¬ 0 < π β§ Β¬ 0 = π)) |
27 | 22, 25, 26 | sylanbrc 417 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β Β¬ (0 < π β¨ 0 = π)) |
28 | | 0zd 9264 |
. . . . . . . . . . 11
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β 0 β β€) |
29 | | zleloe 9299 |
. . . . . . . . . . 11
β’ ((0
β β€ β§ π
β β€) β (0 β€ π β (0 < π β¨ 0 = π))) |
30 | 28, 20, 29 | syl2anc 411 |
. . . . . . . . . 10
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (0 β€ π β (0 < π β¨ 0 = π))) |
31 | 27, 30 | mtbird 673 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β Β¬ 0 β€ π) |
32 | | zltnle 9298 |
. . . . . . . . . 10
β’ ((π β β€ β§ 0 β
β€) β (π < 0
β Β¬ 0 β€ π)) |
33 | 20, 28, 32 | syl2anc 411 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (π < 0 β Β¬ 0 β€ π)) |
34 | 31, 33 | mpbird 167 |
. . . . . . . 8
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β π < 0) |
35 | 20 | zred 9374 |
. . . . . . . . 9
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β π β β) |
36 | 35 | lt0neg1d 8471 |
. . . . . . . 8
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (π < 0 β 0 < -π)) |
37 | 34, 36 | mpbid 147 |
. . . . . . 7
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β 0 < -π) |
38 | | elnnz 9262 |
. . . . . . 7
β’ (-π β β β (-π β β€ β§ 0 <
-π)) |
39 | 21, 37, 38 | sylanbrc 417 |
. . . . . 6
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β -π β β) |
40 | 19, 39 | ffvelcdmd 5652 |
. . . . 5
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (seq1( Β· , (β Γ
{π΄}))β-π) β
β) |
41 | 2 | ad2antrr 488 |
. . . . . 6
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β π΄ β β) |
42 | | simpll3 1038 |
. . . . . . 7
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (π΄ # 0 β¨ 0 β€ π)) |
43 | 31, 42 | ecased 1349 |
. . . . . 6
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β π΄ # 0) |
44 | 41, 43, 39 | exp3vallem 10520 |
. . . . 5
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (seq1( Β· , (β Γ
{π΄}))β-π) # 0) |
45 | 40, 44 | recclapd 8737 |
. . . 4
β’ ((((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β§ Β¬ 0 < π) β (1 / (seq1( Β· , (β
Γ {π΄}))β-π)) β
β) |
46 | | 0zd 9264 |
. . . . 5
β’ (((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β 0 β
β€) |
47 | | simpl2 1001 |
. . . . 5
β’ (((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β π β β€) |
48 | | zdclt 9329 |
. . . . 5
β’ ((0
β β€ β§ π
β β€) β DECID 0 < π) |
49 | 46, 47, 48 | syl2anc 411 |
. . . 4
β’ (((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β DECID 0 <
π) |
50 | 18, 45, 49 | ifcldadc 3563 |
. . 3
β’ (((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β§ Β¬ π = 0) β if(0 < π, (seq1( Β· , (β Γ {π΄}))βπ), (1 / (seq1( Β· , (β Γ
{π΄}))β-π))) β
β) |
51 | | 0zd 9264 |
. . . 4
β’ ((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β 0 β
β€) |
52 | | zdceq 9327 |
. . . 4
β’ ((π β β€ β§ 0 β
β€) β DECID π = 0) |
53 | 13, 51, 52 | syl2anc 411 |
. . 3
β’ ((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β DECID
π = 0) |
54 | 1, 50, 53 | ifcldadc 3563 |
. 2
β’ ((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β if(π = 0, 1, if(0 < π, (seq1( Β· , (β Γ {π΄}))βπ), (1 / (seq1( Β· , (β Γ
{π΄}))β-π)))) β
β) |
55 | | sneq 3603 |
. . . . . . . 8
β’ (π₯ = π΄ β {π₯} = {π΄}) |
56 | 55 | xpeq2d 4650 |
. . . . . . 7
β’ (π₯ = π΄ β (β Γ {π₯}) = (β Γ {π΄})) |
57 | 56 | seqeq3d 10452 |
. . . . . 6
β’ (π₯ = π΄ β seq1( Β· , (β Γ
{π₯})) = seq1( Β· ,
(β Γ {π΄}))) |
58 | 57 | fveq1d 5517 |
. . . . 5
β’ (π₯ = π΄ β (seq1( Β· , (β Γ
{π₯}))βπ¦) = (seq1( Β· , (β
Γ {π΄}))βπ¦)) |
59 | 57 | fveq1d 5517 |
. . . . . 6
β’ (π₯ = π΄ β (seq1( Β· , (β Γ
{π₯}))β-π¦) = (seq1( Β· , (β
Γ {π΄}))β-π¦)) |
60 | 59 | oveq2d 5890 |
. . . . 5
β’ (π₯ = π΄ β (1 / (seq1( Β· , (β
Γ {π₯}))β-π¦)) = (1 / (seq1( Β· ,
(β Γ {π΄}))β-π¦))) |
61 | 58, 60 | ifeq12d 3553 |
. . . 4
β’ (π₯ = π΄ β if(0 < π¦, (seq1( Β· , (β Γ {π₯}))βπ¦), (1 / (seq1( Β· , (β Γ
{π₯}))β-π¦))) = if(0 < π¦, (seq1( Β· , (β
Γ {π΄}))βπ¦), (1 / (seq1( Β· ,
(β Γ {π΄}))β-π¦)))) |
62 | 61 | ifeq2d 3552 |
. . 3
β’ (π₯ = π΄ β if(π¦ = 0, 1, if(0 < π¦, (seq1( Β· , (β Γ {π₯}))βπ¦), (1 / (seq1( Β· , (β Γ
{π₯}))β-π¦)))) = if(π¦ = 0, 1, if(0 < π¦, (seq1( Β· , (β Γ {π΄}))βπ¦), (1 / (seq1( Β· , (β Γ
{π΄}))β-π¦))))) |
63 | | eqeq1 2184 |
. . . 4
β’ (π¦ = π β (π¦ = 0 β π = 0)) |
64 | | breq2 4007 |
. . . . 5
β’ (π¦ = π β (0 < π¦ β 0 < π)) |
65 | | fveq2 5515 |
. . . . 5
β’ (π¦ = π β (seq1( Β· , (β Γ
{π΄}))βπ¦) = (seq1( Β· , (β
Γ {π΄}))βπ)) |
66 | | negeq 8149 |
. . . . . . 7
β’ (π¦ = π β -π¦ = -π) |
67 | 66 | fveq2d 5519 |
. . . . . 6
β’ (π¦ = π β (seq1( Β· , (β Γ
{π΄}))β-π¦) = (seq1( Β· , (β
Γ {π΄}))β-π)) |
68 | 67 | oveq2d 5890 |
. . . . 5
β’ (π¦ = π β (1 / (seq1( Β· , (β
Γ {π΄}))β-π¦)) = (1 / (seq1( Β· ,
(β Γ {π΄}))β-π))) |
69 | 64, 65, 68 | ifbieq12d 3560 |
. . . 4
β’ (π¦ = π β if(0 < π¦, (seq1( Β· , (β Γ {π΄}))βπ¦), (1 / (seq1( Β· , (β Γ
{π΄}))β-π¦))) = if(0 < π, (seq1( Β· , (β
Γ {π΄}))βπ), (1 / (seq1( Β· ,
(β Γ {π΄}))β-π)))) |
70 | 63, 69 | ifbieq2d 3558 |
. . 3
β’ (π¦ = π β if(π¦ = 0, 1, if(0 < π¦, (seq1( Β· , (β Γ {π΄}))βπ¦), (1 / (seq1( Β· , (β Γ
{π΄}))β-π¦)))) = if(π = 0, 1, if(0 < π, (seq1( Β· , (β Γ {π΄}))βπ), (1 / (seq1( Β· , (β Γ
{π΄}))β-π))))) |
71 | | df-exp 10519 |
. . 3
β’ β =
(π₯ β β, π¦ β β€ β¦ if(π¦ = 0, 1, if(0 < π¦, (seq1( Β· , (β
Γ {π₯}))βπ¦), (1 / (seq1( Β· ,
(β Γ {π₯}))β-π¦))))) |
72 | 62, 70, 71 | ovmpog 6008 |
. 2
β’ ((π΄ β β β§ π β β€ β§ if(π = 0, 1, if(0 < π, (seq1( Β· , (β
Γ {π΄}))βπ), (1 / (seq1( Β· ,
(β Γ {π΄}))β-π)))) β β) β (π΄βπ) = if(π = 0, 1, if(0 < π, (seq1( Β· , (β Γ {π΄}))βπ), (1 / (seq1( Β· , (β Γ
{π΄}))β-π))))) |
73 | 54, 72 | syld3an3 1283 |
1
β’ ((π΄ β β β§ π β β€ β§ (π΄ # 0 β¨ 0 β€ π)) β (π΄βπ) = if(π = 0, 1, if(0 < π, (seq1( Β· , (β Γ {π΄}))βπ), (1 / (seq1( Β· , (β Γ
{π΄}))β-π))))) |