Proof of Theorem prmdvdsbc
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . 3
⊢
((!‘𝑃) /
((!‘(𝑃 − 𝑁)) · (!‘𝑁))) = ((!‘𝑃) / ((!‘(𝑃 − 𝑁)) · (!‘𝑁))) | 
| 2 |  | simpl 482 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ) | 
| 3 |  | prmnn 16711 | . . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 4 | 3 | nnzd 12640 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 5 |  | 1nn0 12542 | . . . . . . . . 9
⊢ 1 ∈
ℕ0 | 
| 6 |  | eluzmn 12885 | . . . . . . . . 9
⊢ ((𝑃 ∈ ℤ ∧ 1 ∈
ℕ0) → 𝑃 ∈ (ℤ≥‘(𝑃 − 1))) | 
| 7 | 4, 5, 6 | sylancl 586 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘(𝑃 − 1))) | 
| 8 |  | fzss2 13604 | . . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘(𝑃 − 1)) → (1...(𝑃 − 1)) ⊆ (1...𝑃)) | 
| 9 | 7, 8 | syl 17 | . . . . . . 7
⊢ (𝑃 ∈ ℙ →
(1...(𝑃 − 1)) ⊆
(1...𝑃)) | 
| 10 |  | fz1ssfz0 13663 | . . . . . . 7
⊢
(1...𝑃) ⊆
(0...𝑃) | 
| 11 | 9, 10 | sstrdi 3996 | . . . . . 6
⊢ (𝑃 ∈ ℙ →
(1...(𝑃 − 1)) ⊆
(0...𝑃)) | 
| 12 | 11 | sselda 3983 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (0...𝑃)) | 
| 13 |  | bcval2 14344 | . . . . 5
⊢ (𝑁 ∈ (0...𝑃) → (𝑃C𝑁) = ((!‘𝑃) / ((!‘(𝑃 − 𝑁)) · (!‘𝑁)))) | 
| 14 | 12, 13 | syl 17 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃C𝑁) = ((!‘𝑃) / ((!‘(𝑃 − 𝑁)) · (!‘𝑁)))) | 
| 15 | 3 | nnnn0d 12587 | . . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ0) | 
| 16 | 15 | adantr 480 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈
ℕ0) | 
| 17 |  | elfzelz 13564 | . . . . . . 7
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℤ) | 
| 18 | 17 | adantl 481 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℤ) | 
| 19 |  | bccl 14361 | . . . . . 6
⊢ ((𝑃 ∈ ℕ0
∧ 𝑁 ∈ ℤ)
→ (𝑃C𝑁) ∈
ℕ0) | 
| 20 | 16, 18, 19 | syl2anc 584 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃C𝑁) ∈
ℕ0) | 
| 21 | 20 | nn0zd 12639 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃C𝑁) ∈ ℤ) | 
| 22 | 14, 21 | eqeltrrd 2842 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((!‘𝑃) / ((!‘(𝑃 − 𝑁)) · (!‘𝑁))) ∈ ℤ) | 
| 23 |  | elfznn 13593 | . . . . . . . . 9
⊢ (𝑁 ∈ (1...(𝑃 − 1)) → 𝑁 ∈ ℕ) | 
| 24 | 23 | adantl 481 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ ℕ) | 
| 25 | 24 | nnnn0d 12587 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈
ℕ0) | 
| 26 |  | 1zzd 12648 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 1 ∈
ℤ) | 
| 27 | 4 | adantr 480 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℤ) | 
| 28 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈ (1...(𝑃 − 1))) | 
| 29 |  | elfzm11 13635 | . . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 𝑃
∈ ℤ) → (𝑁
∈ (1...(𝑃 − 1))
↔ (𝑁 ∈ ℤ
∧ 1 ≤ 𝑁 ∧ 𝑁 < 𝑃))) | 
| 30 | 29 | biimpa 476 | . . . . . . . . 9
⊢ (((1
∈ ℤ ∧ 𝑃
∈ ℤ) ∧ 𝑁
∈ (1...(𝑃 − 1)))
→ (𝑁 ∈ ℤ
∧ 1 ≤ 𝑁 ∧ 𝑁 < 𝑃)) | 
| 31 | 30 | simp3d 1145 | . . . . . . . 8
⊢ (((1
∈ ℤ ∧ 𝑃
∈ ℤ) ∧ 𝑁
∈ (1...(𝑃 − 1)))
→ 𝑁 < 𝑃) | 
| 32 | 26, 27, 28, 31 | syl21anc 838 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 < 𝑃) | 
| 33 |  | ltsubnn0 12577 | . . . . . . . 8
⊢ ((𝑃 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 < 𝑃 → (𝑃 − 𝑁) ∈
ℕ0)) | 
| 34 | 33 | imp 406 | . . . . . . 7
⊢ (((𝑃 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 < 𝑃) → (𝑃 − 𝑁) ∈
ℕ0) | 
| 35 | 16, 25, 32, 34 | syl21anc 838 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 𝑁) ∈
ℕ0) | 
| 36 | 35 | faccld 14323 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘(𝑃 − 𝑁)) ∈ ℕ) | 
| 37 | 36 | nnzd 12640 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘(𝑃 − 𝑁)) ∈ ℤ) | 
| 38 | 25 | faccld 14323 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘𝑁) ∈
ℕ) | 
| 39 | 38 | nnzd 12640 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘𝑁) ∈
ℤ) | 
| 40 | 37, 39 | zmulcld 12728 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((!‘(𝑃 − 𝑁)) · (!‘𝑁)) ∈ ℤ) | 
| 41 | 37 | zcnd 12723 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘(𝑃 − 𝑁)) ∈ ℂ) | 
| 42 | 39 | zcnd 12723 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘𝑁) ∈
ℂ) | 
| 43 |  | facne0 14325 | . . . . 5
⊢ ((𝑃 − 𝑁) ∈ ℕ0 →
(!‘(𝑃 − 𝑁)) ≠ 0) | 
| 44 | 35, 43 | syl 17 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘(𝑃 − 𝑁)) ≠ 0) | 
| 45 |  | facne0 14325 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (!‘𝑁) ≠
0) | 
| 46 | 25, 45 | syl 17 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (!‘𝑁) ≠ 0) | 
| 47 | 41, 42, 44, 46 | mulne0d 11915 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ((!‘(𝑃 − 𝑁)) · (!‘𝑁)) ≠ 0) | 
| 48 |  | uzid 12893 | . . . . . 6
⊢ (𝑃 ∈ ℤ → 𝑃 ∈
(ℤ≥‘𝑃)) | 
| 49 | 4, 48 | syl 17 | . . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘𝑃)) | 
| 50 |  | dvdsfac 16363 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘𝑃)) → 𝑃 ∥ (!‘𝑃)) | 
| 51 | 3, 49, 50 | syl2anc 584 | . . . 4
⊢ (𝑃 ∈ ℙ → 𝑃 ∥ (!‘𝑃)) | 
| 52 | 51 | adantr 480 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (!‘𝑃)) | 
| 53 | 16 | nn0red 12588 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℝ) | 
| 54 | 24 | nnrpd 13075 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑁 ∈
ℝ+) | 
| 55 | 53, 54 | ltsubrpd 13109 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → (𝑃 − 𝑁) < 𝑃) | 
| 56 |  | prmndvdsfaclt 16762 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 − 𝑁) ∈ ℕ0) → ((𝑃 − 𝑁) < 𝑃 → ¬ 𝑃 ∥ (!‘(𝑃 − 𝑁)))) | 
| 57 | 56 | imp 406 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 − 𝑁) ∈ ℕ0) ∧ (𝑃 − 𝑁) < 𝑃) → ¬ 𝑃 ∥ (!‘(𝑃 − 𝑁))) | 
| 58 | 2, 35, 55, 57 | syl21anc 838 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (!‘(𝑃 − 𝑁))) | 
| 59 |  | prmndvdsfaclt 16762 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
→ (𝑁 < 𝑃 → ¬ 𝑃 ∥ (!‘𝑁))) | 
| 60 | 59 | imp 406 | . . . . 5
⊢ (((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0)
∧ 𝑁 < 𝑃) → ¬ 𝑃 ∥ (!‘𝑁)) | 
| 61 | 2, 25, 32, 60 | syl21anc 838 | . . . 4
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (!‘𝑁)) | 
| 62 |  | ioran 986 | . . . . . 6
⊢ (¬
(𝑃 ∥ (!‘(𝑃 − 𝑁)) ∨ 𝑃 ∥ (!‘𝑁)) ↔ (¬ 𝑃 ∥ (!‘(𝑃 − 𝑁)) ∧ ¬ 𝑃 ∥ (!‘𝑁))) | 
| 63 |  | euclemma 16750 | . . . . . . . 8
⊢ ((𝑃 ∈ ℙ ∧
(!‘(𝑃 − 𝑁)) ∈ ℤ ∧
(!‘𝑁) ∈ ℤ)
→ (𝑃 ∥
((!‘(𝑃 − 𝑁)) · (!‘𝑁)) ↔ (𝑃 ∥ (!‘(𝑃 − 𝑁)) ∨ 𝑃 ∥ (!‘𝑁)))) | 
| 64 | 63 | biimpd 229 | . . . . . . 7
⊢ ((𝑃 ∈ ℙ ∧
(!‘(𝑃 − 𝑁)) ∈ ℤ ∧
(!‘𝑁) ∈ ℤ)
→ (𝑃 ∥
((!‘(𝑃 − 𝑁)) · (!‘𝑁)) → (𝑃 ∥ (!‘(𝑃 − 𝑁)) ∨ 𝑃 ∥ (!‘𝑁)))) | 
| 65 | 64 | con3d 152 | . . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(!‘(𝑃 − 𝑁)) ∈ ℤ ∧
(!‘𝑁) ∈ ℤ)
→ (¬ (𝑃 ∥
(!‘(𝑃 − 𝑁)) ∨ 𝑃 ∥ (!‘𝑁)) → ¬ 𝑃 ∥ ((!‘(𝑃 − 𝑁)) · (!‘𝑁)))) | 
| 66 | 62, 65 | biimtrrid 243 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧
(!‘(𝑃 − 𝑁)) ∈ ℤ ∧
(!‘𝑁) ∈ ℤ)
→ ((¬ 𝑃 ∥
(!‘(𝑃 − 𝑁)) ∧ ¬ 𝑃 ∥ (!‘𝑁)) → ¬ 𝑃 ∥ ((!‘(𝑃 − 𝑁)) · (!‘𝑁)))) | 
| 67 | 66 | imp 406 | . . . 4
⊢ (((𝑃 ∈ ℙ ∧
(!‘(𝑃 − 𝑁)) ∈ ℤ ∧
(!‘𝑁) ∈ ℤ)
∧ (¬ 𝑃 ∥
(!‘(𝑃 − 𝑁)) ∧ ¬ 𝑃 ∥ (!‘𝑁))) → ¬ 𝑃 ∥ ((!‘(𝑃 − 𝑁)) · (!‘𝑁))) | 
| 68 | 2, 37, 39, 58, 61, 67 | syl32anc 1380 | . . 3
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ ((!‘(𝑃 − 𝑁)) · (!‘𝑁))) | 
| 69 | 1, 2, 22, 40, 47, 52, 68 | dvdszzq 16758 | . 2
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ ((!‘𝑃) / ((!‘(𝑃 − 𝑁)) · (!‘𝑁)))) | 
| 70 | 69, 14 | breqtrrd 5171 | 1
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑁)) |