Metamath Proof Explorer

Theorem brbtwn2

Description: Alternate characterization of betweenness, with no existential quantifiers. (Contributed by Scott Fenton, 24-Jun-2013)

Ref Expression
Assertion brbtwn2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i

Proof

Step Hyp Ref Expression
1 brbtwn ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
2 fveere ⊢B∈𝔼⁡N∧i∈1…N→B⁡i∈ℝ
3 2 3ad2antl2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→B⁡i∈ℝ
4 fveere ⊢C∈𝔼⁡N∧i∈1…N→C⁡i∈ℝ
5 4 3ad2antl3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→C⁡i∈ℝ
6 3 5 jca ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→B⁡i∈ℝ∧C⁡i∈ℝ
7 resubcl ⊢B⁡i∈ℝ∧C⁡i∈ℝ→B⁡i−C⁡i∈ℝ
8 7 3adant3 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−C⁡i∈ℝ
9 8 recnd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−C⁡i∈ℂ
10 9 sqvald ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−C⁡i2=B⁡i−C⁡i⁢B⁡i−C⁡i
11 10 oveq2d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢−1−t⁢B⁡i−C⁡i2=t⁢−1−t⁢B⁡i−C⁡i⁢B⁡i−C⁡i
12 elicc01 ⊢t∈01↔t∈ℝ∧0≤t∧t≤1
13 12 simp1bi ⊢t∈01→t∈ℝ
14 13 recnd ⊢t∈01→t∈ℂ
15 14 3ad2ant3 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t∈ℂ
16 1re ⊢1∈ℝ
17 resubcl ⊢1∈ℝ∧t∈ℝ→1−t∈ℝ
18 16 13 17 sylancr ⊢t∈01→1−t∈ℝ
19 18 3ad2ant3 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t∈ℝ
20 19 recnd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t∈ℂ
21 20 negcld ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→−1−t∈ℂ
22 15 9 21 9 mul4d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢B⁡i−C⁡i⁢−1−t⁢B⁡i−C⁡i=t⁢−1−t⁢B⁡i−C⁡i⁢B⁡i−C⁡i
23 recn ⊢B⁡i∈ℝ→B⁡i∈ℂ
24 23 3ad2ant1 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i∈ℂ
25 recn ⊢C⁡i∈ℝ→C⁡i∈ℂ
26 25 3ad2ant2 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→C⁡i∈ℂ
27 15 24 26 subdid ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢B⁡i−C⁡i=t⁢B⁡i−t⁢C⁡i
28 ax-1cn ⊢1∈ℂ
29 subdir ⊢1∈ℂ∧1−t∈ℂ∧B⁡i∈ℂ→1−1−t⁢B⁡i=1⁢B⁡i−1−t⁢B⁡i
30 28 20 24 29 mp3an2i ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−1−t⁢B⁡i=1⁢B⁡i−1−t⁢B⁡i
31 nncan ⊢1∈ℂ∧t∈ℂ→1−1−t=t
32 28 15 31 sylancr ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−1−t=t
33 32 oveq1d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−1−t⁢B⁡i=t⁢B⁡i
34 24 mullidd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1⁢B⁡i=B⁡i
35 34 oveq1d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1⁢B⁡i−1−t⁢B⁡i=B⁡i−1−t⁢B⁡i
36 30 33 35 3eqtr3d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢B⁡i=B⁡i−1−t⁢B⁡i
37 36 oveq1d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢B⁡i−t⁢C⁡i=B⁡i-1−t⁢B⁡i-t⁢C⁡i
38 simp1 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i∈ℝ
39 19 38 remulcld ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i∈ℝ
40 39 recnd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i∈ℂ
41 13 3ad2ant3 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t∈ℝ
42 simp2 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→C⁡i∈ℝ
43 41 42 remulcld ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢C⁡i∈ℝ
44 43 recnd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢C⁡i∈ℂ
45 24 40 44 subsub4d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i-1−t⁢B⁡i-t⁢C⁡i=B⁡i−1−t⁢B⁡i+t⁢C⁡i
46 27 37 45 3eqtrd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢B⁡i−C⁡i=B⁡i−1−t⁢B⁡i+t⁢C⁡i
47 20 9 mulneg1d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→−1−t⁢B⁡i−C⁡i=−1−t⁢B⁡i−C⁡i
48 20 24 26 subdid ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i−C⁡i=1−t⁢B⁡i−1−t⁢C⁡i
49 subdir ⊢1∈ℂ∧t∈ℂ∧C⁡i∈ℂ→1−t⁢C⁡i=1⁢C⁡i−t⁢C⁡i
50 28 15 26 49 mp3an2i ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢C⁡i=1⁢C⁡i−t⁢C⁡i
51 26 mullidd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1⁢C⁡i=C⁡i
52 51 oveq1d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1⁢C⁡i−t⁢C⁡i=C⁡i−t⁢C⁡i
53 50 52 eqtrd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢C⁡i=C⁡i−t⁢C⁡i
54 53 oveq2d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i−1−t⁢C⁡i=1−t⁢B⁡i−C⁡i−t⁢C⁡i
55 40 26 44 subsub3d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i−C⁡i−t⁢C⁡i=1−t⁢B⁡i+t⁢C⁡i-C⁡i
56 48 54 55 3eqtrd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i−C⁡i=1−t⁢B⁡i+t⁢C⁡i-C⁡i
57 56 negeqd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→−1−t⁢B⁡i−C⁡i=−1−t⁢B⁡i+t⁢C⁡i-C⁡i
58 39 43 readdcld ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i+t⁢C⁡i∈ℝ
59 58 recnd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→1−t⁢B⁡i+t⁢C⁡i∈ℂ
60 59 26 negsubdi2d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→−1−t⁢B⁡i+t⁢C⁡i-C⁡i=C⁡i−1−t⁢B⁡i+t⁢C⁡i
61 47 57 60 3eqtrd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→−1−t⁢B⁡i−C⁡i=C⁡i−1−t⁢B⁡i+t⁢C⁡i
62 46 61 oveq12d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢B⁡i−C⁡i⁢−1−t⁢B⁡i−C⁡i=B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
63 11 22 62 3eqtr2rd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i=t⁢−1−t⁢B⁡i−C⁡i2
64 15 20 mulneg2d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢−1−t=−t⁢1−t
65 64 oveq1d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢−1−t⁢B⁡i−C⁡i2=−t⁢1−t⁢B⁡i−C⁡i2
66 41 19 remulcld ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢1−t∈ℝ
67 66 recnd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢1−t∈ℂ
68 8 resqcld ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−C⁡i2∈ℝ
69 68 recnd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−C⁡i2∈ℂ
70 67 69 mulneg1d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→−t⁢1−t⁢B⁡i−C⁡i2=−t⁢1−t⁢B⁡i−C⁡i2
71 65 70 eqtrd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢−1−t⁢B⁡i−C⁡i2=−t⁢1−t⁢B⁡i−C⁡i2
72 12 simp2bi ⊢t∈01→0≤t
73 12 simp3bi ⊢t∈01→t≤1
74 subge0 ⊢1∈ℝ∧t∈ℝ→0≤1−t↔t≤1
75 16 13 74 sylancr ⊢t∈01→0≤1−t↔t≤1
76 73 75 mpbird ⊢t∈01→0≤1−t
77 13 18 72 76 mulge0d ⊢t∈01→0≤t⁢1−t
78 77 3ad2ant3 ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→0≤t⁢1−t
79 8 sqge0d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→0≤B⁡i−C⁡i2
80 66 68 78 79 mulge0d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→0≤t⁢1−t⁢B⁡i−C⁡i2
81 66 68 remulcld ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢1−t⁢B⁡i−C⁡i2∈ℝ
82 81 le0neg2d ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→0≤t⁢1−t⁢B⁡i−C⁡i2↔−t⁢1−t⁢B⁡i−C⁡i2≤0
83 80 82 mpbid ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→−t⁢1−t⁢B⁡i−C⁡i2≤0
84 71 83 eqbrtrd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→t⁢−1−t⁢B⁡i−C⁡i2≤0
85 63 84 eqbrtrd ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
86 85 3expa ⊢B⁡i∈ℝ∧C⁡i∈ℝ∧t∈01→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
87 6 86 sylan ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N∧t∈01→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
88 87 an32s ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧i∈1…N→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
89 88 ralrimiva ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01→∀i∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
90 fveecn ⊢B∈𝔼⁡N∧i∈1…N→B⁡i∈ℂ
91 fveecn ⊢C∈𝔼⁡N∧i∈1…N→C⁡i∈ℂ
92 90 91 anim12i ⊢B∈𝔼⁡N∧i∈1…N∧C∈𝔼⁡N∧i∈1…N→B⁡i∈ℂ∧C⁡i∈ℂ
93 92 anandirs ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→B⁡i∈ℂ∧C⁡i∈ℂ
94 fveecn ⊢B∈𝔼⁡N∧j∈1…N→B⁡j∈ℂ
95 fveecn ⊢C∈𝔼⁡N∧j∈1…N→C⁡j∈ℂ
96 94 95 anim12i ⊢B∈𝔼⁡N∧j∈1…N∧C∈𝔼⁡N∧j∈1…N→B⁡j∈ℂ∧C⁡j∈ℂ
97 96 anandirs ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧j∈1…N→B⁡j∈ℂ∧C⁡j∈ℂ
98 93 97 anim12dan ⊢B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N∧j∈1…N→B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ
99 98 3adantl1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N∧j∈1…N→B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ
100 subcl ⊢B⁡i∈ℂ∧C⁡i∈ℂ→B⁡i−C⁡i∈ℂ
101 100 3ad2ant1 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡i−C⁡i∈ℂ
102 subcl ⊢C⁡j∈ℂ∧B⁡j∈ℂ→C⁡j−B⁡j∈ℂ
103 102 ancoms ⊢B⁡j∈ℂ∧C⁡j∈ℂ→C⁡j−B⁡j∈ℂ
104 103 3ad2ant2 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡j−B⁡j∈ℂ
105 101 104 mulcomd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡i−C⁡i⁢C⁡j−B⁡j=C⁡j−B⁡j⁢B⁡i−C⁡i
106 simp2r ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡j∈ℂ
107 simp2l ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡j∈ℂ
108 simp1l ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡i∈ℂ
109 simp1r ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡i∈ℂ
110 mulsub2 ⊢C⁡j∈ℂ∧B⁡j∈ℂ∧B⁡i∈ℂ∧C⁡i∈ℂ→C⁡j−B⁡j⁢B⁡i−C⁡i=B⁡j−C⁡j⁢C⁡i−B⁡i
111 106 107 108 109 110 syl22anc ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡j−B⁡j⁢B⁡i−C⁡i=B⁡j−C⁡j⁢C⁡i−B⁡i
112 105 111 eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡i−C⁡i⁢C⁡j−B⁡j=B⁡j−C⁡j⁢C⁡i−B⁡i
113 112 oveq2d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢1−t⁢B⁡i−C⁡i⁢C⁡j−B⁡j=t⁢1−t⁢B⁡j−C⁡j⁢C⁡i−B⁡i
114 simp3 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t∈ℂ
115 subcl ⊢1∈ℂ∧t∈ℂ→1−t∈ℂ
116 28 115 mpan ⊢t∈ℂ→1−t∈ℂ
117 116 3ad2ant3 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t∈ℂ
118 114 117 101 104 mul4d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢1−t⁢B⁡i−C⁡i⁢C⁡j−B⁡j=t⁢B⁡i−C⁡i⁢1−t⁢C⁡j−B⁡j
119 114 108 109 subdid ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡i−C⁡i=t⁢B⁡i−t⁢C⁡i
120 28 117 108 29 mp3an2i ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−1−t⁢B⁡i=1⁢B⁡i−1−t⁢B⁡i
121 28 31 mpan ⊢t∈ℂ→1−1−t=t
122 121 3ad2ant3 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−1−t=t
123 122 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−1−t⁢B⁡i=t⁢B⁡i
124 108 mullidd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢B⁡i=B⁡i
125 124 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢B⁡i−1−t⁢B⁡i=B⁡i−1−t⁢B⁡i
126 120 123 125 3eqtr3d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡i=B⁡i−1−t⁢B⁡i
127 126 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡i−t⁢C⁡i=B⁡i-1−t⁢B⁡i-t⁢C⁡i
128 117 108 mulcld ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢B⁡i∈ℂ
129 114 109 mulcld ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢C⁡i∈ℂ
130 108 128 129 subsub4d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡i-1−t⁢B⁡i-t⁢C⁡i=B⁡i−1−t⁢B⁡i+t⁢C⁡i
131 119 127 130 3eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡i−C⁡i=B⁡i−1−t⁢B⁡i+t⁢C⁡i
132 117 106 107 subdid ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡j−B⁡j=1−t⁢C⁡j−1−t⁢B⁡j
133 subdir ⊢1∈ℂ∧t∈ℂ∧C⁡j∈ℂ→1−t⁢C⁡j=1⁢C⁡j−t⁢C⁡j
134 28 114 106 133 mp3an2i ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡j=1⁢C⁡j−t⁢C⁡j
135 106 mullidd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢C⁡j=C⁡j
136 135 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢C⁡j−t⁢C⁡j=C⁡j−t⁢C⁡j
137 134 136 eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡j=C⁡j−t⁢C⁡j
138 137 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡j−1−t⁢B⁡j=C⁡j-t⁢C⁡j-1−t⁢B⁡j
139 132 138 eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡j−B⁡j=C⁡j-t⁢C⁡j-1−t⁢B⁡j
140 114 106 mulcld ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢C⁡j∈ℂ
141 117 107 mulcld ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢B⁡j∈ℂ
142 106 140 141 sub32d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡j-t⁢C⁡j-1−t⁢B⁡j=C⁡j-1−t⁢B⁡j-t⁢C⁡j
143 106 141 140 subsub4d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡j-1−t⁢B⁡j-t⁢C⁡j=C⁡j−1−t⁢B⁡j+t⁢C⁡j
144 139 142 143 3eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡j−B⁡j=C⁡j−1−t⁢B⁡j+t⁢C⁡j
145 131 144 oveq12d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡i−C⁡i⁢1−t⁢C⁡j−B⁡j=B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j
146 118 145 eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢1−t⁢B⁡i−C⁡i⁢C⁡j−B⁡j=B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j
147 subcl ⊢B⁡j∈ℂ∧C⁡j∈ℂ→B⁡j−C⁡j∈ℂ
148 147 3ad2ant2 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡j−C⁡j∈ℂ
149 subcl ⊢C⁡i∈ℂ∧B⁡i∈ℂ→C⁡i−B⁡i∈ℂ
150 149 ancoms ⊢B⁡i∈ℂ∧C⁡i∈ℂ→C⁡i−B⁡i∈ℂ
151 150 3ad2ant1 ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡i−B⁡i∈ℂ
152 114 117 148 151 mul4d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢1−t⁢B⁡j−C⁡j⁢C⁡i−B⁡i=t⁢B⁡j−C⁡j⁢1−t⁢C⁡i−B⁡i
153 114 107 106 subdid ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡j−C⁡j=t⁢B⁡j−t⁢C⁡j
154 subdir ⊢1∈ℂ∧1−t∈ℂ∧B⁡j∈ℂ→1−1−t⁢B⁡j=1⁢B⁡j−1−t⁢B⁡j
155 28 117 107 154 mp3an2i ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−1−t⁢B⁡j=1⁢B⁡j−1−t⁢B⁡j
156 122 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−1−t⁢B⁡j=t⁢B⁡j
157 107 mullidd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢B⁡j=B⁡j
158 157 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢B⁡j−1−t⁢B⁡j=B⁡j−1−t⁢B⁡j
159 155 156 158 3eqtr3rd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡j−1−t⁢B⁡j=t⁢B⁡j
160 159 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡j-1−t⁢B⁡j-t⁢C⁡j=t⁢B⁡j−t⁢C⁡j
161 107 141 140 subsub4d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡j-1−t⁢B⁡j-t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j
162 153 160 161 3eqtr2d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡j−C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j
163 117 109 108 subdid ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡i−B⁡i=1−t⁢C⁡i−1−t⁢B⁡i
164 28 114 109 49 mp3an2i ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡i=1⁢C⁡i−t⁢C⁡i
165 109 mullidd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢C⁡i=C⁡i
166 165 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1⁢C⁡i−t⁢C⁡i=C⁡i−t⁢C⁡i
167 164 166 eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡i=C⁡i−t⁢C⁡i
168 167 oveq1d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡i−1−t⁢B⁡i=C⁡i-t⁢C⁡i-1−t⁢B⁡i
169 109 129 128 sub32d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡i-t⁢C⁡i-1−t⁢B⁡i=C⁡i-1−t⁢B⁡i-t⁢C⁡i
170 109 128 129 subsub4d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡i-1−t⁢B⁡i-t⁢C⁡i=C⁡i−1−t⁢B⁡i+t⁢C⁡i
171 169 170 eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→C⁡i-t⁢C⁡i-1−t⁢B⁡i=C⁡i−1−t⁢B⁡i+t⁢C⁡i
172 163 168 171 3eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→1−t⁢C⁡i−B⁡i=C⁡i−1−t⁢B⁡i+t⁢C⁡i
173 162 172 oveq12d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢B⁡j−C⁡j⁢1−t⁢C⁡i−B⁡i=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
174 152 173 eqtrd ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→t⁢1−t⁢B⁡j−C⁡j⁢C⁡i−B⁡i=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
175 113 146 174 3eqtr3d ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
176 175 3expa ⊢B⁡i∈ℂ∧C⁡i∈ℂ∧B⁡j∈ℂ∧C⁡j∈ℂ∧t∈ℂ→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
177 99 14 176 syl2an ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N∧j∈1…N∧t∈01→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
178 177 an32s ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧i∈1…N∧j∈1…N→B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
179 178 ralrimivva ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01→∀i∈1…N∀j∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
180 fveq2 ⊢k=i→A⁡k=A⁡i
181 fveq2 ⊢k=i→B⁡k=B⁡i
182 181 oveq2d ⊢k=i→1−t⁢B⁡k=1−t⁢B⁡i
183 fveq2 ⊢k=i→C⁡k=C⁡i
184 183 oveq2d ⊢k=i→t⁢C⁡k=t⁢C⁡i
185 182 184 oveq12d ⊢k=i→1−t⁢B⁡k+t⁢C⁡k=1−t⁢B⁡i+t⁢C⁡i
186 180 185 eqeq12d ⊢k=i→A⁡k=1−t⁢B⁡k+t⁢C⁡k↔A⁡i=1−t⁢B⁡i+t⁢C⁡i
187 186 rspccva ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k∧i∈1…N→A⁡i=1−t⁢B⁡i+t⁢C⁡i
188 oveq2 ⊢A⁡i=1−t⁢B⁡i+t⁢C⁡i→B⁡i−A⁡i=B⁡i−1−t⁢B⁡i+t⁢C⁡i
189 oveq2 ⊢A⁡i=1−t⁢B⁡i+t⁢C⁡i→C⁡i−A⁡i=C⁡i−1−t⁢B⁡i+t⁢C⁡i
190 188 189 oveq12d ⊢A⁡i=1−t⁢B⁡i+t⁢C⁡i→B⁡i−A⁡i⁢C⁡i−A⁡i=B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
191 190 breq1d ⊢A⁡i=1−t⁢B⁡i+t⁢C⁡i→B⁡i−A⁡i⁢C⁡i−A⁡i≤0↔B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
192 187 191 syl ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k∧i∈1…N→B⁡i−A⁡i⁢C⁡i−A⁡i≤0↔B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
193 192 ralbidva ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0↔∀i∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0
194 fveq2 ⊢k=j→A⁡k=A⁡j
195 fveq2 ⊢k=j→B⁡k=B⁡j
196 195 oveq2d ⊢k=j→1−t⁢B⁡k=1−t⁢B⁡j
197 fveq2 ⊢k=j→C⁡k=C⁡j
198 197 oveq2d ⊢k=j→t⁢C⁡k=t⁢C⁡j
199 196 198 oveq12d ⊢k=j→1−t⁢B⁡k+t⁢C⁡k=1−t⁢B⁡j+t⁢C⁡j
200 194 199 eqeq12d ⊢k=j→A⁡k=1−t⁢B⁡k+t⁢C⁡k↔A⁡j=1−t⁢B⁡j+t⁢C⁡j
201 200 rspccva ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k∧j∈1…N→A⁡j=1−t⁢B⁡j+t⁢C⁡j
202 oveq2 ⊢A⁡j=1−t⁢B⁡j+t⁢C⁡j→C⁡j−A⁡j=C⁡j−1−t⁢B⁡j+t⁢C⁡j
203 188 202 oveqan12d ⊢A⁡i=1−t⁢B⁡i+t⁢C⁡i∧A⁡j=1−t⁢B⁡j+t⁢C⁡j→B⁡i−A⁡i⁢C⁡j−A⁡j=B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j
204 oveq2 ⊢A⁡j=1−t⁢B⁡j+t⁢C⁡j→B⁡j−A⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j
205 204 189 oveqan12rd ⊢A⁡i=1−t⁢B⁡i+t⁢C⁡i∧A⁡j=1−t⁢B⁡j+t⁢C⁡j→B⁡j−A⁡j⁢C⁡i−A⁡i=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
206 203 205 eqeq12d ⊢A⁡i=1−t⁢B⁡i+t⁢C⁡i∧A⁡j=1−t⁢B⁡j+t⁢C⁡j→B⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
207 187 201 206 syl2an ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k∧i∈1…N∧∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k∧j∈1…N→B⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
208 207 anandis ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k∧i∈1…N∧j∈1…N→B⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔B⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
209 208 2ralbidva ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…N∀j∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
210 193 209 anbi12d ⊢∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i
211 210 biimprcd ⊢∀i∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−1−t⁢B⁡i+t⁢C⁡i⁢C⁡j−1−t⁢B⁡j+t⁢C⁡j=B⁡j−1−t⁢B⁡j+t⁢C⁡j⁢C⁡i−1−t⁢B⁡i+t⁢C⁡i→∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
212 89 179 211 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01→∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
213 212 rexlimdva ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
214 fveere ⊢A∈𝔼⁡N∧i∈1…N→A⁡i∈ℝ
215 214 3ad2antl1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→A⁡i∈ℝ
216 mulsuble0b ⊢B⁡i∈ℝ∧A⁡i∈ℝ∧C⁡i∈ℝ→B⁡i−A⁡i⁢C⁡i−A⁡i≤0↔B⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
217 3 215 5 216 syl3anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧i∈1…N→B⁡i−A⁡i⁢C⁡i−A⁡i≤0↔B⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
218 217 ralbidva ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0↔∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
219 218 anbi1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
220 simpl2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C→B∈𝔼⁡N
221 simpl1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C→A∈𝔼⁡N
222 eqeefv ⊢B∈𝔼⁡N∧A∈𝔼⁡N→B=A↔∀i∈1…NB⁡i=A⁡i
223 220 221 222 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C→B=A↔∀i∈1…NB⁡i=A⁡i
224 3 adantlr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧i∈1…N→B⁡i∈ℝ
225 215 adantlr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧i∈1…N→A⁡i∈ℝ
226 224 225 letri3d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧i∈1…N→B⁡i=A⁡i↔B⁡i≤A⁡i∧A⁡i≤B⁡i
227 pm4.25 ⊢B⁡i≤A⁡i∧A⁡i≤B⁡i↔B⁡i≤A⁡i∧A⁡i≤B⁡i∨B⁡i≤A⁡i∧A⁡i≤B⁡i
228 fveq1 ⊢B=C→B⁡i=C⁡i
229 228 breq2d ⊢B=C→A⁡i≤B⁡i↔A⁡i≤C⁡i
230 229 anbi2d ⊢B=C→B⁡i≤A⁡i∧A⁡i≤B⁡i↔B⁡i≤A⁡i∧A⁡i≤C⁡i
231 228 breq1d ⊢B=C→B⁡i≤A⁡i↔C⁡i≤A⁡i
232 231 anbi1d ⊢B=C→B⁡i≤A⁡i∧A⁡i≤B⁡i↔C⁡i≤A⁡i∧A⁡i≤B⁡i
233 230 232 orbi12d ⊢B=C→B⁡i≤A⁡i∧A⁡i≤B⁡i∨B⁡i≤A⁡i∧A⁡i≤B⁡i↔B⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
234 233 ad2antlr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧i∈1…N→B⁡i≤A⁡i∧A⁡i≤B⁡i∨B⁡i≤A⁡i∧A⁡i≤B⁡i↔B⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
235 227 234 bitrid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧i∈1…N→B⁡i≤A⁡i∧A⁡i≤B⁡i↔B⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
236 226 235 bitrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧i∈1…N→B⁡i=A⁡i↔B⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
237 236 ralbidva ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C→∀i∈1…NB⁡i=A⁡i↔∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
238 223 237 bitrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C→B=A↔∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i
239 238 biimprd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i→B=A
240 239 adantrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→B=A
241 240 ex ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B=C→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→B=A
242 0elunit ⊢0∈01
243 fveecn ⊢A∈𝔼⁡N∧k∈1…N→A⁡k∈ℂ
244 243 3ad2antl1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧k∈1…N→A⁡k∈ℂ
245 fveecn ⊢B∈𝔼⁡N∧k∈1…N→B⁡k∈ℂ
246 245 3ad2antl2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧k∈1…N→B⁡k∈ℂ
247 fveecn ⊢C∈𝔼⁡N∧k∈1…N→C⁡k∈ℂ
248 247 3ad2antl3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧k∈1…N→C⁡k∈ℂ
249 244 246 248 3jca ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧k∈1…N→A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ
250 mullid ⊢B⁡k∈ℂ→1⁢B⁡k=B⁡k
251 mul02 ⊢C⁡k∈ℂ→0⋅C⁡k=0
252 250 251 oveqan12d ⊢B⁡k∈ℂ∧C⁡k∈ℂ→1⁢B⁡k+0⋅C⁡k=B⁡k+0
253 addrid ⊢B⁡k∈ℂ→B⁡k+0=B⁡k
254 253 adantr ⊢B⁡k∈ℂ∧C⁡k∈ℂ→B⁡k+0=B⁡k
255 252 254 eqtrd ⊢B⁡k∈ℂ∧C⁡k∈ℂ→1⁢B⁡k+0⋅C⁡k=B⁡k
256 255 3adant1 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ→1⁢B⁡k+0⋅C⁡k=B⁡k
257 256 adantr ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧B=C∧B=A→1⁢B⁡k+0⋅C⁡k=B⁡k
258 fveq1 ⊢B=A→B⁡k=A⁡k
259 258 ad2antll ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧B=C∧B=A→B⁡k=A⁡k
260 257 259 eqtr2d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧B=C∧B=A→A⁡k=1⁢B⁡k+0⋅C⁡k
261 249 260 sylan ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧k∈1…N∧B=C∧B=A→A⁡k=1⁢B⁡k+0⋅C⁡k
262 261 an32s ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧B=A∧k∈1…N→A⁡k=1⁢B⁡k+0⋅C⁡k
263 262 ralrimiva ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧B=A→∀k∈1…NA⁡k=1⁢B⁡k+0⋅C⁡k
264 oveq2 ⊢t=0→1−t=1−0
265 1m0e1 ⊢1−0=1
266 264 265 eqtrdi ⊢t=0→1−t=1
267 266 oveq1d ⊢t=0→1−t⁢B⁡k=1⁢B⁡k
268 oveq1 ⊢t=0→t⁢C⁡k=0⋅C⁡k
269 267 268 oveq12d ⊢t=0→1−t⁢B⁡k+t⁢C⁡k=1⁢B⁡k+0⋅C⁡k
270 269 eqeq2d ⊢t=0→A⁡k=1−t⁢B⁡k+t⁢C⁡k↔A⁡k=1⁢B⁡k+0⋅C⁡k
271 270 ralbidv ⊢t=0→∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k↔∀k∈1…NA⁡k=1⁢B⁡k+0⋅C⁡k
272 271 rspcev ⊢0∈01∧∀k∈1…NA⁡k=1⁢B⁡k+0⋅C⁡k→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
273 242 263 272 sylancr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧B=C∧B=A→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
274 273 exp32 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B=C→B=A→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
275 241 274 syldd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B=C→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
276 eqeefv ⊢B∈𝔼⁡N∧C∈𝔼⁡N→B=C↔∀p∈1…NB⁡p=C⁡p
277 276 3adant1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B=C↔∀p∈1…NB⁡p=C⁡p
278 277 necon3abid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B≠C↔¬∀p∈1…NB⁡p=C⁡p
279 df-ne ⊢B⁡p≠C⁡p↔¬B⁡p=C⁡p
280 279 rexbii ⊢∃p∈1…NB⁡p≠C⁡p↔∃p∈1…N¬B⁡p=C⁡p
281 rexnal ⊢∃p∈1…N¬B⁡p=C⁡p↔¬∀p∈1…NB⁡p=C⁡p
282 280 281 bitri ⊢∃p∈1…NB⁡p≠C⁡p↔¬∀p∈1…NB⁡p=C⁡p
283 278 282 bitr4di ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B≠C↔∃p∈1…NB⁡p≠C⁡p
284 fveq2 ⊢i=p→B⁡i=B⁡p
285 fveq2 ⊢i=p→A⁡i=A⁡p
286 284 285 breq12d ⊢i=p→B⁡i≤A⁡i↔B⁡p≤A⁡p
287 fveq2 ⊢i=p→C⁡i=C⁡p
288 285 287 breq12d ⊢i=p→A⁡i≤C⁡i↔A⁡p≤C⁡p
289 286 288 anbi12d ⊢i=p→B⁡i≤A⁡i∧A⁡i≤C⁡i↔B⁡p≤A⁡p∧A⁡p≤C⁡p
290 287 285 breq12d ⊢i=p→C⁡i≤A⁡i↔C⁡p≤A⁡p
291 285 284 breq12d ⊢i=p→A⁡i≤B⁡i↔A⁡p≤B⁡p
292 290 291 anbi12d ⊢i=p→C⁡i≤A⁡i∧A⁡i≤B⁡i↔C⁡p≤A⁡p∧A⁡p≤B⁡p
293 289 292 orbi12d ⊢i=p→B⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i↔B⁡p≤A⁡p∧A⁡p≤C⁡p∨C⁡p≤A⁡p∧A⁡p≤B⁡p
294 293 rspcv ⊢p∈1…N→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i→B⁡p≤A⁡p∧A⁡p≤C⁡p∨C⁡p≤A⁡p∧A⁡p≤B⁡p
295 294 ad2antrl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i→B⁡p≤A⁡p∧A⁡p≤C⁡p∨C⁡p≤A⁡p∧A⁡p≤B⁡p
296 simprr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→A⁡p≤C⁡p
297 simp1 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→A∈𝔼⁡N
298 simpl ⊢p∈1…N∧B⁡p≠C⁡p→p∈1…N
299 fveere ⊢A∈𝔼⁡N∧p∈1…N→A⁡p∈ℝ
300 297 298 299 syl2an ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→A⁡p∈ℝ
301 simp3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→C∈𝔼⁡N
302 fveere ⊢C∈𝔼⁡N∧p∈1…N→C⁡p∈ℝ
303 301 298 302 syl2an ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p∈ℝ
304 simpl2 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B∈𝔼⁡N
305 simprl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→p∈1…N
306 fveere ⊢B∈𝔼⁡N∧p∈1…N→B⁡p∈ℝ
307 304 305 306 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p∈ℝ
308 300 303 307 lesub1d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→A⁡p≤C⁡p↔A⁡p−B⁡p≤C⁡p−B⁡p
309 308 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→A⁡p≤C⁡p↔A⁡p−B⁡p≤C⁡p−B⁡p
310 296 309 mpbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→A⁡p−B⁡p≤C⁡p−B⁡p
311 300 307 resubcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→A⁡p−B⁡p∈ℝ
312 311 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→A⁡p−B⁡p∈ℝ
313 simprl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p≤A⁡p
314 300 307 subge0d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→0≤A⁡p−B⁡p↔B⁡p≤A⁡p
315 314 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→0≤A⁡p−B⁡p↔B⁡p≤A⁡p
316 313 315 mpbird ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→0≤A⁡p−B⁡p
317 303 307 resubcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p−B⁡p∈ℝ
318 317 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→C⁡p−B⁡p∈ℝ
319 letr ⊢B⁡p∈ℝ∧A⁡p∈ℝ∧C⁡p∈ℝ→B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p≤C⁡p
320 307 300 303 319 syl3anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p≤C⁡p
321 320 imp ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p≤C⁡p
322 simplrr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p≠C⁡p
323 322 necomd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→C⁡p≠B⁡p
324 307 303 ltlend ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p<C⁡p↔B⁡p≤C⁡p∧C⁡p≠B⁡p
325 324 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p<C⁡p↔B⁡p≤C⁡p∧C⁡p≠B⁡p
326 321 323 325 mpbir2and ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p<C⁡p
327 307 303 posdifd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p<C⁡p↔0<C⁡p−B⁡p
328 327 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→B⁡p<C⁡p↔0<C⁡p−B⁡p
329 326 328 mpbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→0<C⁡p−B⁡p
330 divelunit ⊢A⁡p−B⁡p∈ℝ∧0≤A⁡p−B⁡p∧C⁡p−B⁡p∈ℝ∧0<C⁡p−B⁡p→A⁡p−B⁡pC⁡p−B⁡p∈01↔A⁡p−B⁡p≤C⁡p−B⁡p
331 312 316 318 329 330 syl22anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→A⁡p−B⁡pC⁡p−B⁡p∈01↔A⁡p−B⁡p≤C⁡p−B⁡p
332 310 331 mpbird ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p→A⁡p−B⁡pC⁡p−B⁡p∈01
333 300 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→A⁡p∈ℂ
334 307 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p∈ℂ
335 303 recnd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p∈ℂ
336 simprr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p≠C⁡p
337 336 necomd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p≠B⁡p
338 333 334 335 334 337 div2subd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→A⁡p−B⁡pC⁡p−B⁡p=B⁡p−A⁡pB⁡p−C⁡p
339 338 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→A⁡p−B⁡pC⁡p−B⁡p=B⁡p−A⁡pB⁡p−C⁡p
340 simprl ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p≤A⁡p
341 303 300 307 lesub2d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p≤A⁡p↔B⁡p−A⁡p≤B⁡p−C⁡p
342 341 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p≤A⁡p↔B⁡p−A⁡p≤B⁡p−C⁡p
343 340 342 mpbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→B⁡p−A⁡p≤B⁡p−C⁡p
344 307 300 resubcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p−A⁡p∈ℝ
345 344 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→B⁡p−A⁡p∈ℝ
346 simprr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→A⁡p≤B⁡p
347 307 300 subge0d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→0≤B⁡p−A⁡p↔A⁡p≤B⁡p
348 347 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→0≤B⁡p−A⁡p↔A⁡p≤B⁡p
349 346 348 mpbird ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→0≤B⁡p−A⁡p
350 307 303 resubcld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p−C⁡p∈ℝ
351 350 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→B⁡p−C⁡p∈ℝ
352 letr ⊢C⁡p∈ℝ∧A⁡p∈ℝ∧B⁡p∈ℝ→C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p≤B⁡p
353 303 300 307 352 syl3anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p≤B⁡p
354 353 imp ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p≤B⁡p
355 simplrr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→B⁡p≠C⁡p
356 303 307 ltlend ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p<B⁡p↔C⁡p≤B⁡p∧B⁡p≠C⁡p
357 356 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p<B⁡p↔C⁡p≤B⁡p∧B⁡p≠C⁡p
358 354 355 357 mpbir2and ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p<B⁡p
359 303 307 posdifd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→C⁡p<B⁡p↔0<B⁡p−C⁡p
360 359 adantr ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→C⁡p<B⁡p↔0<B⁡p−C⁡p
361 358 360 mpbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→0<B⁡p−C⁡p
362 divelunit ⊢B⁡p−A⁡p∈ℝ∧0≤B⁡p−A⁡p∧B⁡p−C⁡p∈ℝ∧0<B⁡p−C⁡p→B⁡p−A⁡pB⁡p−C⁡p∈01↔B⁡p−A⁡p≤B⁡p−C⁡p
363 345 349 351 361 362 syl22anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→B⁡p−A⁡pB⁡p−C⁡p∈01↔B⁡p−A⁡p≤B⁡p−C⁡p
364 343 363 mpbird ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→B⁡p−A⁡pB⁡p−C⁡p∈01
365 339 364 eqeltrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧C⁡p≤A⁡p∧A⁡p≤B⁡p→A⁡p−B⁡pC⁡p−B⁡p∈01
366 332 365 jaodan ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧B⁡p≤A⁡p∧A⁡p≤C⁡p∨C⁡p≤A⁡p∧A⁡p≤B⁡p→A⁡p−B⁡pC⁡p−B⁡p∈01
367 366 ex ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→B⁡p≤A⁡p∧A⁡p≤C⁡p∨C⁡p≤A⁡p∧A⁡p≤B⁡p→A⁡p−B⁡pC⁡p−B⁡p∈01
368 295 367 syld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i→A⁡p−B⁡pC⁡p−B⁡p∈01
369 simp2l ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→p∈1…N
370 simp3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→k∈1…N
371 284 285 oveq12d ⊢i=p→B⁡i−A⁡i=B⁡p−A⁡p
372 371 oveq1d ⊢i=p→B⁡i−A⁡i⁢C⁡j−A⁡j=B⁡p−A⁡p⁢C⁡j−A⁡j
373 287 285 oveq12d ⊢i=p→C⁡i−A⁡i=C⁡p−A⁡p
374 373 oveq2d ⊢i=p→B⁡j−A⁡j⁢C⁡i−A⁡i=B⁡j−A⁡j⁢C⁡p−A⁡p
375 372 374 eqeq12d ⊢i=p→B⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i↔B⁡p−A⁡p⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡p−A⁡p
376 fveq2 ⊢j=k→C⁡j=C⁡k
377 fveq2 ⊢j=k→A⁡j=A⁡k
378 376 377 oveq12d ⊢j=k→C⁡j−A⁡j=C⁡k−A⁡k
379 378 oveq2d ⊢j=k→B⁡p−A⁡p⁢C⁡j−A⁡j=B⁡p−A⁡p⁢C⁡k−A⁡k
380 fveq2 ⊢j=k→B⁡j=B⁡k
381 380 377 oveq12d ⊢j=k→B⁡j−A⁡j=B⁡k−A⁡k
382 381 oveq1d ⊢j=k→B⁡j−A⁡j⁢C⁡p−A⁡p=B⁡k−A⁡k⁢C⁡p−A⁡p
383 379 382 eqeq12d ⊢j=k→B⁡p−A⁡p⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡p−A⁡p↔B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p
384 375 383 rspc2v ⊢p∈1…N∧k∈1…N→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p
385 369 370 384 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p
386 simp11 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→A∈𝔼⁡N
387 386 370 243 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→A⁡k∈ℂ
388 simp12 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→B∈𝔼⁡N
389 388 370 245 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→B⁡k∈ℂ
390 simp13 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→C∈𝔼⁡N
391 390 370 247 syl2anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→C⁡k∈ℂ
392 333 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→A⁡p∈ℂ
393 334 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→B⁡p∈ℂ
394 335 3adant3 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→C⁡p∈ℂ
395 simp2r ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→B⁡p≠C⁡p
396 395 necomd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→C⁡p≠B⁡p
397 simpl23 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p∈ℂ
398 simpl21 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡p∈ℂ
399 397 398 subcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p∈ℂ
400 simpl12 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡k∈ℂ
401 399 400 mulcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡k∈ℂ
402 simpl22 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p∈ℂ
403 398 402 subcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡p−B⁡p∈ℂ
404 simpl13 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡k∈ℂ
405 403 404 mulcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡p−B⁡p⁢C⁡k∈ℂ
406 397 402 subcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡p∈ℂ
407 simpl3 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p≠B⁡p
408 397 402 407 subne0d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡p≠0
409 401 405 406 408 divdird ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡k+A⁡p−B⁡p⁢C⁡kC⁡p−B⁡p=C⁡p−A⁡p⁢B⁡kC⁡p−B⁡p+A⁡p−B⁡p⁢C⁡kC⁡p−B⁡p
410 npncan2 ⊢B⁡p∈ℂ∧A⁡p∈ℂ→B⁡p−A⁡p+A⁡p-B⁡p=0
411 402 398 410 syl2anc ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p+A⁡p-B⁡p=0
412 411 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p+A⁡p-B⁡p⁢C⁡k=0⋅C⁡k
413 402 398 subcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p∈ℂ
414 413 403 404 adddird ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p+A⁡p-B⁡p⁢C⁡k=B⁡p−A⁡p⁢C⁡k+A⁡p−B⁡p⁢C⁡k
415 404 mul02d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→0⋅C⁡k=0
416 412 414 415 3eqtr3d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+A⁡p−B⁡p⁢C⁡k=0
417 416 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+A⁡p−B⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k=0+C⁡p−B⁡p⁢A⁡k
418 413 404 mulcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k∈ℂ
419 simpl11 ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡k∈ℂ
420 406 419 mulcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡p⁢A⁡k∈ℂ
421 418 405 420 add32d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+A⁡p−B⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k
422 420 addlidd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→0+C⁡p−B⁡p⁢A⁡k=C⁡p−B⁡p⁢A⁡k
423 417 421 422 3eqtr3rd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k
424 399 419 mulcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢A⁡k∈ℂ
425 413 419 mulcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢A⁡k∈ℂ
426 418 424 425 addsubd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+C⁡p−A⁡p⁢A⁡k-B⁡p−A⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k-B⁡p−A⁡p⁢A⁡k+C⁡p−A⁡p⁢A⁡k
427 397 402 398 nnncan2d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p-A⁡p-B⁡p−A⁡p=C⁡p−B⁡p
428 427 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p-A⁡p-B⁡p−A⁡p⁢A⁡k=C⁡p−B⁡p⁢A⁡k
429 399 413 419 subdird ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p-A⁡p-B⁡p−A⁡p⁢A⁡k=C⁡p−A⁡p⁢A⁡k−B⁡p−A⁡p⁢A⁡k
430 428 429 eqtr3d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡p⁢A⁡k=C⁡p−A⁡p⁢A⁡k−B⁡p−A⁡p⁢A⁡k
431 430 oveq2d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k+C⁡p−A⁡p⁢A⁡k-B⁡p−A⁡p⁢A⁡k
432 418 424 425 addsubassd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+C⁡p−A⁡p⁢A⁡k-B⁡p−A⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k+C⁡p−A⁡p⁢A⁡k-B⁡p−A⁡p⁢A⁡k
433 431 432 eqtr4d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k+C⁡p−A⁡p⁢A⁡k-B⁡p−A⁡p⁢A⁡k
434 413 404 419 subdid ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡p−A⁡p⁢C⁡k−B⁡p−A⁡p⁢A⁡k
435 434 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k-B⁡p−A⁡p⁢A⁡k+C⁡p−A⁡p⁢A⁡k
436 426 433 435 3eqtr4d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k
437 436 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k+C⁡p−B⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k=B⁡p−A⁡p⁢C⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k
438 423 437 eqtrd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡p⁢A⁡k=B⁡p−A⁡p⁢C⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k
439 simpr ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p
440 439 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p+C⁡p−A⁡p⁢A⁡k
441 440 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡p−A⁡p⁢C⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p+C⁡p−A⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k
442 400 419 subcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡k−A⁡k∈ℂ
443 442 399 mulcomd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡k−A⁡k⁢C⁡p−A⁡p=C⁡p−A⁡p⁢B⁡k−A⁡k
444 443 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡k−A⁡k⁢C⁡p−A⁡p+C⁡p−A⁡p⁢A⁡k=C⁡p−A⁡p⁢B⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k
445 399 442 419 adddid ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡k-A⁡k+A⁡k=C⁡p−A⁡p⁢B⁡k−A⁡k+C⁡p−A⁡p⁢A⁡k
446 400 419 npcand ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡k-A⁡k+A⁡k=B⁡k
447 446 oveq2d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡k-A⁡k+A⁡k=C⁡p−A⁡p⁢B⁡k
448 444 445 447 3eqtr2d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡k−A⁡k⁢C⁡p−A⁡p+C⁡p−A⁡p⁢A⁡k=C⁡p−A⁡p⁢B⁡k
449 448 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→B⁡k−A⁡k⁢C⁡p−A⁡p+C⁡p−A⁡p⁢A⁡k+A⁡p−B⁡p⁢C⁡k=C⁡p−A⁡p⁢B⁡k+A⁡p−B⁡p⁢C⁡k
450 438 441 449 3eqtrd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡p⁢A⁡k=C⁡p−A⁡p⁢B⁡k+A⁡p−B⁡p⁢C⁡k
451 401 405 addcld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡k+A⁡p−B⁡p⁢C⁡k∈ℂ
452 451 406 419 408 divmuld ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡k+A⁡p−B⁡p⁢C⁡kC⁡p−B⁡p=A⁡k↔C⁡p−B⁡p⁢A⁡k=C⁡p−A⁡p⁢B⁡k+A⁡p−B⁡p⁢C⁡k
453 450 452 mpbird ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡k+A⁡p−B⁡p⁢C⁡kC⁡p−B⁡p=A⁡k
454 399 400 406 408 div23d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡kC⁡p−B⁡p=C⁡p−A⁡pC⁡p−B⁡p⁢B⁡k
455 406 403 406 408 divsubdird ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p-B⁡p-A⁡p−B⁡pC⁡p−B⁡p=C⁡p−B⁡pC⁡p−B⁡p−A⁡p−B⁡pC⁡p−B⁡p
456 397 398 402 nnncan2d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p-B⁡p-A⁡p−B⁡p=C⁡p−A⁡p
457 456 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p-B⁡p-A⁡p−B⁡pC⁡p−B⁡p=C⁡p−A⁡pC⁡p−B⁡p
458 406 408 dividd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡pC⁡p−B⁡p=1
459 458 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−B⁡pC⁡p−B⁡p−A⁡p−B⁡pC⁡p−B⁡p=1−A⁡p−B⁡pC⁡p−B⁡p
460 455 457 459 3eqtr3d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡pC⁡p−B⁡p=1−A⁡p−B⁡pC⁡p−B⁡p
461 460 oveq1d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡pC⁡p−B⁡p⁢B⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k
462 454 461 eqtrd ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡kC⁡p−B⁡p=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k
463 403 404 406 408 div23d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡p−B⁡p⁢C⁡kC⁡p−B⁡p=A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
464 462 463 oveq12d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→C⁡p−A⁡p⁢B⁡kC⁡p−B⁡p+A⁡p−B⁡p⁢C⁡kC⁡p−B⁡p=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
465 409 453 464 3eqtr3d ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p∧B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
466 465 ex ⊢A⁡k∈ℂ∧B⁡k∈ℂ∧C⁡k∈ℂ∧A⁡p∈ℂ∧B⁡p∈ℂ∧C⁡p∈ℂ∧C⁡p≠B⁡p→B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
467 387 389 391 392 393 394 396 466 syl331anc ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→B⁡p−A⁡p⁢C⁡k−A⁡k=B⁡k−A⁡k⁢C⁡p−A⁡p→A⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
468 385 467 syld ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p∧k∈1…N→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→A⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
469 468 3expia ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→k∈1…N→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→A⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
470 469 com23 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→k∈1…N→A⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
471 470 ralrimdv ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∀k∈1…NA⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
472 368 471 anim12d ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→A⁡p−B⁡pC⁡p−B⁡p∈01∧∀k∈1…NA⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
473 oveq2 ⊢t=A⁡p−B⁡pC⁡p−B⁡p→1−t=1−A⁡p−B⁡pC⁡p−B⁡p
474 473 oveq1d ⊢t=A⁡p−B⁡pC⁡p−B⁡p→1−t⁢B⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k
475 oveq1 ⊢t=A⁡p−B⁡pC⁡p−B⁡p→t⁢C⁡k=A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
476 474 475 oveq12d ⊢t=A⁡p−B⁡pC⁡p−B⁡p→1−t⁢B⁡k+t⁢C⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
477 476 eqeq2d ⊢t=A⁡p−B⁡pC⁡p−B⁡p→A⁡k=1−t⁢B⁡k+t⁢C⁡k↔A⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
478 477 ralbidv ⊢t=A⁡p−B⁡pC⁡p−B⁡p→∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k↔∀k∈1…NA⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k
479 478 rspcev ⊢A⁡p−B⁡pC⁡p−B⁡p∈01∧∀k∈1…NA⁡k=1−A⁡p−B⁡pC⁡p−B⁡p⁢B⁡k+A⁡p−B⁡pC⁡p−B⁡p⁢C⁡k→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
480 472 479 syl6 ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧p∈1…N∧B⁡p≠C⁡p→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
481 480 rexlimdvaa ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∃p∈1…NB⁡p≠C⁡p→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
482 283 481 sylbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→B≠C→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
483 275 482 pm2.61dne ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…NB⁡i≤A⁡i∧A⁡i≤C⁡i∨C⁡i≤A⁡i∧A⁡i≤B⁡i∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
484 219 483 sylbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k
485 213 484 impbid ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→∃t∈01∀k∈1…NA⁡k=1−t⁢B⁡k+t⁢C⁡k↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i
486 1 485 bitrd ⊢A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N→ABtwnBC↔∀i∈1…NB⁡i−A⁡i⁢C⁡i−A⁡i≤0∧∀i∈1…N∀j∈1…NB⁡i−A⁡i⁢C⁡j−A⁡j=B⁡j−A⁡j⁢C⁡i−A⁡i