Beginning of Section Conj_mul_SNo_Lt__23__10

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo z

Hypothesis H2 : SNo w

Hypothesis H3 : SNo (x * y)

Hypothesis H4 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H5 : SNo (z * y)

Hypothesis H6 : SNo (x * w)

Hypothesis H7 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H8 : SNo (z * w)

Hypothesis H9 : SNo (z * y + x * w)

Hypothesis H11 : z ∈ SNoL x

Hypothesis H12 : SNo u

Hypothesis H13 : w < u

Hypothesis H14 : SNoLev u ∈ SNoLev w

Hypothesis H15 : u ∈ SNoL y

Theorem. (Conj_mul_SNo_Lt__23__10)

u ∈ SNoR w → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 470ad9... and proposition id is 63f307...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__23__10

Beginning of Section Conj_mul_SNo_Lt__24__6

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : SNo (x * y)

Hypothesis H5 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (x * w)

Hypothesis H8 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H9 : SNo (z * w)

Hypothesis H10 : SNo (z * y + x * w)

Hypothesis H11 : SNo (x * y + z * w)

Hypothesis H12 : z ∈ SNoL x

Hypothesis H13 : SNo u

Hypothesis H14 : w < u

Hypothesis H15 : u < y

Hypothesis H16 : SNoLev u ∈ SNoLev w

Hypothesis H17 : SNoLev u ∈ SNoLev y

Theorem. (Conj_mul_SNo_Lt__24__6)

u ∈ SNoL y → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 2e623a... and proposition id is 2bfa44...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__24__6

Beginning of Section Conj_mul_SNo_Lt__24__9

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : SNo (x * y)

Hypothesis H5 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H6 : SNo (z * y)

Hypothesis H7 : SNo (x * w)

Hypothesis H8 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H10 : SNo (z * y + x * w)

Hypothesis H11 : SNo (x * y + z * w)

Hypothesis H12 : z ∈ SNoL x

Hypothesis H13 : SNo u

Hypothesis H14 : w < u

Hypothesis H15 : u < y

Hypothesis H16 : SNoLev u ∈ SNoLev w

Hypothesis H17 : SNoLev u ∈ SNoLev y

Theorem. (Conj_mul_SNo_Lt__24__9)

u ∈ SNoL y → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 7a2d12... and proposition id is 341bad...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__24__9

Beginning of Section Conj_mul_SNo_Lt__26__4

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H5 : SNo (z * y + x * w)

Hypothesis H6 : SNo (x * y + z * w)

Hypothesis H7 : u ∈ SNoR z

Hypothesis H8 : SNo (u * y)

Hypothesis H9 : SNo (u * w)

Hypothesis H10 : SNo (z * w + u * y)

Hypothesis H11 : SNo (u * w + x * y)

Hypothesis H12 : SNo (x * w + u * y)

Hypothesis H13 : SNo (u * w + z * y)

Hypothesis H14 : y ∈ SNoR w

Hypothesis H15 : (x * w + u * y) < u * w + x * y

Theorem. (Conj_mul_SNo_Lt__26__4)

(u * w + z * y) < z * w + u * y → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 8b64f4... and proposition id is c49d57...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__26__4

Beginning of Section Conj_mul_SNo_Lt__27__13

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H4 : SNo (z * w)

Hypothesis H5 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H6 : SNo (z * y + x * w)

Hypothesis H7 : SNo (x * y + z * w)

Hypothesis H8 : u ∈ SNoL x

Hypothesis H9 : u ∈ SNoR z

Hypothesis H10 : SNo (u * y)

Hypothesis H11 : SNo (u * w)

Hypothesis H12 : SNo (z * w + u * y)

Hypothesis H14 : SNo (x * w + u * y)

Hypothesis H15 : SNo (u * w + z * y)

Hypothesis H16 : y ∈ SNoR w

Theorem. (Conj_mul_SNo_Lt__27__13)

(x * w + u * y) < u * w + x * y → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is c6344f... and proposition id is 2688d7...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__27__13

Beginning of Section Conj_mul_SNo_Lt__29__0

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H3 : SNo (x * w)

Hypothesis H4 : SNo (z * w)

Hypothesis H5 : SNo (z * y + x * w)

Hypothesis H6 : SNo (x * y + z * w)

Hypothesis H7 : u ∈ SNoR z

Hypothesis H8 : SNo (u * y)

Hypothesis H9 : SNo (u * w)

Hypothesis H10 : SNo (u * y + x * w)

Hypothesis H11 : SNo (u * y + z * w)

Hypothesis H12 : SNo (x * y + u * w)

Hypothesis H13 : SNo (z * y + u * w)

Hypothesis H14 : w ∈ SNoL y

Hypothesis H15 : (u * y + x * w) < x * y + u * w

Theorem. (Conj_mul_SNo_Lt__29__0)

(z * y + u * w) < u * y + z * w → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 613dc4... and proposition id is 47c069...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__29__0

Beginning of Section Conj_mul_SNo_Lt__29__6

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H3 : SNo (x * w)

Hypothesis H4 : SNo (z * w)

Hypothesis H5 : SNo (z * y + x * w)

Hypothesis H7 : u ∈ SNoR z

Hypothesis H8 : SNo (u * y)

Hypothesis H9 : SNo (u * w)

Hypothesis H10 : SNo (u * y + x * w)

Hypothesis H11 : SNo (u * y + z * w)

Hypothesis H12 : SNo (x * y + u * w)

Hypothesis H13 : SNo (z * y + u * w)

Hypothesis H14 : w ∈ SNoL y

Hypothesis H15 : (u * y + x * w) < x * y + u * w

Theorem. (Conj_mul_SNo_Lt__29__6)

(z * y + u * w) < u * y + z * w → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 29b223... and proposition id is ee4bd8...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__29__6

Beginning of Section Conj_mul_SNo_Lt__29__10

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H3 : SNo (x * w)

Hypothesis H4 : SNo (z * w)

Hypothesis H5 : SNo (z * y + x * w)

Hypothesis H6 : SNo (x * y + z * w)

Hypothesis H7 : u ∈ SNoR z

Hypothesis H8 : SNo (u * y)

Hypothesis H9 : SNo (u * w)

Hypothesis H11 : SNo (u * y + z * w)

Hypothesis H12 : SNo (x * y + u * w)

