Metamath Proof Explorer


Theorem ax5seglem6

Description: Lemma for ax5seg . Given two line segments that are divided into pieces, if the pieces are congruent, then the scaling constant is the same. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion ax5seglem6 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T = S

Proof

Step Hyp Ref Expression
1 simp22l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 0 1
2 elicc01 T 0 1 T 0 T T 1
3 2 simp1bi T 0 1 T
4 resqcl T T 2
5 4 recnd T T 2
6 1 3 5 3syl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 2
7 simp22r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F S 0 1
8 elicc01 S 0 1 S 0 S S 1
9 8 simp1bi S 0 1 S
10 resqcl S S 2
11 10 recnd S S 2
12 7 9 11 3syl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F S 2
13 fzfid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F 1 N Fin
14 simprl1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A 𝔼 N
15 14 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F A 𝔼 N
16 fveecn A 𝔼 N j 1 N A j
17 15 16 sylan N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j 1 N A j
18 simprl3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N C 𝔼 N
19 18 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F C 𝔼 N
20 fveecn C 𝔼 N j 1 N C j
21 19 20 sylan N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j 1 N C j
22 17 21 subcld N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j 1 N A j C j
23 22 sqcld N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j 1 N A j C j 2
24 13 23 fsumcl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j = 1 N A j C j 2
25 simp1l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F N
26 simp1rl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F A 𝔼 N B 𝔼 N C 𝔼 N
27 simp21 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F A B
28 simp23l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F i 1 N B i = 1 T A i + T C i
29 ax5seglem5 N A 𝔼 N B 𝔼 N C 𝔼 N A B T 0 1 i 1 N B i = 1 T A i + T C i j = 1 N A j C j 2 0
30 25 26 27 1 28 29 syl23anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j = 1 N A j C j 2 0
31 simp3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F A B Cgr D E
32 simprl2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N B 𝔼 N
33 simprr1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N
34 simprr2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N E 𝔼 N
35 brcgr A 𝔼 N B 𝔼 N D 𝔼 N E 𝔼 N A B Cgr D E j = 1 N A j B j 2 = j = 1 N D j E j 2
36 14 32 33 34 35 syl22anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Cgr D E j = 1 N A j B j 2 = j = 1 N D j E j 2
37 36 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F A B Cgr D E j = 1 N A j B j 2 = j = 1 N D j E j 2
38 31 37 mpbid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j = 1 N A j B j 2 = j = 1 N D j E j 2
39 ax5seglem1 N A 𝔼 N C 𝔼 N T 0 1 i 1 N B i = 1 T A i + T C i j = 1 N A j B j 2 = T 2 j = 1 N A j C j 2
40 25 15 19 1 28 39 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j = 1 N A j B j 2 = T 2 j = 1 N A j C j 2
41 33 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F D 𝔼 N
42 simprr3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N F 𝔼 N
43 42 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F F 𝔼 N
44 simp23r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F i 1 N E i = 1 S D i + S F i
45 ax5seglem1 N D 𝔼 N F 𝔼 N S 0 1 i 1 N E i = 1 S D i + S F i j = 1 N D j E j 2 = S 2 j = 1 N D j F j 2
46 25 41 43 7 44 45 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j = 1 N D j E j 2 = S 2 j = 1 N D j F j 2
47 38 40 46 3eqtr3d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 2 j = 1 N A j C j 2 = S 2 j = 1 N D j F j 2
48 simp1rr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F D 𝔼 N E 𝔼 N F 𝔼 N
49 simp22 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 0 1 S 0 1
50 simp23 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i
51 simp3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F B C Cgr E F
52 ax5seglem3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j = 1 N A j C j 2 = j = 1 N D j F j 2
53 25 26 48 49 50 31 51 52 syl322anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F j = 1 N A j C j 2 = j = 1 N D j F j 2
54 53 oveq2d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F S 2 j = 1 N A j C j 2 = S 2 j = 1 N D j F j 2
55 47 54 eqtr4d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 2 j = 1 N A j C j 2 = S 2 j = 1 N A j C j 2
56 6 12 24 30 55 mulcan2ad N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 2 = S 2
57 2 simp2bi T 0 1 0 T
58 3 57 jca T 0 1 T 0 T
59 1 58 syl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 0 T
60 8 simp2bi S 0 1 0 S
61 9 60 jca S 0 1 S 0 S
62 7 61 syl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F S 0 S
63 sq11 T 0 T S 0 S T 2 = S 2 T = S
64 59 62 63 syl2anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T 2 = S 2 T = S
65 56 64 mpbid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B T 0 1 S 0 1 i 1 N B i = 1 T A i + T C i i 1 N E i = 1 S D i + S F i A B Cgr D E B C Cgr E F T = S