Step |
Hyp |
Ref |
Expression |
1 |
|
oveq2 |
โข ( ๐ฅ = 0 โ ( ๐ด โ ๐ฅ ) = ( ๐ด โ 0 ) ) |
2 |
1
|
oveq2d |
โข ( ๐ฅ = 0 โ ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ pCnt ( ๐ด โ 0 ) ) ) |
3 |
|
oveq1 |
โข ( ๐ฅ = 0 โ ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) = ( 0 ยท ( ๐ pCnt ๐ด ) ) ) |
4 |
2 3
|
eqeq12d |
โข ( ๐ฅ = 0 โ ( ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ 0 ) ) = ( 0 ยท ( ๐ pCnt ๐ด ) ) ) ) |
5 |
|
oveq2 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ด โ ๐ฅ ) = ( ๐ด โ ๐ฆ ) ) |
6 |
5
|
oveq2d |
โข ( ๐ฅ = ๐ฆ โ ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) ) |
7 |
|
oveq1 |
โข ( ๐ฅ = ๐ฆ โ ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) |
8 |
6 7
|
eqeq12d |
โข ( ๐ฅ = ๐ฆ โ ( ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) ) |
9 |
|
oveq2 |
โข ( ๐ฅ = ( ๐ฆ + 1 ) โ ( ๐ด โ ๐ฅ ) = ( ๐ด โ ( ๐ฆ + 1 ) ) ) |
10 |
9
|
oveq2d |
โข ( ๐ฅ = ( ๐ฆ + 1 ) โ ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ pCnt ( ๐ด โ ( ๐ฆ + 1 ) ) ) ) |
11 |
|
oveq1 |
โข ( ๐ฅ = ( ๐ฆ + 1 ) โ ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) = ( ( ๐ฆ + 1 ) ยท ( ๐ pCnt ๐ด ) ) ) |
12 |
10 11
|
eqeq12d |
โข ( ๐ฅ = ( ๐ฆ + 1 ) โ ( ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ ( ๐ฆ + 1 ) ) ) = ( ( ๐ฆ + 1 ) ยท ( ๐ pCnt ๐ด ) ) ) ) |
13 |
|
oveq2 |
โข ( ๐ฅ = - ๐ฆ โ ( ๐ด โ ๐ฅ ) = ( ๐ด โ - ๐ฆ ) ) |
14 |
13
|
oveq2d |
โข ( ๐ฅ = - ๐ฆ โ ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ pCnt ( ๐ด โ - ๐ฆ ) ) ) |
15 |
|
oveq1 |
โข ( ๐ฅ = - ๐ฆ โ ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) = ( - ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) |
16 |
14 15
|
eqeq12d |
โข ( ๐ฅ = - ๐ฆ โ ( ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ - ๐ฆ ) ) = ( - ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) ) |
17 |
|
oveq2 |
โข ( ๐ฅ = ๐ โ ( ๐ด โ ๐ฅ ) = ( ๐ด โ ๐ ) ) |
18 |
17
|
oveq2d |
โข ( ๐ฅ = ๐ โ ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ pCnt ( ๐ด โ ๐ ) ) ) |
19 |
|
oveq1 |
โข ( ๐ฅ = ๐ โ ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) = ( ๐ ยท ( ๐ pCnt ๐ด ) ) ) |
20 |
18 19
|
eqeq12d |
โข ( ๐ฅ = ๐ โ ( ( ๐ pCnt ( ๐ด โ ๐ฅ ) ) = ( ๐ฅ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ ๐ ) ) = ( ๐ ยท ( ๐ pCnt ๐ด ) ) ) ) |
21 |
|
pc1 |
โข ( ๐ โ โ โ ( ๐ pCnt 1 ) = 0 ) |
22 |
21
|
adantr |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ pCnt 1 ) = 0 ) |
23 |
|
qcn |
โข ( ๐ด โ โ โ ๐ด โ โ ) |
24 |
23
|
ad2antrl |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ๐ด โ โ ) |
25 |
24
|
exp0d |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ด โ 0 ) = 1 ) |
26 |
25
|
oveq2d |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ pCnt ( ๐ด โ 0 ) ) = ( ๐ pCnt 1 ) ) |
27 |
|
pcqcl |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ pCnt ๐ด ) โ โค ) |
28 |
27
|
zcnd |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ pCnt ๐ด ) โ โ ) |
29 |
28
|
mul02d |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( 0 ยท ( ๐ pCnt ๐ด ) ) = 0 ) |
30 |
22 26 29
|
3eqtr4d |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ pCnt ( ๐ด โ 0 ) ) = ( 0 ยท ( ๐ pCnt ๐ด ) ) ) |
31 |
|
oveq1 |
โข ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) โ ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) + ( ๐ pCnt ๐ด ) ) = ( ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) + ( ๐ pCnt ๐ด ) ) ) |
32 |
|
expp1 |
โข ( ( ๐ด โ โ โง ๐ฆ โ โ0 ) โ ( ๐ด โ ( ๐ฆ + 1 ) ) = ( ( ๐ด โ ๐ฆ ) ยท ๐ด ) ) |
33 |
24 32
|
sylan |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ๐ด โ ( ๐ฆ + 1 ) ) = ( ( ๐ด โ ๐ฆ ) ยท ๐ด ) ) |
34 |
33
|
oveq2d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ๐ pCnt ( ๐ด โ ( ๐ฆ + 1 ) ) ) = ( ๐ pCnt ( ( ๐ด โ ๐ฆ ) ยท ๐ด ) ) ) |
35 |
|
simpll |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ๐ โ โ ) |
36 |
|
simplrl |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ๐ด โ โ ) |
37 |
|
simplrr |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ๐ด โ 0 ) |
38 |
|
nn0z |
โข ( ๐ฆ โ โ0 โ ๐ฆ โ โค ) |
39 |
38
|
adantl |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ๐ฆ โ โค ) |
40 |
|
qexpclz |
โข ( ( ๐ด โ โ โง ๐ด โ 0 โง ๐ฆ โ โค ) โ ( ๐ด โ ๐ฆ ) โ โ ) |
41 |
36 37 39 40
|
syl3anc |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ๐ด โ ๐ฆ ) โ โ ) |
42 |
24
|
adantr |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ๐ด โ โ ) |
43 |
42 37 39
|
expne0d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ๐ด โ ๐ฆ ) โ 0 ) |
44 |
|
pcqmul |
โข ( ( ๐ โ โ โง ( ( ๐ด โ ๐ฆ ) โ โ โง ( ๐ด โ ๐ฆ ) โ 0 ) โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ pCnt ( ( ๐ด โ ๐ฆ ) ยท ๐ด ) ) = ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) + ( ๐ pCnt ๐ด ) ) ) |
45 |
35 41 43 36 37 44
|
syl122anc |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ๐ pCnt ( ( ๐ด โ ๐ฆ ) ยท ๐ด ) ) = ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) + ( ๐ pCnt ๐ด ) ) ) |
46 |
34 45
|
eqtrd |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ๐ pCnt ( ๐ด โ ( ๐ฆ + 1 ) ) ) = ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) + ( ๐ pCnt ๐ด ) ) ) |
47 |
|
nn0cn |
โข ( ๐ฆ โ โ0 โ ๐ฆ โ โ ) |
48 |
47
|
adantl |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ๐ฆ โ โ ) |
49 |
28
|
adantr |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ๐ pCnt ๐ด ) โ โ ) |
50 |
48 49
|
adddirp1d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ( ๐ฆ + 1 ) ยท ( ๐ pCnt ๐ด ) ) = ( ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) + ( ๐ pCnt ๐ด ) ) ) |
51 |
46 50
|
eqeq12d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ( ๐ pCnt ( ๐ด โ ( ๐ฆ + 1 ) ) ) = ( ( ๐ฆ + 1 ) ยท ( ๐ pCnt ๐ด ) ) โ ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) + ( ๐ pCnt ๐ด ) ) = ( ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) + ( ๐ pCnt ๐ด ) ) ) ) |
52 |
31 51
|
syl5ibr |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ0 ) โ ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ ( ๐ฆ + 1 ) ) ) = ( ( ๐ฆ + 1 ) ยท ( ๐ pCnt ๐ด ) ) ) ) |
53 |
52
|
ex |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ฆ โ โ0 โ ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ ( ๐ฆ + 1 ) ) ) = ( ( ๐ฆ + 1 ) ยท ( ๐ pCnt ๐ด ) ) ) ) ) |
54 |
|
negeq |
โข ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) โ - ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = - ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) |
55 |
|
nnnn0 |
โข ( ๐ฆ โ โ โ ๐ฆ โ โ0 ) |
56 |
|
expneg |
โข ( ( ๐ด โ โ โง ๐ฆ โ โ0 ) โ ( ๐ด โ - ๐ฆ ) = ( 1 / ( ๐ด โ ๐ฆ ) ) ) |
57 |
24 55 56
|
syl2an |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ๐ด โ - ๐ฆ ) = ( 1 / ( ๐ด โ ๐ฆ ) ) ) |
58 |
57
|
oveq2d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ๐ pCnt ( ๐ด โ - ๐ฆ ) ) = ( ๐ pCnt ( 1 / ( ๐ด โ ๐ฆ ) ) ) ) |
59 |
|
simpll |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ๐ โ โ ) |
60 |
55 41
|
sylan2 |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ๐ด โ ๐ฆ ) โ โ ) |
61 |
55 43
|
sylan2 |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ๐ด โ ๐ฆ ) โ 0 ) |
62 |
|
pcrec |
โข ( ( ๐ โ โ โง ( ( ๐ด โ ๐ฆ ) โ โ โง ( ๐ด โ ๐ฆ ) โ 0 ) ) โ ( ๐ pCnt ( 1 / ( ๐ด โ ๐ฆ ) ) ) = - ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) ) |
63 |
59 60 61 62
|
syl12anc |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ๐ pCnt ( 1 / ( ๐ด โ ๐ฆ ) ) ) = - ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) ) |
64 |
58 63
|
eqtrd |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ๐ pCnt ( ๐ด โ - ๐ฆ ) ) = - ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) ) |
65 |
|
nncn |
โข ( ๐ฆ โ โ โ ๐ฆ โ โ ) |
66 |
|
mulneg1 |
โข ( ( ๐ฆ โ โ โง ( ๐ pCnt ๐ด ) โ โ ) โ ( - ๐ฆ ยท ( ๐ pCnt ๐ด ) ) = - ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) |
67 |
65 28 66
|
syl2anr |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( - ๐ฆ ยท ( ๐ pCnt ๐ด ) ) = - ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) |
68 |
64 67
|
eqeq12d |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ( ๐ pCnt ( ๐ด โ - ๐ฆ ) ) = ( - ๐ฆ ยท ( ๐ pCnt ๐ด ) ) โ - ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = - ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) ) |
69 |
54 68
|
syl5ibr |
โข ( ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โง ๐ฆ โ โ ) โ ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ - ๐ฆ ) ) = ( - ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) ) |
70 |
69
|
ex |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ฆ โ โ โ ( ( ๐ pCnt ( ๐ด โ ๐ฆ ) ) = ( ๐ฆ ยท ( ๐ pCnt ๐ด ) ) โ ( ๐ pCnt ( ๐ด โ - ๐ฆ ) ) = ( - ๐ฆ ยท ( ๐ pCnt ๐ด ) ) ) ) ) |
71 |
4 8 12 16 20 30 53 70
|
zindd |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) ) โ ( ๐ โ โค โ ( ๐ pCnt ( ๐ด โ ๐ ) ) = ( ๐ ยท ( ๐ pCnt ๐ด ) ) ) ) |
72 |
71
|
3impia |
โข ( ( ๐ โ โ โง ( ๐ด โ โ โง ๐ด โ 0 ) โง ๐ โ โค ) โ ( ๐ pCnt ( ๐ด โ ๐ ) ) = ( ๐ ยท ( ๐ pCnt ๐ด ) ) ) |