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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 < 𝐵 → gcdOLD ( 𝐴 , 𝐵 ) = gcdOLD ( 𝐴 , ( 𝐵 − 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 nndivsub ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑥 ∈ ℕ ) ∧ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ 𝐴 < 𝐵 ) ) → ( ( 𝐵 / 𝑥 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) )
2 1 exp32 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑥 ∈ ℕ ) → ( ( 𝐴 / 𝑥 ) ∈ ℕ → ( 𝐴 < 𝐵 → ( ( 𝐵 / 𝑥 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) ) ) )
3 2 com23 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑥 ∈ ℕ ) → ( 𝐴 < 𝐵 → ( ( 𝐴 / 𝑥 ) ∈ ℕ → ( ( 𝐵 / 𝑥 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) ) ) )
4 3 3expia ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝑥 ∈ ℕ → ( 𝐴 < 𝐵 → ( ( 𝐴 / 𝑥 ) ∈ ℕ → ( ( 𝐵 / 𝑥 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) ) ) ) )
5 4 com23 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 < 𝐵 → ( 𝑥 ∈ ℕ → ( ( 𝐴 / 𝑥 ) ∈ ℕ → ( ( 𝐵 / 𝑥 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) ) ) ) )
6 5 imp ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ℕ → ( ( 𝐴 / 𝑥 ) ∈ ℕ → ( ( 𝐵 / 𝑥 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) ) ) )
7 6 imp ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ℕ ) → ( ( 𝐴 / 𝑥 ) ∈ ℕ → ( ( 𝐵 / 𝑥 ) ∈ ℕ ↔ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) ) )
8 7 pm5.32d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐴 < 𝐵 ) ∧ 𝑥 ∈ ℕ ) → ( ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) ↔ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) ) )
9 8 rabbidva ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐴 < 𝐵 ) → { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) } = { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) } )
10 9 supeq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐴 < 𝐵 ) → sup ( { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) } , ℕ , < ) = sup ( { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) } , ℕ , < ) )
11 df-gcdOLD ⊢ gcdOLD ( 𝐴 , 𝐵 ) = sup ( { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) } , ℕ , < )
12 df-gcdOLD ⊢ gcdOLD ( 𝐴 , ( 𝐵 − 𝐴 ) ) = sup ( { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( ( 𝐵 − 𝐴 ) / 𝑥 ) ∈ ℕ ) } , ℕ , < )
13 10 11 12 3eqtr4g ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝐴 < 𝐵 ) → gcdOLD ( 𝐴 , 𝐵 ) = gcdOLD ( 𝐴 , ( 𝐵 − 𝐴 ) ) )
14 13 ex ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 < 𝐵 → gcdOLD ( 𝐴 , 𝐵 ) = gcdOLD ( 𝐴 , ( 𝐵 − 𝐴 ) ) ) )