Step | Hyp | Ref
| Expression |
1 | | hpgid.l |
. . . 4
β’ πΏ = (LineGβπΊ) |
2 | | hpgid.g |
. . . 4
β’ (π β πΊ β TarskiG) |
3 | | hpgid.d |
. . . 4
β’ (π β π· β ran πΏ) |
4 | 1, 2, 3 | tglnne0 27679 |
. . 3
β’ (π β π· β β
) |
5 | | n0 4326 |
. . 3
β’ (π· β β
β
βπ₯ π₯ β π·) |
6 | 4, 5 | sylib 217 |
. 2
β’ (π β βπ₯ π₯ β π·) |
7 | | hpgid.p |
. . . 4
β’ π = (BaseβπΊ) |
8 | | eqid 2731 |
. . . 4
β’
(distβπΊ) =
(distβπΊ) |
9 | | hpgid.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
10 | 2 | adantr 481 |
. . . 4
β’ ((π β§ π₯ β π·) β πΊ β TarskiG) |
11 | | hpgid.a |
. . . . 5
β’ (π β π΄ β π) |
12 | 11 | adantr 481 |
. . . 4
β’ ((π β§ π₯ β π·) β π΄ β π) |
13 | 3 | adantr 481 |
. . . . 5
β’ ((π β§ π₯ β π·) β π· β ran πΏ) |
14 | | simpr 485 |
. . . . 5
β’ ((π β§ π₯ β π·) β π₯ β π·) |
15 | 7, 1, 9, 10, 13, 14 | tglnpt 27588 |
. . . 4
β’ ((π β§ π₯ β π·) β π₯ β π) |
16 | 3 | adantr 481 |
. . . . . . 7
β’ ((π β§ (β―βπ) = 1) β π· β ran πΏ) |
17 | 2 | adantr 481 |
. . . . . . . 8
β’ ((π β§ (β―βπ) = 1) β πΊ β TarskiG) |
18 | | simpr 485 |
. . . . . . . 8
β’ ((π β§ (β―βπ) = 1) β
(β―βπ) =
1) |
19 | 7, 9, 1, 17, 18 | tglndim0 27668 |
. . . . . . 7
β’ ((π β§ (β―βπ) = 1) β Β¬ π· β ran πΏ) |
20 | 16, 19 | pm2.65da 815 |
. . . . . 6
β’ (π β Β¬ (β―βπ) = 1) |
21 | 7, 11 | tgldimor 27541 |
. . . . . . 7
β’ (π β ((β―βπ) = 1 β¨ 2 β€
(β―βπ))) |
22 | 21 | ord 862 |
. . . . . 6
β’ (π β (Β¬
(β―βπ) = 1
β 2 β€ (β―βπ))) |
23 | 20, 22 | mpd 15 |
. . . . 5
β’ (π β 2 β€
(β―βπ)) |
24 | 23 | adantr 481 |
. . . 4
β’ ((π β§ π₯ β π·) β 2 β€ (β―βπ)) |
25 | 7, 8, 9, 10, 12, 15, 24 | tgbtwndiff 27545 |
. . 3
β’ ((π β§ π₯ β π·) β βπ β π (π₯ β (π΄πΌπ) β§ π₯ β π)) |
26 | | hpgid.1 |
. . . . . . . . 9
β’ (π β Β¬ π΄ β π·) |
27 | 26 | ad4antr 730 |
. . . . . . . 8
β’
(((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β Β¬ π΄ β π·) |
28 | 10 | ad4antr 730 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β πΊ β TarskiG) |
29 | 15 | ad4antr 730 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π₯ β π) |
30 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π·) β§ π β π) β π β π) |
31 | 30 | ad3antrrr 728 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π β π) |
32 | 12 | ad4antr 730 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π΄ β π) |
33 | | simplr 767 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π₯ β π) |
34 | | simplr 767 |
. . . . . . . . . . . 12
β’
(((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β π₯ β (π΄πΌπ)) |
35 | 34 | adantr 481 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π₯ β (π΄πΌπ)) |
36 | 7, 9, 1, 28, 29, 31, 32, 33, 35 | btwnlng2 27659 |
. . . . . . . . . 10
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π΄ β (π₯πΏπ)) |
37 | 13 | ad4antr 730 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π· β ran πΏ) |
38 | 14 | ad4antr 730 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π₯ β π·) |
39 | | simpr 485 |
. . . . . . . . . . 11
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π β π·) |
40 | 7, 9, 1, 28, 29, 31, 33, 33, 37, 38, 39 | tglinethru 27675 |
. . . . . . . . . 10
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π· = (π₯πΏπ)) |
41 | 36, 40 | eleqtrrd 2835 |
. . . . . . . . 9
β’
((((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β§ π β π·) β π΄ β π·) |
42 | 27, 41 | mtand 814 |
. . . . . . . 8
β’
(((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β Β¬ π β π·) |
43 | | eleq1w 2815 |
. . . . . . . . . 10
β’ (π‘ = π₯ β (π‘ β (π΄πΌπ) β π₯ β (π΄πΌπ))) |
44 | 43 | rspcev 3595 |
. . . . . . . . 9
β’ ((π₯ β π· β§ π₯ β (π΄πΌπ)) β βπ‘ β π· π‘ β (π΄πΌπ)) |
45 | 44 | ad5ant24 759 |
. . . . . . . 8
β’
(((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β βπ‘ β π· π‘ β (π΄πΌπ)) |
46 | 27, 42, 45 | jca31 515 |
. . . . . . 7
β’
(((((π β§ π₯ β π·) β§ π β π) β§ π₯ β (π΄πΌπ)) β§ π₯ β π) β ((Β¬ π΄ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ))) |
47 | 46 | anasss 467 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π β π) β§ (π₯ β (π΄πΌπ) β§ π₯ β π)) β ((Β¬ π΄ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ))) |
48 | | hpgid.o |
. . . . . . . 8
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
49 | 12 | adantr 481 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β π) β π΄ β π) |
50 | 7, 8, 9, 48, 49, 30 | islnopp 27778 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β π) β (π΄ππ β ((Β¬ π΄ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ)))) |
51 | 50 | adantr 481 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π β π) β§ (π₯ β (π΄πΌπ) β§ π₯ β π)) β (π΄ππ β ((Β¬ π΄ β π· β§ Β¬ π β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ)))) |
52 | 47, 51 | mpbird 256 |
. . . . 5
β’ ((((π β§ π₯ β π·) β§ π β π) β§ (π₯ β (π΄πΌπ) β§ π₯ β π)) β π΄ππ) |
53 | 52 | ex 413 |
. . . 4
β’ (((π β§ π₯ β π·) β§ π β π) β ((π₯ β (π΄πΌπ) β§ π₯ β π) β π΄ππ)) |
54 | 53 | reximdva 3167 |
. . 3
β’ ((π β§ π₯ β π·) β (βπ β π (π₯ β (π΄πΌπ) β§ π₯ β π) β βπ β π π΄ππ)) |
55 | 25, 54 | mpd 15 |
. 2
β’ ((π β§ π₯ β π·) β βπ β π π΄ππ) |
56 | 6, 55 | exlimddv 1938 |
1
β’ (π β βπ β π π΄ππ) |