Step | Hyp | Ref
| Expression |
1 | | ncoprmgcdgt1b 15202 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ 1 < (𝐴 gcd 𝐵))) |
2 | 1 | bicomd 212 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (1 <
(𝐴 gcd 𝐵) ↔ ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
3 | 2 | 3adant3 1074 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → (1 < (𝐴 gcd 𝐵) ↔ ∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
4 | | simp1 1054 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → 𝐴 ∈ ℕ) |
5 | | eluzelz 11573 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈
(ℤ≥‘2) → 𝑖 ∈ ℤ) |
6 | 4, 5 | anim12ci 589 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ (𝑖 ∈ ℤ
∧ 𝐴 ∈
ℕ)) |
7 | | dvdsle 14870 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ℤ ∧ 𝐴 ∈ ℕ) → (𝑖 ∥ 𝐴 → 𝑖 ≤ 𝐴)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ (𝑖 ∥ 𝐴 → 𝑖 ≤ 𝐴)) |
9 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℝ) |
10 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
11 | | eluzelre 11574 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈
(ℤ≥‘2) → 𝑖 ∈ ℝ) |
12 | 9, 10, 11 | 3anim123i 1240 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘2)) → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑖 ∈ ℝ)) |
13 | | 3anrot 1036 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑖 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑖 ∈
ℝ)) |
14 | 12, 13 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘2)) → (𝑖 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
15 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑖 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑖 ≤ 𝐴 ∧ 𝐴 < 𝐵) → 𝑖 < 𝐵)) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘2)) → ((𝑖 ≤ 𝐴 ∧ 𝐴 < 𝐵) → 𝑖 < 𝐵)) |
17 | 16 | expcomd 453 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑖 ∈
(ℤ≥‘2)) → (𝐴 < 𝐵 → (𝑖 ≤ 𝐴 → 𝑖 < 𝐵))) |
18 | 17 | 3exp 1256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ ℕ → (𝐵 ∈ ℕ → (𝑖 ∈
(ℤ≥‘2) → (𝐴 < 𝐵 → (𝑖 ≤ 𝐴 → 𝑖 < 𝐵))))) |
19 | 18 | com34 89 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ ℕ → (𝐵 ∈ ℕ → (𝐴 < 𝐵 → (𝑖 ∈ (ℤ≥‘2)
→ (𝑖 ≤ 𝐴 → 𝑖 < 𝐵))))) |
20 | 19 | 3imp1 1272 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ (𝑖 ≤ 𝐴 → 𝑖 < 𝐵)) |
21 | 20 | imp 444 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ 𝑖 ≤ 𝐴) → 𝑖 < 𝐵) |
22 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
23 | 22 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℤ) |
24 | 23, 5 | anim12ci 589 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ (𝑖 ∈ ℤ
∧ 𝐵 ∈
ℤ)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ 𝑖 ≤ 𝐴) → (𝑖 ∈ ℤ ∧ 𝐵 ∈ ℤ)) |
26 | | zltlem1 11307 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑖 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑖 < 𝐵 ↔ 𝑖 ≤ (𝐵 − 1))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ 𝑖 ≤ 𝐴) → (𝑖 < 𝐵 ↔ 𝑖 ≤ (𝐵 − 1))) |
28 | 21, 27 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ 𝑖 ≤ 𝐴) → 𝑖 ≤ (𝐵 − 1)) |
29 | 28 | ex 449 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ (𝑖 ≤ 𝐴 → 𝑖 ≤ (𝐵 − 1))) |
30 | 8, 29 | syld 46 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ (𝑖 ∥ 𝐴 → 𝑖 ≤ (𝐵 − 1))) |
31 | 30 | com12 32 |
. . . . . . . . . . 11
⊢ (𝑖 ∥ 𝐴 → (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ 𝑖 ≤ (𝐵 − 1))) |
32 | 31 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ 𝑖 ≤ (𝐵 − 1))) |
33 | 32 | impcom 445 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ≤ (𝐵 − 1)) |
34 | | peano2zm 11297 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ ℤ → (𝐵 − 1) ∈
ℤ) |
35 | 22, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ ℕ → (𝐵 − 1) ∈
ℤ) |
36 | 35 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → (𝐵 − 1) ∈ ℤ) |
37 | 36 | anim1i 590 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ ((𝐵 − 1)
∈ ℤ ∧ 𝑖
∈ (ℤ≥‘2))) |
38 | 37 | ancomd 466 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ (𝑖 ∈
(ℤ≥‘2) ∧ (𝐵 − 1) ∈
ℤ)) |
39 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝑖 ∈ (ℤ≥‘2)
∧ (𝐵 − 1) ∈
ℤ)) |
40 | | elfz5 12205 |
. . . . . . . . . 10
⊢ ((𝑖 ∈
(ℤ≥‘2) ∧ (𝐵 − 1) ∈ ℤ) → (𝑖 ∈ (2...(𝐵 − 1)) ↔ 𝑖 ≤ (𝐵 − 1))) |
41 | 39, 40 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (𝑖 ∈ (2...(𝐵 − 1)) ↔ 𝑖 ≤ (𝐵 − 1))) |
42 | 33, 41 | mpbird 246 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ∈ (2...(𝐵 − 1))) |
43 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑗 = 𝑖 → (𝑗 ∥ 𝐵 ↔ 𝑖 ∥ 𝐵)) |
44 | 43 | adantl 481 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℕ ∧ 𝐵 ∈
ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) ∧ 𝑗 = 𝑖) → (𝑗 ∥ 𝐵 ↔ 𝑖 ∥ 𝐵)) |
45 | | simprr 792 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝑖 ∥ 𝐵) |
46 | 42, 44, 45 | rspcedvd 3289 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → ∃𝑗 ∈ (2...(𝐵 − 1))𝑗 ∥ 𝐵) |
47 | | rexnal 2978 |
. . . . . . . 8
⊢
(∃𝑗 ∈
(2...(𝐵 − 1)) ¬
¬ 𝑗 ∥ 𝐵 ↔ ¬ ∀𝑗 ∈ (2...(𝐵 − 1)) ¬ 𝑗 ∥ 𝐵) |
48 | | notnotb 303 |
. . . . . . . . . 10
⊢ (𝑗 ∥ 𝐵 ↔ ¬ ¬ 𝑗 ∥ 𝐵) |
49 | 48 | bicomi 213 |
. . . . . . . . 9
⊢ (¬
¬ 𝑗 ∥ 𝐵 ↔ 𝑗 ∥ 𝐵) |
50 | 49 | rexbii 3023 |
. . . . . . . 8
⊢
(∃𝑗 ∈
(2...(𝐵 − 1)) ¬
¬ 𝑗 ∥ 𝐵 ↔ ∃𝑗 ∈ (2...(𝐵 − 1))𝑗 ∥ 𝐵) |
51 | 47, 50 | bitr3i 265 |
. . . . . . 7
⊢ (¬
∀𝑗 ∈
(2...(𝐵 − 1)) ¬
𝑗 ∥ 𝐵 ↔ ∃𝑗 ∈ (2...(𝐵 − 1))𝑗 ∥ 𝐵) |
52 | 46, 51 | sylibr 223 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → ¬ ∀𝑗 ∈ (2...(𝐵 − 1)) ¬ 𝑗 ∥ 𝐵) |
53 | 52 | olcd 407 |
. . . . 5
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → (¬ 𝐵 ∈ (ℤ≥‘2)
∨ ¬ ∀𝑗 ∈
(2...(𝐵 − 1)) ¬
𝑗 ∥ 𝐵)) |
54 | | df-nel 2783 |
. . . . . 6
⊢ (𝐵 ∉ ℙ ↔ ¬
𝐵 ∈
ℙ) |
55 | | ianor 508 |
. . . . . . 7
⊢ (¬
(𝐵 ∈
(ℤ≥‘2) ∧ ∀𝑗 ∈ (2...(𝐵 − 1)) ¬ 𝑗 ∥ 𝐵) ↔ (¬ 𝐵 ∈ (ℤ≥‘2)
∨ ¬ ∀𝑗 ∈
(2...(𝐵 − 1)) ¬
𝑗 ∥ 𝐵)) |
56 | | isprm3 15234 |
. . . . . . 7
⊢ (𝐵 ∈ ℙ ↔ (𝐵 ∈
(ℤ≥‘2) ∧ ∀𝑗 ∈ (2...(𝐵 − 1)) ¬ 𝑗 ∥ 𝐵)) |
57 | 55, 56 | xchnxbir 322 |
. . . . . 6
⊢ (¬
𝐵 ∈ ℙ ↔
(¬ 𝐵 ∈
(ℤ≥‘2) ∨ ¬ ∀𝑗 ∈ (2...(𝐵 − 1)) ¬ 𝑗 ∥ 𝐵)) |
58 | 54, 57 | bitri 263 |
. . . . 5
⊢ (𝐵 ∉ ℙ ↔ (¬
𝐵 ∈
(ℤ≥‘2) ∨ ¬ ∀𝑗 ∈ (2...(𝐵 − 1)) ¬ 𝑗 ∥ 𝐵)) |
59 | 53, 58 | sylibr 223 |
. . . 4
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) → 𝐵 ∉ ℙ) |
60 | 59 | ex 449 |
. . 3
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) ∧ 𝑖 ∈ (ℤ≥‘2))
→ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝐵 ∉ ℙ)) |
61 | 60 | rexlimdva 3013 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → (∃𝑖 ∈
(ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝐵 ∉ ℙ)) |
62 | 3, 61 | sylbid 229 |
1
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → (1 < (𝐴 gcd 𝐵) → 𝐵 ∉ ℙ)) |