Step | Hyp | Ref
| Expression |
1 | | recidpirqlemcalc.a |
. . . . 5
โข (๐ โ ๐ด โ P) |
2 | | 1pr 7552 |
. . . . . 6
โข
1P โ P |
3 | 2 | a1i 9 |
. . . . 5
โข (๐ โ
1P โ P) |
4 | | addclpr 7535 |
. . . . 5
โข ((๐ด โ P โง
1P โ P) โ (๐ด +P
1P) โ P) |
5 | 1, 3, 4 | syl2anc 411 |
. . . 4
โข (๐ โ (๐ด +P
1P) โ P) |
6 | | recidpirqlemcalc.b |
. . . . 5
โข (๐ โ ๐ต โ P) |
7 | | addclpr 7535 |
. . . . 5
โข ((๐ต โ P โง
1P โ P) โ (๐ต +P
1P) โ P) |
8 | 6, 3, 7 | syl2anc 411 |
. . . 4
โข (๐ โ (๐ต +P
1P) โ P) |
9 | | addclpr 7535 |
. . . 4
โข (((๐ด +P
1P) โ P โง (๐ต +P
1P) โ P) โ ((๐ด +P
1P) +P (๐ต +P
1P)) โ P) |
10 | 5, 8, 9 | syl2anc 411 |
. . 3
โข (๐ โ ((๐ด +P
1P) +P (๐ต +P
1P)) โ P) |
11 | | addassprg 7577 |
. . 3
โข ((((๐ด +P
1P) +P (๐ต +P
1P)) โ P โง
1P โ P โง
1P โ P) โ ((((๐ด +P
1P) +P (๐ต +P
1P)) +P
1P) +P
1P) = (((๐ด +P
1P) +P (๐ต +P
1P)) +P
(1P +P
1P))) |
12 | 10, 3, 3, 11 | syl3anc 1238 |
. 2
โข (๐ โ ((((๐ด +P
1P) +P (๐ต +P
1P)) +P
1P) +P
1P) = (((๐ด +P
1P) +P (๐ต +P
1P)) +P
(1P +P
1P))) |
13 | | distrprg 7586 |
. . . . . . 7
โข (((๐ด +P
1P) โ P โง ๐ต โ P โง
1P โ P) โ ((๐ด +P
1P) ยทP (๐ต +P
1P)) = (((๐ด +P
1P) ยทP ๐ต) +P
((๐ด
+P 1P)
ยทP
1P))) |
14 | 5, 6, 3, 13 | syl3anc 1238 |
. . . . . 6
โข (๐ โ ((๐ด +P
1P) ยทP (๐ต +P
1P)) = (((๐ด +P
1P) ยทP ๐ต) +P
((๐ด
+P 1P)
ยทP
1P))) |
15 | | 1idpr 7590 |
. . . . . . . 8
โข ((๐ด +P
1P) โ P โ ((๐ด +P
1P) ยทP
1P) = (๐ด +P
1P)) |
16 | 5, 15 | syl 14 |
. . . . . . 7
โข (๐ โ ((๐ด +P
1P) ยทP
1P) = (๐ด +P
1P)) |
17 | 16 | oveq2d 5890 |
. . . . . 6
โข (๐ โ (((๐ด +P
1P) ยทP ๐ต) +P
((๐ด
+P 1P)
ยทP 1P)) = (((๐ด +P
1P) ยทP ๐ต) +P
(๐ด
+P 1P))) |
18 | | mulcomprg 7578 |
. . . . . . . . 9
โข (((๐ด +P
1P) โ P โง ๐ต โ P) โ ((๐ด +P
1P) ยทP ๐ต) = (๐ต ยทP (๐ด +P
1P))) |
19 | 5, 6, 18 | syl2anc 411 |
. . . . . . . 8
โข (๐ โ ((๐ด +P
1P) ยทP ๐ต) = (๐ต ยทP (๐ด +P
1P))) |
20 | | distrprg 7586 |
. . . . . . . . 9
โข ((๐ต โ P โง
๐ด โ P
โง 1P โ P) โ (๐ต
ยทP (๐ด +P
1P)) = ((๐ต ยทP ๐ด) +P
(๐ต
ยทP
1P))) |
21 | 6, 1, 3, 20 | syl3anc 1238 |
. . . . . . . 8
โข (๐ โ (๐ต ยทP (๐ด +P
1P)) = ((๐ต ยทP ๐ด) +P
(๐ต
ยทP
1P))) |
22 | | mulcomprg 7578 |
. . . . . . . . . . 11
โข ((๐ต โ P โง
๐ด โ P)
โ (๐ต
ยทP ๐ด) = (๐ด ยทP ๐ต)) |
23 | 6, 1, 22 | syl2anc 411 |
. . . . . . . . . 10
โข (๐ โ (๐ต ยทP ๐ด) = (๐ด ยทP ๐ต)) |
24 | | recidpirqlemcalc.rec |
. . . . . . . . . 10
โข (๐ โ (๐ด ยทP ๐ต) =
1P) |
25 | 23, 24 | eqtrd 2210 |
. . . . . . . . 9
โข (๐ โ (๐ต ยทP ๐ด) =
1P) |
26 | | 1idpr 7590 |
. . . . . . . . . 10
โข (๐ต โ P โ
(๐ต
ยทP 1P) = ๐ต) |
27 | 6, 26 | syl 14 |
. . . . . . . . 9
โข (๐ โ (๐ต ยทP
1P) = ๐ต) |
28 | 25, 27 | oveq12d 5892 |
. . . . . . . 8
โข (๐ โ ((๐ต ยทP ๐ด) +P
(๐ต
ยทP 1P)) =
(1P +P ๐ต)) |
29 | 19, 21, 28 | 3eqtrd 2214 |
. . . . . . 7
โข (๐ โ ((๐ด +P
1P) ยทP ๐ต) = (1P
+P ๐ต)) |
30 | 29 | oveq1d 5889 |
. . . . . 6
โข (๐ โ (((๐ด +P
1P) ยทP ๐ต) +P
(๐ด
+P 1P)) =
((1P +P ๐ต) +P (๐ด +P
1P))) |
31 | 14, 17, 30 | 3eqtrd 2214 |
. . . . 5
โข (๐ โ ((๐ด +P
1P) ยทP (๐ต +P
1P)) = ((1P
+P ๐ต) +P (๐ด +P
1P))) |
32 | | 1idpr 7590 |
. . . . . 6
โข
(1P โ P โ
(1P ยทP
1P) = 1P) |
33 | 2, 32 | mp1i 10 |
. . . . 5
โข (๐ โ
(1P ยทP
1P) = 1P) |
34 | 31, 33 | oveq12d 5892 |
. . . 4
โข (๐ โ (((๐ด +P
1P) ยทP (๐ต +P
1P)) +P
(1P ยทP
1P)) = (((1P
+P ๐ต) +P (๐ด +P
1P)) +P
1P)) |
35 | | addcomprg 7576 |
. . . . . . . 8
โข
((1P โ P โง ๐ต โ P) โ
(1P +P ๐ต) = (๐ต +P
1P)) |
36 | 3, 6, 35 | syl2anc 411 |
. . . . . . 7
โข (๐ โ
(1P +P ๐ต) = (๐ต +P
1P)) |
37 | 36 | oveq1d 5889 |
. . . . . 6
โข (๐ โ
((1P +P ๐ต) +P (๐ด +P
1P)) = ((๐ต +P
1P) +P (๐ด +P
1P))) |
38 | | addcomprg 7576 |
. . . . . . 7
โข (((๐ต +P
1P) โ P โง (๐ด +P
1P) โ P) โ ((๐ต +P
1P) +P (๐ด +P
1P)) = ((๐ด +P
1P) +P (๐ต +P
1P))) |
39 | 8, 5, 38 | syl2anc 411 |
. . . . . 6
โข (๐ โ ((๐ต +P
1P) +P (๐ด +P
1P)) = ((๐ด +P
1P) +P (๐ต +P
1P))) |
40 | 37, 39 | eqtrd 2210 |
. . . . 5
โข (๐ โ
((1P +P ๐ต) +P (๐ด +P
1P)) = ((๐ด +P
1P) +P (๐ต +P
1P))) |
41 | 40 | oveq1d 5889 |
. . . 4
โข (๐ โ
(((1P +P ๐ต) +P (๐ด +P
1P)) +P
1P) = (((๐ด +P
1P) +P (๐ต +P
1P)) +P
1P)) |
42 | 34, 41 | eqtrd 2210 |
. . 3
โข (๐ โ (((๐ด +P
1P) ยทP (๐ต +P
1P)) +P
(1P ยทP
1P)) = (((๐ด +P
1P) +P (๐ต +P
1P)) +P
1P)) |
43 | 42 | oveq1d 5889 |
. 2
โข (๐ โ ((((๐ด +P
1P) ยทP (๐ต +P
1P)) +P
(1P ยทP
1P)) +P
1P) = ((((๐ด +P
1P) +P (๐ต +P
1P)) +P
1P) +P
1P)) |
44 | | mulcomprg 7578 |
. . . . . 6
โข
((1P โ P โง (๐ต +P
1P) โ P) โ
(1P ยทP (๐ต +P
1P)) = ((๐ต +P
1P) ยทP
1P)) |
45 | 3, 8, 44 | syl2anc 411 |
. . . . 5
โข (๐ โ
(1P ยทP (๐ต +P
1P)) = ((๐ต +P
1P) ยทP
1P)) |
46 | | 1idpr 7590 |
. . . . . 6
โข ((๐ต +P
1P) โ P โ ((๐ต +P
1P) ยทP
1P) = (๐ต +P
1P)) |
47 | 8, 46 | syl 14 |
. . . . 5
โข (๐ โ ((๐ต +P
1P) ยทP
1P) = (๐ต +P
1P)) |
48 | 45, 47 | eqtrd 2210 |
. . . 4
โข (๐ โ
(1P ยทP (๐ต +P
1P)) = (๐ต +P
1P)) |
49 | 16, 48 | oveq12d 5892 |
. . 3
โข (๐ โ (((๐ด +P
1P) ยทP
1P) +P
(1P ยทP (๐ต +P
1P))) = ((๐ด +P
1P) +P (๐ต +P
1P))) |
50 | 49 | oveq1d 5889 |
. 2
โข (๐ โ ((((๐ด +P
1P) ยทP
1P) +P
(1P ยทP (๐ต +P
1P))) +P
(1P +P
1P)) = (((๐ด +P
1P) +P (๐ต +P
1P)) +P
(1P +P
1P))) |
51 | 12, 43, 50 | 3eqtr4d 2220 |
1
โข (๐ โ ((((๐ด +P
1P) ยทP (๐ต +P
1P)) +P
(1P ยทP
1P)) +P
1P) = ((((๐ด +P
1P) ยทP
1P) +P
(1P ยทP (๐ต +P
1P))) +P
(1P +P
1P))) |