Step * 1 1 2 1 1 of Lemma rat-int-part_wf2


1. Base
2. q1 Base
3. q1 ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) tt))
4. q ∈ ℤ ⋃ (ℤ × ℤ-o)
5. q1 ∈ ℤ ⋃ (ℤ × ℤ-o)
6. qeq(q;q1) tt
7. v2 : ℤ
8. v3 : ℚ
9. 0 ≤ v3
10. v3 < 1
11. (v2 v3) ∈ ℚ
12. rat-int-part(q) = <v2, v3> ∈ {p:ℤ × {r:ℚ(0 ≤ r) ∧ r < 1} let x,r in (x r) ∈ ℚ
13. v4 : ℤ
14. v5 : ℚ
15. 0 ≤ v5
16. v5 < 1
17. q1 (v4 v5) ∈ ℚ
18. rat-int-part(q1) = <v4, v5> ∈ {p:ℤ × {r:ℚ(0 ≤ r) ∧ r < 1} let x,r in q1 (x r) ∈ ℚ
19. q1 ∈ ℚ
20. (v4 v3) (v4 v5) ∈ ℚ
21. v2 v4 ∈ ℤ
22. (-(v4) v4 v3) (-(v4) v4 v5) ∈ ℚ
⊢ v3 v5 ∈ ℚ
BY
(QNorm (-1) THEN Auto) }


Latex:


Latex:

1.  q  :  Base
2.  q1  :  Base
3.  q  =  q1
4.  q  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
5.  q1  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
6.  qeq(q;q1)  =  tt
7.  v2  :  \mBbbZ{}
8.  v3  :  \mBbbQ{}
9.  0  \mleq{}  v3
10.  v3  <  1
11.  q  =  (v2  +  v3)
12.  rat-int-part(q)  =  <v2,  v3>
13.  v4  :  \mBbbZ{}
14.  v5  :  \mBbbQ{}
15.  0  \mleq{}  v5
16.  v5  <  1
17.  q1  =  (v4  +  v5)
18.  rat-int-part(q1)  =  <v4,  v5>
19.  q  =  q1
20.  (v4  +  v3)  =  (v4  +  v5)
21.  v2  =  v4
22.  (-(v4)  +  v4  +  v3)  =  (-(v4)  +  v4  +  v5)
\mvdash{}  v3  =  v5


By


Latex:
(QNorm  (-1)  THEN  Auto)




Home Index