Hypothesis H13 : SNo (z * y + u * w)

Hypothesis H14 : w ∈ SNoL y

Hypothesis H15 : (u * y + x * w) < x * y + u * w

Theorem. (Conj_mul_SNo_Lt__29__10)

(z * y + u * w) < u * y + z * w → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is ce4345... and proposition id is 82e9e4...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__29__10

Beginning of Section Conj_mul_SNo_Lt__31__9

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo y

Hypothesis H1 : SNo w

Hypothesis H2 : w < y

Hypothesis H3 : SNo (x * y)

Hypothesis H4 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H5 : SNo (z * y)

Hypothesis H6 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H7 : SNo (x * w)

Hypothesis H8 : SNo (z * w)

Hypothesis H10 : SNo (x * y + z * w)

Hypothesis H11 : u ∈ SNoL x

Hypothesis H12 : u ∈ SNoR z

Hypothesis H13 : SNo (u * y)

Hypothesis H14 : SNo (u * w)

Hypothesis H15 : SNo (u * y + x * w)

Hypothesis H16 : SNo (u * y + z * w)

Hypothesis H17 : SNo (x * y + u * w)

Hypothesis H18 : SNo (z * y + u * w)

Hypothesis H19 : SNoLev w ∈ SNoLev y

Theorem. (Conj_mul_SNo_Lt__31__9)

w ∈ SNoL y → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 55d6c9... and proposition id is b8cac6...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__31__9

Beginning of Section Conj_mul_SNo_Lt__32__13

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H18 : SNo (z * y + u * v)

Hypothesis H19 : SNo (x * w + u * v)

Hypothesis H20 : SNo (u * w + z * v)

Hypothesis H21 : SNo (u * y + x * v)

Hypothesis H22 : SNo (x * y + u * v)

Theorem. (Conj_mul_SNo_Lt__32__13)

SNo (z * w + u * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is d71cf3... and proposition id is 060be0...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__32__13

Beginning of Section Conj_mul_SNo_Lt__33__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H18 : SNo (z * y + u * v)

Hypothesis H19 : SNo (x * w + u * v)

Hypothesis H20 : SNo (u * w + z * v)

Hypothesis H21 : SNo (u * y + x * v)

Theorem. (Conj_mul_SNo_Lt__33__2)

SNo (x * y + u * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is 455322... and proposition id is ab71e3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__33__2

Beginning of Section Conj_mul_SNo_Lt__33__21

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H18 : SNo (z * y + u * v)

Hypothesis H19 : SNo (x * w + u * v)

Hypothesis H20 : SNo (u * w + z * v)

Theorem. (Conj_mul_SNo_Lt__33__21)

SNo (x * y + u * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is 7bd88f... and proposition id is a62a05...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__33__21

Beginning of Section Conj_mul_SNo_Lt__34__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H18 : SNo (z * y + u * v)

Hypothesis H19 : SNo (x * w + u * v)

Hypothesis H20 : SNo (u * w + z * v)

Theorem. (Conj_mul_SNo_Lt__34__7)

SNo (u * y + x * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is 2bbeee... and proposition id is 9ada80...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__34__7

Beginning of Section Conj_mul_SNo_Lt__35__7

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H18 : SNo (z * y + u * v)

Hypothesis H19 : SNo (x * w + u * v)

Hypothesis H20 : SNo (u * w + z * v)

Theorem. (Conj_mul_SNo_Lt__35__7)

SNo (x * y + x * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is ea7056... and proposition id is fe94c2...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__35__7

Beginning of Section Conj_mul_SNo_Lt__35__18

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H19 : SNo (x * w + u * v)

Hypothesis H20 : SNo (u * w + z * v)

Theorem. (Conj_mul_SNo_Lt__35__18)

SNo (x * y + x * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is de8939... and proposition id is 1ec8d1...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__35__18

Beginning of Section Conj_mul_SNo_Lt__36__19

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H18 : SNo (z * y + u * v)

Theorem. (Conj_mul_SNo_Lt__36__19)

SNo (u * w + z * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is d2a442... and proposition id is ec348c...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__36__19

Beginning of Section Conj_mul_SNo_Lt__37__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Hypothesis H18 : SNo (z * y + u * v)

Theorem. (Conj_mul_SNo_Lt__37__3)

SNo (x * w + u * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is c81e74... and proposition id is 43eb45...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__37__3

Beginning of Section Conj_mul_SNo_Lt__37__17

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H18 : SNo (z * y + u * v)

Theorem. (Conj_mul_SNo_Lt__37__17)

SNo (x * w + u * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is 92329e... and proposition id is 89b243...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__37__17

Beginning of Section Conj_mul_SNo_Lt__38__15

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H16 : SNo (u * y + z * v)

Hypothesis H17 : SNo (u * w + x * v)

Theorem. (Conj_mul_SNo_Lt__38__15)

SNo (z * y + u * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is 2237d1... and proposition id is ddb245...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__38__15

Beginning of Section Conj_mul_SNo_Lt__39__12

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Hypothesis H16 : SNo (u * y + z * v)

Theorem. (Conj_mul_SNo_Lt__39__12)

SNo (u * w + x * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is 63dabc... and proposition id is 9e443f...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__39__12

Beginning of Section Conj_mul_SNo_Lt__40__13

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Hypothesis H15 : SNo (u * v + u * v)

Theorem. (Conj_mul_SNo_Lt__40__13)

SNo (u * y + z * v) → ((z * y + x * w) + u * v + u * v) < (x * y + z * w) + u * v + u * v

In Proofgold the corresponding term root is ba378f... and proposition id is 09451a...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__40__13

Beginning of Section Conj_mul_SNo_Lt__41__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H2 : SNo (x * w)

Hypothesis H3 : SNo (z * w)

Hypothesis H4 : SNo (z * y + x * w)

Hypothesis H5 : SNo (x * y + z * w)

Hypothesis H6 : SNo (u * y)

Hypothesis H7 : SNo (u * w)

Hypothesis H8 : SNo (x * v)

Hypothesis H9 : SNo (z * v)

Hypothesis H10 : SNo (u * v)

Hypothesis H11 : (u * y + x * v) < x * y + u * v

Hypothesis H12 : (u * w + z * v) < z * w + u * v

Hypothesis H13 : (x * w + u * v) < u * w + x * v

Hypothesis H14 : (z * y + u * v) < u * y + z * v

Theorem. (Conj_mul_SNo_Lt__41__1)

SNo (u * v + u * v) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is cc2d9e... and proposition id is a5eba2...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__41__1

Beginning of Section Conj_mul_SNo_Lt__42__12

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H3 : SNo (x * w)

Hypothesis H4 : SNo (z * w)

Hypothesis H5 : SNo (z * y + x * w)

Hypothesis H6 : SNo (x * y + z * w)

Hypothesis H7 : u ∈ SNoR z

Hypothesis H8 : SNo (u * y)

Hypothesis H9 : SNo (u * w)

Hypothesis H10 : v ∈ SNoL y

Hypothesis H11 : SNo (x * v)

Hypothesis H13 : SNo (u * v)

Hypothesis H14 : (u * y + x * v) < x * y + u * v

Hypothesis H15 : (u * w + z * v) < z * w + u * v

Hypothesis H16 : (x * w + u * v) < u * w + x * v

Theorem. (Conj_mul_SNo_Lt__42__12)

(z * y + u * v) < u * y + z * v → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is d78767... and proposition id is 657cc6...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__42__12

Beginning of Section Conj_mul_SNo_Lt__44__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H2 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H3 : SNo (x * w)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR w → (x * w + x2 * y2) < x2 * w + x * y2))

Hypothesis H5 : SNo (z * w)

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoR w → (x2 * w + z * y2) < z * w + x2 * y2))

Hypothesis H7 : SNo (z * y + x * w)

Hypothesis H8 : SNo (x * y + z * w)

Hypothesis H9 : u ∈ SNoL x

Hypothesis H10 : u ∈ SNoR z

Hypothesis H11 : SNo (u * y)

Hypothesis H12 : SNo (u * w)

Hypothesis H13 : v ∈ SNoL y

Hypothesis H14 : v ∈ SNoR w

Hypothesis H15 : SNo (x * v)

Hypothesis H16 : SNo (z * v)

Hypothesis H17 : SNo (u * v)

Hypothesis H18 : (u * y + x * v) < x * y + u * v

Theorem. (Conj_mul_SNo_Lt__44__1)

(u * w + z * v) < z * w + u * v → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 0d724e... and proposition id is f5c363...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__44__1

Beginning of Section Conj_mul_SNo_Lt__44__18

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo (x * y)

Hypothesis H1 : SNo (z * y)

Hypothesis H2 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H3 : SNo (x * w)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR w → (x * w + x2 * y2) < x2 * w + x * y2))

Hypothesis H5 : SNo (z * w)

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoR w → (x2 * w + z * y2) < z * w + x2 * y2))

Hypothesis H7 : SNo (z * y + x * w)

Hypothesis H8 : SNo (x * y + z * w)

Hypothesis H9 : u ∈ SNoL x

Hypothesis H10 : u ∈ SNoR z

Hypothesis H11 : SNo (u * y)

Hypothesis H12 : SNo (u * w)

Hypothesis H13 : v ∈ SNoL y

Hypothesis H14 : v ∈ SNoR w

Hypothesis H15 : SNo (x * v)

Hypothesis H16 : SNo (z * v)

Hypothesis H17 : SNo (u * v)

Theorem. (Conj_mul_SNo_Lt__44__18)

(u * w + z * v) < z * w + u * v → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 4f77de... and proposition id is 5bbd27...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__44__18

Beginning of Section Conj_mul_SNo_Lt__48__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo z

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → (x2 * y + x * y2) < x * y + x2 * y2))

Hypothesis H4 : SNo (z * y)

Hypothesis H5 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H6 : SNo (x * w)

Hypothesis H7 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR w → (x * w + x2 * y2) < x2 * w + x * y2))

