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 ( 𝐴 , ( 𝐵 − 𝐴 ) ) ) ) |