Step * of Lemma sq_stable__coprime

i,j:ℤ.  SqStable(CoPrime(i,j))
BY
(RepUnfolds ``sq_stable coprime gcd_p`` THEN Auto) }

1
1. : ℤ@i
2. : ℤ@i
3. ↓(1 i) ∧ (1 j) ∧ (∀z:ℤ(((z i) ∧ (z j))  (z 1)))@i
4. i
5. j
6. : ℤ@i
7. i@i
8. j@i
⊢ 1


Latex:


Latex:
\mforall{}i,j:\mBbbZ{}.    SqStable(CoPrime(i,j))


By


Latex:
(RepUnfolds  ``sq\_stable  coprime  gcd\_p``  0  THEN  Auto)




Home Index