Hypothesis H8 : SNo (z * w)

Hypothesis H9 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoR w → (x2 * w + z * y2) < z * w + x2 * y2))

Hypothesis H10 : SNo (z * y + x * w)

Hypothesis H11 : SNo (x * y + z * w)

Hypothesis H12 : SNo u

Hypothesis H13 : u ∈ SNoL x

Hypothesis H14 : u ∈ SNoR z

Hypothesis H15 : SNo (u * y)

Hypothesis H16 : SNo (u * w)

Hypothesis H17 : SNo v

Hypothesis H18 : v ∈ SNoL y

Hypothesis H19 : v ∈ SNoR w

Theorem. (Conj_mul_SNo_Lt__48__2)

SNo (x * v) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 8ee58f... and proposition id is 313339...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__48__2

Beginning of Section Conj_mul_SNo_Lt__49__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo w

Hypothesis H3 : SNo (x * y)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → (x2 * y + x * y2) < x * y + x2 * y2))

Hypothesis H5 : SNo (z * y)

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H7 : SNo (x * w)

Hypothesis H8 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR w → (x * w + x2 * y2) < x2 * w + x * y2))

Hypothesis H9 : SNo (z * w)

Hypothesis H10 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoR w → (x2 * w + z * y2) < z * w + x2 * y2))

Hypothesis H11 : SNo (z * y + x * w)

Hypothesis H12 : SNo (x * y + z * w)

Hypothesis H13 : SNo u

Hypothesis H14 : u ∈ SNoL x

Hypothesis H15 : u ∈ SNoR z

Hypothesis H16 : SNo (u * y)

Hypothesis H17 : SNo (u * w)

Hypothesis H18 : SNo v

Hypothesis H19 : w < v

Hypothesis H20 : SNoLev v ∈ SNoLev w

Hypothesis H21 : v ∈ SNoL y

Theorem. (Conj_mul_SNo_Lt__49__1)

v ∈ SNoR w → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 9ad680... and proposition id is 65ec26...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__49__1

Beginning of Section Conj_mul_SNo_Lt__49__12

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo z

Hypothesis H2 : SNo w

Hypothesis H3 : SNo (x * y)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → (x2 * y + x * y2) < x * y + x2 * y2))

Hypothesis H5 : SNo (z * y)

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H7 : SNo (x * w)

Hypothesis H8 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR w → (x * w + x2 * y2) < x2 * w + x * y2))

Hypothesis H9 : SNo (z * w)

Hypothesis H10 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoR w → (x2 * w + z * y2) < z * w + x2 * y2))

