Step | Hyp | Ref
| Expression |
1 | | pceu.7 |
. . . . . . . . . . 11
โข (๐ โ (๐ฅ โ โค โง ๐ฆ โ โ)) |
2 | 1 | simprd 114 |
. . . . . . . . . 10
โข (๐ โ ๐ฆ โ โ) |
3 | 2 | nncnd 8932 |
. . . . . . . . 9
โข (๐ โ ๐ฆ โ โ) |
4 | | pceu.9 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โค โง ๐ก โ โ)) |
5 | 4 | simpld 112 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
6 | 5 | zcnd 9375 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
7 | 3, 6 | mulcomd 7978 |
. . . . . . . 8
โข (๐ โ (๐ฆ ยท ๐ ) = (๐ ยท ๐ฆ)) |
8 | | pceu.10 |
. . . . . . . . . 10
โข (๐ โ ๐ = (๐ / ๐ก)) |
9 | | pceu.8 |
. . . . . . . . . 10
โข (๐ โ ๐ = (๐ฅ / ๐ฆ)) |
10 | 8, 9 | eqtr3d 2212 |
. . . . . . . . 9
โข (๐ โ (๐ / ๐ก) = (๐ฅ / ๐ฆ)) |
11 | 4 | simprd 114 |
. . . . . . . . . . 11
โข (๐ โ ๐ก โ โ) |
12 | 11 | nncnd 8932 |
. . . . . . . . . 10
โข (๐ โ ๐ก โ โ) |
13 | 1 | simpld 112 |
. . . . . . . . . . 11
โข (๐ โ ๐ฅ โ โค) |
14 | 13 | zcnd 9375 |
. . . . . . . . . 10
โข (๐ โ ๐ฅ โ โ) |
15 | 11 | nnap0d 8964 |
. . . . . . . . . 10
โข (๐ โ ๐ก # 0) |
16 | 2 | nnap0d 8964 |
. . . . . . . . . 10
โข (๐ โ ๐ฆ # 0) |
17 | 6, 12, 14, 3, 15, 16 | divmuleqapd 8789 |
. . . . . . . . 9
โข (๐ โ ((๐ / ๐ก) = (๐ฅ / ๐ฆ) โ (๐ ยท ๐ฆ) = (๐ฅ ยท ๐ก))) |
18 | 10, 17 | mpbid 147 |
. . . . . . . 8
โข (๐ โ (๐ ยท ๐ฆ) = (๐ฅ ยท ๐ก)) |
19 | 7, 18 | eqtrd 2210 |
. . . . . . 7
โข (๐ โ (๐ฆ ยท ๐ ) = (๐ฅ ยท ๐ก)) |
20 | 19 | breq2d 4015 |
. . . . . 6
โข (๐ โ ((๐โ๐ง) โฅ (๐ฆ ยท ๐ ) โ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก))) |
21 | 20 | rabbidv 2726 |
. . . . 5
โข (๐ โ {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฆ ยท ๐ )} = {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก)}) |
22 | | oveq2 5882 |
. . . . . . 7
โข (๐ = ๐ง โ (๐โ๐) = (๐โ๐ง)) |
23 | 22 | breq1d 4013 |
. . . . . 6
โข (๐ = ๐ง โ ((๐โ๐) โฅ (๐ฆ ยท ๐ ) โ (๐โ๐ง) โฅ (๐ฆ ยท ๐ ))) |
24 | 23 | cbvrabv 2736 |
. . . . 5
โข {๐ โ โ0
โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )} = {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฆ ยท ๐ )} |
25 | 22 | breq1d 4013 |
. . . . . 6
โข (๐ = ๐ง โ ((๐โ๐) โฅ (๐ฅ ยท ๐ก) โ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก))) |
26 | 25 | cbvrabv 2736 |
. . . . 5
โข {๐ โ โ0
โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)} = {๐ง โ โ0 โฃ (๐โ๐ง) โฅ (๐ฅ ยท ๐ก)} |
27 | 21, 24, 26 | 3eqtr4g 2235 |
. . . 4
โข (๐ โ {๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )} = {๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}) |
28 | 27 | supeq1d 6985 |
. . 3
โข (๐ โ sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < )) |
29 | | pceu.5 |
. . . 4
โข (๐ โ ๐ โ โ) |
30 | 2 | nnzd 9373 |
. . . 4
โข (๐ โ ๐ฆ โ โค) |
31 | 2 | nnne0d 8963 |
. . . 4
โข (๐ โ ๐ฆ โ 0) |
32 | | pceu.6 |
. . . . 5
โข (๐ โ ๐ โ 0) |
33 | 12, 15 | div0apd 8743 |
. . . . . . . 8
โข (๐ โ (0 / ๐ก) = 0) |
34 | | oveq1 5881 |
. . . . . . . . 9
โข (๐ = 0 โ (๐ / ๐ก) = (0 / ๐ก)) |
35 | 34 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ = 0 โ ((๐ / ๐ก) = 0 โ (0 / ๐ก) = 0)) |
36 | 33, 35 | syl5ibrcom 157 |
. . . . . . 7
โข (๐ โ (๐ = 0 โ (๐ / ๐ก) = 0)) |
37 | 8 | eqeq1d 2186 |
. . . . . . 7
โข (๐ โ (๐ = 0 โ (๐ / ๐ก) = 0)) |
38 | 36, 37 | sylibrd 169 |
. . . . . 6
โข (๐ โ (๐ = 0 โ ๐ = 0)) |
39 | 38 | necon3d 2391 |
. . . . 5
โข (๐ โ (๐ โ 0 โ ๐ โ 0)) |
40 | 32, 39 | mpd 13 |
. . . 4
โข (๐ โ ๐ โ 0) |
41 | | pcval.2 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฆ}, โ, < ) |
42 | | pceu.3 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ }, โ, < ) |
43 | | eqid 2177 |
. . . . 5
โข
sup({๐ โ
โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < ) |
44 | 41, 42, 43 | pcpremul 12292 |
. . . 4
โข ((๐ โ โ โง (๐ฆ โ โค โง ๐ฆ โ 0) โง (๐ โ โค โง ๐ โ 0)) โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < )) |
45 | 29, 30, 31, 5, 40, 44 | syl122anc 1247 |
. . 3
โข (๐ โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฆ ยท ๐ )}, โ, < )) |
46 | 3, 16 | div0apd 8743 |
. . . . . . . 8
โข (๐ โ (0 / ๐ฆ) = 0) |
47 | | oveq1 5881 |
. . . . . . . . 9
โข (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = (0 / ๐ฆ)) |
48 | 47 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ฅ = 0 โ ((๐ฅ / ๐ฆ) = 0 โ (0 / ๐ฆ) = 0)) |
49 | 46, 48 | syl5ibrcom 157 |
. . . . . . 7
โข (๐ โ (๐ฅ = 0 โ (๐ฅ / ๐ฆ) = 0)) |
50 | 9 | eqeq1d 2186 |
. . . . . . 7
โข (๐ โ (๐ = 0 โ (๐ฅ / ๐ฆ) = 0)) |
51 | 49, 50 | sylibrd 169 |
. . . . . 6
โข (๐ โ (๐ฅ = 0 โ ๐ = 0)) |
52 | 51 | necon3d 2391 |
. . . . 5
โข (๐ โ (๐ โ 0 โ ๐ฅ โ 0)) |
53 | 32, 52 | mpd 13 |
. . . 4
โข (๐ โ ๐ฅ โ 0) |
54 | 11 | nnzd 9373 |
. . . 4
โข (๐ โ ๐ก โ โค) |
55 | 11 | nnne0d 8963 |
. . . 4
โข (๐ โ ๐ก โ 0) |
56 | | pcval.1 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฅ}, โ, < ) |
57 | | pceu.4 |
. . . . 5
โข ๐ = sup({๐ โ โ0 โฃ (๐โ๐) โฅ ๐ก}, โ, < ) |
58 | | eqid 2177 |
. . . . 5
โข
sup({๐ โ
โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < ) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < ) |
59 | 56, 57, 58 | pcpremul 12292 |
. . . 4
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฅ โ 0) โง (๐ก โ โค โง ๐ก โ 0)) โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < )) |
60 | 29, 13, 53, 54, 55, 59 | syl122anc 1247 |
. . 3
โข (๐ โ (๐ + ๐) = sup({๐ โ โ0 โฃ (๐โ๐) โฅ (๐ฅ ยท ๐ก)}, โ, < )) |
61 | 28, 45, 60 | 3eqtr4d 2220 |
. 2
โข (๐ โ (๐ + ๐) = (๐ + ๐)) |
62 | | prmuz2 12130 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
63 | 29, 62 | syl 14 |
. . . . 5
โข (๐ โ ๐ โ
(โคโฅโ2)) |
64 | | eqid 2177 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ฆ} = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฆ} |
65 | 64, 41 | pcprecl 12288 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ฆ โ โค โง ๐ฆ โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ฆ)) |
66 | 65 | simpld 112 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ฆ โ โค โง ๐ฆ โ 0)) โ ๐ โ
โ0) |
67 | 63, 30, 31, 66 | syl12anc 1236 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
68 | 67 | nn0cnd 9230 |
. . 3
โข (๐ โ ๐ โ โ) |
69 | | eqid 2177 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ } = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ } |
70 | 69, 42 | pcprecl 12288 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ )) |
71 | 70 | simpld 112 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ โ โค โง ๐ โ 0)) โ ๐ โ
โ0) |
72 | 63, 5, 40, 71 | syl12anc 1236 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
73 | 72 | nn0cnd 9230 |
. . 3
โข (๐ โ ๐ โ โ) |
74 | | eqid 2177 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ฅ} = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ฅ} |
75 | 74, 56 | pcprecl 12288 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ฅ)) |
76 | 75 | simpld 112 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ฅ โ โค โง ๐ฅ โ 0)) โ ๐ โ
โ0) |
77 | 63, 13, 53, 76 | syl12anc 1236 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
78 | 77 | nn0cnd 9230 |
. . 3
โข (๐ โ ๐ โ โ) |
79 | | eqid 2177 |
. . . . . . 7
โข {๐ โ โ0
โฃ (๐โ๐) โฅ ๐ก} = {๐ โ โ0 โฃ (๐โ๐) โฅ ๐ก} |
80 | 79, 57 | pcprecl 12288 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐ก โ โค โง ๐ก โ 0)) โ (๐ โ โ0 โง (๐โ๐) โฅ ๐ก)) |
81 | 80 | simpld 112 |
. . . . 5
โข ((๐ โ
(โคโฅโ2) โง (๐ก โ โค โง ๐ก โ 0)) โ ๐ โ
โ0) |
82 | 63, 54, 55, 81 | syl12anc 1236 |
. . . 4
โข (๐ โ ๐ โ
โ0) |
83 | 82 | nn0cnd 9230 |
. . 3
โข (๐ โ ๐ โ โ) |
84 | 68, 73, 78, 83 | addsubeq4d 8318 |
. 2
โข (๐ โ ((๐ + ๐) = (๐ + ๐) โ (๐ โ ๐) = (๐ โ ๐))) |
85 | 61, 84 | mpbid 147 |
1
โข (๐ โ (๐ โ ๐) = (๐ โ ๐)) |