Proof of Theorem fvprmselgcd1
Step | Hyp | Ref
| Expression |
1 | | fvprmselelfz.f |
. . . . . . 7
⊢ 𝐹 = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1)) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝐹 = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
3 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑚 = 𝑋 → (𝑚 ∈ ℙ ↔ 𝑋 ∈ ℙ)) |
4 | | id 22 |
. . . . . . . 8
⊢ (𝑚 = 𝑋 → 𝑚 = 𝑋) |
5 | 3, 4 | ifbieq1d 4109 |
. . . . . . 7
⊢ (𝑚 = 𝑋 → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑋 ∈ ℙ, 𝑋, 1)) |
6 | | iftrue 4092 |
. . . . . . . 8
⊢ (𝑋 ∈ ℙ → if(𝑋 ∈ ℙ, 𝑋, 1) = 𝑋) |
7 | 6 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑋 ∈ ℙ, 𝑋, 1) = 𝑋) |
8 | 5, 7 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑋) → if(𝑚 ∈ ℙ, 𝑚, 1) = 𝑋) |
9 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝑋 ∈ (1...𝑁) → 𝑋 ∈ ℕ) |
10 | 9 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → 𝑋 ∈ ℕ) |
11 | 10 | adantl 482 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ ℕ) |
12 | | simpll 790 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ ℙ) |
13 | 2, 8, 11, 12 | fvmptd 6288 |
. . . . 5
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑋) = 𝑋) |
14 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑚 = 𝑌 → (𝑚 ∈ ℙ ↔ 𝑌 ∈ ℙ)) |
15 | | id 22 |
. . . . . . . 8
⊢ (𝑚 = 𝑌 → 𝑚 = 𝑌) |
16 | 14, 15 | ifbieq1d 4109 |
. . . . . . 7
⊢ (𝑚 = 𝑌 → if(𝑚 ∈ ℙ, 𝑚, 1) = if(𝑌 ∈ ℙ, 𝑌, 1)) |
17 | | iftrue 4092 |
. . . . . . . 8
⊢ (𝑌 ∈ ℙ → if(𝑌 ∈ ℙ, 𝑌, 1) = 𝑌) |
18 | 17 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑌 ∈ ℙ, 𝑌, 1) = 𝑌) |
19 | 16, 18 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑌) → if(𝑚 ∈ ℙ, 𝑚, 1) = 𝑌) |
20 | | elfznn 12370 |
. . . . . . . 8
⊢ (𝑌 ∈ (1...𝑁) → 𝑌 ∈ ℕ) |
21 | 20 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → 𝑌 ∈ ℕ) |
22 | 21 | adantl 482 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ ℕ) |
23 | | simplr 792 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ ℙ) |
24 | 2, 19, 22, 23 | fvmptd 6288 |
. . . . 5
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑌) = 𝑌) |
25 | 13, 24 | oveq12d 6668 |
. . . 4
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = (𝑋 gcd 𝑌)) |
26 | | prmrp 15424 |
. . . . . . 7
⊢ ((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) → ((𝑋 gcd 𝑌) = 1 ↔ 𝑋 ≠ 𝑌)) |
27 | 26 | biimprcd 240 |
. . . . . 6
⊢ (𝑋 ≠ 𝑌 → ((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) → (𝑋 gcd 𝑌) = 1)) |
28 | 27 | 3ad2ant3 1084 |
. . . . 5
⊢ ((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → ((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) → (𝑋 gcd 𝑌) = 1)) |
29 | 28 | impcom 446 |
. . . 4
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝑋 gcd 𝑌) = 1) |
30 | 25, 29 | eqtrd 2656 |
. . 3
⊢ (((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) ∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1) |
31 | 30 | ex 450 |
. 2
⊢ ((𝑋 ∈ ℙ ∧ 𝑌 ∈ ℙ) → ((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1)) |
32 | 1 | a1i 11 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝐹 = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
33 | 6 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑋 ∈ ℙ, 𝑋, 1) = 𝑋) |
34 | 5, 33 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑋) → if(𝑚 ∈ ℙ, 𝑚, 1) = 𝑋) |
35 | 10 | adantl 482 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ ℕ) |
36 | | simpll 790 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ ℙ) |
37 | 32, 34, 35, 36 | fvmptd 6288 |
. . . . 5
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑋) = 𝑋) |
38 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
𝑌 ∈ ℙ →
if(𝑌 ∈ ℙ, 𝑌, 1) = 1) |
39 | 38 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑌 ∈ ℙ, 𝑌, 1) = 1) |
40 | 16, 39 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑌) → if(𝑚 ∈ ℙ, 𝑚, 1) = 1) |
41 | 21 | adantl 482 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ ℕ) |
42 | | 1nn 11031 |
. . . . . . 7
⊢ 1 ∈
ℕ |
43 | 42 | a1i 11 |
. . . . . 6
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 1 ∈ ℕ) |
44 | 32, 40, 41, 43 | fvmptd 6288 |
. . . . 5
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑌) = 1) |
45 | 37, 44 | oveq12d 6668 |
. . . 4
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = (𝑋 gcd 1)) |
46 | | prmz 15389 |
. . . . . 6
⊢ (𝑋 ∈ ℙ → 𝑋 ∈
ℤ) |
47 | | gcd1 15249 |
. . . . . 6
⊢ (𝑋 ∈ ℤ → (𝑋 gcd 1) = 1) |
48 | 46, 47 | syl 17 |
. . . . 5
⊢ (𝑋 ∈ ℙ → (𝑋 gcd 1) = 1) |
49 | 48 | ad2antrr 762 |
. . . 4
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝑋 gcd 1) = 1) |
50 | 45, 49 | eqtrd 2656 |
. . 3
⊢ (((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1) |
51 | 50 | ex 450 |
. 2
⊢ ((𝑋 ∈ ℙ ∧ ¬
𝑌 ∈ ℙ) →
((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1)) |
52 | 1 | a1i 11 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝐹 = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
53 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
𝑋 ∈ ℙ →
if(𝑋 ∈ ℙ, 𝑋, 1) = 1) |
54 | 53 | ad2antrr 762 |
. . . . . . 7
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑋 ∈ ℙ, 𝑋, 1) = 1) |
55 | 5, 54 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑋) → if(𝑚 ∈ ℙ, 𝑚, 1) = 1) |
56 | 10 | adantl 482 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ ℕ) |
57 | 42 | a1i 11 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 1 ∈ ℕ) |
58 | 52, 55, 56, 57 | fvmptd 6288 |
. . . . 5
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑋) = 1) |
59 | 17 | ad2antlr 763 |
. . . . . . 7
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑌 ∈ ℙ, 𝑌, 1) = 𝑌) |
60 | 16, 59 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑌) → if(𝑚 ∈ ℙ, 𝑚, 1) = 𝑌) |
61 | 21 | adantl 482 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ ℕ) |
62 | | simplr 792 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ ℙ) |
63 | 52, 60, 61, 62 | fvmptd 6288 |
. . . . 5
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑌) = 𝑌) |
64 | 58, 63 | oveq12d 6668 |
. . . 4
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = (1 gcd 𝑌)) |
65 | | prmz 15389 |
. . . . . 6
⊢ (𝑌 ∈ ℙ → 𝑌 ∈
ℤ) |
66 | | 1gcd 15254 |
. . . . . 6
⊢ (𝑌 ∈ ℤ → (1 gcd
𝑌) = 1) |
67 | 65, 66 | syl 17 |
. . . . 5
⊢ (𝑌 ∈ ℙ → (1 gcd
𝑌) = 1) |
68 | 67 | ad2antlr 763 |
. . . 4
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (1 gcd 𝑌) = 1) |
69 | 64, 68 | eqtrd 2656 |
. . 3
⊢ (((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) ∧
(𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1) |
70 | 69 | ex 450 |
. 2
⊢ ((¬
𝑋 ∈ ℙ ∧
𝑌 ∈ ℙ) →
((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1)) |
71 | 1 | a1i 11 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝐹 = (𝑚 ∈ ℕ ↦ if(𝑚 ∈ ℙ, 𝑚, 1))) |
72 | 53 | ad2antrr 762 |
. . . . . . 7
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑋 ∈ ℙ, 𝑋, 1) = 1) |
73 | 5, 72 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑋) → if(𝑚 ∈ ℙ, 𝑚, 1) = 1) |
74 | 10 | adantl 482 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ ℕ) |
75 | 42 | a1i 11 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 1 ∈ ℕ) |
76 | 71, 73, 74, 75 | fvmptd 6288 |
. . . . 5
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑋) = 1) |
77 | 38 | ad2antlr 763 |
. . . . . . 7
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → if(𝑌 ∈ ℙ, 𝑌, 1) = 1) |
78 | 16, 77 | sylan9eqr 2678 |
. . . . . 6
⊢ ((((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) ∧ 𝑚 = 𝑌) → if(𝑚 ∈ ℙ, 𝑚, 1) = 1) |
79 | 21 | adantl 482 |
. . . . . 6
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ ℕ) |
80 | 71, 78, 79, 75 | fvmptd 6288 |
. . . . 5
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑌) = 1) |
81 | 76, 80 | oveq12d 6668 |
. . . 4
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = (1 gcd 1)) |
82 | | 1z 11407 |
. . . . 5
⊢ 1 ∈
ℤ |
83 | | 1gcd 15254 |
. . . . 5
⊢ (1 ∈
ℤ → (1 gcd 1) = 1) |
84 | 82, 83 | mp1i 13 |
. . . 4
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → (1 gcd 1) = 1) |
85 | 81, 84 | eqtrd 2656 |
. . 3
⊢ (((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
∧ (𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌)) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1) |
86 | 85 | ex 450 |
. 2
⊢ ((¬
𝑋 ∈ ℙ ∧
¬ 𝑌 ∈ ℙ)
→ ((𝑋 ∈
(1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1)) |
87 | 31, 51, 70, 86 | 4cases 990 |
1
⊢ ((𝑋 ∈ (1...𝑁) ∧ 𝑌 ∈ (1...𝑁) ∧ 𝑋 ≠ 𝑌) → ((𝐹‘𝑋) gcd (𝐹‘𝑌)) = 1) |