Step | Hyp | Ref
| Expression |
1 | | pceu.7 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โค โง ๐ฆ โ โ)) |
2 | 1 | simprd 497 |
. . . . . . . . . 10
โข (๐ โ ๐ฆ โ โ) |
3 | 2 | nncnd 12176 |
. . . . . . . . 9
โข (๐ โ ๐ฆ โ โ) |
4 | | pceu.9 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โค โง ๐ก โ โ)) |
5 | 4 | simpld 496 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
6 | 5 | zcnd 12615 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
7 | 3, 6 | mulcomd 11183 |
. . . . . . . 8
โข (๐ โ (๐ฆ ยท ๐ ) = (๐ ยท ๐ฆ)) |
8 | | pceu.10 |
. . . . . . . . . 10
โข (๐ โ ๐ = (๐ / ๐ก)) |
9 | | pceu.8 |
. . . . . . . . . 10
โข (๐ โ ๐ = (๐ฅ / ๐ฆ)) |
10 | 8, 9 | eqtr3d 2779 |
. . . . . . . . 9
โข (๐ โ (๐ / ๐ก) = (๐ฅ / ๐ฆ)) |
11 | 4 | simprd 497 |
. . . . . . . . . . 11
โข (๐ โ ๐ก โ โ) |
12 | 11 | nncnd 12176 |
. . . . . . . . . 10
โข (๐ โ ๐ก โ โ) |
13 | 1 | simpld 496 |
. . . . . . . . . . 11
โข (๐ โ ๐ฅ โ โค) |
14 | 13 | zcnd 12615 |
. . . . . . . . . 10
โข (๐ โ ๐ฅ โ โ) |
15 | 11 | nnne0d 12210 |
. . . . . . . . . 10
โข (๐ โ ๐ก โ 0) |
16 | 2 | nnne0d 12210 |
. . . . . . . . . 10
โข (๐ โ ๐ฆ โ 0) |
17 | 6, 12, 14, 3, 15, 16 | divmuleqd 11984 |
. . . . . . . . 9
โข (๐ โ ((๐ / ๐ก) = (๐ฅ / ๐ฆ) โ (๐ ยท ๐ฆ) = (๐ฅ ยท ๐ก))) |
18 | 10, 17 | mpbid 231 |
. . . . . . . 8
โข (๐ โ (๐ ยท ๐ฆ) = (๐ฅ ยท ๐ก)) |
19 | 7, 18 | eqtrd 2777 |
. . . . . . 7
โข (๐ โ (๐ฆ ยท ๐ ) = (๐ฅ ยท ๐ก)) |
20 | 19 | breq2d 5122 |
. . . . . 6
โข (๐ โ ((๐โ๐ง) โฅ (๐ฆ ยท ๐ ) โ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก))) |
21 | 20 | rabbidv 3418 |
. . . . 5
โข (๐ โ {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฆ ยท ๐ )} = {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก)}) |
22 | | oveq2 7370 |
. . . . . . 7
โข (๐ = ๐ง โ (๐โ๐) = (๐โ๐ง)) |
23 | 22 | breq1d 5120 |
. . . . . 6
โข (๐ = ๐ง โ ((๐โ๐) โฅ (๐ฆ ยท ๐ ) โ (๐โ๐ง) โฅ (๐ฆ ยท ๐ ))) |
24 | 23 | cbvrabv 3420 |
. . . . 5
โข {๐ โ โ0
โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )} = {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฆ ยท ๐ )} |
25 | 22 | breq1d 5120 |
. . . . . 6
โข (๐ = ๐ง โ ((๐โ๐) โฅ (๐ฅ ยท ๐ก) โ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก))) |
26 | 25 | cbvrabv 3420 |
. . . . 5
โข {๐ โ โ0
โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)} = {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก)} |
27 | 21, 24, 26 | 3eqtr4g 2802 |
. . . 4
โข (๐ โ {๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )} = {๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}) |
28 | 27 | supeq1d 9389 |
. . 3
โข (๐ โ sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < )) |
29 | | pceu.5 |
. . . 4
โข (๐ โ ๐ โ โ) |
30 | 2 | nnzd 12533 |
. . . 4
โข (๐ โ ๐ฆ โ โค) |
31 | | pceu.6 |
. . . . 5
โข (๐ โ ๐ โ 0) |
32 | 12, 15 | div0d 11937 |
. . . . . . . 8
โข (๐ โ (0 / ๐ก) = 0) |
33 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ / ๐ก) = (0 / ๐ก)) |
34 | 33 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ = 0 โ ((๐ / ๐ก) = 0 โ (0 / ๐ก) = 0)) |
35 | 32, 34 | syl5ibrcom 247 |
. . . . . . 7
โข (๐ โ (๐ = 0 โ (๐ / ๐ก) = 0)) |
36 | 8 | eqeq1d 2739 |
. . . . . . 7
โข (๐ โ (๐ = 0 โ (๐ / ๐ก) = 0)) |
37 | 35, 36 | sylibrd 259 |
. . . . . 6
โข (๐ โ (๐ = 0 โ ๐ = 0)) |
38 | 37 | necon3d 2965 |
. . . . 5
โข (๐ โ (๐ โ 0 โ ๐ โ 0)) |
39 | 31, 38 | mpd 15 |
. . . 4
โข (๐ โ ๐ โ 0) |
40 | | pcval.2 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฆ}, โ, < ) |
41 | | pceu.3 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ }, โ, < ) |
42 | | eqid 2737 |
. . . . 5
โข
sup({๐ โ
โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < ) |
43 | 40, 41, 42 | pcpremul 16722 |
. . . 4
โข ((๐ โ โ โง (๐ฆ โ โค โง ๐ฆ โ 0) โง (๐ โ โค โง ๐ โ 0)) โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < )) |
44 | 29, 30, 16, 5, 39, 43 | syl122anc 1380 |
. . 3
โข (๐ โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < )) |
45 | 3, 16 | div0d 11937 |
. . . . . . . 8
โข (๐ โ (0 / ๐ฆ) = 0) |
46 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = (0 / ๐ฆ)) |
47 | 46 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ฅ = 0 โ ((๐ฅ / ๐ฆ) = 0 โ (0 / ๐ฆ) = 0)) |
48 | 45, 47 | syl5ibrcom 247 |
. . . . . . 7
โข (๐ โ (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = 0)) |
49 | 9 | eqeq1d 2739 |
. . . . . . 7
โข (๐ โ (๐ = 0 โ (๐ฅ / ๐ฆ) = 0)) |
50 | 48, 49 | sylibrd 259 |
. . . . . 6
โข (๐ โ (๐ฅ = 0 โ ๐ = 0)) |
51 | 50 | necon3d 2965 |
. . . . 5
โข (๐ โ (๐ โ 0 โ ๐ฅ โ 0)) |
52 | 31, 51 | mpd 15 |
. . . 4
โข (๐ โ ๐ฅ โ 0) |
53 | 11 | nnzd 12533 |
. . . 4
โข (๐ โ ๐ก โ โค) |
54 | | pcval.1 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฅ}, โ, < ) |
55 | | pceu.4 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ก}, โ, < ) |
56 | | eqid 2737 |
. . . . 5
โข
sup({๐ โ
โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < ) |
57 | 54, 55, 56 | pcpremul 16722 |
. . . 4
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0) โง (๐ก โ โค โง ๐ก โ 0)) โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < )) |
58 | 29, 13, 52, 53, 15, 57 | syl122anc 1380 |
. . 3
โข (๐ โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < )) |
59 | 28, 44, 58 | 3eqtr4d 2787 |
. 2
โข (๐ โ (๐ + ๐) = (๐ + ๐)) |
60 | | prmuz2 16579 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
61 | 29, 60 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ
(โคโฅโ2)) |
62 | | eqid 2737 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ฆ} = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฆ} |
63 | 62, 40 | pcprecl 16718 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ฆ โ โค โง ๐ฆ โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ฆ)) |
64 | 63 | simpld 496 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ฆ โ โค โง ๐ฆ โ 0)) โ ๐ โ
โ0) |
65 | 61, 30, 16, 64 | syl12anc 836 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
66 | 65 | nn0cnd 12482 |
. . 3
โข (๐ โ ๐ โ โ) |
67 | | eqid 2737 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ } = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ } |
68 | 67, 41 | pcprecl 16718 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ )) |
69 | 68 | simpld 496 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ 0)) โ ๐ โ
โ0) |
70 | 61, 5, 39, 69 | syl12anc 836 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
71 | 70 | nn0cnd 12482 |
. . 3
โข (๐ โ ๐ โ โ) |
72 | | eqid 2737 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ฅ} = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฅ} |
73 | 72, 54 | pcprecl 16718 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ฅ)) |
74 | 73 | simpld 496 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ ๐ โ
โ0) |
75 | 61, 13, 52, 74 | syl12anc 836 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
76 | 75 | nn0cnd 12482 |
. . 3
โข (๐ โ ๐ โ โ) |
77 | | eqid 2737 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ก} = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ก} |
78 | 77, 55 | pcprecl 16718 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ก โ โค โง ๐ก โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ก)) |
79 | 78 | simpld 496 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ก โ โค โง ๐ก โ 0)) โ ๐ โ
โ0) |
80 | 61, 53, 15, 79 | syl12anc 836 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
81 | 80 | nn0cnd 12482 |
. . 3
โข (๐ โ ๐ โ โ) |
82 | 66, 71, 76, 81 | addsubeq4d 11570 |
. 2
โข (๐ โ ((๐ + ๐) = (๐ + ๐) โ (๐ โ ๐) = (๐ โ ๐))) |
83 | 59, 82 | mpbid 231 |
1
โข (๐ โ (๐ โ ๐) = (๐ โ ๐)) |