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→DBtwnAC∧EBtwnBC→∃x∈𝔼⁡NxBtwnDB∧xBtwnEA

Proof

Step Hyp Ref Expression
1 axpaschlem ⊢t∈01∧s∈01→∃r∈01∃q∈01q=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∈01∧s∈01→∃r∈01∃q∈01q=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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s∧i∈1…N→r∈01
16 elicc01 ⊢r∈01↔r∈ℝ∧0≤r∧r≤1
17 16 simp1bi ⊢r∈01→r∈ℝ
18 15 17 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s→t∈01
23 22 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s∧i∈1…N→t∈01
24 elicc01 ⊢t∈01↔t∈ℝ∧0≤t∧t≤1
25 24 simp1bi ⊢t∈01→t∈ℝ
26 23 25 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s∧i∈1…N→q∈01
64 elicc01 ⊢q∈01↔q∈ℝ∧0≤q∧q≤1
65 64 simp1bi ⊢q∈01→q∈ℝ
66 63 65 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s→s∈01
70 69 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s∧i∈1…N→s∈01
71 elicc01 ⊢s∈01↔s∈ℝ∧0≤s∧s≤1
72 71 simp1bi ⊢s∈01→s∈ℝ
73 70 72 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01∧q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s→∀i∈1…N1−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∈01∧s∈01∧r∈01∧q∈01→q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s→∀i∈1…N1−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∈01∧s∈01→∃r∈01∃q∈01q=1−r⁢1−t∧r=1−q⁢1−s∧1−r⁢t=1−q⁢s→∃r∈01∃q∈01∀i∈1…N1−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∈01∧s∈01→∃r∈01∃q∈01∀i∈1…N1−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∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→r∈01
105 104 17 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→r∈ℝ
106 14 105 19 sylancr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→1−r∈ℝ
107 simpl3l ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→t∈01
108 107 adantr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→t∈01
109 108 25 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→t∈ℝ
110 14 109 27 sylancr ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→1−t∈ℝ
111 simpl21 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→A∈𝔼⁡N
112 fveere ⊢A∈𝔼⁡N∧k∈1…N→A⁡k∈ℝ
113 111 112 sylan ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→A⁡k∈ℝ
114 110 113 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→1−t⁢A⁡k∈ℝ
115 simpl23 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→C∈𝔼⁡N
116 fveere ⊢C∈𝔼⁡N∧k∈1…N→C⁡k∈ℝ
117 115 116 sylan ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→C⁡k∈ℝ
118 109 117 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→t⁢C⁡k∈ℝ
119 114 118 readdcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→1−t⁢A⁡k+t⁢C⁡k∈ℝ
120 106 119 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→1−r⁢1−t⁢A⁡k+t⁢C⁡k∈ℝ
121 simpl22 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→B∈𝔼⁡N
122 fveere ⊢B∈𝔼⁡N∧k∈1…N→B⁡k∈ℝ
123 121 122 sylan ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→B⁡k∈ℝ
124 105 123 remulcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧k∈1…N→r⁢B⁡k∈ℝ
125 120 124 readdcld ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01∧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∈01∧s∈01∧r∈01∧q∈01→∀k∈1…N1−r⁢1−t⁢A⁡k+t⁢C⁡k+r⁢B⁡k∈ℝ
127 126 anassrs ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→∀k∈1…N1−r⁢1−t⁢A⁡k+t⁢C⁡k+r⁢B⁡k∈ℝ
128 simpll1 ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→N∈ℕ
129 mptelee ⊢N∈ℕ→k∈1…N⟼1−r⁢1−t⁢A⁡k+t⁢C⁡k+r⁢B⁡k∈𝔼⁡N↔∀k∈1…N1−r⁢1−t⁢A⁡k+t⁢C⁡k+r⁢B⁡k∈ℝ
130 128 129 syl ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→k∈1…N⟼1−r⁢1−t⁢A⁡k+t⁢C⁡k+r⁢B⁡k∈𝔼⁡N↔∀k∈1…N1−r⁢1−t⁢A⁡k+t⁢C⁡k+r⁢B⁡k∈ℝ
131 127 130 mpbird ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧t∈01∧s∈01∧r∈01∧q∈01→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…Nx⁡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…N1−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…N1−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…Nx⁡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…N1−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…Nx⁡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∈01∧s∈01∧r∈01∧q∈01→∀i∈1…N1−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…Nx⁡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∈01∧s∈01∧r∈01→∃q∈01∀i∈1…N1−r⁢1−t⁢A⁡i+t⁢C⁡i+r⁢B⁡i=1−q⁢1−s⁢B⁡i+s⁢C⁡i+q⁢A⁡i→∃q∈01∃x∈𝔼⁡N∀i∈1…Nx⁡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∈01∧s∈01→∃r∈01∃q∈01∀i∈1…N1−r⁢1−t⁢A⁡i+t⁢C⁡i+r⁢B⁡i=1−q⁢1−s⁢B⁡i+s⁢C⁡i+q⁢A⁡i→∃r∈01∃q∈01∃x∈𝔼⁡N∀i∈1…Nx⁡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∈01∧s∈01→∃r∈01∃q∈01∃x∈𝔼⁡N∀i∈1…Nx⁡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∈01∃x∈𝔼⁡N∀i∈1…Nx⁡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∈01∀i∈1…Nx⁡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∈01∃q∈01∃x∈𝔼⁡N∀i∈1…Nx⁡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∈01∃x∈𝔼⁡N∃q∈01∀i∈1…Nx⁡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∈01∃x∈𝔼⁡N∃q∈01∀i∈1…Nx⁡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∈01∃q∈01∀i∈1…Nx⁡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∈01∃q∈01∃x∈𝔼⁡N∀i∈1…Nx⁡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∈01∃q∈01∀i∈1…Nx⁡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∈01∧s∈01→∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡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…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∀i∈1…Nx⁡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…Nx⁡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…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧x⁡i=1−q⁢E⁡i+q⁢A⁡i↔∀i∈1…Nx⁡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…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧x⁡i=1−q⁢E⁡i+q⁢A⁡i↔∀i∈1…Nx⁡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…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∃q∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧x⁡i=1−q⁢E⁡i+q⁢A⁡i↔∃q∈01∀i∈1…Nx⁡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…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧x⁡i=1−q⁢E⁡i+q⁢A⁡i↔∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡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∈01∧s∈01→∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡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∈01∧s∈01→∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡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∈01∃s∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡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∈01∃s∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i→∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡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→DBtwnAC↔∃t∈01∀i∈1…ND⁡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→DBtwnAC↔∃t∈01∀i∈1…ND⁡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→EBtwnBC↔∃s∈01∀i∈1…NE⁡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→EBtwnBC↔∃s∈01∀i∈1…NE⁡i=1−s⁢B⁡i+s⁢C⁡i
189 184 188 anbi12d ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→DBtwnAC∧EBtwnBC↔∃t∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧∃s∈01∀i∈1…NE⁡i=1−s⁢B⁡i+s⁢C⁡i
190 r19.26 ⊢∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i↔∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧∀i∈1…NE⁡i=1−s⁢B⁡i+s⁢C⁡i
191 190 2rexbii ⊢∃t∈01∃s∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i↔∃t∈01∃s∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧∀i∈1…NE⁡i=1−s⁢B⁡i+s⁢C⁡i
192 reeanv ⊢∃t∈01∃s∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧∀i∈1…NE⁡i=1−s⁢B⁡i+s⁢C⁡i↔∃t∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧∃s∈01∀i∈1…NE⁡i=1−s⁢B⁡i+s⁢C⁡i
193 191 192 bitri ⊢∃t∈01∃s∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧E⁡i=1−s⁢B⁡i+s⁢C⁡i↔∃t∈01∀i∈1…ND⁡i=1−t⁢A⁡i+t⁢C⁡i∧∃s∈01∀i∈1…NE⁡i=1−s⁢B⁡i+s⁢C⁡i
194 189 193 bitr4di ⊢N∈ℕ∧A∈𝔼⁡N∧B∈𝔼⁡N∧C∈𝔼⁡N∧D∈𝔼⁡N∧E∈𝔼⁡N→DBtwnAC∧EBtwnBC↔∃t∈01∃s∈01∀i∈1…ND⁡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→xBtwnDB↔∃r∈01∀i∈1…Nx⁡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→xBtwnDB↔∃r∈01∀i∈1…Nx⁡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→xBtwnEA↔∃q∈01∀i∈1…Nx⁡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→xBtwnEA↔∃q∈01∀i∈1…Nx⁡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→xBtwnDB∧xBtwnEA↔∃r∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧∃q∈01∀i∈1…Nx⁡i=1−q⁢E⁡i+q⁢A⁡i
205 r19.26 ⊢∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧x⁡i=1−q⁢E⁡i+q⁢A⁡i↔∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧∀i∈1…Nx⁡i=1−q⁢E⁡i+q⁢A⁡i
206 205 2rexbii ⊢∃r∈01∃q∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧x⁡i=1−q⁢E⁡i+q⁢A⁡i↔∃r∈01∃q∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧∀i∈1…Nx⁡i=1−q⁢E⁡i+q⁢A⁡i
207 reeanv ⊢∃r∈01∃q∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧∀i∈1…Nx⁡i=1−q⁢E⁡i+q⁢A⁡i↔∃r∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧∃q∈01∀i∈1…Nx⁡i=1−q⁢E⁡i+q⁢A⁡i
208 206 207 bitri ⊢∃r∈01∃q∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧x⁡i=1−q⁢E⁡i+q⁢A⁡i↔∃r∈01∀i∈1…Nx⁡i=1−r⁢D⁡i+r⁢B⁡i∧∃q∈01∀i∈1…Nx⁡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→xBtwnDB∧xBtwnEA↔∃r∈01∃q∈01∀i∈1…Nx⁡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∈𝔼⁡NxBtwnDB∧xBtwnEA↔∃x∈𝔼⁡N∃r∈01∃q∈01∀i∈1…Nx⁡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→DBtwnAC∧EBtwnBC→∃x∈𝔼⁡NxBtwnDB∧xBtwnEA