Step | Hyp | Ref
| Expression |
1 | | tglngval.p |
. . . . 5
β’ π = (BaseβπΊ) |
2 | | lnxfr.d |
. . . . 5
β’ β =
(distβπΊ) |
3 | | tglngval.i |
. . . . 5
β’ πΌ = (ItvβπΊ) |
4 | | tglngval.g |
. . . . 5
β’ (π β πΊ β TarskiG) |
5 | | lnxfr.a |
. . . . 5
β’ (π β π΄ β π) |
6 | | lnxfr.b |
. . . . 5
β’ (π β π΅ β π) |
7 | | tglngval.y |
. . . . 5
β’ (π β π β π) |
8 | | tgcolg.z |
. . . . 5
β’ (π β π β π) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | axtgsegcon 27695 |
. . . 4
β’ (π β βπ β π (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) |
10 | 9 | adantr 482 |
. . 3
β’ ((π β§ π β (ππΌπ)) β βπ β π (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) |
11 | | lnxfr.r |
. . . . . 6
β’ βΌ =
(cgrGβπΊ) |
12 | 4 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β πΊ β TarskiG) |
13 | | tglngval.x |
. . . . . . 7
β’ (π β π β π) |
14 | 13 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π β π) |
15 | 7 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π β π) |
16 | 8 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π β π) |
17 | 5 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π΄ β π) |
18 | 6 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π΅ β π) |
19 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π β π) |
20 | | lnext.2 |
. . . . . . 7
β’ (π β (π β π) = (π΄ β π΅)) |
21 | 20 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β (π β π) = (π΄ β π΅)) |
22 | | simprr 772 |
. . . . . . 7
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β (π΅ β π) = (π β π)) |
23 | 22 | eqcomd 2739 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β (π β π) = (π΅ β π)) |
24 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π β (ππΌπ)) |
25 | | simprl 770 |
. . . . . . . 8
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β π΅ β (π΄πΌπ)) |
26 | 1, 2, 3, 12, 14, 15, 16, 17, 18, 19, 24, 25, 21, 23 | tgcgrextend 27716 |
. . . . . . 7
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β (π β π) = (π΄ β π)) |
27 | 1, 2, 3, 12, 14, 16, 17, 19, 26 | tgcgrcomlr 27711 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β (π β π) = (π β π΄)) |
28 | 1, 2, 11, 12, 14, 15, 16, 17, 18, 19, 21, 23, 27 | trgcgr 27747 |
. . . . 5
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π))) β β¨βπππββ© βΌ β¨βπ΄π΅πββ©) |
29 | 28 | ex 414 |
. . . 4
β’ (((π β§ π β (ππΌπ)) β§ π β π) β ((π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π)) β β¨βπππββ© βΌ β¨βπ΄π΅πββ©)) |
30 | 29 | reximdva 3169 |
. . 3
β’ ((π β§ π β (ππΌπ)) β (βπ β π (π΅ β (π΄πΌπ) β§ (π΅ β π) = (π β π)) β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©)) |
31 | 10, 30 | mpd 15 |
. 2
β’ ((π β§ π β (ππΌπ)) β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©) |
32 | 1, 2, 3, 4, 6, 5, 13, 8 | axtgsegcon 27695 |
. . . 4
β’ (π β βπ β π (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) |
33 | 32 | adantr 482 |
. . 3
β’ ((π β§ π β (ππΌπ)) β βπ β π (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) |
34 | 4 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β πΊ β TarskiG) |
35 | 13 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π β π) |
36 | 7 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π β π) |
37 | 8 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π β π) |
38 | 5 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π΄ β π) |
39 | 6 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π΅ β π) |
40 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π β π) |
41 | 20 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β (π β π) = (π΄ β π΅)) |
42 | | simpllr 775 |
. . . . . . 7
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π β (ππΌπ)) |
43 | | simprl 770 |
. . . . . . 7
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β π΄ β (π΅πΌπ)) |
44 | 1, 2, 3, 34, 35, 36, 38, 39, 41 | tgcgrcomlr 27711 |
. . . . . . 7
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β (π β π) = (π΅ β π΄)) |
45 | | simprr 772 |
. . . . . . . 8
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β (π΄ β π) = (π β π)) |
46 | 45 | eqcomd 2739 |
. . . . . . 7
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β (π β π) = (π΄ β π)) |
47 | 1, 2, 3, 34, 36, 35, 37, 39, 38, 40, 42, 43, 44, 46 | tgcgrextend 27716 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β (π β π) = (π΅ β π)) |
48 | 1, 2, 3, 34, 35, 37, 38, 40, 46 | tgcgrcomlr 27711 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β (π β π) = (π β π΄)) |
49 | 1, 2, 11, 34, 35, 36, 37, 38, 39, 40, 41, 47, 48 | trgcgr 27747 |
. . . . 5
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π))) β β¨βπππββ© βΌ β¨βπ΄π΅πββ©) |
50 | 49 | ex 414 |
. . . 4
β’ (((π β§ π β (ππΌπ)) β§ π β π) β ((π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π)) β β¨βπππββ© βΌ β¨βπ΄π΅πββ©)) |
51 | 50 | reximdva 3169 |
. . 3
β’ ((π β§ π β (ππΌπ)) β (βπ β π (π΄ β (π΅πΌπ) β§ (π΄ β π) = (π β π)) β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©)) |
52 | 33, 51 | mpd 15 |
. 2
β’ ((π β§ π β (ππΌπ)) β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©) |
53 | 4 | adantr 482 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β πΊ β TarskiG) |
54 | 13 | adantr 482 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β π β π) |
55 | 8 | adantr 482 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β π β π) |
56 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β π β π) |
57 | 5 | adantr 482 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β π΄ β π) |
58 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β π΅ β π) |
59 | | simpr 486 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β π β (ππΌπ)) |
60 | 20 | adantr 482 |
. . . 4
β’ ((π β§ π β (ππΌπ)) β (π β π) = (π΄ β π΅)) |
61 | 1, 2, 3, 11, 53, 54, 55, 56, 57, 58, 59, 60 | tgcgrxfr 27749 |
. . 3
β’ ((π β§ π β (ππΌπ)) β βπ β π (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) |
62 | 4 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β πΊ β TarskiG) |
63 | 13 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β π β π) |
64 | 8 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β π β π) |
65 | 7 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β π β π) |
66 | 5 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β π΄ β π) |
67 | | simplr 768 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β π β π) |
68 | 6 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β π΅ β π) |
69 | | simprr 772 |
. . . . . 6
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©) |
70 | 1, 2, 3, 11, 62, 63, 64, 65, 66, 67, 68, 69 | cgr3swap23 27755 |
. . . . 5
β’ ((((π β§ π β (ππΌπ)) β§ π β π) β§ (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©)) β β¨βπππββ© βΌ β¨βπ΄π΅πββ©) |
71 | 70 | ex 414 |
. . . 4
β’ (((π β§ π β (ππΌπ)) β§ π β π) β ((π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©) β β¨βπππββ© βΌ β¨βπ΄π΅πββ©)) |
72 | 71 | reximdva 3169 |
. . 3
β’ ((π β§ π β (ππΌπ)) β (βπ β π (π β (π΄πΌπ΅) β§ β¨βπππββ© βΌ β¨βπ΄ππ΅ββ©) β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©)) |
73 | 61, 72 | mpd 15 |
. 2
β’ ((π β§ π β (ππΌπ)) β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©) |
74 | | lnext.1 |
. . 3
β’ (π β (π β (ππΏπ) β¨ π = π)) |
75 | | tglngval.l |
. . . 4
β’ πΏ = (LineGβπΊ) |
76 | 1, 75, 3, 4, 13, 8,
7 | tgcolg 27785 |
. . 3
β’ (π β ((π β (ππΏπ) β¨ π = π) β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ)))) |
77 | 74, 76 | mpbid 231 |
. 2
β’ (π β (π β (ππΌπ) β¨ π β (ππΌπ) β¨ π β (ππΌπ))) |
78 | 31, 52, 73, 77 | mpjao3dan 1432 |
1
β’ (π β βπ β π β¨βπππββ© βΌ β¨βπ΄π΅πββ©) |