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 → gcd OLD A B = gcd OLD A B − A

Proof

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