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 e. NN /\ B e. NN ) -> ( A < B -> gcdOLD ( A , B ) = gcdOLD ( A , ( B - A ) ) ) )

Proof

Step Hyp Ref Expression
1 nndivsub 
 |-  ( ( ( A e. NN /\ B e. NN /\ x e. NN ) /\ ( ( A / x ) e. NN /\ A < B ) ) -> ( ( B / x ) e. NN <-> ( ( B - A ) / x ) e. NN ) )
2 1 exp32 
 |-  ( ( A e. NN /\ B e. NN /\ x e. NN ) -> ( ( A / x ) e. NN -> ( A < B -> ( ( B / x ) e. NN <-> ( ( B - A ) / x ) e. NN ) ) ) )
3 2 com23 
 |-  ( ( A e. NN /\ B e. NN /\ x e. NN ) -> ( A < B -> ( ( A / x ) e. NN -> ( ( B / x ) e. NN <-> ( ( B - A ) / x ) e. NN ) ) ) )
4 3 3expia 
 |-  ( ( A e. NN /\ B e. NN ) -> ( x e. NN -> ( A < B -> ( ( A / x ) e. NN -> ( ( B / x ) e. NN <-> ( ( B - A ) / x ) e. NN ) ) ) ) )
5 4 com23 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A < B -> ( x e. NN -> ( ( A / x ) e. NN -> ( ( B / x ) e. NN <-> ( ( B - A ) / x ) e. NN ) ) ) ) )
6 5 imp 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ A < B ) -> ( x e. NN -> ( ( A / x ) e. NN -> ( ( B / x ) e. NN <-> ( ( B - A ) / x ) e. NN ) ) ) )
7 6 imp 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ A < B ) /\ x e. NN ) -> ( ( A / x ) e. NN -> ( ( B / x ) e. NN <-> ( ( B - A ) / x ) e. NN ) ) )
8 7 pm5.32d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ A < B ) /\ x e. NN ) -> ( ( ( A / x ) e. NN /\ ( B / x ) e. NN ) <-> ( ( A / x ) e. NN /\ ( ( B - A ) / x ) e. NN ) ) )
9 8 rabbidva 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ A < B ) -> { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } = { x e. NN | ( ( A / x ) e. NN /\ ( ( B - A ) / x ) e. NN ) } )
10 9 supeq1d 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ A < B ) -> sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( ( B - A ) / x ) e. NN ) } , NN , < ) )
11 df-gcdOLD 
 |-  gcdOLD ( A , B ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )
12 df-gcdOLD 
 |-  gcdOLD ( A , ( B - A ) ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( ( B - A ) / x ) e. NN ) } , NN , < )
13 10 11 12 3eqtr4g 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ A < B ) -> gcdOLD ( A , B ) = gcdOLD ( A , ( B - A ) ) )
14 13 ex 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A < B -> gcdOLD ( A , B ) = gcdOLD ( A , ( B - A ) ) ) )