| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks4d1p8.1 | . 2
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) | 
| 2 |  | aks4d1p8.2 | . 2
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) | 
| 3 |  | aks4d1p8.3 | . 2
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) | 
| 4 |  | aks4d1p8.4 | . 2
⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) | 
| 5 | 4 | a1i 11 | . . . . . 6
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < )) | 
| 6 |  | ssrab2 4079 | . . . . . . . . . . . . 13
⊢ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ (1...𝐵) | 
| 7 | 6 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ (1...𝐵)) | 
| 8 |  | elfznn 13594 | . . . . . . . . . . . . . . . 16
⊢ (𝑜 ∈ (1...𝐵) → 𝑜 ∈ ℕ) | 
| 9 | 8 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑜 ∈ (1...𝐵)) → 𝑜 ∈ ℕ) | 
| 10 | 9 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑜 ∈ (1...𝐵)) → 𝑜 ∈ ℝ) | 
| 11 | 10 | ex 412 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑜 ∈ (1...𝐵) → 𝑜 ∈ ℝ)) | 
| 12 | 11 | ssrdv 3988 | . . . . . . . . . . . 12
⊢ (𝜑 → (1...𝐵) ⊆ ℝ) | 
| 13 | 7, 12 | sstrd 3993 | . . . . . . . . . . 11
⊢ (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 14 | 13 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 15 | 14 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 16 | 15 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 17 | 16 | adantr 480 | . . . . . . 7
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 18 |  | fzfid 14015 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1...𝐵) ∈ Fin) | 
| 19 | 18, 7 | ssfid 9302 | . . . . . . . . . . . 12
⊢ (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) | 
| 20 | 1, 2, 3 | aks4d1p3 42080 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟 ∥ 𝐴) | 
| 21 |  | rabn0 4388 | . . . . . . . . . . . . 13
⊢ ({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ≠ ∅ ↔ ∃𝑟 ∈ (1...𝐵) ¬ 𝑟 ∥ 𝐴) | 
| 22 | 20, 21 | sylibr 234 | . . . . . . . . . . . 12
⊢ (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ≠ ∅) | 
| 23 |  | fiminre 12216 | . . . . . . . . . . . 12
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ≠ ∅) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}𝑥 ≤ 𝑦) | 
| 24 | 13, 19, 22, 23 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}𝑥 ≤ 𝑦) | 
| 25 | 24 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}𝑥 ≤ 𝑦) | 
| 26 | 25 | adantr 480 | . . . . . . . . 9
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}𝑥 ≤ 𝑦) | 
| 27 | 26 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}𝑥 ≤ 𝑦) | 
| 28 | 27 | adantr 480 | . . . . . . 7
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}𝑥 ≤ 𝑦) | 
| 29 |  | breq1 5145 | . . . . . . . . 9
⊢ (𝑟 = (𝑅 / 𝑝) → (𝑟 ∥ 𝐴 ↔ (𝑅 / 𝑝) ∥ 𝐴)) | 
| 30 | 29 | notbid 318 | . . . . . . . 8
⊢ (𝑟 = (𝑅 / 𝑝) → (¬ 𝑟 ∥ 𝐴 ↔ ¬ (𝑅 / 𝑝) ∥ 𝐴)) | 
| 31 |  | 1zzd 12650 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ∈ ℤ) | 
| 32 | 3 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) | 
| 33 |  | 2re 12341 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ | 
| 34 | 33 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ) | 
| 35 |  | 2pos 12370 | . . . . . . . . . . . . . . 15
⊢ 0 <
2 | 
| 36 | 35 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 2) | 
| 37 |  | eluzelz 12889 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) | 
| 38 | 1, 37 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 39 | 38 | zred 12724 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 40 |  | 0red 11265 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℝ) | 
| 41 |  | 3re 12347 | . . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ | 
| 42 | 41 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 ∈
ℝ) | 
| 43 |  | 3pos 12372 | . . . . . . . . . . . . . . . 16
⊢ 0 <
3 | 
| 44 | 43 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 3) | 
| 45 |  | eluzle 12892 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) | 
| 46 | 1, 45 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 ≤ 𝑁) | 
| 47 | 40, 42, 39, 44, 46 | ltletrd 11422 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) | 
| 48 |  | 1red 11263 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) | 
| 49 |  | 1lt2 12438 | . . . . . . . . . . . . . . . . 17
⊢ 1 <
2 | 
| 50 | 49 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 < 2) | 
| 51 | 48, 50 | ltned 11398 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≠ 2) | 
| 52 | 51 | necomd 2995 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 1) | 
| 53 | 34, 36, 39, 47, 52 | relogbcld 41975 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) | 
| 54 |  | 5nn0 12548 | . . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ0 | 
| 55 | 54 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 5 ∈
ℕ0) | 
| 56 | 53, 55 | reexpcld 14204 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) | 
| 57 | 56 | ceilcld 13884 | . . . . . . . . . . 11
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) | 
| 58 | 32, 57 | eqeltrd 2840 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 59 | 58 | ad4antr 732 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝐵 ∈ ℤ) | 
| 60 |  | simplrl 776 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∥ 𝑅) | 
| 61 |  | prmnn 16712 | . . . . . . . . . . . . . 14
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) | 
| 62 | 61 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ) | 
| 63 | 62 | ad2antrr 726 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℕ) | 
| 64 | 63 | nnzd 12642 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℤ) | 
| 65 | 62 | nnne0d 12317 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ≠ 0) | 
| 66 | 65 | ad2antrr 726 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ≠ 0) | 
| 67 | 1, 2, 3, 4 | aks4d1p4 42081 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅 ∥ 𝐴)) | 
| 68 | 67 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑅 ∈ (1...𝐵)) | 
| 69 |  | elfznn 13594 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ (1...𝐵) → 𝑅 ∈ ℕ) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 71 | 70 | ad4antr 732 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) → 𝑅 ∈ ℕ) | 
| 72 | 71 | adantr 480 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℕ) | 
| 73 | 72 | nnzd 12642 | . . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ) | 
| 74 |  | anass 468 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) ↔ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁))) | 
| 75 | 74 | anbi1i 624 | . . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) ↔ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴)) | 
| 76 | 75 | imbi1i 349 | . . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ) ↔ (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ)) | 
| 77 | 73, 76 | mpbi 230 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ) | 
| 78 |  | dvdsval2 16294 | . . . . . . . . . . 11
⊢ ((𝑝 ∈ ℤ ∧ 𝑝 ≠ 0 ∧ 𝑅 ∈ ℤ) → (𝑝 ∥ 𝑅 ↔ (𝑅 / 𝑝) ∈ ℤ)) | 
| 79 | 64, 66, 77, 78 | syl3anc 1372 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑝 ∥ 𝑅 ↔ (𝑅 / 𝑝) ∈ ℤ)) | 
| 80 | 60, 79 | mpbid 232 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ ℤ) | 
| 81 | 63 | nncnd 12283 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℂ) | 
| 82 | 81 | mullidd 11280 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (1 · 𝑝) = 𝑝) | 
| 83 | 75, 72 | sylbir 235 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℕ) | 
| 84 | 64, 83 | jca 511 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ)) | 
| 85 |  | dvdsle 16348 | . . . . . . . . . . . . 13
⊢ ((𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ) → (𝑝 ∥ 𝑅 → 𝑝 ≤ 𝑅)) | 
| 86 | 85 | imp 406 | . . . . . . . . . . . 12
⊢ (((𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ) ∧ 𝑝 ∥ 𝑅) → 𝑝 ≤ 𝑅) | 
| 87 | 84, 60, 86 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ≤ 𝑅) | 
| 88 | 82, 87 | eqbrtrd 5164 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (1 · 𝑝) ≤ 𝑅) | 
| 89 |  | 1red 11263 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ∈ ℝ) | 
| 90 | 70 | nnred 12282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 91 | 90 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑅 ∈ ℝ) | 
| 92 | 91 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ∈ ℝ) | 
| 93 | 92 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 ∈ ℝ) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℝ) | 
| 95 | 63 | nnrpd 13076 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℝ+) | 
| 96 | 89, 94, 95 | lemuldivd 13127 | . . . . . . . . . 10
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ((1 · 𝑝) ≤ 𝑅 ↔ 1 ≤ (𝑅 / 𝑝))) | 
| 97 | 88, 96 | mpbid 232 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ≤ (𝑅 / 𝑝)) | 
| 98 | 90 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ∈ ℝ) | 
| 99 | 58 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ) | 
| 100 | 99 | zred 12724 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℝ) | 
| 101 | 62 | nnred 12282 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ) | 
| 102 | 100, 101 | remulcld 11292 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → (𝐵 · 𝑝) ∈ ℝ) | 
| 103 |  | elfzle2 13569 | . . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ (1...𝐵) → 𝑅 ≤ 𝐵) | 
| 104 | 68, 103 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ≤ 𝐵) | 
| 105 | 104 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑅 ≤ 𝐵) | 
| 106 | 105 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ≤ 𝐵) | 
| 107 | 58 | zred 12724 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 108 |  | 9re 12366 | . . . . . . . . . . . . . . . . . . 19
⊢ 9 ∈
ℝ | 
| 109 | 108 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 9 ∈
ℝ) | 
| 110 |  | 9pos 12380 | . . . . . . . . . . . . . . . . . . 19
⊢ 0 <
9 | 
| 111 | 110 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 < 9) | 
| 112 | 32, 107 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℝ) | 
| 113 | 39, 46 | 3lexlogpow5ineq4 42058 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 9 < ((2 logb
𝑁)↑5)) | 
| 114 | 56 | ceilged 13887 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤
(⌈‘((2 logb 𝑁)↑5))) | 
| 115 | 109, 56, 112, 113, 114 | ltletrd 11422 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 9 < (⌈‘((2
logb 𝑁)↑5))) | 
| 116 | 115, 32 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 9 < 𝐵) | 
| 117 | 40, 109, 107, 111, 116 | lttrd 11423 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 𝐵) | 
| 118 | 40, 107, 117 | ltled 11410 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 𝐵) | 
| 119 | 118 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 0 ≤ 𝐵) | 
| 120 | 119 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 0 ≤ 𝐵) | 
| 121 | 62 | nnge1d 12315 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 1 ≤ 𝑝) | 
| 122 | 100, 101,
120, 121 | lemulge11d 12206 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝐵 ≤ (𝐵 · 𝑝)) | 
| 123 | 98, 100, 102, 106, 122 | letrd 11419 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ≤ (𝐵 · 𝑝)) | 
| 124 | 62 | nnrpd 13076 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+) | 
| 125 | 98, 100, 124 | ledivmul2d 13132 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → ((𝑅 / 𝑝) ≤ 𝐵 ↔ 𝑅 ≤ (𝐵 · 𝑝))) | 
| 126 | 123, 125 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → (𝑅 / 𝑝) ≤ 𝐵) | 
| 127 | 126 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / 𝑝) ≤ 𝐵) | 
| 128 | 127 | adantr 480 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ≤ 𝐵) | 
| 129 | 31, 59, 80, 97, 128 | elfzd 13556 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ (1...𝐵)) | 
| 130 | 93 | recnd 11290 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 ∈ ℂ) | 
| 131 | 62 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ∈ ℕ) | 
| 132 | 131 | nnzd 12642 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ∈ ℤ) | 
| 133 |  | simplr 768 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ∈ ℙ) | 
| 134 | 71 | anasss 466 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 ∈ ℕ) | 
| 135 | 133, 134 | pccld 16889 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝 pCnt 𝑅) ∈
ℕ0) | 
| 136 | 132, 135 | zexpcld 14129 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℤ) | 
| 137 | 136 | zcnd 12725 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℂ) | 
| 138 | 131 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ∈ ℂ) | 
| 139 | 65 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ≠ 0) | 
| 140 | 135 | nn0zd 12641 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝 pCnt 𝑅) ∈ ℤ) | 
| 141 | 138, 139,
140 | expne0d 14193 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ≠ 0) | 
| 142 | 130, 137,
141 | divcan1d 12045 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) · (𝑝↑(𝑝 pCnt 𝑅))) = 𝑅) | 
| 143 | 142 | eqcomd 2742 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 = ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) · (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 144 |  | pcdvds 16903 | . . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ ℙ ∧ 𝑅 ∈ ℕ) → (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅) | 
| 145 | 133, 134,
144 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅) | 
| 146 | 134 | nnzd 12642 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 ∈ ℤ) | 
| 147 |  | dvdsval2 16294 | . . . . . . . . . . . . . 14
⊢ (((𝑝↑(𝑝 pCnt 𝑅)) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt 𝑅)) ≠ 0 ∧ 𝑅 ∈ ℤ) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℤ)) | 
| 148 | 136, 141,
146, 147 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℤ)) | 
| 149 | 145, 148 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℤ) | 
| 150 | 38, 47 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 0 < 𝑁)) | 
| 151 |  | elnnz 12625 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) | 
| 152 | 151 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))) | 
| 153 | 150, 152 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 154 | 153 | nnzd 12642 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 155 | 34, 36, 107, 117, 52 | relogbcld 41975 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) | 
| 156 | 155 | flcld 13839 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℤ) | 
| 157 | 34 | recnd 11290 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 2 ∈
ℂ) | 
| 158 | 40, 36 | gtned 11397 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 2 ≠ 0) | 
| 159 |  | logb1 26813 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) =
0) | 
| 160 | 157, 158,
52, 159 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (2 logb 1) =
0) | 
| 161 | 160 | eqcomd 2742 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 = (2 logb
1)) | 
| 162 |  | 2z 12651 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℤ | 
| 163 | 162 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ∈
ℤ) | 
| 164 | 34 | leidd 11830 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ≤ 2) | 
| 165 |  | 0lt1 11786 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 <
1 | 
| 166 | 165 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 < 1) | 
| 167 |  | 1lt9 12473 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 <
9 | 
| 168 | 167 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 < 9) | 
| 169 | 48, 109, 107, 168, 116 | lttrd 11423 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 < 𝐵) | 
| 170 | 48, 107, 169 | ltled 11410 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ 𝐵) | 
| 171 | 163, 164,
48, 166, 107, 117, 170 | logblebd 41978 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (2 logb 1) ≤
(2 logb 𝐵)) | 
| 172 | 161, 171 | eqbrtrd 5164 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ (2 logb
𝐵)) | 
| 173 |  | 0zd 12627 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 ∈
ℤ) | 
| 174 |  | flge 13846 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((2
logb 𝐵) ∈
ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) | 
| 175 | 155, 173,
174 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (0 ≤ (2 logb
𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) | 
| 176 | 172, 175 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (⌊‘(2
logb 𝐵))) | 
| 177 | 156, 176 | jca 511 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))) | 
| 178 |  | elnn0z 12628 | . . . . . . . . . . . . . . . . . 18
⊢
((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔
((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵)))) | 
| 179 | 178 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℕ0 ↔ ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵))))) | 
| 180 | 177, 179 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℕ0) | 
| 181 | 154, 180 | zexpcld 14129 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁↑(⌊‘(2 logb
𝐵))) ∈
ℤ) | 
| 182 |  | fzfid 14015 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ∈ Fin) | 
| 183 | 154 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℤ) | 
| 184 |  | elfznn 13594 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ) | 
| 185 | 184 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ) | 
| 186 | 185 | nnnn0d 12589 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) | 
| 187 | 183, 186 | zexpcld 14129 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℤ) | 
| 188 |  | 1zzd 12650 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℤ) | 
| 189 | 187, 188 | zsubcld 12729 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℤ) | 
| 190 | 182, 189 | fprodzcl 15991 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℤ) | 
| 191 | 181, 190 | zmulcld 12730 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℤ) | 
| 192 | 2 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) | 
| 193 | 192 | eleq1d 2825 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 ∈ ℤ ↔ ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℤ)) | 
| 194 | 191, 193 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 195 | 194 | ad3antrrr 730 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝐴 ∈ ℤ) | 
| 196 |  | simprl 770 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ∥ 𝑅) | 
| 197 | 134, 133,
196 | aks4d1p8d3 42088 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) gcd (𝑝↑(𝑝 pCnt 𝑅))) = 1) | 
| 198 | 138 | exp0d 14181 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑0) = 1) | 
| 199 |  | pcelnn 16909 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ ℙ ∧ 𝑅 ∈ ℕ) → ((𝑝 pCnt 𝑅) ∈ ℕ ↔ 𝑝 ∥ 𝑅)) | 
| 200 | 133, 134,
199 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑝 pCnt 𝑅) ∈ ℕ ↔ 𝑝 ∥ 𝑅)) | 
| 201 | 196, 200 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝 pCnt 𝑅) ∈ ℕ) | 
| 202 | 201 | nngt0d 12316 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 0 < (𝑝 pCnt 𝑅)) | 
| 203 | 101 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ∈ ℝ) | 
| 204 | 173 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 0 ∈ ℤ) | 
| 205 |  | prmgt1 16735 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 ∈ ℙ → 1 <
𝑝) | 
| 206 | 205 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 1 < 𝑝) | 
| 207 | 206 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 < 𝑝) | 
| 208 | 203, 204,
140, 207 | ltexp2d 14291 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (0 < (𝑝 pCnt 𝑅) ↔ (𝑝↑0) < (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 209 | 202, 208 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑0) < (𝑝↑(𝑝 pCnt 𝑅))) | 
| 210 | 198, 209 | eqbrtrrd 5166 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 < (𝑝↑(𝑝 pCnt 𝑅))) | 
| 211 | 136 | zred 12724 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℝ) | 
| 212 | 70 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑅 ∈
ℝ+) | 
| 213 | 212 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑅 ∈
ℝ+) | 
| 214 | 213 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ∈
ℝ+) | 
| 215 | 214 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 ∈
ℝ+) | 
| 216 | 211, 215 | ltmulgt11d 13113 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (1 < (𝑝↑(𝑝 pCnt 𝑅)) ↔ 𝑅 < (𝑅 · (𝑝↑(𝑝 pCnt 𝑅))))) | 
| 217 | 210, 216 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 < (𝑅 · (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 218 | 124 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑝 ∈ ℝ+) | 
| 219 | 218, 140 | rpexpcld 14287 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈
ℝ+) | 
| 220 | 93, 93, 219 | ltdivmul2d 13130 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) < 𝑅 ↔ 𝑅 < (𝑅 · (𝑝↑(𝑝 pCnt 𝑅))))) | 
| 221 | 217, 220 | mpbird 257 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) < 𝑅) | 
| 222 | 93, 211, 141 | redivcld 12096 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℝ) | 
| 223 | 222, 93 | ltnled 11409 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) < 𝑅 ↔ ¬ 𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))) | 
| 224 | 221, 223 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ¬ 𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 225 | 4 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < )) | 
| 226 | 225 | breq1d 5152 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ↔ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))) | 
| 227 | 226 | notbid 318 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (¬ 𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ↔ ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))) | 
| 228 | 224, 227 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 229 |  | elfznn 13594 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ (1...𝐵) → 𝑓 ∈ ℕ) | 
| 230 | 229 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓 ∈ (1...𝐵)) → 𝑓 ∈ ℕ) | 
| 231 | 230 | nnred 12282 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ (1...𝐵)) → 𝑓 ∈ ℝ) | 
| 232 | 231 | ex 412 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑓 ∈ (1...𝐵) → 𝑓 ∈ ℝ)) | 
| 233 | 232 | ssrdv 3988 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (1...𝐵) ⊆ ℝ) | 
| 234 | 7, 233 | sstrd 3993 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 235 | 234 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 236 | 235 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 237 | 236 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ) | 
| 238 | 19 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) | 
| 239 | 238 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) | 
| 240 | 239 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) | 
| 241 |  | infrefilb 12255 | . . . . . . . . . . . . . . . . . 18
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin ∧ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 242 | 241 | 3expa 1118 | . . . . . . . . . . . . . . . . 17
⊢ ((({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) ∧ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 243 | 242 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))) | 
| 244 | 243 | con3d 152 | . . . . . . . . . . . . . . 15
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴})) | 
| 245 | 237, 240,
244 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴})) | 
| 246 | 228, 245 | mpd 15 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) | 
| 247 |  | 1zzd 12650 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 ∈ ℤ) | 
| 248 | 99 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝐵 ∈ ℤ) | 
| 249 | 137 | mullidd 11280 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (1 · (𝑝↑(𝑝 pCnt 𝑅))) = (𝑝↑(𝑝 pCnt 𝑅))) | 
| 250 |  | dvdsle 16348 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑝↑(𝑝 pCnt 𝑅)) ∈ ℤ ∧ 𝑅 ∈ ℕ) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝑅)) | 
| 251 | 136, 134,
250 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝑅)) | 
| 252 | 145, 251 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝑅) | 
| 253 | 249, 252 | eqbrtrd 5164 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (1 · (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅) | 
| 254 | 48 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 1 ∈ ℝ) | 
| 255 | 254 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 ∈ ℝ) | 
| 256 | 255, 93, 219 | lemuldivd 13127 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((1 · (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅 ↔ 1 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))) | 
| 257 | 253, 256 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 258 | 100 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝐵 ∈ ℝ) | 
| 259 | 121 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 ≤ 𝑝) | 
| 260 | 203, 135,
259 | expge1d 14206 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 ≤ (𝑝↑(𝑝 pCnt 𝑅))) | 
| 261 |  | nnledivrp 13148 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ∈ ℕ ∧ (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℝ+) → (1
≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅)) | 
| 262 | 134, 219,
261 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (1 ≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅)) | 
| 263 | 260, 262 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅) | 
| 264 | 106 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 ≤ 𝐵) | 
| 265 | 222, 93, 258, 263, 264 | letrd 11419 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝐵) | 
| 266 | 247, 248,
149, 257, 265 | elfzd 13556 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ (1...𝐵)) | 
| 267 |  | breq1 5145 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 = (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → (𝑟 ∥ 𝐴 ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴)) | 
| 268 | 267 | notbid 318 | . . . . . . . . . . . . . . . 16
⊢ (𝑟 = (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → (¬ 𝑟 ∥ 𝐴 ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴)) | 
| 269 | 268 | elrab3 3692 | . . . . . . . . . . . . . . 15
⊢ ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ (1...𝐵) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴)) | 
| 270 | 269 | con2bid 354 | . . . . . . . . . . . . . 14
⊢ ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ (1...𝐵) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴 ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴})) | 
| 271 | 266, 270 | syl 17 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴 ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴})) | 
| 272 | 246, 271 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴) | 
| 273 | 134 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → 𝑅 ∈ ℕ) | 
| 274 | 153 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑁 ∈ ℕ) | 
| 275 | 274 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ) | 
| 276 | 275 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) → 𝑁 ∈ ℕ) | 
| 277 | 276 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) → 𝑁 ∈ ℕ) | 
| 278 | 74, 277 | sylbir 235 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑁 ∈ ℕ) | 
| 279 | 278 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → 𝑁 ∈ ℕ) | 
| 280 | 133 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → 𝑝 ∈ ℙ) | 
| 281 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → 𝑞 ∈ ℙ) | 
| 282 | 196 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → 𝑝 ∥ 𝑅) | 
| 283 |  | simprr 772 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → 𝑞 ∥ 𝑅) | 
| 284 |  | simplrr 777 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) → ¬ 𝑝 ∥ 𝑁) | 
| 285 | 284 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → ¬ 𝑝 ∥ 𝑁) | 
| 286 |  | simprl 770 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → 𝑞 ∥ 𝑁) | 
| 287 | 273, 279,
280, 281, 282, 283, 285, 286 | aks4d1p8d2 42087 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) → (𝑝↑(𝑝 pCnt 𝑅)) < 𝑅) | 
| 288 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 1 < (𝑁 gcd 𝑅)) | 
| 289 | 288 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 < (𝑁 gcd 𝑅)) | 
| 290 | 255, 289 | ltned 11398 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 1 ≠ (𝑁 gcd 𝑅)) | 
| 291 | 290 | necomd 2995 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑁 gcd 𝑅) ≠ 1) | 
| 292 | 278, 134 | prmdvdsncoprmbd 16765 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (∃𝑞 ∈ ℙ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅) ↔ (𝑁 gcd 𝑅) ≠ 1)) | 
| 293 | 292 | bicomd 223 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑁 gcd 𝑅) ≠ 1 ↔ ∃𝑞 ∈ ℙ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅))) | 
| 294 | 293 | biimpd 229 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑁 gcd 𝑅) ≠ 1 → ∃𝑞 ∈ ℙ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅))) | 
| 295 | 291, 294 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ∃𝑞 ∈ ℙ (𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅)) | 
| 296 | 287, 295 | r19.29a 3161 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) < 𝑅) | 
| 297 | 211, 93 | ltnled 11409 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) < 𝑅 ↔ ¬ 𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 298 | 296, 297 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ¬ 𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅))) | 
| 299 | 225 | breq1d 5152 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 300 | 299 | notbid 318 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (¬ 𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 301 | 298, 300 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅))) | 
| 302 |  | infrefilb 12255 | . . . . . . . . . . . . . . . . . 18
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin ∧ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅))) | 
| 303 | 302 | 3expa 1118 | . . . . . . . . . . . . . . . . 17
⊢ ((({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) ∧ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅))) | 
| 304 | 303 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) → ((𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)))) | 
| 305 | 304 | con3d 152 | . . . . . . . . . . . . . . 15
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ∈ Fin) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)) → ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴})) | 
| 306 | 237, 240,
305 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)) → ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴})) | 
| 307 | 301, 306 | mpd 15 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) | 
| 308 | 211, 93, 258, 252, 264 | letrd 11419 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝐵) | 
| 309 | 247, 248,
136, 260, 308 | elfzd 13556 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ (1...𝐵)) | 
| 310 |  | breq1 5145 | . . . . . . . . . . . . . . . . 17
⊢ (𝑟 = (𝑝↑(𝑝 pCnt 𝑅)) → (𝑟 ∥ 𝐴 ↔ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴)) | 
| 311 | 310 | notbid 318 | . . . . . . . . . . . . . . . 16
⊢ (𝑟 = (𝑝↑(𝑝 pCnt 𝑅)) → (¬ 𝑟 ∥ 𝐴 ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴)) | 
| 312 | 311 | elrab3 3692 | . . . . . . . . . . . . . . 15
⊢ ((𝑝↑(𝑝 pCnt 𝑅)) ∈ (1...𝐵) → ((𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴)) | 
| 313 | 309, 312 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴)) | 
| 314 | 313 | con2bid 354 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴 ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴})) | 
| 315 | 307, 314 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴) | 
| 316 | 149, 136,
195, 197, 272, 315 | coprmdvds2d 42003 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) · (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴) | 
| 317 | 143, 316 | eqbrtrd 5164 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → 𝑅 ∥ 𝐴) | 
| 318 | 317 | adantr 480 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∥ 𝐴) | 
| 319 | 67 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑅 ∥ 𝐴) | 
| 320 | 319 | ad5antr 734 | . . . . . . . . . 10
⊢
((((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝 ∥ 𝑅) ∧ ¬ 𝑝 ∥ 𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ 𝑅 ∥ 𝐴) | 
| 321 | 75, 320 | sylbir 235 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ 𝑅 ∥ 𝐴) | 
| 322 | 318, 321 | pm2.21dd 195 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ (𝑅 / 𝑝) ∥ 𝐴) | 
| 323 | 30, 129, 322 | elrabd 3693 | . . . . . . 7
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) | 
| 324 |  | lbinfle 12224 | . . . . . . 7
⊢ (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴} ⊆ ℝ ∧ ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}𝑥 ≤ 𝑦 ∧ (𝑅 / 𝑝) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / 𝑝)) | 
| 325 | 17, 28, 323, 324 | syl3anc 1372 | . . . . . 6
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) ≤ (𝑅 / 𝑝)) | 
| 326 | 5, 325 | eqbrtrd 5164 | . . . . 5
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ≤ (𝑅 / 𝑝)) | 
| 327 | 207 | adantr 480 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 < 𝑝) | 
| 328 |  | 1rp 13039 | . . . . . . . . . 10
⊢ 1 ∈
ℝ+ | 
| 329 | 328 | a1i 11 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ∈
ℝ+) | 
| 330 | 215 | adantr 480 | . . . . . . . . 9
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈
ℝ+) | 
| 331 | 329, 95, 330 | ltdiv2d 13101 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (1 < 𝑝 ↔ (𝑅 / 𝑝) < (𝑅 / 1))) | 
| 332 | 327, 331 | mpbid 232 | . . . . . . 7
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) < (𝑅 / 1)) | 
| 333 | 130 | adantr 480 | . . . . . . . 8
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℂ) | 
| 334 | 333 | div1d 12036 | . . . . . . 7
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 1) = 𝑅) | 
| 335 | 332, 334 | breqtrd 5168 | . . . . . 6
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) < 𝑅) | 
| 336 | 98, 101, 65 | redivcld 12096 | . . . . . . . . 9
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → (𝑅 / 𝑝) ∈ ℝ) | 
| 337 | 336 | adantr 480 | . . . . . . . 8
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → (𝑅 / 𝑝) ∈ ℝ) | 
| 338 | 337 | adantr 480 | . . . . . . 7
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ ℝ) | 
| 339 | 338, 94 | ltnled 11409 | . . . . . 6
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ((𝑅 / 𝑝) < 𝑅 ↔ ¬ 𝑅 ≤ (𝑅 / 𝑝))) | 
| 340 | 335, 339 | mpbid 232 | . . . . 5
⊢
(((((𝜑 ∧ 1 <
(𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ 𝑅 ≤ (𝑅 / 𝑝)) | 
| 341 | 326, 340 | pm2.65da 816 | . . . 4
⊢ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) | 
| 342 | 1, 2, 3, 4 | aks4d1p7 42085 | . . . . 5
⊢ (𝜑 → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) | 
| 343 | 342 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → ∃𝑝 ∈ ℙ (𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁)) | 
| 344 | 341, 343 | r19.29a 3161 | . . 3
⊢ ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) | 
| 345 | 344 | adantr 480 | . 2
⊢ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) | 
| 346 | 1, 2, 3, 4, 345 | aks4d1p5 42082 | 1
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) |