Metamath Proof Explorer

Theorem ee7.2aOLD

Description: Lemma for Euclid's Elements, Book 7, proposition 2. The original mentions the smaller measure being 'continually subtracted' from the larger. Many authors interpret this phrase as A mod B . Here, just one subtraction step is proved to preserve the gcdOLD . The rec function will be used in other proofs for iterated subtraction. (Contributed by Jeff Hoffman, 17-Jun-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ee7.2aOLD ⊢A∈ℕ∧B∈ℕ→A<B→gcdOLDAB=gcdOLDAB−A

Proof

Step Hyp Ref Expression
1 nndivsub ⊢A∈ℕ∧B∈ℕ∧x∈ℕ∧Ax∈ℕ∧A<B→Bx∈ℕ↔B−Ax∈ℕ
2 1 exp32 ⊢A∈ℕ∧B∈ℕ∧x∈ℕ→Ax∈ℕ→A<B→Bx∈ℕ↔B−Ax∈ℕ
3 2 com23 ⊢A∈ℕ∧B∈ℕ∧x∈ℕ→A<B→Ax∈ℕ→Bx∈ℕ↔B−Ax∈ℕ
4 3 3expia ⊢A∈ℕ∧B∈ℕ→x∈ℕ→A<B→Ax∈ℕ→Bx∈ℕ↔B−Ax∈ℕ
5 4 com23 ⊢A∈ℕ∧B∈ℕ→A<B→x∈ℕ→Ax∈ℕ→Bx∈ℕ↔B−Ax∈ℕ
6 5 imp ⊢A∈ℕ∧B∈ℕ∧A<B→x∈ℕ→Ax∈ℕ→Bx∈ℕ↔B−Ax∈ℕ
7 6 imp ⊢A∈ℕ∧B∈ℕ∧A<B∧x∈ℕ→Ax∈ℕ→Bx∈ℕ↔B−Ax∈ℕ
8 7 pm5.32d ⊢A∈ℕ∧B∈ℕ∧A<B∧x∈ℕ→Ax∈ℕ∧Bx∈ℕ↔Ax∈ℕ∧B−Ax∈ℕ
9 8 rabbidva ⊢A∈ℕ∧B∈ℕ∧A<B→x∈ℕ|Ax∈ℕ∧Bx∈ℕ=x∈ℕ|Ax∈ℕ∧B−Ax∈ℕ
10 9 supeq1d ⊢A∈ℕ∧B∈ℕ∧A<B→supx∈ℕ|Ax∈ℕ∧Bx∈ℕℕ<=supx∈ℕ|Ax∈ℕ∧B−Ax∈ℕℕ<
11 df-gcdOLD ⊢gcdOLDAB=supx∈ℕ|Ax∈ℕ∧Bx∈ℕℕ<
12 df-gcdOLD ⊢gcdOLDAB−A=supx∈ℕ|Ax∈ℕ∧B−Ax∈ℕℕ<
13 10 11 12 3eqtr4g ⊢A∈ℕ∧B∈ℕ∧A<B→gcdOLDAB=gcdOLDAB−A
14 13 ex ⊢A∈ℕ∧B∈ℕ→A<B→gcdOLDAB=gcdOLDAB−A