Step | Hyp | Ref
| Expression |
1 | | r19.26 3092 |
. . . 4
⊢
(∀𝑝 ∈
ℙ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) ↔ (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1 ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐵) ≤ 1)) |
2 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
3 | | simpl1 1193 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℕ) |
4 | 2, 3 | pccld 16403 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
5 | 4 | nn0red 12151 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℝ) |
6 | | simpl2 1194 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℕ) |
7 | 2, 6 | pccld 16403 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈
ℕ0) |
8 | 7 | nn0red 12151 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈ ℝ) |
9 | | 1red 10834 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℝ) |
10 | | le2add 11314 |
. . . . . . . 8
⊢ ((((𝑝 pCnt 𝐴) ∈ ℝ ∧ (𝑝 pCnt 𝐵) ∈ ℝ) ∧ (1 ∈ ℝ
∧ 1 ∈ ℝ)) → (((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) → ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ (1 + 1))) |
11 | 5, 8, 9, 9, 10 | syl22anc 839 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) → ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ (1 + 1))) |
12 | | ax-1ne0 10798 |
. . . . . . . . . . . 12
⊢ 1 ≠
0 |
13 | | simpl3 1195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝐴 gcd 𝐵) = 1) |
14 | 13 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = (𝑝 pCnt 1)) |
15 | 3 | nnzd 12281 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℤ) |
16 | 6 | nnzd 12281 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ) |
17 | | pcgcd 16431 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))) |
18 | 2, 15, 16, 17 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝐴 gcd 𝐵)) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))) |
19 | | pc1 16408 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ ℙ → (𝑝 pCnt 1) = 0) |
20 | 19 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 1) = 0) |
21 | 14, 18, 20 | 3eqtr3d 2785 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) = 0) |
22 | | ifid 4479 |
. . . . . . . . . . . . . . . 16
⊢ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), 1, 1) = 1 |
23 | | ifeq12 4457 |
. . . . . . . . . . . . . . . 16
⊢ ((1 =
(𝑝 pCnt 𝐴) ∧ 1 = (𝑝 pCnt 𝐵)) → if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), 1, 1) = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))) |
24 | 22, 23 | eqtr3id 2792 |
. . . . . . . . . . . . . . 15
⊢ ((1 =
(𝑝 pCnt 𝐴) ∧ 1 = (𝑝 pCnt 𝐵)) → 1 = if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵))) |
25 | 24 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ ((1 =
(𝑝 pCnt 𝐴) ∧ 1 = (𝑝 pCnt 𝐵)) → (1 = 0 ↔ if((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵), (𝑝 pCnt 𝐴), (𝑝 pCnt 𝐵)) = 0)) |
26 | 21, 25 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((1 = (𝑝 pCnt 𝐴) ∧ 1 = (𝑝 pCnt 𝐵)) → 1 = 0)) |
27 | 26 | necon3ad 2953 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (1 ≠ 0 →
¬ (1 = (𝑝 pCnt 𝐴) ∧ 1 = (𝑝 pCnt 𝐵)))) |
28 | 12, 27 | mpi 20 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ¬ (1 = (𝑝 pCnt 𝐴) ∧ 1 = (𝑝 pCnt 𝐵))) |
29 | | ax-1cn 10787 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
30 | 5 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈ ℂ) |
31 | | subeq0 11104 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (𝑝
pCnt 𝐴) ∈ ℂ)
→ ((1 − (𝑝 pCnt
𝐴)) = 0 ↔ 1 = (𝑝 pCnt 𝐴))) |
32 | 29, 30, 31 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((1 − (𝑝 pCnt 𝐴)) = 0 ↔ 1 = (𝑝 pCnt 𝐴))) |
33 | 8 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐵) ∈ ℂ) |
34 | | subeq0 11104 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ (𝑝
pCnt 𝐵) ∈ ℂ)
→ ((1 − (𝑝 pCnt
𝐵)) = 0 ↔ 1 = (𝑝 pCnt 𝐵))) |
35 | 29, 33, 34 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((1 − (𝑝 pCnt 𝐵)) = 0 ↔ 1 = (𝑝 pCnt 𝐵))) |
36 | 32, 35 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0) ↔ (1 = (𝑝 pCnt 𝐴) ∧ 1 = (𝑝 pCnt 𝐵)))) |
37 | 28, 36 | mtbird 328 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ¬ ((1 −
(𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0)) |
38 | 37 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) ∧ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1)) → ¬ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0)) |
39 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ ((1 + 1)
= ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ↔ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) = (1 + 1)) |
40 | | 1re 10833 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
41 | 40, 40 | readdcli 10848 |
. . . . . . . . . . . . . . . . 17
⊢ (1 + 1)
∈ ℝ |
42 | 41 | recni 10847 |
. . . . . . . . . . . . . . . 16
⊢ (1 + 1)
∈ ℂ |
43 | 4, 7 | nn0addcld 12154 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ∈
ℕ0) |
44 | 43 | nn0red 12151 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ∈ ℝ) |
45 | 44 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ∈ ℂ) |
46 | | subeq0 11104 |
. . . . . . . . . . . . . . . 16
⊢ (((1 + 1)
∈ ℂ ∧ ((𝑝
pCnt 𝐴) + (𝑝 pCnt 𝐵)) ∈ ℂ) → (((1 + 1) −
((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) = 0 ↔ (1 + 1) = ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)))) |
47 | 42, 45, 46 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((1 + 1) −
((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) = 0 ↔ (1 + 1) = ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)))) |
48 | 47, 39 | bitrdi 290 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((1 + 1) −
((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) = 0 ↔ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) = (1 + 1))) |
49 | 9 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → 1 ∈
ℂ) |
50 | 49, 49, 30, 33 | addsub4d 11236 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((1 + 1) −
((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) = ((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵)))) |
51 | 50 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((1 + 1) −
((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) = 0 ↔ ((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0)) |
52 | 48, 51 | bitr3d 284 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) = (1 + 1) ↔ ((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0)) |
53 | 52 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) ∧ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1)) → (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) = (1 + 1) ↔ ((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0)) |
54 | | subge0 11345 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ (𝑝
pCnt 𝐴) ∈ ℝ)
→ (0 ≤ (1 − (𝑝 pCnt 𝐴)) ↔ (𝑝 pCnt 𝐴) ≤ 1)) |
55 | 40, 5, 54 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (0 ≤ (1 −
(𝑝 pCnt 𝐴)) ↔ (𝑝 pCnt 𝐴) ≤ 1)) |
56 | | subge0 11345 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ (𝑝
pCnt 𝐵) ∈ ℝ)
→ (0 ≤ (1 − (𝑝 pCnt 𝐵)) ↔ (𝑝 pCnt 𝐵) ≤ 1)) |
57 | 40, 8, 56 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (0 ≤ (1 −
(𝑝 pCnt 𝐵)) ↔ (𝑝 pCnt 𝐵) ≤ 1)) |
58 | 55, 57 | anbi12d 634 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((0 ≤ (1 −
(𝑝 pCnt 𝐴)) ∧ 0 ≤ (1 − (𝑝 pCnt 𝐵))) ↔ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1))) |
59 | | resubcl 11142 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ (𝑝
pCnt 𝐴) ∈ ℝ)
→ (1 − (𝑝 pCnt
𝐴)) ∈
ℝ) |
60 | 40, 5, 59 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (1 − (𝑝 pCnt 𝐴)) ∈ ℝ) |
61 | | resubcl 11142 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ ∧ (𝑝
pCnt 𝐵) ∈ ℝ)
→ (1 − (𝑝 pCnt
𝐵)) ∈
ℝ) |
62 | 40, 8, 61 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (1 − (𝑝 pCnt 𝐵)) ∈ ℝ) |
63 | | add20 11344 |
. . . . . . . . . . . . . . . . 17
⊢ ((((1
− (𝑝 pCnt 𝐴)) ∈ ℝ ∧ 0 ≤
(1 − (𝑝 pCnt 𝐴))) ∧ ((1 − (𝑝 pCnt 𝐵)) ∈ ℝ ∧ 0 ≤ (1 −
(𝑝 pCnt 𝐵)))) → (((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0 ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0))) |
64 | 63 | an4s 660 |
. . . . . . . . . . . . . . . 16
⊢ ((((1
− (𝑝 pCnt 𝐴)) ∈ ℝ ∧ (1
− (𝑝 pCnt 𝐵)) ∈ ℝ) ∧ (0 ≤
(1 − (𝑝 pCnt 𝐴)) ∧ 0 ≤ (1 −
(𝑝 pCnt 𝐵)))) → (((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0 ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0))) |
65 | 64 | ex 416 |
. . . . . . . . . . . . . . 15
⊢ (((1
− (𝑝 pCnt 𝐴)) ∈ ℝ ∧ (1
− (𝑝 pCnt 𝐵)) ∈ ℝ) → ((0
≤ (1 − (𝑝 pCnt
𝐴)) ∧ 0 ≤ (1 −
(𝑝 pCnt 𝐵))) → (((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0 ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0)))) |
66 | 60, 62, 65 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((0 ≤ (1 −
(𝑝 pCnt 𝐴)) ∧ 0 ≤ (1 − (𝑝 pCnt 𝐵))) → (((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0 ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0)))) |
67 | 58, 66 | sylbird 263 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) → (((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0 ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0)))) |
68 | 67 | imp 410 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) ∧ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1)) → (((1 − (𝑝 pCnt 𝐴)) + (1 − (𝑝 pCnt 𝐵))) = 0 ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0))) |
69 | 53, 68 | bitrd 282 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) ∧ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1)) → (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) = (1 + 1) ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0))) |
70 | 39, 69 | syl5bb 286 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) ∧ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1)) → ((1 + 1) = ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ↔ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0))) |
71 | 70 | necon3abid 2977 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) ∧ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1)) → ((1 + 1) ≠ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ↔ ¬ ((1 − (𝑝 pCnt 𝐴)) = 0 ∧ (1 − (𝑝 pCnt 𝐵)) = 0))) |
72 | 38, 71 | mpbird 260 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) ∧ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1)) → (1 + 1) ≠ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) |
73 | 72 | ex 416 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) → (1 + 1) ≠ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)))) |
74 | 11, 73 | jcad 516 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) → (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ (1 + 1) ∧ (1 + 1) ≠ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))))) |
75 | | nnz 12199 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
76 | | nnne0 11864 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) |
77 | 75, 76 | jca 515 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) |
78 | 3, 77 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0)) |
79 | | nnz 12199 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℤ) |
80 | | nnne0 11864 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 𝐵 ≠ 0) |
81 | 79, 80 | jca 515 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) |
82 | 6, 81 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) |
83 | | pcmul 16404 |
. . . . . . . . 9
⊢ ((𝑝 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑝 pCnt (𝐴 · 𝐵)) = ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) |
84 | 2, 78, 82, 83 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝐴 · 𝐵)) = ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))) |
85 | 84 | breq1d 5063 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (𝐴 · 𝐵)) ≤ 1 ↔ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ 1)) |
86 | | 1nn0 12106 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
87 | | nn0leltp1 12236 |
. . . . . . . 8
⊢ ((((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ∈ ℕ0 ∧ 1 ∈
ℕ0) → (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ 1 ↔ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) < (1 + 1))) |
88 | 43, 86, 87 | sylancl 589 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ 1 ↔ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) < (1 + 1))) |
89 | | ltlen 10933 |
. . . . . . . 8
⊢ ((((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ∈ ℝ ∧ (1 + 1) ∈
ℝ) → (((𝑝 pCnt
𝐴) + (𝑝 pCnt 𝐵)) < (1 + 1) ↔ (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ (1 + 1) ∧ (1 + 1) ≠ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))))) |
90 | 44, 41, 89 | sylancl 589 |
. . . . . . 7
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) < (1 + 1) ↔ (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ (1 + 1) ∧ (1 + 1) ≠ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))))) |
91 | 85, 88, 90 | 3bitrd 308 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt (𝐴 · 𝐵)) ≤ 1 ↔ (((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵)) ≤ (1 + 1) ∧ (1 + 1) ≠ ((𝑝 pCnt 𝐴) + (𝑝 pCnt 𝐵))))) |
92 | 74, 91 | sylibrd 262 |
. . . . 5
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ 𝑝 ∈ ℙ) → (((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) → (𝑝 pCnt (𝐴 · 𝐵)) ≤ 1)) |
93 | 92 | ralimdva 3100 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → (∀𝑝 ∈ ℙ ((𝑝 pCnt 𝐴) ≤ 1 ∧ (𝑝 pCnt 𝐵) ≤ 1) → ∀𝑝 ∈ ℙ (𝑝 pCnt (𝐴 · 𝐵)) ≤ 1)) |
94 | 1, 93 | syl5bir 246 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → ((∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1 ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐵) ≤ 1) → ∀𝑝 ∈ ℙ (𝑝 pCnt (𝐴 · 𝐵)) ≤ 1)) |
95 | | issqf 26018 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
((μ‘𝐴) ≠ 0
↔ ∀𝑝 ∈
ℙ (𝑝 pCnt 𝐴) ≤ 1)) |
96 | | issqf 26018 |
. . . . 5
⊢ (𝐵 ∈ ℕ →
((μ‘𝐵) ≠ 0
↔ ∀𝑝 ∈
ℙ (𝑝 pCnt 𝐵) ≤ 1)) |
97 | 95, 96 | bi2anan9 639 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(((μ‘𝐴) ≠ 0
∧ (μ‘𝐵) ≠
0) ↔ (∀𝑝 ∈
ℙ (𝑝 pCnt 𝐴) ≤ 1 ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐵) ≤ 1))) |
98 | 97 | 3adant3 1134 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → (((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0) ↔ (∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ 1 ∧ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐵) ≤ 1))) |
99 | | nnmulcl 11854 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 · 𝐵) ∈ ℕ) |
100 | 99 | 3adant3 1134 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → (𝐴 · 𝐵) ∈ ℕ) |
101 | | issqf 26018 |
. . . 4
⊢ ((𝐴 · 𝐵) ∈ ℕ → ((μ‘(𝐴 · 𝐵)) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (𝐴 · 𝐵)) ≤ 1)) |
102 | 100, 101 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → ((μ‘(𝐴 · 𝐵)) ≠ 0 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt (𝐴 · 𝐵)) ≤ 1)) |
103 | 94, 98, 102 | 3imtr4d 297 |
. 2
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) → (((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0) →
(μ‘(𝐴 ·
𝐵)) ≠
0)) |
104 | 103 | imp 410 |
1
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ (𝐴 gcd 𝐵) = 1) ∧ ((μ‘𝐴) ≠ 0 ∧ (μ‘𝐵) ≠ 0)) → (μ‘(𝐴 · 𝐵)) ≠ 0) |