Step * of Lemma qmul-qdiv-cancel6

[a,b,c:ℚ].  (((b/c a) a) (b/c) ∈ ℚsupposing ((¬(c 0 ∈ ℚ)) and (a 0 ∈ ℚ)))
BY
xxx(Auto THEN QMul ⌜c⌝ 0⋅ THEN Auto)xxx }

1
1. : ℚ
2. : ℚ
3. : ℚ
4. ¬(a 0 ∈ ℚ)
5. ¬(c 0 ∈ ℚ)
⊢ ¬((c a) 0 ∈ ℚ)

2
.....rewrite subgoal..... 
1. : ℚ
2. : ℚ
3. : ℚ
4. ¬(a 0 ∈ ℚ)
5. ¬(c 0 ∈ ℚ)
⊢ ¬((a c) 0 ∈ ℚ)


Latex:


Latex:
\mforall{}[a,b,c:\mBbbQ{}].    (((b/c  *  a)  *  a)  =  (b/c))  supposing  ((\mneg{}(c  =  0))  and  (\mneg{}(a  =  0)))


By


Latex:
xxx(Auto  THEN  QMul  \mkleeneopen{}c\mkleeneclose{}  0\mcdot{}  THEN  Auto)xxx




Home Index