Metamath Proof Explorer


Theorem axpasch

Description: The inner Pasch axiom. Take a triangle A C E , a point D on A C , and a point B extending C E . Then A E and D B intersect at some point x . Axiom A7 of Schwabhauser p. 12. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axpasch N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N D Btwn A C E Btwn B C x 𝔼 N x Btwn D B x Btwn E A

Proof

Step Hyp Ref Expression
1 axpaschlem t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s
2 1 3ad2ant3 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s
3 simp1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s q = 1 r 1 t
4 3 oveq1d q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s q A i = 1 r 1 t A i
5 4 eqcomd q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s 1 r 1 t A i = q A i
6 simp2 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s r = 1 q 1 s
7 6 oveq1d q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s r B i = 1 q 1 s B i
8 5 7 oveq12d q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s 1 r 1 t A i + r B i = q A i + 1 q 1 s B i
9 simp3 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s 1 r t = 1 q s
10 9 oveq1d q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s 1 r t C i = 1 q s C i
11 8 10 oveq12d q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s 1 r 1 t A i + r B i + 1 r t C i = q A i + 1 q 1 s B i + 1 q s C i
12 11 3ad2ant3 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s 1 r 1 t A i + r B i + 1 r t C i = q A i + 1 q 1 s B i + 1 q s C i
13 12 adantr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + r B i + 1 r t C i = q A i + 1 q 1 s B i + 1 q s C i
14 1re 1
15 simpl2l N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N r 0 1
16 elicc01 r 0 1 r 0 r r 1
17 16 simp1bi r 0 1 r
18 15 17 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N r
19 resubcl 1 r 1 r
20 14 18 19 sylancr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r
21 20 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r
22 simp13l N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s t 0 1
23 22 adantr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N t 0 1
24 elicc01 t 0 1 t 0 t t 1
25 24 simp1bi t 0 1 t
26 23 25 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N t
27 resubcl 1 t 1 t
28 14 26 27 sylancr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 t
29 simp121 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s A 𝔼 N
30 fveere A 𝔼 N i 1 N A i
31 29 30 sylan N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N A i
32 28 31 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 t A i
33 32 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 t A i
34 simp123 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s C 𝔼 N
35 fveere C 𝔼 N i 1 N C i
36 34 35 sylan N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N C i
37 26 36 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N t C i
38 37 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N t C i
39 21 33 38 adddid N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + t C i = 1 r 1 t A i + 1 r t C i
40 28 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 t
41 31 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N A i
42 21 40 41 mulassd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i = 1 r 1 t A i
43 26 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N t
44 fveecn C 𝔼 N i 1 N C i
45 34 44 sylan N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N C i
46 21 43 45 mulassd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r t C i = 1 r t C i
47 42 46 oveq12d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + 1 r t C i = 1 r 1 t A i + 1 r t C i
48 39 47 eqtr4d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + t C i = 1 r 1 t A i + 1 r t C i
49 48 oveq1d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + t C i + r B i = 1 r 1 t A i + 1 r t C i + r B i
50 20 28 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t
51 50 31 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i
52 51 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i
53 20 26 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r t
54 53 36 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r t C i
55 54 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r t C i
56 simp122 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s B 𝔼 N
57 fveere B 𝔼 N i 1 N B i
58 56 57 sylan N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N B i
59 18 58 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N r B i
60 59 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N r B i
61 52 55 60 add32d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + 1 r t C i + r B i = 1 r 1 t A i + r B i + 1 r t C i
62 49 61 eqtrd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + t C i + r B i = 1 r 1 t A i + r B i + 1 r t C i
63 simpl2r N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N q 0 1
64 elicc01 q 0 1 q 0 q q 1
65 64 simp1bi q 0 1 q
66 63 65 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N q
67 resubcl 1 q 1 q
68 14 66 67 sylancr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q
69 simp13r N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s s 0 1
70 69 adantr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N s 0 1
71 elicc01 s 0 1 s 0 s s 1
72 71 simp1bi s 0 1 s
73 70 72 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N s
74 resubcl 1 s 1 s
75 14 73 74 sylancr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 s
76 75 58 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 s B i
77 68 76 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q 1 s B i
78 77 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q 1 s B i
79 73 36 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N s C i
80 68 79 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q s C i
81 80 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q s C i
82 66 31 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N q A i
83 82 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N q A i
84 78 81 83 add32d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q 1 s B i + 1 q s C i + q A i = 1 q 1 s B i + q A i + 1 q s C i
85 68 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q
86 76 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 s B i
87 79 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N s C i
88 85 86 87 adddid N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q 1 s B i + s C i = 1 q 1 s B i + 1 q s C i
89 88 oveq1d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q 1 s B i + s C i + q A i = 1 q 1 s B i + 1 q s C i + q A i
90 75 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 s
91 58 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N B i
92 85 90 91 mulassd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q 1 s B i = 1 q 1 s B i
93 92 oveq2d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N q A i + 1 q 1 s B i = q A i + 1 q 1 s B i
94 83 78 93 comraddd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N q A i + 1 q 1 s B i = 1 q 1 s B i + q A i
95 73 recnd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N s
96 85 95 45 mulassd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q s C i = 1 q s C i
97 94 96 oveq12d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N q A i + 1 q 1 s B i + 1 q s C i = 1 q 1 s B i + q A i + 1 q s C i
98 84 89 97 3eqtr4d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 q 1 s B i + s C i + q A i = q A i + 1 q 1 s B i + 1 q s C i
99 13 62 98 3eqtr4d N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
100 99 ralrimiva N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
101 100 3expia N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
102 101 reximdvva N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 q = 1 r 1 t r = 1 q 1 s 1 r t = 1 q s r 0 1 q 0 1 i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
103 2 102 mpd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
104 simplrl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N r 0 1
105 104 17 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N r
106 14 105 19 sylancr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 r
107 simpl3l N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 t 0 1
108 107 adantr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N t 0 1
109 108 25 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N t
110 14 109 27 sylancr N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 t
111 simpl21 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 A 𝔼 N
112 fveere A 𝔼 N k 1 N A k
113 111 112 sylan N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N A k
114 110 113 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 t A k
115 simpl23 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 C 𝔼 N
116 fveere C 𝔼 N k 1 N C k
117 115 116 sylan N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N C k
118 109 117 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N t C k
119 114 118 readdcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 t A k + t C k
120 106 119 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 r 1 t A k + t C k
121 simpl22 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 B 𝔼 N
122 fveere B 𝔼 N k 1 N B k
123 121 122 sylan N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N B k
124 105 123 remulcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N r B k
125 120 124 readdcld N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 r 1 t A k + t C k + r B k
126 125 ralrimiva N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 r 1 t A k + t C k + r B k
127 126 anassrs N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 r 1 t A k + t C k + r B k
128 simpll1 N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 N
129 mptelee N k 1 N 1 r 1 t A k + t C k + r B k 𝔼 N k 1 N 1 r 1 t A k + t C k + r B k
130 128 129 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 r 1 t A k + t C k + r B k 𝔼 N k 1 N 1 r 1 t A k + t C k + r B k
131 127 130 mpbird N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 k 1 N 1 r 1 t A k + t C k + r B k 𝔼 N
132 fveq1 x = k 1 N 1 r 1 t A k + t C k + r B k x i = k 1 N 1 r 1 t A k + t C k + r B k i
133 fveq2 k = i A k = A i
134 133 oveq2d k = i 1 t A k = 1 t A i
135 fveq2 k = i C k = C i
136 135 oveq2d k = i t C k = t C i
137 134 136 oveq12d k = i 1 t A k + t C k = 1 t A i + t C i
138 137 oveq2d k = i 1 r 1 t A k + t C k = 1 r 1 t A i + t C i
139 fveq2 k = i B k = B i
140 139 oveq2d k = i r B k = r B i
141 138 140 oveq12d k = i 1 r 1 t A k + t C k + r B k = 1 r 1 t A i + t C i + r B i
142 eqid k 1 N 1 r 1 t A k + t C k + r B k = k 1 N 1 r 1 t A k + t C k + r B k
143 ovex 1 r 1 t A i + t C i + r B i V
144 141 142 143 fvmpt i 1 N k 1 N 1 r 1 t A k + t C k + r B k i = 1 r 1 t A i + t C i + r B i
145 132 144 sylan9eq x = k 1 N 1 r 1 t A k + t C k + r B k i 1 N x i = 1 r 1 t A i + t C i + r B i
146 145 eqeq1d x = k 1 N 1 r 1 t A k + t C k + r B k i 1 N x i = 1 r 1 t A i + t C i + r B i 1 r 1 t A i + t C i + r B i = 1 r 1 t A i + t C i + r B i
147 145 eqeq1d x = k 1 N 1 r 1 t A k + t C k + r B k i 1 N x i = 1 q 1 s B i + s C i + q A i 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
148 146 147 anbi12d x = k 1 N 1 r 1 t A k + t C k + r B k i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i 1 r 1 t A i + t C i + r B i = 1 r 1 t A i + t C i + r B i 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
149 eqid 1 r 1 t A i + t C i + r B i = 1 r 1 t A i + t C i + r B i
150 149 biantrur 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i 1 r 1 t A i + t C i + r B i = 1 r 1 t A i + t C i + r B i 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
151 148 150 bitr4di x = k 1 N 1 r 1 t A k + t C k + r B k i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
152 151 ralbidva x = k 1 N 1 r 1 t A k + t C k + r B k i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i
153 152 rspcev k 1 N 1 r 1 t A k + t C k + r B k 𝔼 N i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
154 153 ex k 1 N 1 r 1 t A k + t C k + r B k 𝔼 N i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
155 131 154 syl N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
156 155 reximdva N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i q 0 1 x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
157 156 reximdva N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 i 1 N 1 r 1 t A i + t C i + r B i = 1 q 1 s B i + s C i + q A i r 0 1 q 0 1 x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
158 103 157 mpd N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 r 0 1 q 0 1 x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
159 rexcom q 0 1 x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i x 𝔼 N q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
160 159 rexbii r 0 1 q 0 1 x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i r 0 1 x 𝔼 N q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
161 rexcom r 0 1 x 𝔼 N q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
162 160 161 bitri r 0 1 q 0 1 x 𝔼 N i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
163 158 162 sylib N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
164 oveq2 D i = 1 t A i + t C i 1 r D i = 1 r 1 t A i + t C i
165 164 oveq1d D i = 1 t A i + t C i 1 r D i + r B i = 1 r 1 t A i + t C i + r B i
166 165 eqeq2d D i = 1 t A i + t C i x i = 1 r D i + r B i x i = 1 r 1 t A i + t C i + r B i
167 oveq2 E i = 1 s B i + s C i 1 q E i = 1 q 1 s B i + s C i
168 167 oveq1d E i = 1 s B i + s C i 1 q E i + q A i = 1 q 1 s B i + s C i + q A i
169 168 eqeq2d E i = 1 s B i + s C i x i = 1 q E i + q A i x i = 1 q 1 s B i + s C i + q A i
170 166 169 bi2anan9 D i = 1 t A i + t C i E i = 1 s B i + s C i x i = 1 r D i + r B i x i = 1 q E i + q A i x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
171 170 ralimi i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
172 ralbi i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
173 171 172 syl i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
174 173 rexbidv i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
175 174 2rexbidv i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r 1 t A i + t C i + r B i x i = 1 q 1 s B i + s C i + q A i
176 163 175 syl5ibrcom N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i
177 176 3expia N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i
178 177 rexlimdvv N A 𝔼 N B 𝔼 N C 𝔼 N t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i
179 178 3adant3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i
180 simp3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N D 𝔼 N
181 simp21 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N A 𝔼 N
182 simp23 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N C 𝔼 N
183 brbtwn D 𝔼 N A 𝔼 N C 𝔼 N D Btwn A C t 0 1 i 1 N D i = 1 t A i + t C i
184 180 181 182 183 syl3anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N D Btwn A C t 0 1 i 1 N D i = 1 t A i + t C i
185 simp3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N E 𝔼 N
186 simp22 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N B 𝔼 N
187 brbtwn E 𝔼 N B 𝔼 N C 𝔼 N E Btwn B C s 0 1 i 1 N E i = 1 s B i + s C i
188 185 186 182 187 syl3anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N E Btwn B C s 0 1 i 1 N E i = 1 s B i + s C i
189 184 188 anbi12d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N D Btwn A C E Btwn B C t 0 1 i 1 N D i = 1 t A i + t C i s 0 1 i 1 N E i = 1 s B i + s C i
190 r19.26 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i i 1 N D i = 1 t A i + t C i i 1 N E i = 1 s B i + s C i
191 190 2rexbii t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i i 1 N E i = 1 s B i + s C i
192 reeanv t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i i 1 N E i = 1 s B i + s C i t 0 1 i 1 N D i = 1 t A i + t C i s 0 1 i 1 N E i = 1 s B i + s C i
193 191 192 bitri t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i t 0 1 i 1 N D i = 1 t A i + t C i s 0 1 i 1 N E i = 1 s B i + s C i
194 189 193 bitr4di N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N D Btwn A C E Btwn B C t 0 1 s 0 1 i 1 N D i = 1 t A i + t C i E i = 1 s B i + s C i
195 simpr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N x 𝔼 N
196 simpl3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N D 𝔼 N
197 simpl22 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N B 𝔼 N
198 brbtwn x 𝔼 N D 𝔼 N B 𝔼 N x Btwn D B r 0 1 i 1 N x i = 1 r D i + r B i
199 195 196 197 198 syl3anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N x Btwn D B r 0 1 i 1 N x i = 1 r D i + r B i
200 simpl3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N E 𝔼 N
201 simpl21 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N A 𝔼 N
202 brbtwn x 𝔼 N E 𝔼 N A 𝔼 N x Btwn E A q 0 1 i 1 N x i = 1 q E i + q A i
203 195 200 201 202 syl3anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N x Btwn E A q 0 1 i 1 N x i = 1 q E i + q A i
204 199 203 anbi12d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N x Btwn D B x Btwn E A r 0 1 i 1 N x i = 1 r D i + r B i q 0 1 i 1 N x i = 1 q E i + q A i
205 r19.26 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i i 1 N x i = 1 r D i + r B i i 1 N x i = 1 q E i + q A i
206 205 2rexbii r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i i 1 N x i = 1 q E i + q A i
207 reeanv r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i i 1 N x i = 1 q E i + q A i r 0 1 i 1 N x i = 1 r D i + r B i q 0 1 i 1 N x i = 1 q E i + q A i
208 206 207 bitri r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i r 0 1 i 1 N x i = 1 r D i + r B i q 0 1 i 1 N x i = 1 q E i + q A i
209 204 208 bitr4di N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N x Btwn D B x Btwn E A r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i
210 209 rexbidva N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N x 𝔼 N x Btwn D B x Btwn E A x 𝔼 N r 0 1 q 0 1 i 1 N x i = 1 r D i + r B i x i = 1 q E i + q A i
211 179 194 210 3imtr4d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N D Btwn A C E Btwn B C x 𝔼 N x Btwn D B x Btwn E A