Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aks4d1p8 Structured version   Visualization version   GIF version

Theorem aks4d1p8 42068
Description: Show that 𝑁 and 𝑅 are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024.) (Proof sketch by Thierry Arnoux.)
Hypotheses
Ref Expression
aks4d1p8.1 (𝜑𝑁 ∈ (ℤ‘3))
aks4d1p8.2 𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1))
aks4d1p8.3 𝐵 = (⌈‘((2 logb 𝑁)↑5))
aks4d1p8.4 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )
Assertion
Ref Expression
aks4d1p8 (𝜑 → (𝑁 gcd 𝑅) = 1)
Distinct variable groups:   𝐴,𝑟   𝐵,𝑟   𝑘,𝑁   𝑁,𝑟   𝑅,𝑘   𝑅,𝑟   𝜑,𝑘
Allowed substitution hints:   𝜑(𝑟)   𝐴(𝑘)   𝐵(𝑘)

Proof of Theorem aks4d1p8
Dummy variables 𝑝 𝑦 𝑥 𝑜 𝑓 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef 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...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < )
54a1i 11 . . . . . 6 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ))
6 ssrab2 4089 . . . . . . . . . . . . 13 {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ (1...𝐵)
76a1i 11 . . . . . . . . . . . 12 (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ (1...𝐵))
8 elfznn 13589 . . . . . . . . . . . . . . . 16 (𝑜 ∈ (1...𝐵) → 𝑜 ∈ ℕ)
98adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑜 ∈ (1...𝐵)) → 𝑜 ∈ ℕ)
109nnred 12278 . . . . . . . . . . . . . 14 ((𝜑𝑜 ∈ (1...𝐵)) → 𝑜 ∈ ℝ)
1110ex 412 . . . . . . . . . . . . 13 (𝜑 → (𝑜 ∈ (1...𝐵) → 𝑜 ∈ ℝ))
1211ssrdv 4000 . . . . . . . . . . . 12 (𝜑 → (1...𝐵) ⊆ ℝ)
137, 12sstrd 4005 . . . . . . . . . . 11 (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
1413adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
1514adantr 480 . . . . . . . . 9 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
1615adantr 480 . . . . . . . 8 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
1716adantr 480 . . . . . . 7 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
18 fzfid 14010 . . . . . . . . . . . . 13 (𝜑 → (1...𝐵) ∈ Fin)
1918, 7ssfid 9298 . . . . . . . . . . . 12 (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin)
201, 2, 3aks4d1p3 42059 . . . . . . . . . . . . 13 (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟𝐴)
21 rabn0 4394 . . . . . . . . . . . . 13 ({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ≠ ∅ ↔ ∃𝑟 ∈ (1...𝐵) ¬ 𝑟𝐴)
2220, 21sylibr 234 . . . . . . . . . . . 12 (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ≠ ∅)
23 fiminre 12212 . . . . . . . . . . . 12 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ≠ ∅) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}𝑥𝑦)
2413, 19, 22, 23syl3anc 1370 . . . . . . . . . . 11 (𝜑 → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}𝑥𝑦)
2524adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}𝑥𝑦)
2625adantr 480 . . . . . . . . 9 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}𝑥𝑦)
2726adantr 480 . . . . . . . 8 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}𝑥𝑦)
2827adantr 480 . . . . . . 7 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}𝑥𝑦)
29 breq1 5150 . . . . . . . . 9 (𝑟 = (𝑅 / 𝑝) → (𝑟𝐴 ↔ (𝑅 / 𝑝) ∥ 𝐴))
3029notbid 318 . . . . . . . 8 (𝑟 = (𝑅 / 𝑝) → (¬ 𝑟𝐴 ↔ ¬ (𝑅 / 𝑝) ∥ 𝐴))
31 1zzd 12645 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ∈ ℤ)
323a1i 11 . . . . . . . . . . 11 (𝜑𝐵 = (⌈‘((2 logb 𝑁)↑5)))
33 2re 12337 . . . . . . . . . . . . . . 15 2 ∈ ℝ
3433a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 2 ∈ ℝ)
35 2pos 12366 . . . . . . . . . . . . . . 15 0 < 2
3635a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 < 2)
37 eluzelz 12885 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 𝑁 ∈ ℤ)
381, 37syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℤ)
3938zred 12719 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
40 0red 11261 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℝ)
41 3re 12343 . . . . . . . . . . . . . . . 16 3 ∈ ℝ
4241a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 3 ∈ ℝ)
43 3pos 12368 . . . . . . . . . . . . . . . 16 0 < 3
4443a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 < 3)
45 eluzle 12888 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ‘3) → 3 ≤ 𝑁)
461, 45syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 3 ≤ 𝑁)
4740, 42, 39, 44, 46ltletrd 11418 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
48 1red 11259 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
49 1lt2 12434 . . . . . . . . . . . . . . . . 17 1 < 2
5049a1i 11 . . . . . . . . . . . . . . . 16 (𝜑 → 1 < 2)
5148, 50ltned 11394 . . . . . . . . . . . . . . 15 (𝜑 → 1 ≠ 2)
5251necomd 2993 . . . . . . . . . . . . . 14 (𝜑 → 2 ≠ 1)
5334, 36, 39, 47, 52relogbcld 41954 . . . . . . . . . . . . 13 (𝜑 → (2 logb 𝑁) ∈ ℝ)
54 5nn0 12543 . . . . . . . . . . . . . 14 5 ∈ ℕ0
5554a1i 11 . . . . . . . . . . . . 13 (𝜑 → 5 ∈ ℕ0)
5653, 55reexpcld 14199 . . . . . . . . . . . 12 (𝜑 → ((2 logb 𝑁)↑5) ∈ ℝ)
5756ceilcld 13879 . . . . . . . . . . 11 (𝜑 → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ)
5832, 57eqeltrd 2838 . . . . . . . . . 10 (𝜑𝐵 ∈ ℤ)
5958ad4antr 732 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝐵 ∈ ℤ)
60 simplrl 777 . . . . . . . . . 10 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝𝑅)
61 prmnn 16707 . . . . . . . . . . . . . 14 (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
6261adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℕ)
6362ad2antrr 726 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℕ)
6463nnzd 12637 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℤ)
6562nnne0d 12313 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ≠ 0)
6665ad2antrr 726 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ≠ 0)
671, 2, 3, 4aks4d1p4 42060 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅𝐴))
6867simpld 494 . . . . . . . . . . . . . . . 16 (𝜑𝑅 ∈ (1...𝐵))
69 elfznn 13589 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (1...𝐵) → 𝑅 ∈ ℕ)
7068, 69syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ ℕ)
7170ad4antr 732 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) → 𝑅 ∈ ℕ)
7271adantr 480 . . . . . . . . . . . . 13 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℕ)
7372nnzd 12637 . . . . . . . . . . . 12 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ)
74 anass 468 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) ↔ (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)))
7574anbi1i 624 . . . . . . . . . . . . 13 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) ↔ ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴))
7675imbi1i 349 . . . . . . . . . . . 12 (((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ) ↔ (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ))
7773, 76mpbi 230 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℤ)
78 dvdsval2 16289 . . . . . . . . . . 11 ((𝑝 ∈ ℤ ∧ 𝑝 ≠ 0 ∧ 𝑅 ∈ ℤ) → (𝑝𝑅 ↔ (𝑅 / 𝑝) ∈ ℤ))
7964, 66, 77, 78syl3anc 1370 . . . . . . . . . 10 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑝𝑅 ↔ (𝑅 / 𝑝) ∈ ℤ))
8060, 79mpbid 232 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ ℤ)
8163nncnd 12279 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℂ)
8281mullidd 11276 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (1 · 𝑝) = 𝑝)
8375, 72sylbir 235 . . . . . . . . . . . . 13 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℕ)
8464, 83jca 511 . . . . . . . . . . . 12 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ))
85 dvdsle 16343 . . . . . . . . . . . . 13 ((𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ) → (𝑝𝑅𝑝𝑅))
8685imp 406 . . . . . . . . . . . 12 (((𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ) ∧ 𝑝𝑅) → 𝑝𝑅)
8784, 60, 86syl2anc 584 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝𝑅)
8882, 87eqbrtrd 5169 . . . . . . . . . 10 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (1 · 𝑝) ≤ 𝑅)
89 1red 11259 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ∈ ℝ)
9070nnred 12278 . . . . . . . . . . . . . . 15 (𝜑𝑅 ∈ ℝ)
9190adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑅 ∈ ℝ)
9291adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ∈ ℝ)
9392adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 ∈ ℝ)
9493adantr 480 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℝ)
9563nnrpd 13072 . . . . . . . . . . 11 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑝 ∈ ℝ+)
9689, 94, 95lemuldivd 13123 . . . . . . . . . 10 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ((1 · 𝑝) ≤ 𝑅 ↔ 1 ≤ (𝑅 / 𝑝)))
9788, 96mpbid 232 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ≤ (𝑅 / 𝑝))
9890ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ∈ ℝ)
9958ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℤ)
10099zred 12719 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝐵 ∈ ℝ)
10162nnred 12278 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
102100, 101remulcld 11288 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → (𝐵 · 𝑝) ∈ ℝ)
103 elfzle2 13564 . . . . . . . . . . . . . . . 16 (𝑅 ∈ (1...𝐵) → 𝑅𝐵)
10468, 103syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑅𝐵)
105104adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑅𝐵)
106105adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅𝐵)
10758zred 12719 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ ℝ)
108 9re 12362 . . . . . . . . . . . . . . . . . . 19 9 ∈ ℝ
109108a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 9 ∈ ℝ)
110 9pos 12376 . . . . . . . . . . . . . . . . . . 19 0 < 9
111110a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 < 9)
11232, 107eqeltrrd 2839 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (⌈‘((2 logb 𝑁)↑5)) ∈ ℝ)
11339, 463lexlogpow5ineq4 42037 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 9 < ((2 logb 𝑁)↑5))
11456ceilged 13882 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 logb 𝑁)↑5) ≤ (⌈‘((2 logb 𝑁)↑5)))
115109, 56, 112, 113, 114ltletrd 11418 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 9 < (⌈‘((2 logb 𝑁)↑5)))
116115, 32breqtrrd 5175 . . . . . . . . . . . . . . . . . 18 (𝜑 → 9 < 𝐵)
11740, 109, 107, 111, 116lttrd 11419 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 𝐵)
11840, 107, 117ltled 11406 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ 𝐵)
119118adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 0 ≤ 𝐵)
120119adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 0 ≤ 𝐵)
12162nnge1d 12311 . . . . . . . . . . . . . 14 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 1 ≤ 𝑝)
122100, 101, 120, 121lemulge11d 12202 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝐵 ≤ (𝐵 · 𝑝))
12398, 100, 102, 106, 122letrd 11415 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ≤ (𝐵 · 𝑝))
12462nnrpd 13072 . . . . . . . . . . . . 13 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ+)
12598, 100, 124ledivmul2d 13128 . . . . . . . . . . . 12 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → ((𝑅 / 𝑝) ≤ 𝐵𝑅 ≤ (𝐵 · 𝑝)))
126123, 125mpbird 257 . . . . . . . . . . 11 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → (𝑅 / 𝑝) ≤ 𝐵)
127126adantr 480 . . . . . . . . . 10 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / 𝑝) ≤ 𝐵)
128127adantr 480 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ≤ 𝐵)
12931, 59, 80, 97, 128elfzd 13551 . . . . . . . 8 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ (1...𝐵))
13093recnd 11286 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 ∈ ℂ)
13162adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℕ)
132131nnzd 12637 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℤ)
133 simplr 769 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℙ)
13471anasss 466 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 ∈ ℕ)
135133, 134pccld 16883 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt 𝑅) ∈ ℕ0)
136132, 135zexpcld 14124 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℤ)
137136zcnd 12720 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℂ)
138131nncnd 12279 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℂ)
13965adantr 480 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝 ≠ 0)
140135nn0zd 12636 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt 𝑅) ∈ ℤ)
141138, 139, 140expne0d 14188 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ≠ 0)
142130, 137, 141divcan1d 12041 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) · (𝑝↑(𝑝 pCnt 𝑅))) = 𝑅)
143142eqcomd 2740 . . . . . . . . . . 11 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 = ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) · (𝑝↑(𝑝 pCnt 𝑅))))
144 pcdvds 16897 . . . . . . . . . . . . . 14 ((𝑝 ∈ ℙ ∧ 𝑅 ∈ ℕ) → (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅)
145133, 134, 144syl2anc 584 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅)
146134nnzd 12637 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 ∈ ℤ)
147 dvdsval2 16289 . . . . . . . . . . . . . 14 (((𝑝↑(𝑝 pCnt 𝑅)) ∈ ℤ ∧ (𝑝↑(𝑝 pCnt 𝑅)) ≠ 0 ∧ 𝑅 ∈ ℤ) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℤ))
148136, 141, 146, 147syl3anc 1370 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℤ))
149145, 148mpbid 232 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℤ)
15038, 47jca 511 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ ℤ ∧ 0 < 𝑁))
151 elnnz 12620 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁))
152151a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 < 𝑁)))
153150, 152mpbird 257 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℕ)
154153nnzd 12637 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
15534, 36, 107, 117, 52relogbcld 41954 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (2 logb 𝐵) ∈ ℝ)
156155flcld 13834 . . . . . . . . . . . . . . . . . 18 (𝜑 → (⌊‘(2 logb 𝐵)) ∈ ℤ)
15734recnd 11286 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 2 ∈ ℂ)
15840, 36gtned 11393 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 2 ≠ 0)
159 logb1 26826 . . . . . . . . . . . . . . . . . . . . . 22 ((2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) = 0)
160157, 158, 52, 159syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 logb 1) = 0)
161160eqcomd 2740 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 = (2 logb 1))
162 2z 12646 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℤ
163162a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ∈ ℤ)
16434leidd 11826 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 2 ≤ 2)
165 0lt1 11782 . . . . . . . . . . . . . . . . . . . . . 22 0 < 1
166165a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < 1)
167 1lt9 12469 . . . . . . . . . . . . . . . . . . . . . . . 24 1 < 9
168167a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 < 9)
16948, 109, 107, 168, 116lttrd 11419 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 < 𝐵)
17048, 107, 169ltled 11406 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝐵)
171163, 164, 48, 166, 107, 117, 170logblebd 41957 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2 logb 1) ≤ (2 logb 𝐵))
172161, 171eqbrtrd 5169 . . . . . . . . . . . . . . . . . . 19 (𝜑 → 0 ≤ (2 logb 𝐵))
173 0zd 12622 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ∈ ℤ)
174 flge 13841 . . . . . . . . . . . . . . . . . . . 20 (((2 logb 𝐵) ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤ (⌊‘(2 logb 𝐵))))
175155, 173, 174syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (0 ≤ (2 logb 𝐵) ↔ 0 ≤ (⌊‘(2 logb 𝐵))))
176172, 175mpbid 232 . . . . . . . . . . . . . . . . . 18 (𝜑 → 0 ≤ (⌊‘(2 logb 𝐵)))
177156, 176jca 511 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵))))
178 elnn0z 12623 . . . . . . . . . . . . . . . . . 18 ((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔ ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵))))
179178a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → ((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔ ((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))))
180177, 179mpbird 257 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘(2 logb 𝐵)) ∈ ℕ0)
181154, 180zexpcld 14124 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁↑(⌊‘(2 logb 𝐵))) ∈ ℤ)
182 fzfid 14010 . . . . . . . . . . . . . . . 16 (𝜑 → (1...(⌊‘((2 logb 𝑁)↑2))) ∈ Fin)
183154adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑁 ∈ ℤ)
184 elfznn 13589 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2))) → 𝑘 ∈ ℕ)
185184adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ ℕ)
186185nnnn0d 12584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0)
187183, 186zexpcld 14124 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → (𝑁𝑘) ∈ ℤ)
188 1zzd 12645 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → 1 ∈ ℤ)
189187, 188zsubcld 12724 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))) → ((𝑁𝑘) − 1) ∈ ℤ)
190182, 189fprodzcl 15986 . . . . . . . . . . . . . . 15 (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1) ∈ ℤ)
191181, 190zmulcld 12725 . . . . . . . . . . . . . 14 (𝜑 → ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) ∈ ℤ)
1922a1i 11 . . . . . . . . . . . . . . 15 (𝜑𝐴 = ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)))
193192eleq1d 2823 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 ∈ ℤ ↔ ((𝑁↑(⌊‘(2 logb 𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2 logb 𝑁)↑2)))((𝑁𝑘) − 1)) ∈ ℤ))
194191, 193mpbird 257 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ ℤ)
195194ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝐴 ∈ ℤ)
196 simprl 771 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝𝑅)
197134, 133, 196aks4d1p8d3 42067 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) gcd (𝑝↑(𝑝 pCnt 𝑅))) = 1)
198138exp0d 14176 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑0) = 1)
199 pcelnn 16903 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ∈ ℙ ∧ 𝑅 ∈ ℕ) → ((𝑝 pCnt 𝑅) ∈ ℕ ↔ 𝑝𝑅))
200133, 134, 199syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑝 pCnt 𝑅) ∈ ℕ ↔ 𝑝𝑅))
201196, 200mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝 pCnt 𝑅) ∈ ℕ)
202201nngt0d 12312 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 0 < (𝑝 pCnt 𝑅))
203101adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℝ)
204173ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 0 ∈ ℤ)
205 prmgt1 16730 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 ∈ ℙ → 1 < 𝑝)
206205adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
207206adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 < 𝑝)
208203, 204, 140, 207ltexp2d 14286 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (0 < (𝑝 pCnt 𝑅) ↔ (𝑝↑0) < (𝑝↑(𝑝 pCnt 𝑅))))
209202, 208mpbid 232 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑0) < (𝑝↑(𝑝 pCnt 𝑅)))
210198, 209eqbrtrrd 5171 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 < (𝑝↑(𝑝 pCnt 𝑅)))
211136zred 12719 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℝ)
21270nnrpd 13072 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑅 ∈ ℝ+)
213212adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑅 ∈ ℝ+)
214213adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑅 ∈ ℝ+)
215214adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 ∈ ℝ+)
216211, 215ltmulgt11d 13109 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (1 < (𝑝↑(𝑝 pCnt 𝑅)) ↔ 𝑅 < (𝑅 · (𝑝↑(𝑝 pCnt 𝑅)))))
217210, 216mpbid 232 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 < (𝑅 · (𝑝↑(𝑝 pCnt 𝑅))))
218124adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑝 ∈ ℝ+)
219218, 140rpexpcld 14282 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℝ+)
22093, 93, 219ltdivmul2d 13126 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) < 𝑅𝑅 < (𝑅 · (𝑝↑(𝑝 pCnt 𝑅)))))
221217, 220mpbird 257 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) < 𝑅)
22293, 211, 141redivcld 12092 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ ℝ)
223222, 93ltnled 11405 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) < 𝑅 ↔ ¬ 𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))))
224221, 223mpbid 232 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ¬ 𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))
2254a1i 11 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ))
226225breq1d 5157 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ↔ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))))
227226notbid 318 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (¬ 𝑅 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ↔ ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))))
228224, 227mpbid 232 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))
229 elfznn 13589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ (1...𝐵) → 𝑓 ∈ ℕ)
230229adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓 ∈ (1...𝐵)) → 𝑓 ∈ ℕ)
231230nnred 12278 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓 ∈ (1...𝐵)) → 𝑓 ∈ ℝ)
232231ex 412 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑓 ∈ (1...𝐵) → 𝑓 ∈ ℝ))
233232ssrdv 4000 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...𝐵) ⊆ ℝ)
2347, 233sstrd 4005 . . . . . . . . . . . . . . . . . 18 (𝜑 → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
235234adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
236235adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
237236adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ)
23819adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin)
239238adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin)
240239adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin)
241 infrefilb 12251 . . . . . . . . . . . . . . . . . 18 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin ∧ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))
2422413expa 1117 . . . . . . . . . . . . . . . . 17 ((({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin) ∧ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))
243242ex 412 . . . . . . . . . . . . . . . 16 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))))
244243con3d 152 . . . . . . . . . . . . . . 15 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}))
245237, 240, 244syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}))
246228, 245mpd 15 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴})
247 1zzd 12645 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 ∈ ℤ)
24899adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝐵 ∈ ℤ)
249137mullidd 11276 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (1 · (𝑝↑(𝑝 pCnt 𝑅))) = (𝑝↑(𝑝 pCnt 𝑅)))
250 dvdsle 16343 . . . . . . . . . . . . . . . . . . 19 (((𝑝↑(𝑝 pCnt 𝑅)) ∈ ℤ ∧ 𝑅 ∈ ℕ) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝑅))
251136, 134, 250syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝑅 → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝑅))
252145, 251mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝑅)
253249, 252eqbrtrd 5169 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (1 · (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅)
25448adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 1 ∈ ℝ)
255254ad2antrr 726 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 ∈ ℝ)
256255, 93, 219lemuldivd 13123 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((1 · (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅 ↔ 1 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅)))))
257253, 256mpbid 232 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 ≤ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))))
258100adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝐵 ∈ ℝ)
259121adantr 480 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 ≤ 𝑝)
260203, 135, 259expge1d 14201 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 ≤ (𝑝↑(𝑝 pCnt 𝑅)))
261 nnledivrp 13144 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ ℕ ∧ (𝑝↑(𝑝 pCnt 𝑅)) ∈ ℝ+) → (1 ≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅))
262134, 219, 261syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (1 ≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅))
263260, 262mpbid 232 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝑅)
264106adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅𝐵)
265222, 93, 258, 263, 264letrd 11415 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ≤ 𝐵)
266247, 248, 149, 257, 265elfzd 13551 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ (1...𝐵))
267 breq1 5150 . . . . . . . . . . . . . . . . 17 (𝑟 = (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → (𝑟𝐴 ↔ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴))
268267notbid 318 . . . . . . . . . . . . . . . 16 (𝑟 = (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) → (¬ 𝑟𝐴 ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴))
269268elrab3 3695 . . . . . . . . . . . . . . 15 ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ (1...𝐵) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴))
270269con2bid 354 . . . . . . . . . . . . . 14 ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ (1...𝐵) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴 ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}))
271266, 270syl 17 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴 ↔ ¬ (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}))
272246, 271mpbird 257 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴)
273134ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → 𝑅 ∈ ℕ)
274153adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 𝑁 ∈ ℕ)
275274adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ)
276275adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) → 𝑁 ∈ ℕ)
277276adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) → 𝑁 ∈ ℕ)
27874, 277sylbir 235 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑁 ∈ ℕ)
279278ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → 𝑁 ∈ ℕ)
280133ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → 𝑝 ∈ ℙ)
281 simplr 769 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → 𝑞 ∈ ℙ)
282196ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → 𝑝𝑅)
283 simprr 773 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → 𝑞𝑅)
284 simplrr 778 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) → ¬ 𝑝𝑁)
285284adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → ¬ 𝑝𝑁)
286 simprl 771 . . . . . . . . . . . . . . . . . 18 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → 𝑞𝑁)
287273, 279, 280, 281, 282, 283, 285, 286aks4d1p8d2 42066 . . . . . . . . . . . . . . . . 17 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ 𝑞 ∈ ℙ) ∧ (𝑞𝑁𝑞𝑅)) → (𝑝↑(𝑝 pCnt 𝑅)) < 𝑅)
288 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → 1 < (𝑁 gcd 𝑅))
289288ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 < (𝑁 gcd 𝑅))
290255, 289ltned 11394 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 1 ≠ (𝑁 gcd 𝑅))
291290necomd 2993 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑁 gcd 𝑅) ≠ 1)
292278, 134prmdvdsncoprmbd 16760 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (∃𝑞 ∈ ℙ (𝑞𝑁𝑞𝑅) ↔ (𝑁 gcd 𝑅) ≠ 1))
293292bicomd 223 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑁 gcd 𝑅) ≠ 1 ↔ ∃𝑞 ∈ ℙ (𝑞𝑁𝑞𝑅)))
294293biimpd 229 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑁 gcd 𝑅) ≠ 1 → ∃𝑞 ∈ ℙ (𝑞𝑁𝑞𝑅)))
295291, 294mpd 15 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ∃𝑞 ∈ ℙ (𝑞𝑁𝑞𝑅))
296287, 295r19.29a 3159 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) < 𝑅)
297211, 93ltnled 11405 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) < 𝑅 ↔ ¬ 𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅))))
298296, 297mpbid 232 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ¬ 𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅)))
299225breq1d 5157 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅))))
300299notbid 318 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (¬ 𝑅 ≤ (𝑝↑(𝑝 pCnt 𝑅)) ↔ ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅))))
301298, 300mpbid 232 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)))
302 infrefilb 12251 . . . . . . . . . . . . . . . . . 18 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin ∧ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)))
3033023expa 1117 . . . . . . . . . . . . . . . . 17 ((({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin) ∧ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)))
304303ex 412 . . . . . . . . . . . . . . . 16 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin) → ((𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅))))
305304con3d 152 . . . . . . . . . . . . . . 15 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ∈ Fin) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)) → ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}))
306237, 240, 305syl2anc 584 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (¬ inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑝↑(𝑝 pCnt 𝑅)) → ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}))
307301, 306mpd 15 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴})
308211, 93, 258, 252, 264letrd 11415 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ≤ 𝐵)
309247, 248, 136, 260, 308elfzd 13551 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∈ (1...𝐵))
310 breq1 5150 . . . . . . . . . . . . . . . . 17 (𝑟 = (𝑝↑(𝑝 pCnt 𝑅)) → (𝑟𝐴 ↔ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴))
311310notbid 318 . . . . . . . . . . . . . . . 16 (𝑟 = (𝑝↑(𝑝 pCnt 𝑅)) → (¬ 𝑟𝐴 ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴))
312311elrab3 3695 . . . . . . . . . . . . . . 15 ((𝑝↑(𝑝 pCnt 𝑅)) ∈ (1...𝐵) → ((𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴))
313309, 312syl 17 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴))
314313con2bid 354 . . . . . . . . . . . . 13 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴 ↔ ¬ (𝑝↑(𝑝 pCnt 𝑅)) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}))
315307, 314mpbird 257 . . . . . . . . . . . 12 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑝↑(𝑝 pCnt 𝑅)) ∥ 𝐴)
316149, 136, 195, 197, 272, 315coprmdvds2d 41982 . . . . . . . . . . 11 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ((𝑅 / (𝑝↑(𝑝 pCnt 𝑅))) · (𝑝↑(𝑝 pCnt 𝑅))) ∥ 𝐴)
317143, 316eqbrtrd 5169 . . . . . . . . . 10 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → 𝑅𝐴)
318317adantr 480 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅𝐴)
31967simprd 495 . . . . . . . . . . 11 (𝜑 → ¬ 𝑅𝐴)
320319ad5antr 734 . . . . . . . . . 10 ((((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ 𝑝𝑅) ∧ ¬ 𝑝𝑁) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ 𝑅𝐴)
32175, 320sylbir 235 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ 𝑅𝐴)
322318, 321pm2.21dd 195 . . . . . . . 8 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ (𝑅 / 𝑝) ∥ 𝐴)
32330, 129, 322elrabd 3696 . . . . . . 7 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴})
324 lbinfle 12220 . . . . . . 7 (({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴} ⊆ ℝ ∧ ∃𝑥 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}∀𝑦 ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}𝑥𝑦 ∧ (𝑅 / 𝑝) ∈ {𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / 𝑝))
32517, 28, 323, 324syl3anc 1370 . . . . . 6 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟𝐴}, ℝ, < ) ≤ (𝑅 / 𝑝))
3265, 325eqbrtrd 5169 . . . . 5 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ≤ (𝑅 / 𝑝))
327207adantr 480 . . . . . . . 8 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 < 𝑝)
328 1rp 13035 . . . . . . . . . 10 1 ∈ ℝ+
329328a1i 11 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 1 ∈ ℝ+)
330215adantr 480 . . . . . . . . 9 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℝ+)
331329, 95, 330ltdiv2d 13097 . . . . . . . 8 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (1 < 𝑝 ↔ (𝑅 / 𝑝) < (𝑅 / 1)))
332327, 331mpbid 232 . . . . . . 7 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) < (𝑅 / 1))
333130adantr 480 . . . . . . . 8 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → 𝑅 ∈ ℂ)
334333div1d 12032 . . . . . . 7 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 1) = 𝑅)
335332, 334breqtrd 5173 . . . . . 6 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) < 𝑅)
33698, 101, 65redivcld 12092 . . . . . . . . 9 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) → (𝑅 / 𝑝) ∈ ℝ)
337336adantr 480 . . . . . . . 8 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → (𝑅 / 𝑝) ∈ ℝ)
338337adantr 480 . . . . . . 7 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → (𝑅 / 𝑝) ∈ ℝ)
339338, 94ltnled 11405 . . . . . 6 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ((𝑅 / 𝑝) < 𝑅 ↔ ¬ 𝑅 ≤ (𝑅 / 𝑝)))
340335, 339mpbid 232 . . . . 5 (((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ 𝑅 ≤ (𝑅 / 𝑝))
341326, 340pm2.65da 817 . . . 4 ((((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ 𝑝 ∈ ℙ) ∧ (𝑝𝑅 ∧ ¬ 𝑝𝑁)) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴)
3421, 2, 3, 4aks4d1p7 42064 . . . . 5 (𝜑 → ∃𝑝 ∈ ℙ (𝑝𝑅 ∧ ¬ 𝑝𝑁))
343342adantr 480 . . . 4 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → ∃𝑝 ∈ ℙ (𝑝𝑅 ∧ ¬ 𝑝𝑁))
344341, 343r19.29a 3159 . . 3 ((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴)
345344adantr 480 . 2 (((𝜑 ∧ 1 < (𝑁 gcd 𝑅)) ∧ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴) → ¬ (𝑅 / (𝑁 gcd 𝑅)) ∥ 𝐴)
3461, 2, 3, 4, 345aks4d1p5 42061 1 (𝜑 → (𝑁 gcd 𝑅) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  wss 3962  c0 4338   class class class wbr 5147  cfv 6562  (class class class)co 7430  Fincfn 8983  infcinf 9478  cc 11150  cr 11151  0cc0 11152  1c1 11153   · cmul 11157   < clt 11292  cle 11293  cmin 11489   / cdiv 11917  cn 12263  2c2 12318  3c3 12319  5c5 12321  9c9 12325  0cn0 12523  cz 12610  cuz 12875  +crp 13031  ...cfz 13543  cfl 13826  cceil 13827  cexp 14098  cprod 15935  cdvds 16286   gcd cgcd 16527  cprime 16704   pCnt cpc 16869   logb clogb 26821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cc 10472  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-symdif 4258  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-ofr 7697  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-omul 8509  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-dju 9938  df-card 9976  df-acn 9979  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-ceil 13829  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-prod 15936  df-ef 16099  df-e 16100  df-sin 16101  df-cos 16102  df-pi 16104  df-dvds 16287  df-gcd 16528  df-lcm 16623  df-lcmf 16624  df-prm 16705  df-pc 16870  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-cmp 23410  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-ovol 25512  df-vol 25513  df-mbf 25667  df-itg1 25668  df-itg2 25669  df-ibl 25670  df-itg 25671  df-0p 25718  df-limc 25915  df-dv 25916  df-log 26612  df-cxp 26613  df-logb 26822
This theorem is referenced by:  aks4d1p9  42069  aks4d1  42070
  Copyright terms: Public domain W3C validator