| 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 480 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐺 ∈ TarskiG) |
| 6 | | tgbtwncgr.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 7 | 6 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐵 ∈ 𝑃) |
| 8 | | tgbtwncgr.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 9 | 8 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐷 ∈ 𝑃) |
| 10 | | tgifscgr.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐹 ∈ 𝑃) |
| 12 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) →
(♯‘𝑃) =
1) |
| 13 | | tgifscgr.h |
. . . 4
⊢ (𝜑 → 𝐻 ∈ 𝑃) |
| 14 | 13 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → 𝐻 ∈ 𝑃) |
| 15 | 1, 2, 3, 5, 7, 9, 11, 12, 14 | tgldim0cgr 28513 |
. 2
⊢ ((𝜑 ∧ (♯‘𝑃) = 1) → (𝐵 − 𝐷) = (𝐹 − 𝐻)) |
| 16 | | tgifscgr.6 |
. . . . 5
⊢ (𝜑 → (𝐶 − 𝐷) = (𝐾 − 𝐻)) |
| 17 | 16 | ad2antrr 726 |
. . . 4
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐶 − 𝐷) = (𝐾 − 𝐻)) |
| 18 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐺 ∈ TarskiG) |
| 19 | | tgbtwncgr.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 20 | 19 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐶 ∈ 𝑃) |
| 21 | 6 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵 ∈ 𝑃) |
| 22 | | tgifscgr.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 23 | 22 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 24 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐴 = 𝐶) |
| 25 | 24 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴𝐼𝐶) = (𝐶𝐼𝐶)) |
| 26 | 23, 25 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐵 ∈ (𝐶𝐼𝐶)) |
| 27 | 1, 2, 3, 18, 20, 21, 26 | axtgbtwnid 28474 |
. . . . 5
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐶 = 𝐵) |
| 28 | 27 | oveq1d 7446 |
. . . 4
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐶 − 𝐷) = (𝐵 − 𝐷)) |
| 29 | | tgifscgr.g |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ 𝑃) |
| 30 | 29 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐾 ∈ 𝑃) |
| 31 | 10 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹 ∈ 𝑃) |
| 32 | | tgifscgr.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐸𝐼𝐾)) |
| 33 | 32 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹 ∈ (𝐸𝐼𝐾)) |
| 34 | | tgifscgr.e |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐸 ∈ 𝑃) |
| 36 | | tgbtwncgr.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 37 | 36 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐴 ∈ 𝑃) |
| 38 | 24 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴 − 𝐴) = (𝐴 − 𝐶)) |
| 39 | | tgifscgr.3 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 𝐶) = (𝐸 − 𝐾)) |
| 40 | 39 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐴 − 𝐶) = (𝐸 − 𝐾)) |
| 41 | 38, 40 | eqtr2d 2778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐸 − 𝐾) = (𝐴 − 𝐴)) |
| 42 | 1, 2, 3, 18, 35, 30, 37, 41 | axtgcgrid 28471 |
. . . . . . . 8
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐸 = 𝐾) |
| 43 | 42 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐸𝐼𝐾) = (𝐾𝐼𝐾)) |
| 44 | 33, 43 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐹 ∈ (𝐾𝐼𝐾)) |
| 45 | 1, 2, 3, 18, 30, 31, 44 | axtgbtwnid 28474 |
. . . . 5
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → 𝐾 = 𝐹) |
| 46 | 45 | oveq1d 7446 |
. . . 4
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐾 − 𝐻) = (𝐹 − 𝐻)) |
| 47 | 17, 28, 46 | 3eqtr3d 2785 |
. . 3
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 = 𝐶) → (𝐵 − 𝐷) = (𝐹 − 𝐻)) |
| 48 | 4 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 ≠ 𝐶) → 𝐺 ∈ TarskiG) |
| 49 | 48 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) → 𝐺 ∈ TarskiG) |
| 50 | 49 | ad2antrr 726 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐺 ∈ TarskiG) |
| 51 | | simp-4r 784 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝑒 ∈ 𝑃) |
| 52 | 19 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 ≠ 𝐶) → 𝐶 ∈ 𝑃) |
| 53 | 52 | ad2antrr 726 |
. . . . . . 7
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) → 𝐶 ∈ 𝑃) |
| 54 | 53 | ad2antrr 726 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐶 ∈ 𝑃) |
| 55 | 6 | ad6antr 736 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐵 ∈ 𝑃) |
| 56 | | simplr 769 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝑓 ∈ 𝑃) |
| 57 | 29 | ad4antr 732 |
. . . . . . 7
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) → 𝐾 ∈ 𝑃) |
| 58 | 57 | ad2antrr 726 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐾 ∈ 𝑃) |
| 59 | 10 | ad6antr 736 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐹 ∈ 𝑃) |
| 60 | 8 | ad6antr 736 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐷 ∈ 𝑃) |
| 61 | 13 | ad6antr 736 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐻 ∈ 𝑃) |
| 62 | | simpllr 776 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) |
| 63 | 62 | simprd 495 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐶 ≠ 𝑒) |
| 64 | 63 | necomd 2996 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝑒 ≠ 𝐶) |
| 65 | 36 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 ≠ 𝐶) → 𝐴 ∈ 𝑃) |
| 66 | 65 | ad4antr 732 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐴 ∈ 𝑃) |
| 67 | 22 | ad6antr 736 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 68 | 62 | simpld 494 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐶 ∈ (𝐴𝐼𝑒)) |
| 69 | 1, 2, 3, 50, 66, 55, 54, 51, 67, 68 | tgbtwnexch3 28502 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐶 ∈ (𝐵𝐼𝑒)) |
| 70 | 1, 2, 3, 50, 55, 54, 51, 69 | tgbtwncom 28496 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐶 ∈ (𝑒𝐼𝐵)) |
| 71 | 34 | ad6antr 736 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐸 ∈ 𝑃) |
| 72 | 32 | ad6antr 736 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐹 ∈ (𝐸𝐼𝐾)) |
| 73 | | simprl 771 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐾 ∈ (𝐸𝐼𝑓)) |
| 74 | 1, 2, 3, 50, 71, 59, 58, 56, 72, 73 | tgbtwnexch3 28502 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐾 ∈ (𝐹𝐼𝑓)) |
| 75 | 1, 2, 3, 50, 59, 58, 56, 74 | tgbtwncom 28496 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐾 ∈ (𝑓𝐼𝐹)) |
| 76 | | simprr 773 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐾 − 𝑓) = (𝐶 − 𝑒)) |
| 77 | 76 | eqcomd 2743 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐶 − 𝑒) = (𝐾 − 𝑓)) |
| 78 | 1, 2, 3, 50, 54, 51, 58, 56, 77 | tgcgrcomlr 28488 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝑒 − 𝐶) = (𝑓 − 𝐾)) |
| 79 | | tgifscgr.4 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐶) = (𝐹 − 𝐾)) |
| 80 | 79 | ad6antr 736 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐵 − 𝐶) = (𝐹 − 𝐾)) |
| 81 | 1, 2, 3, 50, 55, 54, 59, 58, 80 | tgcgrcomlr 28488 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐶 − 𝐵) = (𝐾 − 𝐹)) |
| 82 | | simp-5r 786 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → 𝐴 ≠ 𝐶) |
| 83 | 39 | ad6antr 736 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐴 − 𝐶) = (𝐸 − 𝐾)) |
| 84 | | tgifscgr.5 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 𝐷) = (𝐸 − 𝐻)) |
| 85 | 84 | ad6antr 736 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐴 − 𝐷) = (𝐸 − 𝐻)) |
| 86 | 16 | ad6antr 736 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐶 − 𝐷) = (𝐾 − 𝐻)) |
| 87 | 1, 2, 3, 50, 66, 54, 51, 71, 58, 56, 60, 61, 82, 68, 73, 83, 77, 85, 86 | axtg5seg 28473 |
. . . . . 6
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝑒 − 𝐷) = (𝑓 − 𝐻)) |
| 88 | 1, 2, 3, 50, 51, 54, 55, 56, 58, 59, 60, 61, 64, 70, 75, 78, 81, 87, 86 | axtg5seg 28473 |
. . . . 5
⊢
(((((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) ∧ 𝑓 ∈ 𝑃) ∧ (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) → (𝐵 − 𝐷) = (𝐹 − 𝐻)) |
| 89 | 34 | ad4antr 732 |
. . . . . 6
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) → 𝐸 ∈ 𝑃) |
| 90 | | simplr 769 |
. . . . . 6
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) → 𝑒 ∈ 𝑃) |
| 91 | 1, 2, 3, 49, 89, 57, 53, 90 | axtgsegcon 28472 |
. . . . 5
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) → ∃𝑓 ∈ 𝑃 (𝐾 ∈ (𝐸𝐼𝑓) ∧ (𝐾 − 𝑓) = (𝐶 − 𝑒))) |
| 92 | 88, 91 | r19.29a 3162 |
. . . 4
⊢
(((((𝜑 ∧ 2 ≤
(♯‘𝑃)) ∧
𝐴 ≠ 𝐶) ∧ 𝑒 ∈ 𝑃) ∧ (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) → (𝐵 − 𝐷) = (𝐹 − 𝐻)) |
| 93 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 ≠ 𝐶) → 2 ≤ (♯‘𝑃)) |
| 94 | 1, 2, 3, 48, 65, 52, 93 | tgbtwndiff 28514 |
. . . 4
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 ≠ 𝐶) → ∃𝑒 ∈ 𝑃 (𝐶 ∈ (𝐴𝐼𝑒) ∧ 𝐶 ≠ 𝑒)) |
| 95 | 92, 94 | r19.29a 3162 |
. . 3
⊢ (((𝜑 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝐴 ≠ 𝐶) → (𝐵 − 𝐷) = (𝐹 − 𝐻)) |
| 96 | 47, 95 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ 2 ≤ (♯‘𝑃)) → (𝐵 − 𝐷) = (𝐹 − 𝐻)) |
| 97 | 1, 36 | tgldimor 28510 |
. 2
⊢ (𝜑 → ((♯‘𝑃) = 1 ∨ 2 ≤
(♯‘𝑃))) |
| 98 | 15, 96, 97 | mpjaodan 961 |
1
⊢ (𝜑 → (𝐵 − 𝐷) = (𝐹 − 𝐻)) |