Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΎ β HL) |
2 | | simp11 1204 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΎ β HL β§ π β π»)) |
3 | | simp12 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΉ β π β§ πΉ β ( I βΎ π΅))) |
4 | | simp13 1206 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β π β§ πΊ β ( I βΎ π΅))) |
5 | | simp21 1207 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β π β π) |
6 | | simp22 1208 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π β π΄ β§ Β¬ π β€ π)) |
7 | | simp23 1209 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΉ) = (π
βπ)) |
8 | | cdlemk5.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
9 | | cdlemk5.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
10 | | cdlemk5.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
11 | | cdlemk5.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
12 | | cdlemk5.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
13 | | cdlemk5.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
14 | | cdlemk5.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
15 | | cdlemk5.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
16 | | cdlemk5.z |
. . . . . 6
β’ π = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) |
17 | | cdlemk5.y |
. . . . . 6
β’ π = ((π β¨ (π
βπ)) β§ (π β¨ (π
β(π β β‘π)))) |
18 | | cdlemk5.x |
. . . . . 6
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπ)) β (π§βπ) = π)) |
19 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cdlemk35s 39446 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β β¦πΊ / πβ¦π β π) |
20 | 2, 3, 4, 5, 6, 7, 19 | syl132anc 1389 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β β¦πΊ / πβ¦π β π) |
21 | 9, 12, 13, 14 | ltrnel 38648 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ β¦πΊ / πβ¦π β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((β¦πΊ / πβ¦πβπ) β π΄ β§ Β¬ (β¦πΊ / πβ¦πβπ) β€ π)) |
22 | 2, 20, 6, 21 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦πβπ) β π΄ β§ Β¬ (β¦πΊ / πβ¦πβπ) β€ π)) |
23 | 22 | simpld 496 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦πΊ / πβ¦πβπ) β π΄) |
24 | | simp31 1210 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΌ β π) |
25 | | simp32 1211 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΌ β ( I βΎ π΅)) |
26 | 8, 12, 13, 14, 15 | trlnidat 38682 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΌ β π β§ πΌ β ( I βΎ π΅)) β (π
βπΌ) β π΄) |
27 | 2, 24, 25, 26 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΌ) β π΄) |
28 | 24, 25 | jca 513 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΌ β π β§ πΌ β ( I βΎ π΅))) |
29 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cdlemk35s 39446 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β β¦πΌ / πβ¦π β π) |
30 | 2, 3, 28, 5, 6, 7,
29 | syl132anc 1389 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β β¦πΌ / πβ¦π β π) |
31 | | simp22l 1293 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β π β π΄) |
32 | 9, 12, 13, 14 | ltrnat 38649 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ β¦πΌ / πβ¦π β π β§ π β π΄) β (β¦πΌ / πβ¦πβπ) β π΄) |
33 | 2, 30, 31, 32 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦πΌ / πβ¦πβπ) β π΄) |
34 | | simp13l 1289 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΊ β π) |
35 | | simp13r 1290 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β πΊ β ( I βΎ π΅)) |
36 | 8, 12, 13, 14, 15 | trlnidat 38682 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΊ β ( I βΎ π΅)) β (π
βπΊ) β π΄) |
37 | 2, 34, 35, 36 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΊ) β π΄) |
38 | 13, 14 | ltrnco 39228 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΌ β π) β (πΊ β πΌ) β π) |
39 | 2, 34, 24, 38 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β πΌ) β π) |
40 | 34, 24 | jca 513 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β π β§ πΌ β π)) |
41 | | simp33 1212 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΊ) β (π
βπΌ)) |
42 | 8, 13, 14, 15 | trlconid 39234 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ πΌ β π) β§ (π
βπΊ) β (π
βπΌ)) β (πΊ β πΌ) β ( I βΎ π΅)) |
43 | 2, 40, 41, 42 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΊ β πΌ) β ( I βΎ π΅)) |
44 | 39, 43 | jca 513 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((πΊ β πΌ) β π β§ (πΊ β πΌ) β ( I βΎ π΅))) |
45 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cdlemk35s 39446 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ ((πΊ β πΌ) β π β§ (πΊ β πΌ) β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ))) β β¦(πΊ β πΌ) / πβ¦π β π) |
46 | 2, 3, 44, 5, 6, 7,
45 | syl132anc 1389 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β β¦(πΊ β πΌ) / πβ¦π β π) |
47 | 9, 12, 13, 14 | ltrnat 38649 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ β¦(πΊ β πΌ) / πβ¦π β π β§ π β π΄) β (β¦(πΊ β πΌ) / πβ¦πβπ) β π΄) |
48 | 2, 46, 31, 47 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β π΄) |
49 | 24, 25, 43 | 3jca 1129 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) |
50 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cdlemk46 39457 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ))) |
51 | 49, 50 | syld3an3 1410 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ))) |
52 | 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18 | cdlemk45 39456 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) |
53 | 49, 52 | syld3an3 1410 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) |
54 | 9, 13, 14, 15 | trlle 38693 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΌ β π) β (π
βπΌ) β€ π) |
55 | 2, 24, 54 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΌ) β€ π) |
56 | 27, 55 | jca 513 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((π
βπΌ) β π΄ β§ (π
βπΌ) β€ π)) |
57 | 9, 13, 14, 15 | trlle 38693 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β€ π) |
58 | 2, 34, 57 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΊ) β€ π) |
59 | 37, 58 | jca 513 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((π
βπΊ) β π΄ β§ (π
βπΊ) β€ π)) |
60 | 41 | necomd 2996 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (π
βπΌ) β (π
βπΊ)) |
61 | 9, 10, 12, 13 | lhp2atne 38543 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ ((β¦πΊ / πβ¦πβπ) β π΄ β§ Β¬ (β¦πΊ / πβ¦πβπ) β€ π) β§ (β¦πΌ / πβ¦πβπ) β π΄) β§ (((π
βπΌ) β π΄ β§ (π
βπΌ) β€ π) β§ ((π
βπΊ) β π΄ β§ (π
βπΊ) β€ π)) β§ (π
βπΌ) β (π
βπΊ)) β ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) |
62 | 2, 22, 33, 56, 59, 60, 61 | syl321anc 1393 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ))) |
63 | 9, 10, 11, 12 | 2atm 38036 |
. 2
β’ (((πΎ β HL β§
(β¦πΊ / πβ¦πβπ) β π΄ β§ (π
βπΌ) β π΄) β§ ((β¦πΌ / πβ¦πβπ) β π΄ β§ (π
βπΊ) β π΄ β§ (β¦(πΊ β πΌ) / πβ¦πβπ) β π΄) β§ ((β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)) β§ ((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)))) β (β¦(πΊ β πΌ) / πβ¦πβπ) = (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)))) |
64 | 1, 23, 27, 33, 37, 48, 51, 53, 62, 63 | syl333anc 1403 |
1
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π
βπΊ) β (π
βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) = (((β¦πΊ / πβ¦πβπ) β¨ (π
βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π
βπΊ)))) |