Hypothesis H11 : SNo (z * y + x * w)

Hypothesis H13 : SNo u

Hypothesis H14 : u ∈ SNoL x

Hypothesis H15 : u ∈ SNoR z

Hypothesis H16 : SNo (u * y)

Hypothesis H17 : SNo (u * w)

Hypothesis H18 : SNo v

Hypothesis H19 : w < v

Hypothesis H20 : SNoLev v ∈ SNoLev w

Hypothesis H21 : v ∈ SNoL y

Theorem. (Conj_mul_SNo_Lt__49__12)

v ∈ SNoR w → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 961d01... and proposition id is fd1b61...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__49__12

Beginning of Section Conj_mul_SNo_Lt__49__20

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo z

Hypothesis H2 : SNo w

Hypothesis H3 : SNo (x * y)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → (x2 * y + x * y2) < x * y + x2 * y2))

Hypothesis H5 : SNo (z * y)

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H7 : SNo (x * w)

Hypothesis H8 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR w → (x * w + x2 * y2) < x2 * w + x * y2))

Hypothesis H9 : SNo (z * w)

Hypothesis H10 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoR w → (x2 * w + z * y2) < z * w + x2 * y2))

Hypothesis H11 : SNo (z * y + x * w)

Hypothesis H12 : SNo (x * y + z * w)

Hypothesis H13 : SNo u

Hypothesis H14 : u ∈ SNoL x

Hypothesis H15 : u ∈ SNoR z

Hypothesis H16 : SNo (u * y)

Hypothesis H17 : SNo (u * w)

Hypothesis H18 : SNo v

Hypothesis H19 : w < v

Hypothesis H21 : v ∈ SNoL y

Theorem. (Conj_mul_SNo_Lt__49__20)

v ∈ SNoR w → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 5c12cd... and proposition id is 2f413b...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__49__20

Beginning of Section Conj_mul_SNo_Lt__50__16

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : SNo (x * y)

Hypothesis H5 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → (x2 * y + x * y2) < x * y + x2 * y2))

Hypothesis H6 : SNo (z * y)

Hypothesis H7 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoL y → (z * y + x2 * y2) < x2 * y + z * y2))

Hypothesis H8 : SNo (x * w)

Hypothesis H9 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR w → (x * w + x2 * y2) < x2 * w + x * y2))

Hypothesis H10 : SNo (z * w)

Hypothesis H11 : (∀x2 : set, x2 ∈ SNoR z → (∀y2 : set, y2 ∈ SNoR w → (x2 * w + z * y2) < z * w + x2 * y2))

Hypothesis H12 : SNo (z * y + x * w)

Hypothesis H13 : SNo (x * y + z * w)

Hypothesis H14 : SNo u

Hypothesis H15 : u ∈ SNoL x

Hypothesis H17 : SNo (u * y)

Hypothesis H18 : SNo (u * w)

Hypothesis H19 : SNo v

Hypothesis H20 : w < v

Hypothesis H21 : v < y

Hypothesis H22 : SNoLev v ∈ SNoLev w

Hypothesis H23 : SNoLev v ∈ SNoLev y

Theorem. (Conj_mul_SNo_Lt__50__16)

v ∈ SNoL y → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is c33c01... and proposition id is f63d4e...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__50__16

Beginning of Section Conj_mul_SNo_Lt__52__23

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Hypothesis H21 : SNo (u * y + z * w)

Hypothesis H22 : SNo (x * y + u * w)

Hypothesis H24 : SNo (z * w + u * y)

Hypothesis H25 : SNo (u * w + x * y)

Theorem. (Conj_mul_SNo_Lt__52__23)

SNo (x * w + u * y) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is ba2a42... and proposition id is 136d67...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__52__23

Beginning of Section Conj_mul_SNo_Lt__53__23

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Hypothesis H21 : SNo (u * y + z * w)

Hypothesis H22 : SNo (x * y + u * w)

Hypothesis H24 : SNo (z * w + u * y)

Theorem. (Conj_mul_SNo_Lt__53__23)

SNo (u * w + x * y) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is d387dc... and proposition id is b9d05d...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__53__23

Beginning of Section Conj_mul_SNo_Lt__53__24

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Hypothesis H21 : SNo (u * y + z * w)

Hypothesis H22 : SNo (x * y + u * w)

Hypothesis H23 : SNo (z * y + u * w)

Theorem. (Conj_mul_SNo_Lt__53__24)

SNo (u * w + x * y) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is b1f40a... and proposition id is 34c999...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__53__24

Beginning of Section Conj_mul_SNo_Lt__54__4

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Hypothesis H21 : SNo (u * y + z * w)

Hypothesis H22 : SNo (x * y + u * w)

Hypothesis H23 : SNo (z * y + u * w)

Theorem. (Conj_mul_SNo_Lt__54__4)

SNo (z * w + u * y) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 0c4dc0... and proposition id is 997f7f...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__54__4

Beginning of Section Conj_mul_SNo_Lt__54__22

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Hypothesis H21 : SNo (u * y + z * w)

Hypothesis H23 : SNo (z * y + u * w)

Theorem. (Conj_mul_SNo_Lt__54__22)

SNo (z * w + u * y) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 38e09f... and proposition id is be0dfb...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__54__22

Beginning of Section Conj_mul_SNo_Lt__55__12

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Hypothesis H21 : SNo (u * y + z * w)

Hypothesis H22 : SNo (x * y + u * w)

Theorem. (Conj_mul_SNo_Lt__55__12)

SNo (z * y + u * w) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is cad011... and proposition id is 5e4d63...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__55__12

Beginning of Section Conj_mul_SNo_Lt__55__22

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Hypothesis H21 : SNo (u * y + z * w)

Theorem. (Conj_mul_SNo_Lt__55__22)

SNo (z * y + u * w) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is cf5038... and proposition id is aecd5b...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__55__22

Beginning of Section Conj_mul_SNo_Lt__57__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Theorem. (Conj_mul_SNo_Lt__57__1)

SNo (u * y + z * w) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 76d8ae... and proposition id is ce5ed5...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__57__1

Beginning of Section Conj_mul_SNo_Lt__57__6

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Theorem. (Conj_mul_SNo_Lt__57__6)

SNo (u * y + z * w) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is be7c12... and proposition id is 24c984...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__57__6

