Proof of Theorem ncoprmgcdne1b
Step | Hyp | Ref
| Expression |
1 | | df-2 8098 |
. . . . . . 7
⊢ 2 = (1 +
1) |
2 | | 2re 8109 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
3 | 2 | a1i 9 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 2 ∈ ℝ) |
4 | | eluzelz 8628 |
. . . . . . . . . 10
⊢ (𝑖 ∈
(ℤ≥‘2) → 𝑖 ∈ ℤ) |
5 | 4 | ad2antlr 472 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ∈ ℤ) |
6 | 5 | zred 8469 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ∈ ℝ) |
7 | | simplll 499 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝐴 ∈ ℕ) |
8 | | simpllr 500 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝐵 ∈ ℕ) |
9 | | gcdnncl 10359 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 gcd 𝐵) ∈ ℕ) |
10 | 7, 8, 9 | syl2anc 403 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝐴 gcd 𝐵) ∈ ℕ) |
11 | 10 | nnred 8052 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝐴 gcd 𝐵) ∈ ℝ) |
12 | | eluzle 8631 |
. . . . . . . . 9
⊢ (𝑖 ∈
(ℤ≥‘2) → 2 ≤ 𝑖) |
13 | 12 | ad2antlr 472 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 2 ≤ 𝑖) |
14 | | simpr 108 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
15 | 7 | nnzd 8468 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝐴 ∈ ℤ) |
16 | 8 | nnzd 8468 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝐵 ∈ ℤ) |
17 | | dvdsgcd 10401 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 ∥ (𝐴 gcd 𝐵))) |
18 | 5, 15, 16, 17 | syl3anc 1169 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 ∥ (𝐴 gcd 𝐵))) |
19 | 14, 18 | mpd 13 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ∥ (𝐴 gcd 𝐵)) |
20 | | dvdsle 10244 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ℤ ∧ (𝐴 gcd 𝐵) ∈ ℕ) → (𝑖 ∥ (𝐴 gcd 𝐵) → 𝑖 ≤ (𝐴 gcd 𝐵))) |
21 | 5, 10, 20 | syl2anc 403 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝑖 ∥ (𝐴 gcd 𝐵) → 𝑖 ≤ (𝐴 gcd 𝐵))) |
22 | 19, 21 | mpd 13 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ≤ (𝐴 gcd 𝐵)) |
23 | 3, 6, 11, 13, 22 | letrd 7233 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 2 ≤ (𝐴 gcd 𝐵)) |
24 | 1, 23 | syl5eqbrr 3819 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (1 + 1) ≤ (𝐴 gcd 𝐵)) |
25 | | 1nn 8050 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
26 | 25 | a1i 9 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 1 ∈ ℕ) |
27 | | nnltp1le 8411 |
. . . . . . 7
⊢ ((1
∈ ℕ ∧ (𝐴 gcd
𝐵) ∈ ℕ) →
(1 < (𝐴 gcd 𝐵) ↔ (1 + 1) ≤ (𝐴 gcd 𝐵))) |
28 | 26, 10, 27 | syl2anc 403 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (1 < (𝐴 gcd 𝐵) ↔ (1 + 1) ≤ (𝐴 gcd 𝐵))) |
29 | 24, 28 | mpbird 165 |
. . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 1 < (𝐴 gcd 𝐵)) |
30 | | nngt1ne1 8073 |
. . . . . 6
⊢ ((𝐴 gcd 𝐵) ∈ ℕ → (1 < (𝐴 gcd 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1)) |
31 | 10, 30 | syl 14 |
. . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (1 < (𝐴 gcd 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1)) |
32 | 29, 31 | mpbid 145 |
. . . 4
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝐴 gcd 𝐵) ≠ 1) |
33 | 32 | ex 113 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑖 ∈
(ℤ≥‘2)) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → (𝐴 gcd 𝐵) ≠ 1)) |
34 | 33 | rexlimdva 2477 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → (𝐴 gcd 𝐵) ≠ 1)) |
35 | 9 | adantr 270 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → (𝐴 gcd 𝐵) ∈ ℕ) |
36 | | simpr 108 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → (𝐴 gcd 𝐵) ≠ 1) |
37 | | eluz2b3 8691 |
. . . . 5
⊢ ((𝐴 gcd 𝐵) ∈ (ℤ≥‘2)
↔ ((𝐴 gcd 𝐵) ∈ ℕ ∧ (𝐴 gcd 𝐵) ≠ 1)) |
38 | 35, 36, 37 | sylanbrc 408 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → (𝐴 gcd 𝐵) ∈
(ℤ≥‘2)) |
39 | | simpll 495 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → 𝐴 ∈ ℕ) |
40 | 39 | nnzd 8468 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → 𝐴 ∈ ℤ) |
41 | | simplr 496 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → 𝐵 ∈ ℕ) |
42 | 41 | nnzd 8468 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → 𝐵 ∈ ℤ) |
43 | | gcddvds 10355 |
. . . . 5
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
44 | 40, 42, 43 | syl2anc 403 |
. . . 4
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) |
45 | | breq1 3788 |
. . . . . 6
⊢ (𝑖 = (𝐴 gcd 𝐵) → (𝑖 ∥ 𝐴 ↔ (𝐴 gcd 𝐵) ∥ 𝐴)) |
46 | | breq1 3788 |
. . . . . 6
⊢ (𝑖 = (𝐴 gcd 𝐵) → (𝑖 ∥ 𝐵 ↔ (𝐴 gcd 𝐵) ∥ 𝐵)) |
47 | 45, 46 | anbi12d 456 |
. . . . 5
⊢ (𝑖 = (𝐴 gcd 𝐵) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵))) |
48 | 47 | rspcev 2701 |
. . . 4
⊢ (((𝐴 gcd 𝐵) ∈ (ℤ≥‘2)
∧ ((𝐴 gcd 𝐵) ∥ 𝐴 ∧ (𝐴 gcd 𝐵) ∥ 𝐵)) → ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
49 | 38, 44, 48 | syl2anc 403 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝐴 gcd 𝐵) ≠ 1) → ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
50 | 49 | ex 113 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) ≠ 1 → ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
51 | 34, 50 | impbid 127 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1)) |