Step | Hyp | Ref
| Expression |
1 | | eqid 2177 |
. . 3
โข
sup({๐ โ
โ0 โฃ (๐โ๐) โฅ ๐ด}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ด}, โ, < ) |
2 | | eqid 2177 |
. . 3
โข
sup({๐ โ
โ0 โฃ (๐โ๐) โฅ ๐ต}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ต}, โ, < ) |
3 | | eqid 2177 |
. . 3
โข
sup({๐ โ
โ0 โฃ (๐โ๐) โฅ (๐ด ยท ๐ต)}, โ, < ) = sup({๐ โ โ0
โฃ (๐โ๐) โฅ (๐ด ยท ๐ต)}, โ, < ) |
4 | 1, 2, 3 | pcpremul 12292 |
. 2
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (sup({๐ โ โ0
โฃ (๐โ๐) โฅ ๐ด}, โ, < ) + sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ต}, โ, < )) = sup({๐ โ โ0
โฃ (๐โ๐) โฅ (๐ด ยท ๐ต)}, โ, < )) |
5 | 1 | pczpre 12296 |
. . . 4
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0)) โ (๐ pCnt ๐ด) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ด}, โ, < )) |
6 | 5 | 3adant3 1017 |
. . 3
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt ๐ด) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ด}, โ, < )) |
7 | 2 | pczpre 12296 |
. . . 4
โข ((๐ โ โ โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt ๐ต) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ต}, โ, < )) |
8 | 7 | 3adant2 1016 |
. . 3
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt ๐ต) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ต}, โ, < )) |
9 | 6, 8 | oveq12d 5892 |
. 2
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ((๐ pCnt ๐ด) + (๐ pCnt ๐ต)) = (sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ด}, โ, < ) + sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ต}, โ, < ))) |
10 | | zmulcl 9305 |
. . . . . 6
โข ((๐ด โ โค โง ๐ต โ โค) โ (๐ด ยท ๐ต) โ โค) |
11 | 10 | ad2ant2r 509 |
. . . . 5
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ด ยท ๐ต) โ โค) |
12 | | zcn 9257 |
. . . . . . . 8
โข (๐ด โ โค โ ๐ด โ
โ) |
13 | 12 | ad2antrr 488 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ด โ
โ) |
14 | | zcn 9257 |
. . . . . . . 8
โข (๐ต โ โค โ ๐ต โ
โ) |
15 | 14 | ad2antrl 490 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ต โ
โ) |
16 | | simplr 528 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ด โ 0) |
17 | | simpll 527 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ด โ
โค) |
18 | | 0zd 9264 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ 0 โ
โค) |
19 | | zapne 9326 |
. . . . . . . . 9
โข ((๐ด โ โค โง 0 โ
โค) โ (๐ด # 0
โ ๐ด โ
0)) |
20 | 17, 18, 19 | syl2anc 411 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ด # 0 โ ๐ด โ 0)) |
21 | 16, 20 | mpbird 167 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ด # 0) |
22 | | simprr 531 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ต โ 0) |
23 | | simprl 529 |
. . . . . . . . 9
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ต โ
โค) |
24 | | zapne 9326 |
. . . . . . . . 9
โข ((๐ต โ โค โง 0 โ
โค) โ (๐ต # 0
โ ๐ต โ
0)) |
25 | 23, 18, 24 | syl2anc 411 |
. . . . . . . 8
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ต # 0 โ ๐ต โ 0)) |
26 | 22, 25 | mpbird 167 |
. . . . . . 7
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ๐ต # 0) |
27 | 13, 15, 21, 26 | mulap0d 8614 |
. . . . . 6
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ด ยท ๐ต) # 0) |
28 | | zapne 9326 |
. . . . . . 7
โข (((๐ด ยท ๐ต) โ โค โง 0 โ โค)
โ ((๐ด ยท ๐ต) # 0 โ (๐ด ยท ๐ต) โ 0)) |
29 | 11, 18, 28 | syl2anc 411 |
. . . . . 6
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) # 0 โ (๐ด ยท ๐ต) โ 0)) |
30 | 27, 29 | mpbid 147 |
. . . . 5
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ด ยท ๐ต) โ 0) |
31 | 11, 30 | jca 306 |
. . . 4
โข (((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) โ โค โง (๐ด ยท ๐ต) โ 0)) |
32 | 3 | pczpre 12296 |
. . . 4
โข ((๐ โ โ โง ((๐ด ยท ๐ต) โ โค โง (๐ด ยท ๐ต) โ 0)) โ (๐ pCnt (๐ด ยท ๐ต)) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ด ยท ๐ต)}, โ, < )) |
33 | 31, 32 | sylan2 286 |
. . 3
โข ((๐ โ โ โง ((๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0))) โ (๐ pCnt (๐ด ยท ๐ต)) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ด ยท ๐ต)}, โ, < )) |
34 | 33 | 3impb 1199 |
. 2
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt (๐ด ยท ๐ต)) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ด ยท ๐ต)}, โ, < )) |
35 | 4, 9, 34 | 3eqtr4rd 2221 |
1
โข ((๐ โ โ โง (๐ด โ โค โง ๐ด โ 0) โง (๐ต โ โค โง ๐ต โ 0)) โ (๐ pCnt (๐ด ยท ๐ต)) = ((๐ pCnt ๐ด) + (๐ pCnt ๐ต))) |