Step |
Hyp |
Ref |
Expression |
1 |
|
nfitg.1 |
โข โฒ ๐ฆ ๐ด |
2 |
|
nfitg.2 |
โข โฒ ๐ฆ ๐ต |
3 |
|
eqid |
โข ( โ โ ( ๐ต / ( i โ ๐ ) ) ) = ( โ โ ( ๐ต / ( i โ ๐ ) ) ) |
4 |
3
|
dfitg |
โข โซ ๐ด ๐ต d ๐ฅ = ฮฃ ๐ โ ( 0 ... 3 ) ( ( i โ ๐ ) ยท ( โซ2 โ ( ๐ฅ โ โ โฆ if ( ( ๐ฅ โ ๐ด โง 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) ) , ( โ โ ( ๐ต / ( i โ ๐ ) ) ) , 0 ) ) ) ) |
5 |
|
nfcv |
โข โฒ ๐ฆ ( 0 ... 3 ) |
6 |
|
nfcv |
โข โฒ ๐ฆ ( i โ ๐ ) |
7 |
|
nfcv |
โข โฒ ๐ฆ ยท |
8 |
|
nfcv |
โข โฒ ๐ฆ โซ2 |
9 |
|
nfcv |
โข โฒ ๐ฆ โ |
10 |
1
|
nfcri |
โข โฒ ๐ฆ ๐ฅ โ ๐ด |
11 |
|
nfcv |
โข โฒ ๐ฆ 0 |
12 |
|
nfcv |
โข โฒ ๐ฆ โค |
13 |
|
nfcv |
โข โฒ ๐ฆ โ |
14 |
|
nfcv |
โข โฒ ๐ฆ / |
15 |
2 14 6
|
nfov |
โข โฒ ๐ฆ ( ๐ต / ( i โ ๐ ) ) |
16 |
13 15
|
nffv |
โข โฒ ๐ฆ ( โ โ ( ๐ต / ( i โ ๐ ) ) ) |
17 |
11 12 16
|
nfbr |
โข โฒ ๐ฆ 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) |
18 |
10 17
|
nfan |
โข โฒ ๐ฆ ( ๐ฅ โ ๐ด โง 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) ) |
19 |
18 16 11
|
nfif |
โข โฒ ๐ฆ if ( ( ๐ฅ โ ๐ด โง 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) ) , ( โ โ ( ๐ต / ( i โ ๐ ) ) ) , 0 ) |
20 |
9 19
|
nfmpt |
โข โฒ ๐ฆ ( ๐ฅ โ โ โฆ if ( ( ๐ฅ โ ๐ด โง 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) ) , ( โ โ ( ๐ต / ( i โ ๐ ) ) ) , 0 ) ) |
21 |
8 20
|
nffv |
โข โฒ ๐ฆ ( โซ2 โ ( ๐ฅ โ โ โฆ if ( ( ๐ฅ โ ๐ด โง 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) ) , ( โ โ ( ๐ต / ( i โ ๐ ) ) ) , 0 ) ) ) |
22 |
6 7 21
|
nfov |
โข โฒ ๐ฆ ( ( i โ ๐ ) ยท ( โซ2 โ ( ๐ฅ โ โ โฆ if ( ( ๐ฅ โ ๐ด โง 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) ) , ( โ โ ( ๐ต / ( i โ ๐ ) ) ) , 0 ) ) ) ) |
23 |
5 22
|
nfsum |
โข โฒ ๐ฆ ฮฃ ๐ โ ( 0 ... 3 ) ( ( i โ ๐ ) ยท ( โซ2 โ ( ๐ฅ โ โ โฆ if ( ( ๐ฅ โ ๐ด โง 0 โค ( โ โ ( ๐ต / ( i โ ๐ ) ) ) ) , ( โ โ ( ๐ต / ( i โ ๐ ) ) ) , 0 ) ) ) ) |
24 |
4 23
|
nfcxfr |
โข โฒ ๐ฆ โซ ๐ด ๐ต d ๐ฅ |