Proof of Theorem ncoprmgcdne1b
Step | Hyp | Ref
| Expression |
1 | | eluz2nn 11602 |
. . . . . . 7
⊢ (𝑖 ∈
(ℤ≥‘2) → 𝑖 ∈ ℕ) |
2 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ∈ ℕ) |
3 | | simpr 476 |
. . . . . . 7
⊢ ((𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
4 | | eluz2b3 11638 |
. . . . . . . . 9
⊢ (𝑖 ∈
(ℤ≥‘2) ↔ (𝑖 ∈ ℕ ∧ 𝑖 ≠ 1)) |
5 | | df-ne 2782 |
. . . . . . . . . . 11
⊢ (𝑖 ≠ 1 ↔ ¬ 𝑖 = 1) |
6 | 5 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑖 ≠ 1 → ¬ 𝑖 = 1) |
7 | 6 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℕ ∧ 𝑖 ≠ 1) → ¬ 𝑖 = 1) |
8 | 4, 7 | sylbi 206 |
. . . . . . . 8
⊢ (𝑖 ∈
(ℤ≥‘2) → ¬ 𝑖 = 1) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → ¬ 𝑖 = 1) |
10 | 3, 9 | jca 553 |
. . . . . 6
⊢ ((𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1)) |
11 | 2, 10 | jca 553 |
. . . . 5
⊢ ((𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1))) |
12 | 5 | biimpri 217 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑖 = 1 → 𝑖 ≠ 1) |
13 | 12 | anim1i 590 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑖 = 1 ∧ 𝑖 ∈ ℕ) → (𝑖 ≠ 1 ∧ 𝑖 ∈ ℕ)) |
14 | 13 | ancomd 466 |
. . . . . . . . . . . 12
⊢ ((¬
𝑖 = 1 ∧ 𝑖 ∈ ℕ) → (𝑖 ∈ ℕ ∧ 𝑖 ≠ 1)) |
15 | 14, 4 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((¬
𝑖 = 1 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈
(ℤ≥‘2)) |
16 | 15 | ex 449 |
. . . . . . . . . 10
⊢ (¬
𝑖 = 1 → (𝑖 ∈ ℕ → 𝑖 ∈
(ℤ≥‘2))) |
17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1) → (𝑖 ∈ ℕ → 𝑖 ∈
(ℤ≥‘2))) |
18 | 17 | impcom 445 |
. . . . . . . 8
⊢ ((𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1)) → 𝑖 ∈
(ℤ≥‘2)) |
19 | 18 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1))) → 𝑖 ∈
(ℤ≥‘2)) |
20 | | simprrl 800 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1))) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
21 | 19, 20 | jca 553 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1))) → (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
22 | 21 | ex 449 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1)) → (𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)))) |
23 | 11, 22 | impbid2 215 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) ↔ (𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1)))) |
24 | 23 | exbidv 1837 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖(𝑖 ∈
(ℤ≥‘2) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) ↔ ∃𝑖(𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1)))) |
25 | | df-rex 2902 |
. . 3
⊢
(∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ ∃𝑖(𝑖 ∈ (ℤ≥‘2)
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
26 | | df-rex 2902 |
. . 3
⊢
(∃𝑖 ∈
ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1) ↔ ∃𝑖(𝑖 ∈ ℕ ∧ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1))) |
27 | 24, 25, 26 | 3bitr4g 302 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ ∃𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1))) |
28 | | rexanali 2981 |
. . 3
⊢
(∃𝑖 ∈
ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1) ↔ ¬ ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1)) |
29 | 28 | a1i 11 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖 ∈ ℕ
((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ∧ ¬ 𝑖 = 1) ↔ ¬ ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1))) |
30 | | coprmgcdb 15200 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑖 ∈ ℕ
((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1)) |
31 | 30 | necon3bbid 2819 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬
∀𝑖 ∈ ℕ
((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) ≠ 1)) |
32 | 27, 29, 31 | 3bitrd 293 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1)) |