Metamath Proof Explorer


Theorem axsegcon

Description: Any segment A B can be extended to a point x such that B x is congruent to C D . Axiom A4 of Schwabhauser p. 11. (Contributed by Scott Fenton, 4-Jun-2013)

Ref Expression
Assertion axsegcon N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x B x Cgr C D

Proof

Step Hyp Ref Expression
1 axsegconlem1 A = B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
2 1 ex A = B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
3 simprll A B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A 𝔼 N
4 simprlr A B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N B 𝔼 N
5 simpl A B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B
6 simprr A B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N C 𝔼 N D 𝔼 N
7 eqid p = 1 N A p B p 2 = p = 1 N A p B p 2
8 eqid p = 1 N C p D p 2 = p = 1 N C p D p 2
9 eqid k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2
10 7 8 9 axsegconlem8 A 𝔼 N B 𝔼 N A B C 𝔼 N D 𝔼 N k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 𝔼 N
11 7 8 axsegconlem7 A 𝔼 N B 𝔼 N A B C 𝔼 N D 𝔼 N p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 0 1
12 7 8 9 axsegconlem10 A 𝔼 N B 𝔼 N A B C 𝔼 N D 𝔼 N i 1 N B i = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 A i + p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
13 7 8 9 axsegconlem9 A 𝔼 N B 𝔼 N A B C 𝔼 N D 𝔼 N i = 1 N B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2 = i = 1 N C i D i 2
14 fveq1 x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 x i = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
15 14 oveq2d x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 t x i = t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
16 15 oveq2d x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 1 t A i + t x i = 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
17 16 eqeq2d x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 B i = 1 t A i + t x i B i = 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
18 17 ralbidv x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 1 N B i = 1 t A i + t x i i 1 N B i = 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
19 14 oveq2d x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 B i x i = B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
20 19 oveq1d x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 B i x i 2 = B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2
21 20 sumeq2sdv x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i = 1 N B i x i 2 = i = 1 N B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2
22 21 eqeq1d x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i = 1 N B i x i 2 = i = 1 N C i D i 2 i = 1 N B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2 = i = 1 N C i D i 2
23 18 22 anbi12d x = k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2 i 1 N B i = 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i i = 1 N B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2 = i = 1 N C i D i 2
24 oveq2 t = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 1 t = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2
25 24 oveq1d t = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 1 t A i = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 A i
26 oveq1 t = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
27 25 26 oveq12d t = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 A i + p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
28 27 eqeq2d t = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 B i = 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i B i = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 A i + p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
29 28 ralbidv t = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 i 1 N B i = 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i i 1 N B i = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 A i + p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i
30 29 anbi1d t = p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 i 1 N B i = 1 t A i + t k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i i = 1 N B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2 = i = 1 N C i D i 2 i 1 N B i = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 A i + p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i i = 1 N B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2 = i = 1 N C i D i 2
31 23 30 rspc2ev k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 𝔼 N p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 0 1 i 1 N B i = 1 p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 A i + p = 1 N A p B p 2 p = 1 N A p B p 2 + p = 1 N C p D p 2 k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i i = 1 N B i k 1 N p = 1 N A p B p 2 + p = 1 N C p D p 2 B k p = 1 N C p D p 2 A k p = 1 N A p B p 2 i 2 = i = 1 N C i D i 2 x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
32 10 11 12 13 31 syl112anc A 𝔼 N B 𝔼 N A B C 𝔼 N D 𝔼 N x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
33 3 4 5 6 32 syl31anc A B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
34 33 ex A B A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
35 2 34 pm2.61ine A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
36 simpllr A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B 𝔼 N
37 simplll A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N A 𝔼 N
38 simpr A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N x 𝔼 N
39 brbtwn B 𝔼 N A 𝔼 N x 𝔼 N B Btwn A x t 0 1 i 1 N B i = 1 t A i + t x i
40 36 37 38 39 syl3anc A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x t 0 1 i 1 N B i = 1 t A i + t x i
41 simplrl A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N C 𝔼 N
42 simplrr A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N D 𝔼 N
43 brcgr B 𝔼 N x 𝔼 N C 𝔼 N D 𝔼 N B x Cgr C D i = 1 N B i x i 2 = i = 1 N C i D i 2
44 36 38 41 42 43 syl22anc A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B x Cgr C D i = 1 N B i x i 2 = i = 1 N C i D i 2
45 40 44 anbi12d A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x B x Cgr C D t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
46 r19.41v t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2 t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
47 45 46 bitr4di A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x B x Cgr C D t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
48 47 rexbidva A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x B x Cgr C D x 𝔼 N t 0 1 i 1 N B i = 1 t A i + t x i i = 1 N B i x i 2 = i = 1 N C i D i 2
49 35 48 mpbird A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x B x Cgr C D
50 49 3adant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x B x Cgr C D