Beginning of Section Conj_mul_SNo_Lt__57__11

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Hypothesis H17 : u ∈ SNoR z

Hypothesis H18 : SNo (u * y)

Hypothesis H19 : SNo (u * w)

Hypothesis H20 : SNo (u * y + x * w)

Theorem. (Conj_mul_SNo_Lt__57__11)

SNo (u * y + z * w) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is e08e78... and proposition id is 989a98...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__57__11

Beginning of Section Conj_mul_SNo_Lt__60__17

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H14 : SNo (x * y + z * w)

Hypothesis H15 : SNo u

Hypothesis H16 : u ∈ SNoL x

Theorem. (Conj_mul_SNo_Lt__60__17)

SNo (u * y) → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is 36e597... and proposition id is 2200ac...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__60__17

Beginning of Section Conj_mul_SNo_Lt__61__14

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : SNo w

Hypothesis H4 : w < y

Hypothesis H5 : SNo (x * y)

Hypothesis H6 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoL y → (v * y + x * x2) < x * y + v * x2))

Hypothesis H7 : SNo (z * y)

Hypothesis H8 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoL y → (z * y + v * x2) < v * y + z * x2))

Hypothesis H9 : SNo (x * w)

Hypothesis H10 : (∀v : set, v ∈ SNoL x → (∀x2 : set, x2 ∈ SNoR w → (x * w + v * x2) < v * w + x * x2))

Hypothesis H11 : SNo (z * w)

Hypothesis H12 : (∀v : set, v ∈ SNoR z → (∀x2 : set, x2 ∈ SNoR w → (v * w + z * x2) < z * w + v * x2))

Hypothesis H13 : SNo (z * y + x * w)

Hypothesis H15 : SNo u

Hypothesis H16 : z < u

Hypothesis H17 : SNoLev u ∈ SNoLev z

Hypothesis H18 : u ∈ SNoL x

Theorem. (Conj_mul_SNo_Lt__61__14)

u ∈ SNoR z → (z * y + x * w) < x * y + z * w

In Proofgold the corresponding term root is cedaca... and proposition id is 3c1bf3...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_Lt__61__14

Beginning of Section Conj_mul_SNo_SNoL_interpolate__2__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoR y → (x2 * y + x * y2) < z + x2 * y2))

Hypothesis H4 : SNo w

Hypothesis H5 : z < w

Hypothesis H6 : u ∈ SNoR x

Hypothesis H7 : v ∈ SNoR y

Hypothesis H8 : (w + u * v) ≤ u * y + x * v

Hypothesis H9 : SNo u

Hypothesis H10 : SNo v

Hypothesis H11 : SNo (u * v)

Theorem. (Conj_mul_SNo_SNoL_interpolate__2__2)

(w + u * v) < z + u * v → x * y < w

In Proofgold the corresponding term root is cfae93... and proposition id is 509b2e...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__2__2

Beginning of Section Conj_mul_SNo_SNoL_interpolate__3__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo z

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoR y → (x2 * y + x * y2) < z + x2 * y2))

Hypothesis H4 : SNo w

Hypothesis H5 : z < w

Hypothesis H6 : u ∈ SNoR x

Hypothesis H7 : v ∈ SNoR y

Hypothesis H8 : (w + u * v) ≤ u * y + x * v

Hypothesis H9 : SNo u

Hypothesis H10 : SNo v

Theorem. (Conj_mul_SNo_SNoL_interpolate__3__1)

SNo (u * v) → x * y < w

In Proofgold the corresponding term root is cf24d5... and proposition id is 70acb8...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__3__1

Beginning of Section Conj_mul_SNo_SNoL_interpolate__3__2

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoR y → (x2 * y + x * y2) < z + x2 * y2))

Hypothesis H4 : SNo w

Hypothesis H5 : z < w

Hypothesis H6 : u ∈ SNoR x

Hypothesis H7 : v ∈ SNoR y

Hypothesis H8 : (w + u * v) ≤ u * y + x * v

Hypothesis H9 : SNo u

Hypothesis H10 : SNo v

Theorem. (Conj_mul_SNo_SNoL_interpolate__3__2)

SNo (u * v) → x * y < w

In Proofgold the corresponding term root is 0401c9... and proposition id is b91486...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__3__2

Beginning of Section Conj_mul_SNo_SNoL_interpolate__3__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoR y → (x2 * y + x * y2) < z + x2 * y2))

Hypothesis H4 : SNo w

Hypothesis H6 : u ∈ SNoR x

Hypothesis H7 : v ∈ SNoR y

Hypothesis H8 : (w + u * v) ≤ u * y + x * v

Hypothesis H9 : SNo u

Hypothesis H10 : SNo v

Theorem. (Conj_mul_SNo_SNoL_interpolate__3__5)

SNo (u * v) → x * y < w

In Proofgold the corresponding term root is 743c37... and proposition id is b71763...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__3__5

Beginning of Section Conj_mul_SNo_SNoL_interpolate__5__9

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → (x2 * y + x * y2) < z + x2 * y2))

Hypothesis H4 : SNo w

Hypothesis H5 : z < w

Hypothesis H6 : u ∈ SNoL x

Hypothesis H7 : v ∈ SNoL y

Hypothesis H8 : (w + u * v) ≤ u * y + x * v

Hypothesis H10 : SNo v

Hypothesis H11 : SNo (u * v)

Theorem. (Conj_mul_SNo_SNoL_interpolate__5__9)

(w + u * v) < z + u * v → x * y < w

In Proofgold the corresponding term root is 25b05d... and proposition id is 5101ed...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__5__9

Beginning of Section Conj_mul_SNo_SNoL_interpolate__7__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo (x * y)

Hypothesis H4 : (∀u : set, u ∈ SNoS_ (SNoLev z) → SNoLev u ∈ SNoLev (x * y) → u < x * y → (∃v : set, v ∈ SNoL x ∧ (∃x2 : set, x2 ∈ SNoL y ∧ (u + v * x2) ≤ v * y + x * x2)) ∨ (∃v : set, v ∈ SNoR x ∧ (∃x2 : set, x2 ∈ SNoR y ∧ (u + v * x2) ≤ v * y + x * x2)))

Hypothesis H5 : SNoLev z ∈ SNoLev (x * y)

