Step | Hyp | Ref
| Expression |
1 | | tgbtwncgr.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | tgbtwncgr.m |
. . 3
β’ β =
(distβπΊ) |
3 | | tgbtwncgr.i |
. . 3
β’ πΌ = (ItvβπΊ) |
4 | | tgbtwncgr.g |
. . . 4
β’ (π β πΊ β TarskiG) |
5 | 4 | adantr 482 |
. . 3
β’ ((π β§ (β―βπ) = 1) β πΊ β TarskiG) |
6 | | tgbtwncgr.b |
. . . 4
β’ (π β π΅ β π) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β§ (β―βπ) = 1) β π΅ β π) |
8 | | tgbtwncgr.d |
. . . 4
β’ (π β π· β π) |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ (β―βπ) = 1) β π· β π) |
10 | | tgifscgr.f |
. . . 4
β’ (π β πΉ β π) |
11 | 10 | adantr 482 |
. . 3
β’ ((π β§ (β―βπ) = 1) β πΉ β π) |
12 | | simpr 486 |
. . 3
β’ ((π β§ (β―βπ) = 1) β
(β―βπ) =
1) |
13 | | tgifscgr.h |
. . . 4
β’ (π β π» β π) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ (β―βπ) = 1) β π» β π) |
15 | 1, 2, 3, 5, 7, 9, 11, 12, 14 | tgldim0cgr 27756 |
. 2
β’ ((π β§ (β―βπ) = 1) β (π΅ β π·) = (πΉ β π»)) |
16 | | tgifscgr.6 |
. . . . 5
β’ (π β (πΆ β π·) = (πΎ β π»)) |
17 | 16 | ad2antrr 725 |
. . . 4
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (πΆ β π·) = (πΎ β π»)) |
18 | 4 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΊ β TarskiG) |
19 | | tgbtwncgr.c |
. . . . . . 7
β’ (π β πΆ β π) |
20 | 19 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΆ β π) |
21 | 6 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β π΅ β π) |
22 | | tgifscgr.1 |
. . . . . . . 8
β’ (π β π΅ β (π΄πΌπΆ)) |
23 | 22 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β π΅ β (π΄πΌπΆ)) |
24 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β π΄ = πΆ) |
25 | 24 | oveq1d 7424 |
. . . . . . 7
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (π΄πΌπΆ) = (πΆπΌπΆ)) |
26 | 23, 25 | eleqtrd 2836 |
. . . . . 6
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β π΅ β (πΆπΌπΆ)) |
27 | 1, 2, 3, 18, 20, 21, 26 | axtgbtwnid 27717 |
. . . . 5
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΆ = π΅) |
28 | 27 | oveq1d 7424 |
. . . 4
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (πΆ β π·) = (π΅ β π·)) |
29 | | tgifscgr.g |
. . . . . . 7
β’ (π β πΎ β π) |
30 | 29 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΎ β π) |
31 | 10 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΉ β π) |
32 | | tgifscgr.2 |
. . . . . . . 8
β’ (π β πΉ β (πΈπΌπΎ)) |
33 | 32 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΉ β (πΈπΌπΎ)) |
34 | | tgifscgr.e |
. . . . . . . . . 10
β’ (π β πΈ β π) |
35 | 34 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΈ β π) |
36 | | tgbtwncgr.a |
. . . . . . . . . 10
β’ (π β π΄ β π) |
37 | 36 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β π΄ β π) |
38 | 24 | oveq2d 7425 |
. . . . . . . . . 10
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (π΄ β π΄) = (π΄ β πΆ)) |
39 | | tgifscgr.3 |
. . . . . . . . . . 11
β’ (π β (π΄ β πΆ) = (πΈ β πΎ)) |
40 | 39 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (π΄ β πΆ) = (πΈ β πΎ)) |
41 | 38, 40 | eqtr2d 2774 |
. . . . . . . . 9
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (πΈ β πΎ) = (π΄ β π΄)) |
42 | 1, 2, 3, 18, 35, 30, 37, 41 | axtgcgrid 27714 |
. . . . . . . 8
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΈ = πΎ) |
43 | 42 | oveq1d 7424 |
. . . . . . 7
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (πΈπΌπΎ) = (πΎπΌπΎ)) |
44 | 33, 43 | eleqtrd 2836 |
. . . . . 6
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΉ β (πΎπΌπΎ)) |
45 | 1, 2, 3, 18, 30, 31, 44 | axtgbtwnid 27717 |
. . . . 5
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β πΎ = πΉ) |
46 | 45 | oveq1d 7424 |
. . . 4
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (πΎ β π») = (πΉ β π»)) |
47 | 17, 28, 46 | 3eqtr3d 2781 |
. . 3
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ = πΆ) β (π΅ β π·) = (πΉ β π»)) |
48 | 4 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ β πΆ) β πΊ β TarskiG) |
49 | 48 | ad2antrr 725 |
. . . . . . 7
β’
(((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β πΊ β TarskiG) |
50 | 49 | ad2antrr 725 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΊ β TarskiG) |
51 | | simp-4r 783 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π β π) |
52 | 19 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ β πΆ) β πΆ β π) |
53 | 52 | ad2antrr 725 |
. . . . . . 7
β’
(((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β πΆ β π) |
54 | 53 | ad2antrr 725 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΆ β π) |
55 | 6 | ad6antr 735 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π΅ β π) |
56 | | simplr 768 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π β π) |
57 | 29 | ad4antr 731 |
. . . . . . 7
β’
(((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β πΎ β π) |
58 | 57 | ad2antrr 725 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΎ β π) |
59 | 10 | ad6antr 735 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΉ β π) |
60 | 8 | ad6antr 735 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π· β π) |
61 | 13 | ad6antr 735 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π» β π) |
62 | | simpllr 775 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (πΆ β (π΄πΌπ) β§ πΆ β π)) |
63 | 62 | simprd 497 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΆ β π) |
64 | 63 | necomd 2997 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π β πΆ) |
65 | 36 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ β πΆ) β π΄ β π) |
66 | 65 | ad4antr 731 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π΄ β π) |
67 | 22 | ad6antr 735 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π΅ β (π΄πΌπΆ)) |
68 | 62 | simpld 496 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΆ β (π΄πΌπ)) |
69 | 1, 2, 3, 50, 66, 55, 54, 51, 67, 68 | tgbtwnexch3 27745 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΆ β (π΅πΌπ)) |
70 | 1, 2, 3, 50, 55, 54, 51, 69 | tgbtwncom 27739 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΆ β (ππΌπ΅)) |
71 | 34 | ad6antr 735 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΈ β π) |
72 | 32 | ad6antr 735 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΉ β (πΈπΌπΎ)) |
73 | | simprl 770 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΎ β (πΈπΌπ)) |
74 | 1, 2, 3, 50, 71, 59, 58, 56, 72, 73 | tgbtwnexch3 27745 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΎ β (πΉπΌπ)) |
75 | 1, 2, 3, 50, 59, 58, 56, 74 | tgbtwncom 27739 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β πΎ β (ππΌπΉ)) |
76 | | simprr 772 |
. . . . . . . 8
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (πΎ β π) = (πΆ β π)) |
77 | 76 | eqcomd 2739 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (πΆ β π) = (πΎ β π)) |
78 | 1, 2, 3, 50, 54, 51, 58, 56, 77 | tgcgrcomlr 27731 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (π β πΆ) = (π β πΎ)) |
79 | | tgifscgr.4 |
. . . . . . . 8
β’ (π β (π΅ β πΆ) = (πΉ β πΎ)) |
80 | 79 | ad6antr 735 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (π΅ β πΆ) = (πΉ β πΎ)) |
81 | 1, 2, 3, 50, 55, 54, 59, 58, 80 | tgcgrcomlr 27731 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (πΆ β π΅) = (πΎ β πΉ)) |
82 | | simp-5r 785 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β π΄ β πΆ) |
83 | 39 | ad6antr 735 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (π΄ β πΆ) = (πΈ β πΎ)) |
84 | | tgifscgr.5 |
. . . . . . . 8
β’ (π β (π΄ β π·) = (πΈ β π»)) |
85 | 84 | ad6antr 735 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (π΄ β π·) = (πΈ β π»)) |
86 | 16 | ad6antr 735 |
. . . . . . 7
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (πΆ β π·) = (πΎ β π»)) |
87 | 1, 2, 3, 50, 66, 54, 51, 71, 58, 56, 60, 61, 82, 68, 73, 83, 77, 85, 86 | axtg5seg 27716 |
. . . . . 6
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (π β π·) = (π β π»)) |
88 | 1, 2, 3, 50, 51, 54, 55, 56, 58, 59, 60, 61, 64, 70, 75, 78, 81, 87, 86 | axtg5seg 27716 |
. . . . 5
β’
(((((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β§ π β π) β§ (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) β (π΅ β π·) = (πΉ β π»)) |
89 | 34 | ad4antr 731 |
. . . . . 6
β’
(((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β πΈ β π) |
90 | | simplr 768 |
. . . . . 6
β’
(((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β π β π) |
91 | 1, 2, 3, 49, 89, 57, 53, 90 | axtgsegcon 27715 |
. . . . 5
β’
(((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β βπ β π (πΎ β (πΈπΌπ) β§ (πΎ β π) = (πΆ β π))) |
92 | 88, 91 | r19.29a 3163 |
. . . 4
β’
(((((π β§ 2 β€
(β―βπ)) β§
π΄ β πΆ) β§ π β π) β§ (πΆ β (π΄πΌπ) β§ πΆ β π)) β (π΅ β π·) = (πΉ β π»)) |
93 | | simplr 768 |
. . . . 5
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ β πΆ) β 2 β€ (β―βπ)) |
94 | 1, 2, 3, 48, 65, 52, 93 | tgbtwndiff 27757 |
. . . 4
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ β πΆ) β βπ β π (πΆ β (π΄πΌπ) β§ πΆ β π)) |
95 | 92, 94 | r19.29a 3163 |
. . 3
β’ (((π β§ 2 β€ (β―βπ)) β§ π΄ β πΆ) β (π΅ β π·) = (πΉ β π»)) |
96 | 47, 95 | pm2.61dane 3030 |
. 2
β’ ((π β§ 2 β€ (β―βπ)) β (π΅ β π·) = (πΉ β π»)) |
97 | 1, 36 | tgldimor 27753 |
. 2
β’ (π β ((β―βπ) = 1 β¨ 2 β€
(β―βπ))) |
98 | 15, 96, 97 | mpjaodan 958 |
1
β’ (π β (π΅ β π·) = (πΉ β π»)) |