Step | Hyp | Ref
| Expression |
1 | | 3anrot 1101 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β β€) β (π β β€ β§ π β β€ β§ π΄ β
β€)) |
2 | | lgsdilem 26675 |
. . . . 5
β’ (((π β β€ β§ π β β€ β§ π΄ β β€) β§ (π β 0 β§ π β 0)) β if((π΄ < 0 β§ (π Β· π) < 0), -1, 1) = (if((π΄ < 0 β§ π < 0), -1, 1) Β· if((π΄ < 0 β§ π < 0), -1, 1))) |
3 | 1, 2 | sylanb 582 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β if((π΄ < 0 β§ (π Β· π) < 0), -1, 1) = (if((π΄ < 0 β§ π < 0), -1, 1) Β· if((π΄ < 0 β§ π < 0), -1, 1))) |
4 | | ancom 462 |
. . . . 5
β’ (((π Β· π) < 0 β§ π΄ < 0) β (π΄ < 0 β§ (π Β· π) < 0)) |
5 | | ifbi 4509 |
. . . . 5
β’ ((((π Β· π) < 0 β§ π΄ < 0) β (π΄ < 0 β§ (π Β· π) < 0)) β if(((π Β· π) < 0 β§ π΄ < 0), -1, 1) = if((π΄ < 0 β§ (π Β· π) < 0), -1, 1)) |
6 | 4, 5 | ax-mp 5 |
. . . 4
β’
if(((π Β·
π) < 0 β§ π΄ < 0), -1, 1) = if((π΄ < 0 β§ (π Β· π) < 0), -1, 1) |
7 | | ancom 462 |
. . . . . 6
β’ ((π < 0 β§ π΄ < 0) β (π΄ < 0 β§ π < 0)) |
8 | | ifbi 4509 |
. . . . . 6
β’ (((π < 0 β§ π΄ < 0) β (π΄ < 0 β§ π < 0)) β if((π < 0 β§ π΄ < 0), -1, 1) = if((π΄ < 0 β§ π < 0), -1, 1)) |
9 | 7, 8 | ax-mp 5 |
. . . . 5
β’ if((π < 0 β§ π΄ < 0), -1, 1) = if((π΄ < 0 β§ π < 0), -1, 1) |
10 | | ancom 462 |
. . . . . 6
β’ ((π < 0 β§ π΄ < 0) β (π΄ < 0 β§ π < 0)) |
11 | | ifbi 4509 |
. . . . . 6
β’ (((π < 0 β§ π΄ < 0) β (π΄ < 0 β§ π < 0)) β if((π < 0 β§ π΄ < 0), -1, 1) = if((π΄ < 0 β§ π < 0), -1, 1)) |
12 | 10, 11 | ax-mp 5 |
. . . . 5
β’ if((π < 0 β§ π΄ < 0), -1, 1) = if((π΄ < 0 β§ π < 0), -1, 1) |
13 | 9, 12 | oveq12i 7370 |
. . . 4
β’
(if((π < 0 β§
π΄ < 0), -1, 1) Β·
if((π < 0 β§ π΄ < 0), -1, 1)) = (if((π΄ < 0 β§ π < 0), -1, 1) Β· if((π΄ < 0 β§ π < 0), -1, 1)) |
14 | 3, 6, 13 | 3eqtr4g 2802 |
. . 3
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β if(((π Β· π) < 0 β§ π΄ < 0), -1, 1) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1))) |
15 | | simpl2 1193 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β π β β€) |
16 | | simpl3 1194 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β π β β€) |
17 | 15, 16 | zmulcld 12614 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π Β· π) β β€) |
18 | 15 | zcnd 12609 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β π β β) |
19 | 16 | zcnd 12609 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β π β β) |
20 | | simprl 770 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β π β 0) |
21 | | simprr 772 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β π β 0) |
22 | 18, 19, 20, 21 | mulne0d 11808 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π Β· π) β 0) |
23 | | nnabscl 15211 |
. . . . . . 7
β’ (((π Β· π) β β€ β§ (π Β· π) β 0) β (absβ(π Β· π)) β β) |
24 | 17, 22, 23 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (absβ(π Β· π)) β β) |
25 | | nnuz 12807 |
. . . . . 6
β’ β =
(β€β₯β1) |
26 | 24, 25 | eleqtrdi 2848 |
. . . . 5
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (absβ(π Β· π)) β
(β€β₯β1)) |
27 | | simpl1 1192 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β π΄ β β€) |
28 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
29 | 28 | lgsfcl3 26669 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)),
1)):ββΆβ€) |
30 | 27, 15, 20, 29 | syl3anc 1372 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)),
1)):ββΆβ€) |
31 | | elfznn 13471 |
. . . . . . 7
β’ (π β (1...(absβ(π Β· π))) β π β β) |
32 | | ffvelcdm 7033 |
. . . . . . 7
β’ (((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)):ββΆβ€ β§ π β β) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
33 | 30, 31, 32 | syl2an 597 |
. . . . . 6
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
34 | 33 | zcnd 12609 |
. . . . 5
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β) |
35 | | eqid 2737 |
. . . . . . . . 9
β’ (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
36 | 35 | lgsfcl3 26669 |
. . . . . . . 8
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)),
1)):ββΆβ€) |
37 | 27, 16, 21, 36 | syl3anc 1372 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)),
1)):ββΆβ€) |
38 | | ffvelcdm 7033 |
. . . . . . 7
β’ (((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)):ββΆβ€ β§ π β β) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
39 | 37, 31, 38 | syl2an 597 |
. . . . . 6
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
40 | 39 | zcnd 12609 |
. . . . 5
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β) |
41 | | simpr 486 |
. . . . . . . . . . 11
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β π β
β) |
42 | 15 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β π β
β€) |
43 | 20 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β π β 0) |
44 | 16 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β π β
β€) |
45 | 21 | ad2antrr 725 |
. . . . . . . . . . 11
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β π β 0) |
46 | | pcmul 16724 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β β€ β§ π β 0) β§ (π β β€ β§ π β 0)) β (π pCnt (π Β· π)) = ((π pCnt π) + (π pCnt π))) |
47 | 41, 42, 43, 44, 45, 46 | syl122anc 1380 |
. . . . . . . . . 10
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β (π pCnt (π Β· π)) = ((π pCnt π) + (π pCnt π))) |
48 | 47 | oveq2d 7374 |
. . . . . . . . 9
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β ((π΄ /L π)β(π pCnt (π Β· π))) = ((π΄ /L π)β((π pCnt π) + (π pCnt π)))) |
49 | 27 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β π΄ β
β€) |
50 | | prmz 16552 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
51 | 50 | adantl 483 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β π β
β€) |
52 | | lgscl 26662 |
. . . . . . . . . . . 12
β’ ((π΄ β β€ β§ π β β€) β (π΄ /L π) β
β€) |
53 | 49, 51, 52 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β (π΄ /L π) β
β€) |
54 | 53 | zcnd 12609 |
. . . . . . . . . 10
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β (π΄ /L π) β
β) |
55 | | pczcl 16721 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β β€ β§ π β 0)) β (π pCnt π) β
β0) |
56 | 41, 44, 45, 55 | syl12anc 836 |
. . . . . . . . . 10
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β (π pCnt π) β
β0) |
57 | | pczcl 16721 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β β€ β§ π β 0)) β (π pCnt π) β
β0) |
58 | 41, 42, 43, 57 | syl12anc 836 |
. . . . . . . . . 10
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β (π pCnt π) β
β0) |
59 | 54, 56, 58 | expaddd 14054 |
. . . . . . . . 9
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β ((π΄ /L π)β((π pCnt π) + (π pCnt π))) = (((π΄ /L π)β(π pCnt π)) Β· ((π΄ /L π)β(π pCnt π)))) |
60 | 48, 59 | eqtrd 2777 |
. . . . . . . 8
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β ((π΄ /L π)β(π pCnt (π Β· π))) = (((π΄ /L π)β(π pCnt π)) Β· ((π΄ /L π)β(π pCnt π)))) |
61 | | iftrue 4493 |
. . . . . . . . 9
β’ (π β β β if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1) = ((π΄ /L π)β(π pCnt (π Β· π)))) |
62 | 61 | adantl 483 |
. . . . . . . 8
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1) = ((π΄ /L π)β(π pCnt (π Β· π)))) |
63 | | iftrue 4493 |
. . . . . . . . . 10
β’ (π β β β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = ((π΄ /L π)β(π pCnt π))) |
64 | | iftrue 4493 |
. . . . . . . . . 10
β’ (π β β β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = ((π΄ /L π)β(π pCnt π))) |
65 | 63, 64 | oveq12d 7376 |
. . . . . . . . 9
β’ (π β β β (if(π β β, ((π΄ /L π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = (((π΄ /L π)β(π pCnt π)) Β· ((π΄ /L π)β(π pCnt π)))) |
66 | 65 | adantl 483 |
. . . . . . . 8
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β
(if(π β β,
((π΄ /L
π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = (((π΄ /L π)β(π pCnt π)) Β· ((π΄ /L π)β(π pCnt π)))) |
67 | 60, 62, 66 | 3eqtr4rd 2788 |
. . . . . . 7
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ π β β) β
(if(π β β,
((π΄ /L
π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
68 | | 1t1e1 12316 |
. . . . . . . . 9
β’ (1
Β· 1) = 1 |
69 | | iffalse 4496 |
. . . . . . . . . 10
β’ (Β¬
π β β β
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1) = 1) |
70 | | iffalse 4496 |
. . . . . . . . . 10
β’ (Β¬
π β β β
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1) = 1) |
71 | 69, 70 | oveq12d 7376 |
. . . . . . . . 9
β’ (Β¬
π β β β
(if(π β β,
((π΄ /L
π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = (1 Β· 1)) |
72 | | iffalse 4496 |
. . . . . . . . 9
β’ (Β¬
π β β β
if(π β β,
((π΄ /L
π)β(π pCnt (π Β· π))), 1) = 1) |
73 | 68, 71, 72 | 3eqtr4a 2803 |
. . . . . . . 8
β’ (Β¬
π β β β
(if(π β β,
((π΄ /L
π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
74 | 73 | adantl 483 |
. . . . . . 7
β’
(((((π΄ β
β€ β§ π β
β€ β§ π β
β€) β§ (π β 0
β§ π β 0)) β§
π β
(1...(absβ(π Β·
π)))) β§ Β¬ π β β) β
(if(π β β,
((π΄ /L
π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
75 | 67, 74 | pm2.61dan 812 |
. . . . . 6
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β (if(π β β, ((π΄ /L π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) = if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
76 | 31 | adantl 483 |
. . . . . . 7
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β π β β) |
77 | | eleq1w 2821 |
. . . . . . . . . 10
β’ (π = π β (π β β β π β β)) |
78 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π = π β (π΄ /L π) = (π΄ /L π)) |
79 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π = π β (π pCnt π) = (π pCnt π)) |
80 | 78, 79 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π = π β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β(π pCnt π))) |
81 | 77, 80 | ifbieq1d 4511 |
. . . . . . . . 9
β’ (π = π β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
82 | | ovex 7391 |
. . . . . . . . . 10
β’ ((π΄ /L π)β(π pCnt π)) β V |
83 | | 1ex 11152 |
. . . . . . . . . 10
β’ 1 β
V |
84 | 82, 83 | ifex 4537 |
. . . . . . . . 9
β’ if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β V |
85 | 81, 28, 84 | fvmpt 6949 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
86 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π = π β (π pCnt π) = (π pCnt π)) |
87 | 78, 86 | oveq12d 7376 |
. . . . . . . . . 10
β’ (π = π β ((π΄ /L π)β(π pCnt π)) = ((π΄ /L π)β(π pCnt π))) |
88 | 77, 87 | ifbieq1d 4511 |
. . . . . . . . 9
β’ (π = π β if(π β β, ((π΄ /L π)β(π pCnt π)), 1) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
89 | | ovex 7391 |
. . . . . . . . . 10
β’ ((π΄ /L π)β(π pCnt π)) β V |
90 | 89, 83 | ifex 4537 |
. . . . . . . . 9
β’ if(π β β, ((π΄ /L π)β(π pCnt π)), 1) β V |
91 | 88, 35, 90 | fvmpt 6949 |
. . . . . . . 8
β’ (π β β β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt π)), 1)) |
92 | 85, 91 | oveq12d 7376 |
. . . . . . 7
β’ (π β β β (((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) Β· ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ)) = (if(π β β, ((π΄ /L π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1))) |
93 | 76, 92 | syl 17 |
. . . . . 6
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β (((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) Β· ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ)) = (if(π β β, ((π΄ /L π)β(π pCnt π)), 1) Β· if(π β β, ((π΄ /L π)β(π pCnt π)), 1))) |
94 | | oveq1 7365 |
. . . . . . . . . 10
β’ (π = π β (π pCnt (π Β· π)) = (π pCnt (π Β· π))) |
95 | 78, 94 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π β ((π΄ /L π)β(π pCnt (π Β· π))) = ((π΄ /L π)β(π pCnt (π Β· π)))) |
96 | 77, 95 | ifbieq1d 4511 |
. . . . . . . 8
β’ (π = π β if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1) = if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
97 | | eqid 2737 |
. . . . . . . 8
β’ (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) = (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
98 | | ovex 7391 |
. . . . . . . . 9
β’ ((π΄ /L π)β(π pCnt (π Β· π))) β V |
99 | 98, 83 | ifex 4537 |
. . . . . . . 8
β’ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1) β V |
100 | 96, 97, 99 | fvmpt 6949 |
. . . . . . 7
β’ (π β β β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
101 | 76, 100 | syl 17 |
. . . . . 6
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1))βπ) = if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)) |
102 | 75, 93, 101 | 3eqtr4rd 2788 |
. . . . 5
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβ(π Β· π)))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1))βπ) = (((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) Β· ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ))) |
103 | 26, 34, 40, 102 | prodfmul 15776 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)))β(absβ(π Β· π))) = ((seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π))) Β· (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π))))) |
104 | 27, 15, 16, 20, 21, 28 | lgsdilem2 26684 |
. . . . 5
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) = (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π)))) |
105 | 27, 16, 15, 21, 20, 35 | lgsdilem2 26684 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) = (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π)))) |
106 | 18, 19 | mulcomd 11177 |
. . . . . . . 8
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π Β· π) = (π Β· π)) |
107 | 106 | fveq2d 6847 |
. . . . . . 7
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (absβ(π Β· π)) = (absβ(π Β· π))) |
108 | 107 | fveq2d 6847 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π))) = (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π)))) |
109 | 105, 108 | eqtr4d 2780 |
. . . . 5
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) = (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π)))) |
110 | 104, 109 | oveq12d 7376 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β ((seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) Β· (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ))) = ((seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π))) Β· (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβ(π Β· π))))) |
111 | 103, 110 | eqtr4d 2780 |
. . 3
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt (π Β· π))), 1)))β(absβ(π Β· π))) = ((seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) Β· (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)))) |
112 | 14, 111 | oveq12d 7376 |
. 2
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (if(((π Β· π) < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt (π Β· π))), 1)))β(absβ(π Β· π)))) = ((if((π < 0 β§ π΄ < 0), -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1)) Β· ((seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) Β· (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ))))) |
113 | 97 | lgsval4 26668 |
. . 3
β’ ((π΄ β β€ β§ (π Β· π) β β€ β§ (π Β· π) β 0) β (π΄ /L (π Β· π)) = (if(((π Β· π) < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt (π Β· π))), 1)))β(absβ(π Β· π))))) |
114 | 27, 17, 22, 113 | syl3anc 1372 |
. 2
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π΄ /L (π Β· π)) = (if(((π Β· π) < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt (π Β· π))), 1)))β(absβ(π Β· π))))) |
115 | 28 | lgsval4 26668 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) |
116 | 27, 15, 20, 115 | syl3anc 1372 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) |
117 | 35 | lgsval4 26668 |
. . . . 5
β’ ((π΄ β β€ β§ π β β€ β§ π β 0) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) |
118 | 27, 16, 21, 117 | syl3anc 1372 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π΄ /L π) = (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) |
119 | 116, 118 | oveq12d 7376 |
. . 3
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β ((π΄ /L π) Β· (π΄ /L π)) = ((if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))) Β· (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))))) |
120 | | neg1cn 12268 |
. . . . . 6
β’ -1 β
β |
121 | | ax-1cn 11110 |
. . . . . 6
β’ 1 β
β |
122 | 120, 121 | ifcli 4534 |
. . . . 5
β’ if((π < 0 β§ π΄ < 0), -1, 1) β
β |
123 | 122 | a1i 11 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β if((π < 0 β§ π΄ < 0), -1, 1) β
β) |
124 | | nnabscl 15211 |
. . . . . . 7
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
125 | 15, 20, 124 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (absβπ) β
β) |
126 | 125, 25 | eleqtrdi 2848 |
. . . . 5
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (absβπ) β
(β€β₯β1)) |
127 | | elfznn 13471 |
. . . . . . 7
β’ (π β (1...(absβπ)) β π β β) |
128 | 30, 127, 32 | syl2an 597 |
. . . . . 6
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
129 | 128 | zcnd 12609 |
. . . . 5
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β) |
130 | | mulcl 11136 |
. . . . . 6
β’ ((π β β β§ π₯ β β) β (π Β· π₯) β β) |
131 | 130 | adantl 483 |
. . . . 5
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ (π β β β§ π₯ β β)) β (π Β· π₯) β β) |
132 | 126, 129,
131 | seqcl 13929 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β β) |
133 | 120, 121 | ifcli 4534 |
. . . . 5
β’ if((π < 0 β§ π΄ < 0), -1, 1) β
β |
134 | 133 | a1i 11 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β if((π < 0 β§ π΄ < 0), -1, 1) β
β) |
135 | | nnabscl 15211 |
. . . . . . 7
β’ ((π β β€ β§ π β 0) β (absβπ) β
β) |
136 | 16, 21, 135 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (absβπ) β
β) |
137 | 136, 25 | eleqtrdi 2848 |
. . . . 5
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (absβπ) β
(β€β₯β1)) |
138 | | elfznn 13471 |
. . . . . . 7
β’ (π β (1...(absβπ)) β π β β) |
139 | 37, 138, 38 | syl2an 597 |
. . . . . 6
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β€) |
140 | 139 | zcnd 12609 |
. . . . 5
β’ ((((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β§ π β (1...(absβπ))) β ((π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1))βπ) β β) |
141 | 137, 140,
131 | seqcl 13929 |
. . . 4
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ)) β β) |
142 | 123, 132,
134, 141 | mul4d 11368 |
. . 3
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β ((if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ))) Β· (if((π < 0 β§ π΄ < 0), -1, 1) Β· (seq1( Β· ,
(π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)))) = ((if((π < 0 β§ π΄ < 0), -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1)) Β· ((seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) Β· (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ))))) |
143 | 119, 142 | eqtrd 2777 |
. 2
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β ((π΄ /L π) Β· (π΄ /L π)) = ((if((π < 0 β§ π΄ < 0), -1, 1) Β· if((π < 0 β§ π΄ < 0), -1, 1)) Β· ((seq1( Β·
, (π β β β¦
if(π β β,
((π΄ /L
π)β(π pCnt π)), 1)))β(absβπ)) Β· (seq1( Β· , (π β β β¦ if(π β β, ((π΄ /L π)β(π pCnt π)), 1)))β(absβπ))))) |
144 | 112, 114,
143 | 3eqtr4d 2787 |
1
β’ (((π΄ β β€ β§ π β β€ β§ π β β€) β§ (π β 0 β§ π β 0)) β (π΄ /L (π Β· π)) = ((π΄ /L π) Β· (π΄ /L π))) |