Hypothesis H6 : (∀u : set, u ∈ SNoL x → (∀v : set, v ∈ SNoL y → (u * y + x * v) < z + u * v))

Hypothesis H7 : (∀u : set, u ∈ SNoR x → (∀v : set, v ∈ SNoR y → (u * y + x * v) < z + u * v))

Hypothesis H8 : SNo w

Hypothesis H9 : SNoLev w ∈ SNoLev z

Hypothesis H10 : z < w

Hypothesis H11 : w < x * y

Theorem. (Conj_mul_SNo_SNoL_interpolate__7__3)

(∃u : set, u ∈ SNoL x ∧ (∃v : set, v ∈ SNoL y ∧ (w + u * v) ≤ u * y + x * v)) ∨ (∃u : set, u ∈ SNoR x ∧ (∃v : set, v ∈ SNoR y ∧ (w + u * v) ≤ u * y + x * v)) → x * y < w

In Proofgold the corresponding term root is 206647... and proposition id is 98f4ce...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__7__3

Beginning of Section Conj_mul_SNo_SNoL_interpolate__8__1

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo (x * y)

Hypothesis H3 : SNo z

Hypothesis H4 : (∀w : set, w ∈ SNoS_ (SNoLev z) → SNoLev w ∈ SNoLev (x * y) → w < x * y → (∃u : set, u ∈ SNoL x ∧ (∃v : set, v ∈ SNoL y ∧ (w + u * v) ≤ u * y + x * v)) ∨ (∃u : set, u ∈ SNoR x ∧ (∃v : set, v ∈ SNoR y ∧ (w + u * v) ≤ u * y + x * v)))

Hypothesis H5 : SNoLev z ∈ SNoLev (x * y)

Hypothesis H6 : z < x * y

Hypothesis H7 : ¬ ((∃w : set, w ∈ SNoL x ∧ (∃u : set, u ∈ SNoL y ∧ (z + w * u) ≤ w * y + x * u)) ∨ (∃w : set, w ∈ SNoR x ∧ (∃u : set, u ∈ SNoR y ∧ (z + w * u) ≤ w * y + x * u)))

Hypothesis H8 : (∀w : set, w ∈ SNoL x → (∀u : set, u ∈ SNoL y → (w * y + x * u) < z + w * u))

Theorem. (Conj_mul_SNo_SNoL_interpolate__8__1)

¬ (∀w : set, w ∈ SNoR x → (∀u : set, u ∈ SNoR y → (w * y + x * u) < z + w * u))

In Proofgold the corresponding term root is af7aac... and proposition id is b6f48a...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__8__1

Beginning of Section Conj_mul_SNo_SNoL_interpolate__9__4

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo (x * y)

Hypothesis H3 : SNo z

Hypothesis H5 : SNoLev z ∈ SNoLev (x * y)

Hypothesis H6 : z < x * y

Theorem. (Conj_mul_SNo_SNoL_interpolate__9__4)

¬ (∀w : set, w ∈ SNoL x → (∀u : set, u ∈ SNoL y → (w * y + x * u) < z + w * u))

In Proofgold the corresponding term root is 184d4f... and proposition id is 5d8b86...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__9__4

Beginning of Section Conj_mul_SNo_SNoL_interpolate__11__0

Variable x : set

Variable y : set

Hypothesis H1 : SNo y

Theorem. (Conj_mul_SNo_SNoL_interpolate__11__0)

SNo (x * y) → (∀z : set, z ∈ SNoL (x * y) → (∃w : set, w ∈ SNoL x ∧ (∃u : set, u ∈ SNoL y ∧ (z + w * u) ≤ w * y + x * u)) ∨ (∃w : set, w ∈ SNoR x ∧ (∃u : set, u ∈ SNoR y ∧ (z + w * u) ≤ w * y + x * u)))

In Proofgold the corresponding term root is 61218f... and proposition id is 326888...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoL_interpolate__11__0

Beginning of Section Conj_mul_SNo_SNoR_interpolate__1__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo z

Hypothesis H1 : SNo w

Hypothesis H2 : w < z

Hypothesis H4 : (z + u * v) < w + u * v

Theorem. (Conj_mul_SNo_SNoR_interpolate__1__3)

z < w → w < x * y

In Proofgold the corresponding term root is ac1d32... and proposition id is 3cff72...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoR_interpolate__1__3

Beginning of Section Conj_mul_SNo_SNoR_interpolate__3__1

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H2 : SNo z

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoL y → (z + x2 * y2) < x2 * y + x * y2))

Hypothesis H4 : SNo w

Hypothesis H5 : w < z

Hypothesis H6 : u ∈ SNoR x

Hypothesis H7 : v ∈ SNoL y

Hypothesis H8 : (u * y + x * v) ≤ w + u * v

Hypothesis H9 : SNo u

Hypothesis H10 : SNo v

Theorem. (Conj_mul_SNo_SNoR_interpolate__3__1)

SNo (u * v) → w < x * y

In Proofgold the corresponding term root is d41b52... and proposition id is 8be274...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoR_interpolate__3__1

Beginning of Section Conj_mul_SNo_SNoR_interpolate__3__8

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoL y → (z + x2 * y2) < x2 * y + x * y2))

Hypothesis H4 : SNo w

Hypothesis H5 : w < z

Hypothesis H6 : u ∈ SNoR x

Hypothesis H7 : v ∈ SNoL y

Hypothesis H9 : SNo u

Hypothesis H10 : SNo v

Theorem. (Conj_mul_SNo_SNoR_interpolate__3__8)

SNo (u * v) → w < x * y

In Proofgold the corresponding term root is 9ad7f7... and proposition id is fbb77a...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoR_interpolate__3__8

Beginning of Section Conj_mul_SNo_SNoR_interpolate__4__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo z

Hypothesis H1 : SNo w

Hypothesis H2 : w < z

Hypothesis H4 : (z + u * v) < w + u * v

Theorem. (Conj_mul_SNo_SNoR_interpolate__4__3)

z < w → w < x * y

In Proofgold the corresponding term root is ac1d32... and proposition id is 3cff72...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoR_interpolate__4__3

Beginning of Section Conj_mul_SNo_SNoR_interpolate__6__4

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo z

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR y → (z + x2 * y2) < x2 * y + x * y2))

