Step |
Hyp |
Ref |
Expression |
1 |
|
nnz |
⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ ) |
2 |
|
nnz |
⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ ) |
3 |
|
gcddvds |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) |
4 |
1 2 3
|
syl2an |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) |
5 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) |
6 |
|
gcdnncl |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ ) |
7 |
6
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ ) |
8 |
|
breq1 |
⊢ ( 𝑖 = ( 𝐴 gcd 𝐵 ) → ( 𝑖 ∥ 𝐴 ↔ ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ) ) |
9 |
|
breq1 |
⊢ ( 𝑖 = ( 𝐴 gcd 𝐵 ) → ( 𝑖 ∥ 𝐵 ↔ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) |
10 |
8 9
|
anbi12d |
⊢ ( 𝑖 = ( 𝐴 gcd 𝐵 ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) ↔ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) ) |
11 |
|
eqeq1 |
⊢ ( 𝑖 = ( 𝐴 gcd 𝐵 ) → ( 𝑖 = 1 ↔ ( 𝐴 gcd 𝐵 ) = 1 ) ) |
12 |
10 11
|
imbi12d |
⊢ ( 𝑖 = ( 𝐴 gcd 𝐵 ) → ( ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) = 1 ) ) ) |
13 |
12
|
rspcv |
⊢ ( ( 𝐴 gcd 𝐵 ) ∈ ℕ → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ( ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) = 1 ) ) ) |
14 |
7 13
|
syl |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ( ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) → ( 𝐴 gcd 𝐵 ) = 1 ) ) ) |
15 |
5 14
|
mpid |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ( 𝐴 gcd 𝐵 ) = 1 ) ) |
16 |
4 15
|
mpdan |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) → ( 𝐴 gcd 𝐵 ) = 1 ) ) |
17 |
|
simpl |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ) |
18 |
17
|
anim1ci |
⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ∈ ℕ ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ) ) |
19 |
|
3anass |
⊢ ( ( 𝑖 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ↔ ( 𝑖 ∈ ℕ ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ) ) |
20 |
18 19
|
sylibr |
⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ) |
21 |
|
nndvdslegcd |
⊢ ( ( 𝑖 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 ≤ ( 𝐴 gcd 𝐵 ) ) ) |
22 |
20 21
|
syl |
⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑖 ∈ ℕ ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 ≤ ( 𝐴 gcd 𝐵 ) ) ) |
23 |
|
breq2 |
⊢ ( ( 𝐴 gcd 𝐵 ) = 1 → ( 𝑖 ≤ ( 𝐴 gcd 𝐵 ) ↔ 𝑖 ≤ 1 ) ) |
24 |
23
|
adantr |
⊢ ( ( ( 𝐴 gcd 𝐵 ) = 1 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ≤ ( 𝐴 gcd 𝐵 ) ↔ 𝑖 ≤ 1 ) ) |
25 |
|
nnge1 |
⊢ ( 𝑖 ∈ ℕ → 1 ≤ 𝑖 ) |
26 |
|
nnre |
⊢ ( 𝑖 ∈ ℕ → 𝑖 ∈ ℝ ) |
27 |
|
1red |
⊢ ( 𝑖 ∈ ℕ → 1 ∈ ℝ ) |
28 |
26 27
|
letri3d |
⊢ ( 𝑖 ∈ ℕ → ( 𝑖 = 1 ↔ ( 𝑖 ≤ 1 ∧ 1 ≤ 𝑖 ) ) ) |
29 |
28
|
biimprd |
⊢ ( 𝑖 ∈ ℕ → ( ( 𝑖 ≤ 1 ∧ 1 ≤ 𝑖 ) → 𝑖 = 1 ) ) |
30 |
25 29
|
mpan2d |
⊢ ( 𝑖 ∈ ℕ → ( 𝑖 ≤ 1 → 𝑖 = 1 ) ) |
31 |
30
|
adantl |
⊢ ( ( ( 𝐴 gcd 𝐵 ) = 1 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ≤ 1 → 𝑖 = 1 ) ) |
32 |
24 31
|
sylbid |
⊢ ( ( ( 𝐴 gcd 𝐵 ) = 1 ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ≤ ( 𝐴 gcd 𝐵 ) → 𝑖 = 1 ) ) |
33 |
32
|
adantll |
⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑖 ∈ ℕ ) → ( 𝑖 ≤ ( 𝐴 gcd 𝐵 ) → 𝑖 = 1 ) ) |
34 |
22 33
|
syld |
⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑖 ∈ ℕ ) → ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ) |
35 |
34
|
ralrimiva |
⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ) |
36 |
35
|
ex |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝐴 gcd 𝐵 ) = 1 → ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ) ) |
37 |
16 36
|
impbid |
⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑖 ∈ ℕ ( ( 𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵 ) → 𝑖 = 1 ) ↔ ( 𝐴 gcd 𝐵 ) = 1 ) ) |