Step | Hyp | Ref
| Expression |
1 | | recexpr 7636 |
. . . . 5
โข (๐ถ โ P โ
โ๐ฆ โ
P (๐ถ
ยทP ๐ฆ) =
1P) |
2 | 1 | 3ad2ant3 1020 |
. . . 4
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ โ๐ฆ โ P (๐ถ ยทP ๐ฆ) =
1P) |
3 | 2 | adantr 276 |
. . 3
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โ โ๐ฆ โ P (๐ถ ยทP ๐ฆ) =
1P) |
4 | | ltexpri 7611 |
. . . . 5
โข ((๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต) โ โ๐ฅ โ P ((๐ถ ยทP ๐ด) +P
๐ฅ) = (๐ถ ยทP ๐ต)) |
5 | 4 | ad2antlr 489 |
. . . 4
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โ
โ๐ฅ โ
P ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต)) |
6 | | simplll 533 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ด โ P โง ๐ต โ P โง
๐ถ โ
P)) |
7 | 6 | simp1d 1009 |
. . . . . 6
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ๐ด โ P) |
8 | | simplrl 535 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ๐ฆ โ P) |
9 | | simprl 529 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ๐ฅ โ P) |
10 | | mulclpr 7570 |
. . . . . . 7
โข ((๐ฆ โ P โง
๐ฅ โ P)
โ (๐ฆ
ยทP ๐ฅ) โ P) |
11 | 8, 9, 10 | syl2anc 411 |
. . . . . 6
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ฆ ยทP ๐ฅ) โ
P) |
12 | | ltaddpr 7595 |
. . . . . 6
โข ((๐ด โ P โง
(๐ฆ
ยทP ๐ฅ) โ P) โ ๐ด<P
(๐ด
+P (๐ฆ ยทP ๐ฅ))) |
13 | 7, 11, 12 | syl2anc 411 |
. . . . 5
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ๐ด<P (๐ด +P
(๐ฆ
ยทP ๐ฅ))) |
14 | | simprr 531 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ((๐ถ ยทP ๐ด) +P
๐ฅ) = (๐ถ ยทP ๐ต)) |
15 | 14 | oveq2d 5890 |
. . . . . 6
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ฆ ยทP ((๐ถ
ยทP ๐ด) +P ๐ฅ)) = (๐ฆ ยทP (๐ถ
ยทP ๐ต))) |
16 | 6 | simp3d 1011 |
. . . . . . . . 9
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ๐ถ โ P) |
17 | | mulclpr 7570 |
. . . . . . . . 9
โข ((๐ถ โ P โง
๐ด โ P)
โ (๐ถ
ยทP ๐ด) โ P) |
18 | 16, 7, 17 | syl2anc 411 |
. . . . . . . 8
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ถ ยทP ๐ด) โ
P) |
19 | | distrprg 7586 |
. . . . . . . 8
โข ((๐ฆ โ P โง
(๐ถ
ยทP ๐ด) โ P โง ๐ฅ โ P) โ
(๐ฆ
ยทP ((๐ถ ยทP ๐ด) +P
๐ฅ)) = ((๐ฆ ยทP (๐ถ
ยทP ๐ด)) +P (๐ฆ
ยทP ๐ฅ))) |
20 | 8, 18, 9, 19 | syl3anc 1238 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ฆ ยทP ((๐ถ
ยทP ๐ด) +P ๐ฅ)) = ((๐ฆ ยทP (๐ถ
ยทP ๐ด)) +P (๐ฆ
ยทP ๐ฅ))) |
21 | | mulassprg 7579 |
. . . . . . . . 9
โข ((๐ฆ โ P โง
๐ถ โ P
โง ๐ด โ
P) โ ((๐ฆ
ยทP ๐ถ) ยทP ๐ด) = (๐ฆ ยทP (๐ถ
ยทP ๐ด))) |
22 | 8, 16, 7, 21 | syl3anc 1238 |
. . . . . . . 8
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ((๐ฆ ยทP ๐ถ)
ยทP ๐ด) = (๐ฆ ยทP (๐ถ
ยทP ๐ด))) |
23 | 22 | oveq1d 5889 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (((๐ฆ ยทP ๐ถ)
ยทP ๐ด) +P (๐ฆ
ยทP ๐ฅ)) = ((๐ฆ ยทP (๐ถ
ยทP ๐ด)) +P (๐ฆ
ยทP ๐ฅ))) |
24 | | mulcomprg 7578 |
. . . . . . . . . . . 12
โข ((๐ฆ โ P โง
๐ถ โ P)
โ (๐ฆ
ยทP ๐ถ) = (๐ถ ยทP ๐ฆ)) |
25 | 8, 16, 24 | syl2anc 411 |
. . . . . . . . . . 11
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ฆ ยทP ๐ถ) = (๐ถ ยทP ๐ฆ)) |
26 | | simplrr 536 |
. . . . . . . . . . 11
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ถ ยทP ๐ฆ) =
1P) |
27 | 25, 26 | eqtrd 2210 |
. . . . . . . . . 10
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ฆ ยทP ๐ถ) =
1P) |
28 | 27 | oveq1d 5889 |
. . . . . . . . 9
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ((๐ฆ ยทP ๐ถ)
ยทP ๐ด) = (1P
ยทP ๐ด)) |
29 | | 1pr 7552 |
. . . . . . . . . . . 12
โข
1P โ P |
30 | | mulcomprg 7578 |
. . . . . . . . . . . 12
โข ((๐ด โ P โง
1P โ P) โ (๐ด ยทP
1P) = (1P
ยทP ๐ด)) |
31 | 29, 30 | mpan2 425 |
. . . . . . . . . . 11
โข (๐ด โ P โ
(๐ด
ยทP 1P) =
(1P ยทP ๐ด)) |
32 | | 1idpr 7590 |
. . . . . . . . . . 11
โข (๐ด โ P โ
(๐ด
ยทP 1P) = ๐ด) |
33 | 31, 32 | eqtr3d 2212 |
. . . . . . . . . 10
โข (๐ด โ P โ
(1P ยทP ๐ด) = ๐ด) |
34 | 7, 33 | syl 14 |
. . . . . . . . 9
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ
(1P ยทP ๐ด) = ๐ด) |
35 | 28, 34 | eqtrd 2210 |
. . . . . . . 8
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ((๐ฆ ยทP ๐ถ)
ยทP ๐ด) = ๐ด) |
36 | 35 | oveq1d 5889 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (((๐ฆ ยทP ๐ถ)
ยทP ๐ด) +P (๐ฆ
ยทP ๐ฅ)) = (๐ด +P (๐ฆ
ยทP ๐ฅ))) |
37 | 20, 23, 36 | 3eqtr2d 2216 |
. . . . . 6
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ฆ ยทP ((๐ถ
ยทP ๐ด) +P ๐ฅ)) = (๐ด +P (๐ฆ
ยทP ๐ฅ))) |
38 | 27 | oveq1d 5889 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ((๐ฆ ยทP ๐ถ)
ยทP ๐ต) = (1P
ยทP ๐ต)) |
39 | 6 | simp2d 1010 |
. . . . . . . 8
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ๐ต โ P) |
40 | | mulassprg 7579 |
. . . . . . . 8
โข ((๐ฆ โ P โง
๐ถ โ P
โง ๐ต โ
P) โ ((๐ฆ
ยทP ๐ถ) ยทP ๐ต) = (๐ฆ ยทP (๐ถ
ยทP ๐ต))) |
41 | 8, 16, 39, 40 | syl3anc 1238 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ((๐ฆ ยทP ๐ถ)
ยทP ๐ต) = (๐ฆ ยทP (๐ถ
ยทP ๐ต))) |
42 | | mulcomprg 7578 |
. . . . . . . . . 10
โข ((๐ต โ P โง
1P โ P) โ (๐ต ยทP
1P) = (1P
ยทP ๐ต)) |
43 | 29, 42 | mpan2 425 |
. . . . . . . . 9
โข (๐ต โ P โ
(๐ต
ยทP 1P) =
(1P ยทP ๐ต)) |
44 | | 1idpr 7590 |
. . . . . . . . 9
โข (๐ต โ P โ
(๐ต
ยทP 1P) = ๐ต) |
45 | 43, 44 | eqtr3d 2212 |
. . . . . . . 8
โข (๐ต โ P โ
(1P ยทP ๐ต) = ๐ต) |
46 | 39, 45 | syl 14 |
. . . . . . 7
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ
(1P ยทP ๐ต) = ๐ต) |
47 | 38, 41, 46 | 3eqtr3d 2218 |
. . . . . 6
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ฆ ยทP (๐ถ
ยทP ๐ต)) = ๐ต) |
48 | 15, 37, 47 | 3eqtr3d 2218 |
. . . . 5
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ (๐ด +P (๐ฆ
ยทP ๐ฅ)) = ๐ต) |
49 | 13, 48 | breqtrd 4029 |
. . . 4
โข
(((((๐ด โ
P โง ๐ต
โ P โง ๐ถ โ P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โง
(๐ฅ โ P
โง ((๐ถ
ยทP ๐ด) +P ๐ฅ) = (๐ถ ยทP ๐ต))) โ ๐ด<P ๐ต) |
50 | 5, 49 | rexlimddv 2599 |
. . 3
โข ((((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โง (๐ฆ โ P โง (๐ถ
ยทP ๐ฆ) = 1P)) โ
๐ด<P ๐ต) |
51 | 3, 50 | rexlimddv 2599 |
. 2
โข (((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โง (๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต)) โ ๐ด<P ๐ต) |
52 | 51 | ex 115 |
1
โข ((๐ด โ P โง
๐ต โ P
โง ๐ถ โ
P) โ ((๐ถ
ยทP ๐ด)<P (๐ถ
ยทP ๐ต) โ ๐ด<P ๐ต)) |