Hypothesis H5 : w < z

Hypothesis H6 : u ∈ SNoL x

Hypothesis H7 : v ∈ SNoR y

Hypothesis H8 : (u * y + x * v) ≤ w + u * v

Hypothesis H9 : SNo u

Hypothesis H10 : SNo v

Theorem. (Conj_mul_SNo_SNoR_interpolate__6__4)

SNo (u * v) → w < x * y

In Proofgold the corresponding term root is 7d9860... and proposition id is 912f6c...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoR_interpolate__6__4

Beginning of Section Conj_mul_SNo_SNoR_interpolate__7__3

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : SNo (x * y)

Hypothesis H4 : (∀u : set, u ∈ SNoS_ (SNoLev z) → SNoLev u ∈ SNoLev (x * y) → x * y < u → (∃v : set, v ∈ SNoL x ∧ (∃x2 : set, x2 ∈ SNoR y ∧ (v * y + x * x2) ≤ u + v * x2)) ∨ (∃v : set, v ∈ SNoR x ∧ (∃x2 : set, x2 ∈ SNoL y ∧ (v * y + x * x2) ≤ u + v * x2)))

Hypothesis H5 : SNoLev z ∈ SNoLev (x * y)

Hypothesis H6 : (∀u : set, u ∈ SNoL x → (∀v : set, v ∈ SNoR y → (z + u * v) < u * y + x * v))

Hypothesis H7 : (∀u : set, u ∈ SNoR x → (∀v : set, v ∈ SNoL y → (z + u * v) < u * y + x * v))

Hypothesis H8 : SNo w

Hypothesis H9 : SNoLev w ∈ SNoLev z

Hypothesis H10 : w < z

Hypothesis H11 : x * y < w

Theorem. (Conj_mul_SNo_SNoR_interpolate__7__3)

(∃u : set, u ∈ SNoL x ∧ (∃v : set, v ∈ SNoR y ∧ (u * y + x * v) ≤ w + u * v)) ∨ (∃u : set, u ∈ SNoR x ∧ (∃v : set, v ∈ SNoL y ∧ (u * y + x * v) ≤ w + u * v)) → w < x * y

In Proofgold the corresponding term root is d39608... and proposition id is 642030...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoR_interpolate__7__3

Beginning of Section Conj_mul_SNo_SNoR_interpolate__8__2

Variable x : set

Variable y : set

Variable z : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H3 : SNo z

Hypothesis H4 : (∀w : set, w ∈ SNoS_ (SNoLev z) → SNoLev w ∈ SNoLev (x * y) → x * y < w → (∃u : set, u ∈ SNoL x ∧ (∃v : set, v ∈ SNoR y ∧ (u * y + x * v) ≤ w + u * v)) ∨ (∃u : set, u ∈ SNoR x ∧ (∃v : set, v ∈ SNoL y ∧ (u * y + x * v) ≤ w + u * v)))

Hypothesis H5 : SNoLev z ∈ SNoLev (x * y)

Hypothesis H6 : x * y < z

Hypothesis H7 : ¬ ((∃w : set, w ∈ SNoL x ∧ (∃u : set, u ∈ SNoR y ∧ (w * y + x * u) ≤ z + w * u)) ∨ (∃w : set, w ∈ SNoR x ∧ (∃u : set, u ∈ SNoL y ∧ (w * y + x * u) ≤ z + w * u)))

Hypothesis H8 : (∀w : set, w ∈ SNoL x → (∀u : set, u ∈ SNoR y → (z + w * u) < w * y + x * u))

Theorem. (Conj_mul_SNo_SNoR_interpolate__8__2)

¬ (∀w : set, w ∈ SNoR x → (∀u : set, u ∈ SNoL y → (z + w * u) < w * y + x * u))

In Proofgold the corresponding term root is babb0e... and proposition id is 69be7a...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_SNoR_interpolate__8__2

Beginning of Section Conj_mul_SNo_oneR__3__0

Variable x : set

Variable y : set

Hypothesis H1 : (∀z : set, z ∈ SNoL x → (∀w : set, w ∈ SNoL (ordsucc Empty) → (z * ordsucc Empty + x * w) < x * ordsucc Empty + z * w))

Hypothesis H2 : Empty ∈ SNoL (ordsucc Empty)

Hypothesis H3 : y ∈ SNoL x

Hypothesis H4 : SNo y

Hypothesis H5 : y * ordsucc Empty + x * Empty = y

Theorem. (Conj_mul_SNo_oneR__3__0)

x * ordsucc Empty + y * Empty = x * ordsucc Empty → y < x * ordsucc Empty

In Proofgold the corresponding term root is 078312... and proposition id is 59fb31...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_oneR__3__0

Beginning of Section Conj_mul_SNo_com__1__0

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H1 : SNo y

Hypothesis H2 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → x2 * y = y * x2)

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → x * x2 = x2 * x)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → (∀y2 : set, y2 ∈ SNoS_ (SNoLev y) → x2 * y2 = y2 * x2))

Hypothesis H5 : (∀x2 : set, x2 ∈ w → (∀P : prop, (∀y2 : set, y2 ∈ SNoL x → (∀z2 : set, z2 ∈ SNoR y → x2 = y2 * y + x * z2 + - (y2 * z2) → P)) → (∀y2 : set, y2 ∈ SNoR x → (∀z2 : set, z2 ∈ SNoL y → x2 = y2 * y + x * z2 + - (y2 * z2) → P)) → P))

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR y → x2 * y + x * y2 + - (x2 * y2) ∈ w))

Hypothesis H7 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoL y → x2 * y + x * y2 + - (x2 * y2) ∈ w))

Hypothesis H8 : (∀x2 : set, x2 ∈ v → (∀P : prop, (∀y2 : set, y2 ∈ SNoL y → (∀z2 : set, z2 ∈ SNoR x → x2 = y2 * x + y * z2 + - (y2 * z2) → P)) → (∀y2 : set, y2 ∈ SNoR y → (∀z2 : set, z2 ∈ SNoL x → x2 = y2 * x + y * z2 + - (y2 * z2) → P)) → P))

Hypothesis H9 : (∀x2 : set, x2 ∈ SNoL y → (∀y2 : set, y2 ∈ SNoR x → x2 * x + y * y2 + - (x2 * y2) ∈ v))

