Proof of Theorem sqf11
Step | Hyp | Ref
| Expression |
1 | | nnnn0 11176 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
2 | | nnnn0 11176 |
. . . 4
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℕ0) |
3 | | pc11 15422 |
. . . 4
⊢ ((𝐴 ∈ ℕ0
∧ 𝐵 ∈
ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
4 | 1, 2, 3 | syl2an 493 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
5 | 4 | ad2ant2r 779 |
. 2
⊢ (((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
6 | | eleq1 2676 |
. . . . 5
⊢ ((𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ (𝑝 pCnt 𝐵) ∈ ℕ)) |
7 | | dfbi3 933 |
. . . . . 6
⊢ (((𝑝 pCnt 𝐴) ∈ ℕ ↔ (𝑝 pCnt 𝐵) ∈ ℕ) ↔ (((𝑝 pCnt 𝐴) ∈ ℕ ∧ (𝑝 pCnt 𝐵) ∈ ℕ) ∨ (¬ (𝑝 pCnt 𝐴) ∈ ℕ ∧ ¬ (𝑝 pCnt 𝐵) ∈ ℕ))) |
8 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) → 𝐴 ∈
ℕ) |
9 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ 𝐴 ∈
ℕ) |
10 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (μ‘𝐴) ≠
0) |
11 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ 𝑝 ∈
ℙ) |
12 | | sqfpc 24663 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0 ∧
𝑝 ∈ ℙ) →
(𝑝 pCnt 𝐴) ≤ 1) |
13 | 9, 10, 11, 12 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (𝑝 pCnt 𝐴) ≤ 1) |
14 | | nnle1eq1 10925 |
. . . . . . . . . 10
⊢ ((𝑝 pCnt 𝐴) ∈ ℕ → ((𝑝 pCnt 𝐴) ≤ 1 ↔ (𝑝 pCnt 𝐴) = 1)) |
15 | 13, 14 | syl5ibcom 234 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐴) ∈ ℕ → (𝑝 pCnt 𝐴) = 1)) |
16 | | simprl 790 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) → 𝐵 ∈
ℕ) |
17 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ 𝐵 ∈
ℕ) |
18 | | simplrr 797 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (μ‘𝐵) ≠
0) |
19 | | sqfpc 24663 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℕ ∧
(μ‘𝐵) ≠ 0 ∧
𝑝 ∈ ℙ) →
(𝑝 pCnt 𝐵) ≤ 1) |
20 | 17, 18, 11, 19 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (𝑝 pCnt 𝐵) ≤ 1) |
21 | | nnle1eq1 10925 |
. . . . . . . . . 10
⊢ ((𝑝 pCnt 𝐵) ∈ ℕ → ((𝑝 pCnt 𝐵) ≤ 1 ↔ (𝑝 pCnt 𝐵) = 1)) |
22 | 20, 21 | syl5ibcom 234 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐵) ∈ ℕ → (𝑝 pCnt 𝐵) = 1)) |
23 | 15, 22 | anim12d 584 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (((𝑝 pCnt 𝐴) ∈ ℕ ∧ (𝑝 pCnt 𝐵) ∈ ℕ) → ((𝑝 pCnt 𝐴) = 1 ∧ (𝑝 pCnt 𝐵) = 1))) |
24 | | eqtr3 2631 |
. . . . . . . 8
⊢ (((𝑝 pCnt 𝐴) = 1 ∧ (𝑝 pCnt 𝐵) = 1) → (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵)) |
25 | 23, 24 | syl6 34 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (((𝑝 pCnt 𝐴) ∈ ℕ ∧ (𝑝 pCnt 𝐵) ∈ ℕ) → (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
26 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) |
27 | | pccl 15392 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
28 | 26, 8, 27 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (𝑝 pCnt 𝐴) ∈
ℕ0) |
29 | | elnn0 11171 |
. . . . . . . . . . 11
⊢ ((𝑝 pCnt 𝐴) ∈ ℕ0 ↔ ((𝑝 pCnt 𝐴) ∈ ℕ ∨ (𝑝 pCnt 𝐴) = 0)) |
30 | 28, 29 | sylib 207 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐴) ∈ ℕ ∨ (𝑝 pCnt 𝐴) = 0)) |
31 | 30 | ord 391 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (¬ (𝑝 pCnt 𝐴) ∈ ℕ → (𝑝 pCnt 𝐴) = 0)) |
32 | | pccl 15392 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ) → (𝑝 pCnt 𝐵) ∈
ℕ0) |
33 | 26, 16, 32 | syl2anr 494 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (𝑝 pCnt 𝐵) ∈
ℕ0) |
34 | | elnn0 11171 |
. . . . . . . . . . 11
⊢ ((𝑝 pCnt 𝐵) ∈ ℕ0 ↔ ((𝑝 pCnt 𝐵) ∈ ℕ ∨ (𝑝 pCnt 𝐵) = 0)) |
35 | 33, 34 | sylib 207 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐵) ∈ ℕ ∨ (𝑝 pCnt 𝐵) = 0)) |
36 | 35 | ord 391 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (¬ (𝑝 pCnt 𝐵) ∈ ℕ → (𝑝 pCnt 𝐵) = 0)) |
37 | 31, 36 | anim12d 584 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((¬ (𝑝 pCnt
𝐴) ∈ ℕ ∧
¬ (𝑝 pCnt 𝐵) ∈ ℕ) → ((𝑝 pCnt 𝐴) = 0 ∧ (𝑝 pCnt 𝐵) = 0))) |
38 | | eqtr3 2631 |
. . . . . . . 8
⊢ (((𝑝 pCnt 𝐴) = 0 ∧ (𝑝 pCnt 𝐵) = 0) → (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵)) |
39 | 37, 38 | syl6 34 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((¬ (𝑝 pCnt
𝐴) ∈ ℕ ∧
¬ (𝑝 pCnt 𝐵) ∈ ℕ) → (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
40 | 25, 39 | jaod 394 |
. . . . . 6
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((((𝑝 pCnt 𝐴) ∈ ℕ ∧ (𝑝 pCnt 𝐵) ∈ ℕ) ∨ (¬ (𝑝 pCnt 𝐴) ∈ ℕ ∧ ¬ (𝑝 pCnt 𝐵) ∈ ℕ)) → (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
41 | 7, 40 | syl5bi 231 |
. . . . 5
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (((𝑝 pCnt 𝐴) ∈ ℕ ↔ (𝑝 pCnt 𝐵) ∈ ℕ) → (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) |
42 | 6, 41 | impbid2 215 |
. . . 4
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵) ↔ ((𝑝 pCnt 𝐴) ∈ ℕ ↔ (𝑝 pCnt 𝐵) ∈ ℕ))) |
43 | | pcelnn 15412 |
. . . . . 6
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ) → ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) |
44 | 26, 8, 43 | syl2anr 494 |
. . . . 5
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐴) ∈ ℕ ↔ 𝑝 ∥ 𝐴)) |
45 | | pcelnn 15412 |
. . . . . 6
⊢ ((𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ) → ((𝑝 pCnt 𝐵) ∈ ℕ ↔ 𝑝 ∥ 𝐵)) |
46 | 26, 16, 45 | syl2anr 494 |
. . . . 5
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐵) ∈ ℕ ↔ 𝑝 ∥ 𝐵)) |
47 | 44, 46 | bibi12d 334 |
. . . 4
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ (((𝑝 pCnt 𝐴) ∈ ℕ ↔ (𝑝 pCnt 𝐵) ∈ ℕ) ↔ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) |
48 | 42, 47 | bitrd 267 |
. . 3
⊢ ((((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) ∧ 𝑝 ∈ ℙ)
→ ((𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵) ↔ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) |
49 | 48 | ralbidva 2968 |
. 2
⊢ (((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) → (∀𝑝
∈ ℙ (𝑝 pCnt
𝐴) = (𝑝 pCnt 𝐵) ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) |
50 | 5, 49 | bitrd 267 |
1
⊢ (((𝐴 ∈ ℕ ∧
(μ‘𝐴) ≠ 0)
∧ (𝐵 ∈ ℕ
∧ (μ‘𝐵) ≠
0)) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵))) |