Step | Hyp | Ref
| Expression |
1 | | o2timesd.u |
. . . . . . 7
β’ (π β 1 β π΅) |
2 | 1, 1 | jca 513 |
. . . . . 6
β’ (π β ( 1 β π΅ β§ 1 β π΅)) |
3 | | rglcom4d.a |
. . . . . 6
β’ (π β βπ₯ β π΅ βπ¦ β π΅ (π₯ + π¦) β π΅) |
4 | | oveq1 7416 |
. . . . . . . 8
β’ (π₯ = 1 β (π₯ + π¦) = ( 1 + π¦)) |
5 | 4 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = 1 β ((π₯ + π¦) β π΅ β ( 1 + π¦) β π΅)) |
6 | | oveq2 7417 |
. . . . . . . 8
β’ (π¦ = 1 β ( 1 + π¦) = ( 1 + 1 )) |
7 | 6 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = 1 β (( 1 + π¦) β π΅ β ( 1 + 1 ) β π΅)) |
8 | 5, 7 | rspc2v 3623 |
. . . . . 6
β’ (( 1 β π΅ β§ 1 β π΅) β (βπ₯ β π΅ βπ¦ β π΅ (π₯ + π¦) β π΅ β ( 1 + 1 ) β π΅)) |
9 | 2, 3, 8 | sylc 65 |
. . . . 5
β’ (π β ( 1 + 1 ) β π΅) |
10 | | o2timesd.x |
. . . . 5
β’ (π β π β π΅) |
11 | | rglcom4d.y |
. . . . 5
β’ (π β π β π΅) |
12 | 9, 10, 11 | 3jca 1129 |
. . . 4
β’ (π β (( 1 + 1 ) β π΅ β§ π β π΅ β§ π β π΅)) |
13 | | rglcom4d.d |
. . . 4
β’ (π β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) |
14 | | oveq1 7416 |
. . . . . 6
β’ (π₯ = ( 1 + 1 ) β (π₯ Β· (π¦ + π§)) = (( 1 + 1 ) Β· (π¦ + π§))) |
15 | | oveq1 7416 |
. . . . . . 7
β’ (π₯ = ( 1 + 1 ) β (π₯ Β· π¦) = (( 1 + 1 ) Β· π¦)) |
16 | | oveq1 7416 |
. . . . . . 7
β’ (π₯ = ( 1 + 1 ) β (π₯ Β· π§) = (( 1 + 1 ) Β· π§)) |
17 | 15, 16 | oveq12d 7427 |
. . . . . 6
β’ (π₯ = ( 1 + 1 ) β ((π₯ Β· π¦) + (π₯ Β· π§)) = ((( 1 + 1 ) Β· π¦) + (( 1 + 1 ) Β· π§))) |
18 | 14, 17 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = ( 1 + 1 ) β ((π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β (( 1 + 1 ) Β· (π¦ + π§)) = ((( 1 + 1 ) Β· π¦) + (( 1 + 1 ) Β· π§)))) |
19 | | oveq1 7416 |
. . . . . . 7
β’ (π¦ = π β (π¦ + π§) = (π + π§)) |
20 | 19 | oveq2d 7425 |
. . . . . 6
β’ (π¦ = π β (( 1 + 1 ) Β· (π¦ + π§)) = (( 1 + 1 ) Β· (π + π§))) |
21 | | oveq2 7417 |
. . . . . . 7
β’ (π¦ = π β (( 1 + 1 ) Β· π¦) = (( 1 + 1 ) Β· π)) |
22 | 21 | oveq1d 7424 |
. . . . . 6
β’ (π¦ = π β ((( 1 + 1 ) Β· π¦) + (( 1 + 1 ) Β· π§)) = ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π§))) |
23 | 20, 22 | eqeq12d 2749 |
. . . . 5
β’ (π¦ = π β ((( 1 + 1 ) Β· (π¦ + π§)) = ((( 1 + 1 ) Β· π¦) + (( 1 + 1 ) Β· π§)) β (( 1 + 1 ) Β· (π + π§)) = ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π§)))) |
24 | | oveq2 7417 |
. . . . . . 7
β’ (π§ = π β (π + π§) = (π + π)) |
25 | 24 | oveq2d 7425 |
. . . . . 6
β’ (π§ = π β (( 1 + 1 ) Β· (π + π§)) = (( 1 + 1 ) Β· (π + π))) |
26 | | oveq2 7417 |
. . . . . . 7
β’ (π§ = π β (( 1 + 1 ) Β· π§) = (( 1 + 1 ) Β· π)) |
27 | 26 | oveq2d 7425 |
. . . . . 6
β’ (π§ = π β ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π§)) = ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π))) |
28 | 25, 27 | eqeq12d 2749 |
. . . . 5
β’ (π§ = π β ((( 1 + 1 ) Β· (π + π§)) = ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π§)) β (( 1 + 1 ) Β· (π + π)) = ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π)))) |
29 | 18, 23, 28 | rspc3v 3628 |
. . . 4
β’ ((( 1 + 1 ) β
π΅ β§ π β π΅ β§ π β π΅) β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β (( 1 + 1 ) Β· (π + π)) = ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π)))) |
30 | 12, 13, 29 | sylc 65 |
. . 3
β’ (π β (( 1 + 1 ) Β· (π + π)) = ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π))) |
31 | | oveq1 7416 |
. . . . . . . 8
β’ (π₯ = π β (π₯ + π¦) = (π + π¦)) |
32 | 31 | eleq1d 2819 |
. . . . . . 7
β’ (π₯ = π β ((π₯ + π¦) β π΅ β (π + π¦) β π΅)) |
33 | | oveq2 7417 |
. . . . . . . 8
β’ (π¦ = π β (π + π¦) = (π + π)) |
34 | 33 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = π β ((π + π¦) β π΅ β (π + π) β π΅)) |
35 | 32, 34 | rspc2va 3624 |
. . . . . 6
β’ (((π β π΅ β§ π β π΅) β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ + π¦) β π΅) β (π + π) β π΅) |
36 | 10, 11, 3, 35 | syl21anc 837 |
. . . . 5
β’ (π β (π + π) β π΅) |
37 | 1, 1, 36 | 3jca 1129 |
. . . 4
β’ (π β ( 1 β π΅ β§ 1 β π΅ β§ (π + π) β π΅)) |
38 | | o2timesd.e |
. . . 4
β’ (π β βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) |
39 | 4 | oveq1d 7424 |
. . . . . 6
β’ (π₯ = 1 β ((π₯ + π¦) Β· π§) = (( 1 + π¦) Β· π§)) |
40 | | oveq1 7416 |
. . . . . . 7
β’ (π₯ = 1 β (π₯ Β· π§) = ( 1 Β· π§)) |
41 | 40 | oveq1d 7424 |
. . . . . 6
β’ (π₯ = 1 β ((π₯ Β· π§) + (π¦ Β· π§)) = (( 1 Β· π§) + (π¦ Β· π§))) |
42 | 39, 41 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = 1 β (((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§)) β (( 1 + π¦) Β· π§) = (( 1 Β· π§) + (π¦ Β· π§)))) |
43 | 6 | oveq1d 7424 |
. . . . . 6
β’ (π¦ = 1 β (( 1 + π¦) Β· π§) = (( 1 + 1 ) Β· π§)) |
44 | | oveq1 7416 |
. . . . . . 7
β’ (π¦ = 1 β (π¦ Β· π§) = ( 1 Β· π§)) |
45 | 44 | oveq2d 7425 |
. . . . . 6
β’ (π¦ = 1 β (( 1 Β· π§) + (π¦ Β· π§)) = (( 1 Β· π§) + ( 1 Β· π§))) |
46 | 43, 45 | eqeq12d 2749 |
. . . . 5
β’ (π¦ = 1 β ((( 1 + π¦) Β· π§) = (( 1 Β· π§) + (π¦ Β· π§)) β (( 1 + 1 ) Β· π§) = (( 1 Β· π§) + ( 1 Β· π§)))) |
47 | | oveq2 7417 |
. . . . . 6
β’ (π§ = (π + π) β (( 1 + 1 ) Β· π§) = (( 1 + 1 ) Β· (π + π))) |
48 | | oveq2 7417 |
. . . . . . 7
β’ (π§ = (π + π) β ( 1 Β· π§) = ( 1 Β· (π + π))) |
49 | 48, 48 | oveq12d 7427 |
. . . . . 6
β’ (π§ = (π + π) β (( 1 Β· π§) + ( 1 Β· π§)) = (( 1 Β· (π + π)) + ( 1 Β· (π + π)))) |
50 | 47, 49 | eqeq12d 2749 |
. . . . 5
β’ (π§ = (π + π) β ((( 1 + 1 ) Β· π§) = (( 1 Β· π§) + ( 1 Β· π§)) β (( 1 + 1 ) Β· (π + π)) = (( 1 Β· (π + π)) + ( 1 Β· (π + π))))) |
51 | 42, 46, 50 | rspc3v 3628 |
. . . 4
β’ (( 1 β π΅ β§ 1 β π΅ β§ (π + π) β π΅) β (βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§)) β (( 1 + 1 ) Β· (π + π)) = (( 1 Β· (π + π)) + ( 1 Β· (π + π))))) |
52 | 37, 38, 51 | sylc 65 |
. . 3
β’ (π β (( 1 + 1 ) Β· (π + π)) = (( 1 Β· (π + π)) + ( 1 Β· (π + π)))) |
53 | 30, 52 | eqtr3d 2775 |
. 2
β’ (π β ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π)) = (( 1 Β· (π + π)) + ( 1 Β· (π + π)))) |
54 | | o2timesd.i |
. . . . 5
β’ (π β βπ₯ β π΅ ( 1 Β· π₯) = π₯) |
55 | 38, 1, 54, 10 | o2timesd 20033 |
. . . 4
β’ (π β (π + π) = (( 1 + 1 ) Β· π)) |
56 | 55 | eqcomd 2739 |
. . 3
β’ (π β (( 1 + 1 ) Β· π) = (π + π)) |
57 | 38, 1, 54, 11 | o2timesd 20033 |
. . . 4
β’ (π β (π + π) = (( 1 + 1 ) Β· π)) |
58 | 57 | eqcomd 2739 |
. . 3
β’ (π β (( 1 + 1 ) Β· π) = (π + π)) |
59 | 56, 58 | oveq12d 7427 |
. 2
β’ (π β ((( 1 + 1 ) Β· π) + (( 1 + 1 ) Β· π)) = ((π + π) + (π + π))) |
60 | | oveq2 7417 |
. . . . . 6
β’ (π₯ = (π + π) β ( 1 Β· π₯) = ( 1 Β· (π + π))) |
61 | | id 22 |
. . . . . 6
β’ (π₯ = (π + π) β π₯ = (π + π)) |
62 | 60, 61 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = (π + π) β (( 1 Β· π₯) = π₯ β ( 1 Β· (π + π)) = (π + π))) |
63 | 62 | rspcva 3611 |
. . . 4
β’ (((π + π) β π΅ β§ βπ₯ β π΅ ( 1 Β· π₯) = π₯) β ( 1 Β· (π + π)) = (π + π)) |
64 | 36, 54, 63 | syl2anc 585 |
. . 3
β’ (π β ( 1 Β· (π + π)) = (π + π)) |
65 | 64, 64 | oveq12d 7427 |
. 2
β’ (π β (( 1 Β· (π + π)) + ( 1 Β· (π + π))) = ((π + π) + (π + π))) |
66 | 53, 59, 65 | 3eqtr3d 2781 |
1
β’ (π β ((π + π) + (π + π)) = ((π + π) + (π + π))) |