Hypothesis H10 : (∀x2 : set, x2 ∈ SNoR y → (∀y2 : set, y2 ∈ SNoL x → x2 * x + y * y2 + - (x2 * y2) ∈ v))

Hypothesis H11 : z = u

Theorem. (Conj_mul_SNo_com__1__0)

w = v → SNoCut z w = SNoCut u v

In Proofgold the corresponding term root is 107a29... and proposition id is 7b761e...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_com__1__0

Beginning of Section Conj_mul_SNo_com__2__5

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → x2 * y = y * x2)

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → x * x2 = x2 * x)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → (∀y2 : set, y2 ∈ SNoS_ (SNoLev y) → x2 * y2 = y2 * x2))

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → x2 * y + x * y2 + - (x2 * y2) ∈ z))

Hypothesis H7 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoR y → x2 * y + x * y2 + - (x2 * y2) ∈ z))

Hypothesis H8 : (∀x2 : set, x2 ∈ w → (∀P : prop, (∀y2 : set, y2 ∈ SNoL x → (∀z2 : set, z2 ∈ SNoR y → x2 = y2 * y + x * z2 + - (y2 * z2) → P)) → (∀y2 : set, y2 ∈ SNoR x → (∀z2 : set, z2 ∈ SNoL y → x2 = y2 * y + x * z2 + - (y2 * z2) → P)) → P))

Hypothesis H9 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoR y → x2 * y + x * y2 + - (x2 * y2) ∈ w))

Hypothesis H10 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoL y → x2 * y + x * y2 + - (x2 * y2) ∈ w))

Hypothesis H11 : (∀x2 : set, x2 ∈ u → (∀P : prop, (∀y2 : set, y2 ∈ SNoL y → (∀z2 : set, z2 ∈ SNoL x → x2 = y2 * x + y * z2 + - (y2 * z2) → P)) → (∀y2 : set, y2 ∈ SNoR y → (∀z2 : set, z2 ∈ SNoR x → x2 = y2 * x + y * z2 + - (y2 * z2) → P)) → P))

Hypothesis H12 : (∀x2 : set, x2 ∈ SNoL y → (∀y2 : set, y2 ∈ SNoL x → x2 * x + y * y2 + - (x2 * y2) ∈ u))

Hypothesis H13 : (∀x2 : set, x2 ∈ SNoR y → (∀y2 : set, y2 ∈ SNoR x → x2 * x + y * y2 + - (x2 * y2) ∈ u))

Hypothesis H14 : (∀x2 : set, x2 ∈ v → (∀P : prop, (∀y2 : set, y2 ∈ SNoL y → (∀z2 : set, z2 ∈ SNoR x → x2 = y2 * x + y * z2 + - (y2 * z2) → P)) → (∀y2 : set, y2 ∈ SNoR y → (∀z2 : set, z2 ∈ SNoL x → x2 = y2 * x + y * z2 + - (y2 * z2) → P)) → P))

Hypothesis H15 : (∀x2 : set, x2 ∈ SNoL y → (∀y2 : set, y2 ∈ SNoR x → x2 * x + y * y2 + - (x2 * y2) ∈ v))

Hypothesis H16 : (∀x2 : set, x2 ∈ SNoR y → (∀y2 : set, y2 ∈ SNoL x → x2 * x + y * y2 + - (x2 * y2) ∈ v))

Theorem. (Conj_mul_SNo_com__2__5)

z = u → SNoCut z w = SNoCut u v

In Proofgold the corresponding term root is 886af3... and proposition id is 9f7679...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_com__2__5

Beginning of Section Conj_mul_SNo_com__2__9

Variable x : set

Variable y : set

Variable z : set

Variable w : set

Variable u : set

Variable v : set

Hypothesis H0 : SNo x

Hypothesis H1 : SNo y

Hypothesis H2 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → x2 * y = y * x2)

Hypothesis H3 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev y) → x * x2 = x2 * x)

Hypothesis H4 : (∀x2 : set, x2 ∈ SNoS_ (SNoLev x) → (∀y2 : set, y2 ∈ SNoS_ (SNoLev y) → x2 * y2 = y2 * x2))

Hypothesis H5 : (∀x2 : set, x2 ∈ z → (∀P : prop, (∀y2 : set, y2 ∈ SNoL x → (∀z2 : set, z2 ∈ SNoL y → x2 = y2 * y + x * z2 + - (y2 * z2) → P)) → (∀y2 : set, y2 ∈ SNoR x → (∀z2 : set, z2 ∈ SNoR y → x2 = y2 * y + x * z2 + - (y2 * z2) → P)) → P))

Hypothesis H6 : (∀x2 : set, x2 ∈ SNoL x → (∀y2 : set, y2 ∈ SNoL y → x2 * y + x * y2 + - (x2 * y2) ∈ z))

Hypothesis H7 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoR y → x2 * y + x * y2 + - (x2 * y2) ∈ z))

Hypothesis H10 : (∀x2 : set, x2 ∈ SNoR x → (∀y2 : set, y2 ∈ SNoL y → x2 * y + x * y2 + - (x2 * y2) ∈ w))

Hypothesis H12 : (∀x2 : set, x2 ∈ SNoL y → (∀y2 : set, y2 ∈ SNoL x → x2 * x + y * y2 + - (x2 * y2) ∈ u))

Hypothesis H13 : (∀x2 : set, x2 ∈ SNoR y → (∀y2 : set, y2 ∈ SNoR x → x2 * x + y * y2 + - (x2 * y2) ∈ u))

Hypothesis H15 : (∀x2 : set, x2 ∈ SNoL y → (∀y2 : set, y2 ∈ SNoR x → x2 * x + y * y2 + - (x2 * y2) ∈ v))

Hypothesis H16 : (∀x2 : set, x2 ∈ SNoR y → (∀y2 : set, y2 ∈ SNoL x → x2 * x + y * y2 + - (x2 * y2) ∈ v))

Theorem. (Conj_mul_SNo_com__2__9)

z = u → SNoCut z w = SNoCut u v

In Proofgold the corresponding term root is 9d3a0e... and proposition id is 462c54...

Proof:

The rest of the proof is missing.

End of Section Conj_mul_SNo_com__2__9

Beginning of Section Conj_mul_SNo_com__2__11