Metamath Proof Explorer

Theorem axsegconlem1

Description: Lemma for axsegcon . Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013)

Ref Expression
Assertion axsegconlem1 ⊢A=B∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢A⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2

Proof

Step Hyp Ref Expression
1 fveere ⊢B∈𝔼⁡N∧k∈1…N→B⁡k∈ℝ
2 1 3ad2antl1 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧k∈1…N→B⁡k∈ℝ
3 fveere ⊢C∈𝔼⁡N∧k∈1…N→C⁡k∈ℝ
4 3 3ad2antl2 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧k∈1…N→C⁡k∈ℝ
5 fveere ⊢D∈𝔼⁡N∧k∈1…N→D⁡k∈ℝ
6 5 3ad2antl3 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧k∈1…N→D⁡k∈ℝ
7 4 6 resubcld ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧k∈1…N→C⁡k−D⁡k∈ℝ
8 2 7 resubcld ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧k∈1…N→B⁡k−C⁡k−D⁡k∈ℝ
9 8 ralrimiva ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∀k∈1…NB⁡k−C⁡k−D⁡k∈ℝ
10 eleenn ⊢B∈𝔼⁡N→N∈ℕ
11 mptelee ⊢N∈ℕ→k∈1…N⟼B⁡k−C⁡k−D⁡k∈𝔼⁡N↔∀k∈1…NB⁡k−C⁡k−D⁡k∈ℝ
12 10 11 syl ⊢B∈𝔼⁡N→k∈1…N⟼B⁡k−C⁡k−D⁡k∈𝔼⁡N↔∀k∈1…NB⁡k−C⁡k−D⁡k∈ℝ
13 12 3ad2ant1 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→k∈1…N⟼B⁡k−C⁡k−D⁡k∈𝔼⁡N↔∀k∈1…NB⁡k−C⁡k−D⁡k∈ℝ
14 9 13 mpbird ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→k∈1…N⟼B⁡k−C⁡k−D⁡k∈𝔼⁡N
15 fveecn ⊢B∈𝔼⁡N∧i∈1…N→B⁡i∈ℂ
16 15 3ad2antl1 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i∈ℂ
17 fveecn ⊢C∈𝔼⁡N∧i∈1…N→C⁡i∈ℂ
18 17 3ad2antl2 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→C⁡i∈ℂ
19 fveecn ⊢D∈𝔼⁡N∧i∈1…N→D⁡i∈ℂ
20 19 3ad2antl3 ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→D⁡i∈ℂ
21 1m0e1 ⊢1−0=1
22 21 oveq1i ⊢1−0⁢B⁡i=1⁢B⁡i
23 mullid ⊢B⁡i∈ℂ→1⁢B⁡i=B⁡i
24 23 3ad2ant1 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→1⁢B⁡i=B⁡i
25 22 24 eqtrid ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→1−0⁢B⁡i=B⁡i
26 subcl ⊢C⁡i∈ℂ∧D⁡i∈ℂ→C⁡i−D⁡i∈ℂ
27 subcl ⊢B⁡i∈ℂ∧C⁡i−D⁡i∈ℂ→B⁡i−C⁡i−D⁡i∈ℂ
28 26 27 sylan2 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→B⁡i−C⁡i−D⁡i∈ℂ
29 28 3impb ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→B⁡i−C⁡i−D⁡i∈ℂ
30 29 mul02d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→0⋅B⁡i−C⁡i−D⁡i=0
31 25 30 oveq12d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i=B⁡i+0
32 addrid ⊢B⁡i∈ℂ→B⁡i+0=B⁡i
33 32 3ad2ant1 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→B⁡i+0=B⁡i
34 31 33 eqtr2d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧D⁡i∈ℂ→B⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i
35 16 18 20 34 syl3anc ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i
36 35 ralrimiva ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∀i∈1…NB⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i
37 18 20 subcld ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→C⁡i−D⁡i∈ℂ
38 16 37 nncand ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i−B⁡i−C⁡i−D⁡i=C⁡i−D⁡i
39 38 oveq1d ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧i∈1…N→B⁡i−B⁡i−C⁡i−D⁡i2=C⁡i−D⁡i2
40 39 sumeq2dv ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2
41 0elunit ⊢0∈01
42 fveq1 ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k→x⁡i=k∈1…N⟼B⁡k−C⁡k−D⁡k⁡i
43 fveq2 ⊢k=i→B⁡k=B⁡i
44 fveq2 ⊢k=i→C⁡k=C⁡i
45 fveq2 ⊢k=i→D⁡k=D⁡i
46 44 45 oveq12d ⊢k=i→C⁡k−D⁡k=C⁡i−D⁡i
47 43 46 oveq12d ⊢k=i→B⁡k−C⁡k−D⁡k=B⁡i−C⁡i−D⁡i
48 eqid ⊢k∈1…N⟼B⁡k−C⁡k−D⁡k=k∈1…N⟼B⁡k−C⁡k−D⁡k
49 ovex ⊢B⁡i−C⁡i−D⁡i∈V
50 47 48 49 fvmpt ⊢i∈1…N→k∈1…N⟼B⁡k−C⁡k−D⁡k⁡i=B⁡i−C⁡i−D⁡i
51 42 50 sylan9eq ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k∧i∈1…N→x⁡i=B⁡i−C⁡i−D⁡i
52 51 oveq2d ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k∧i∈1…N→t⁢x⁡i=t⁢B⁡i−C⁡i−D⁡i
53 52 oveq2d ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k∧i∈1…N→1−t⁢B⁡i+t⁢x⁡i=1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i
54 53 eqeq2d ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k∧i∈1…N→B⁡i=1−t⁢B⁡i+t⁢x⁡i↔B⁡i=1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i
55 54 ralbidva ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k→∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i↔∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i
56 51 oveq2d ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k∧i∈1…N→B⁡i−x⁡i=B⁡i−B⁡i−C⁡i−D⁡i
57 56 oveq1d ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k∧i∈1…N→B⁡i−x⁡i2=B⁡i−B⁡i−C⁡i−D⁡i2
58 57 sumeq2dv ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k→∑i=1NB⁡i−x⁡i2=∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2
59 58 eqeq1d ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k→∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2↔∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2
60 55 59 anbi12d ⊢x=k∈1…N⟼B⁡k−C⁡k−D⁡k→∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2↔∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i∧∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2
61 oveq2 ⊢t=0→1−t=1−0
62 61 oveq1d ⊢t=0→1−t⁢B⁡i=1−0⁢B⁡i
63 oveq1 ⊢t=0→t⁢B⁡i−C⁡i−D⁡i=0⋅B⁡i−C⁡i−D⁡i
64 62 63 oveq12d ⊢t=0→1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i
65 64 eqeq2d ⊢t=0→B⁡i=1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i↔B⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i
66 65 ralbidv ⊢t=0→∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i↔∀i∈1…NB⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i
67 66 anbi1d ⊢t=0→∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢B⁡i−C⁡i−D⁡i∧∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2↔∀i∈1…NB⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i∧∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2
68 60 67 rspc2ev ⊢k∈1…N⟼B⁡k−C⁡k−D⁡k∈𝔼⁡N∧0∈01∧∀i∈1…NB⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i∧∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
69 41 68 mp3an2 ⊢k∈1…N⟼B⁡k−C⁡k−D⁡k∈𝔼⁡N∧∀i∈1…NB⁡i=1−0⁢B⁡i+0⋅B⁡i−C⁡i−D⁡i∧∑i=1NB⁡i−B⁡i−C⁡i−D⁡i2=∑i=1NC⁡i−D⁡i2→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
70 14 36 40 69 syl12anc ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
71 70 3expb ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
72 71 adantll ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
73 fveq1 ⊢A=B→A⁡i=B⁡i
74 73 oveq2d ⊢A=B→1−t⁢A⁡i=1−t⁢B⁡i
75 74 oveq1d ⊢A=B→1−t⁢A⁡i+t⁢x⁡i=1−t⁢B⁡i+t⁢x⁡i
76 75 eqeq2d ⊢A=B→B⁡i=1−t⁢A⁡i+t⁢x⁡i↔B⁡i=1−t⁢B⁡i+t⁢x⁡i
77 76 ralbidv ⊢A=B→∀i∈1…NB⁡i=1−t⁢A⁡i+t⁢x⁡i↔∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i
78 77 anbi1d ⊢A=B→∀i∈1…NB⁡i=1−t⁢A⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2↔∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
79 78 2rexbidv ⊢A=B→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢A⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2↔∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢B⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
80 72 79 imbitrrid ⊢A=B→A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢A⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2
81 80 imp ⊢A=B∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N→∃x∈𝔼⁡N∃t∈01∀i∈1…NB⁡i=1−t⁢A⁡i+t⁢x⁡i∧∑i=1NB⁡i−x⁡i2=∑i=1NC⁡i−D⁡i2