Metamath Proof Explorer


Theorem btwnconn1lem14

Description: Lemma for btwnconn1 . Final statement of the theorem when B =/= C . (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1lem14 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B B C B Btwn A C B Btwn A D C Btwn A D D Btwn A C

Proof

Step Hyp Ref Expression
1 simp1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N N
2 simp2l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A 𝔼 N
3 simp3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N D 𝔼 N
4 simp3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N C 𝔼 N D 𝔼 N
5 axsegcon N A 𝔼 N D 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N D Btwn A c D c Cgr C D
6 1 2 3 4 5 syl121anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N D Btwn A c D c Cgr C D
7 simp3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N C 𝔼 N
8 axsegcon N A 𝔼 N C 𝔼 N C 𝔼 N D 𝔼 N d 𝔼 N C Btwn A d C d Cgr C D
9 1 2 7 4 8 syl121anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N d 𝔼 N C Btwn A d C d Cgr C D
10 reeanv c 𝔼 N d 𝔼 N D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c 𝔼 N D Btwn A c D c Cgr C D d 𝔼 N C Btwn A d C d Cgr C D
11 6 9 10 sylanbrc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D
12 11 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B B C B Btwn A C B Btwn A D c 𝔼 N d 𝔼 N D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D
13 simpl1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N N
14 simpl2l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A 𝔼 N
15 simprl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N c 𝔼 N
16 simpl3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N C 𝔼 N
17 simpl2r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N B 𝔼 N
18 axsegcon N A 𝔼 N c 𝔼 N C 𝔼 N B 𝔼 N b 𝔼 N c Btwn A b c b Cgr C B
19 13 14 15 16 17 18 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N c Btwn A b c b Cgr C B
20 simprr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N d 𝔼 N
21 simpl3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N D 𝔼 N
22 axsegcon N A 𝔼 N d 𝔼 N D 𝔼 N B 𝔼 N x 𝔼 N d Btwn A x d x Cgr D B
23 13 14 20 21 17 22 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N x 𝔼 N d Btwn A x d x Cgr D B
24 19 23 jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N c Btwn A b c b Cgr C B x 𝔼 N d Btwn A x d x Cgr D B
25 24 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D b 𝔼 N c Btwn A b c b Cgr C B x 𝔼 N d Btwn A x d x Cgr D B
26 reeanv b 𝔼 N x 𝔼 N c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B b 𝔼 N c Btwn A b c b Cgr C B x 𝔼 N d Btwn A x d x Cgr D B
27 25 26 sylibr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D b 𝔼 N x 𝔼 N c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B
28 13 14 17 3jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N N A 𝔼 N B 𝔼 N
29 28 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N N A 𝔼 N B 𝔼 N
30 16 21 15 3jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N
31 30 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N
32 simplrr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N d 𝔼 N
33 simprl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N b 𝔼 N
34 simprr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N x 𝔼 N
35 32 33 34 3jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N
36 29 31 35 3jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N
37 simpll A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B A B B C B Btwn A C B Btwn A D
38 simplr A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D
39 simpr A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B
40 37 38 39 3jca A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B
41 btwnconn1lem2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B x = b
42 36 40 41 syl2an N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B x = b
43 opeq2 x = b A x = A b
44 43 breq2d x = b d Btwn A x d Btwn A b
45 opeq2 x = b d x = d b
46 45 breq1d x = b d x Cgr D B d b Cgr D B
47 44 46 anbi12d x = b d Btwn A x d x Cgr D B d Btwn A b d b Cgr D B
48 47 anbi2d x = b c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B
49 48 anbi2d x = b A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B
50 49 biimpac A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B x = b A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B
51 32 33 jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N d 𝔼 N b 𝔼 N
52 29 31 51 jca32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N
53 simpll A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B A B B C B Btwn A C B Btwn A D
54 simplr A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D
55 simpr A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B
56 53 54 55 3jca A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B
57 btwnconn1lem13 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B C = c D = d
58 52 56 57 syl2an N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B C = c D = d
59 58 ex N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A b d b Cgr D B C = c D = d
60 50 59 syl5 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B x = b C = c D = d
61 60 expdimp N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B x = b C = c D = d
62 42 61 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N b 𝔼 N x 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B C = c D = d
63 62 an4s N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D b 𝔼 N x 𝔼 N c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B C = c D = d
64 63 exp32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D b 𝔼 N x 𝔼 N c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B C = c D = d
65 64 rexlimdvv N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D b 𝔼 N x 𝔼 N c Btwn A b c b Cgr C B d Btwn A x d x Cgr D B C = c D = d
66 27 65 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C = c D = d
67 orcom C = c D = d D = d C = c
68 simprrl A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C Btwn A d
69 68 adantl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C Btwn A d
70 opeq2 D = d A D = A d
71 70 breq2d D = d C Btwn A D C Btwn A d
72 69 71 syl5ibrcom N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D D = d C Btwn A D
73 simprll A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D D Btwn A c
74 73 adantl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D D Btwn A c
75 opeq2 C = c A C = A c
76 75 breq2d C = c D Btwn A C D Btwn A c
77 74 76 syl5ibrcom N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C = c D Btwn A C
78 72 77 orim12d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D D = d C = c C Btwn A D D Btwn A C
79 67 78 syl5bi N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C = c D = d C Btwn A D D Btwn A C
80 66 79 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N c 𝔼 N d 𝔼 N A B B C B Btwn A C B Btwn A D D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C Btwn A D D Btwn A C
81 80 an4s N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B B C B Btwn A C B Btwn A D c 𝔼 N d 𝔼 N D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C Btwn A D D Btwn A C
82 81 exp32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B B C B Btwn A C B Btwn A D c 𝔼 N d 𝔼 N D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C Btwn A D D Btwn A C
83 82 rexlimdvv N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B B C B Btwn A C B Btwn A D c 𝔼 N d 𝔼 N D Btwn A c D c Cgr C D C Btwn A d C d Cgr C D C Btwn A D D Btwn A C
84 12 83 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B B C B Btwn A C B Btwn A D C Btwn A D D Btwn A C