Metamath Proof Explorer

Theorem aks4d1p8

Description: Show that N and R are coprime for AKS existence theorem, with eliminated hypothesis. (Contributed by metakunt, 10-Nov-2024) (Proof sketch by Thierry Arnoux.)

Ref Expression
Hypotheses aks4d1p8.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
aks4d1p8.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
aks4d1p8.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
aks4d1p8.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
Assertion aks4d1p8 ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )

Proof

Step Hyp Ref Expression
1 aks4d1p8.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p8.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p8.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p8.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
5 4 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) )
6 ssrab2 ⊢ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 )
7 6 a1i ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 ) )
8 elfznn ⊢ ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℕ )
9 8 adantl ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℕ )
10 9 nnred ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℝ )
11 10 ex ⊢ ( 𝜑 → ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℝ ) )
12 11 ssrdv ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ⊆ ℝ )
13 7 12 sstrd ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
14 13 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
15 14 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
16 15 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
17 16 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
18 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ∈ Fin )
19 18 7 ssfid ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
20 1 2 3 aks4d1p3 ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
21 rabn0 ⊢ ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ↔ ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
22 20 21 sylibr ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ )
23 fiminre ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
24 13 19 22 23 syl3anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
25 24 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
27 26 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
28 27 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
29 breq1 ⊢ ( 𝑟 = ( 𝑅 / 𝑝 ) → ( 𝑟 ∥ 𝐴 ↔ ( 𝑅 / 𝑝 ) ∥ 𝐴 ) )
30 29 notbid ⊢ ( 𝑟 = ( 𝑅 / 𝑝 ) → ( ¬ 𝑟 ∥ 𝐴 ↔ ¬ ( 𝑅 / 𝑝 ) ∥ 𝐴 ) )
31 1zzd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 1 ∈ ℤ )
32 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
33 2re ⊢ 2 ∈ ℝ
34 33 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
35 2pos ⊢ 0 < 2
36 35 a1i ⊢ ( 𝜑 → 0 < 2 )
37 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
38 1 37 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
39 38 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
40 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
41 3re ⊢ 3 ∈ ℝ
42 41 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
43 3pos ⊢ 0 < 3
44 43 a1i ⊢ ( 𝜑 → 0 < 3 )
45 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
46 1 45 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
47 40 42 39 44 46 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
48 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
49 1lt2 ⊢ 1 < 2
50 49 a1i ⊢ ( 𝜑 → 1 < 2 )
51 48 50 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
52 51 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
53 34 36 39 47 52 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
54 5nn0 ⊢ 5 ∈ ℕ0
55 54 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
56 53 55 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
57 56 ceilcld ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
58 32 57 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
59 58 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝐵 ∈ ℤ )
60 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑝 ∥ 𝑅 )
61 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
62 61 adantl ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℕ )
63 62 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑝 ∈ ℕ )
64 63 nnzd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑝 ∈ ℤ )
65 62 nnne0d ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ≠ 0 )
66 65 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑝 ≠ 0 )
67 1 2 3 4 aks4d1p4 ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
68 67 simpld ⊢ ( 𝜑 → 𝑅 ∈ ( 1 ... 𝐵 ) )
69 elfznn ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ∈ ℕ )
70 68 69 syl ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
71 70 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) → 𝑅 ∈ ℕ )
72 71 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℕ )
73 72 nnzd ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℤ )
74 anass ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) )
75 74 anbi1i ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) ↔ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) )
76 75 imbi1i ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℤ ) ↔ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℤ ) )
77 73 76 mpbi ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℤ )
78 dvdsval2 ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑝 ≠ 0 ∧ 𝑅 ∈ ℤ ) → ( 𝑝 ∥ 𝑅 ↔ ( 𝑅 / 𝑝 ) ∈ ℤ ) )
79 64 66 77 78 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑝 ∥ 𝑅 ↔ ( 𝑅 / 𝑝 ) ∈ ℤ ) )
80 60 79 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 𝑝 ) ∈ ℤ )
81 63 nncnd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑝 ∈ ℂ )
82 81 mullidd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 1 · 𝑝 ) = 𝑝 )
83 75 72 sylbir ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℕ )
84 64 83 jca ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ ) )
85 dvdsle ⊢ ( ( 𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ ) → ( 𝑝 ∥ 𝑅 → 𝑝 ≤ 𝑅 ) )
86 85 imp ⊢ ( ( ( 𝑝 ∈ ℤ ∧ 𝑅 ∈ ℕ ) ∧ 𝑝 ∥ 𝑅 ) → 𝑝 ≤ 𝑅 )
87 84 60 86 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑝 ≤ 𝑅 )
88 82 87 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 1 · 𝑝 ) ≤ 𝑅 )
89 1red ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 1 ∈ ℝ )
90 70 nnred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
91 90 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ∈ ℝ )
92 91 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑅 ∈ ℝ )
93 92 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 ∈ ℝ )
94 93 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℝ )
95 63 nnrpd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑝 ∈ ℝ+ )
96 89 94 95 lemuldivd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( ( 1 · 𝑝 ) ≤ 𝑅 ↔ 1 ≤ ( 𝑅 / 𝑝 ) ) )
97 88 96 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 1 ≤ ( 𝑅 / 𝑝 ) )
98 90 ad2antrr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑅 ∈ ℝ )
99 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℤ )
100 99 zred ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℝ )
101 62 nnred ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℝ )
102 100 101 remulcld ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝐵 · 𝑝 ) ∈ ℝ )
103 elfzle2 ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ≤ 𝐵 )
104 68 103 syl ⊢ ( 𝜑 → 𝑅 ≤ 𝐵 )
105 104 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ≤ 𝐵 )
106 105 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑅 ≤ 𝐵 )
107 58 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
108 9re ⊢ 9 ∈ ℝ
109 108 a1i ⊢ ( 𝜑 → 9 ∈ ℝ )
110 9pos ⊢ 0 < 9
111 110 a1i ⊢ ( 𝜑 → 0 < 9 )
112 32 107 eqeltrrd ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
113 39 46 3lexlogpow5ineq4 ⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
114 56 ceilged ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
115 109 56 112 113 114 ltletrd ⊢ ( 𝜑 → 9 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
116 115 32 breqtrrd ⊢ ( 𝜑 → 9 < 𝐵 )
117 40 109 107 111 116 lttrd ⊢ ( 𝜑 → 0 < 𝐵 )
118 40 107 117 ltled ⊢ ( 𝜑 → 0 ≤ 𝐵 )
119 118 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 0 ≤ 𝐵 )
120 119 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 0 ≤ 𝐵 )
121 62 nnge1d ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 1 ≤ 𝑝 )
122 100 101 120 121 lemulge11d ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ≤ ( 𝐵 · 𝑝 ) )
123 98 100 102 106 122 letrd ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑅 ≤ ( 𝐵 · 𝑝 ) )
124 62 nnrpd ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℝ+ )
125 98 100 124 ledivmul2d ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑅 / 𝑝 ) ≤ 𝐵 ↔ 𝑅 ≤ ( 𝐵 · 𝑝 ) ) )
126 123 125 mpbird ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑅 / 𝑝 ) ≤ 𝐵 )
127 126 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / 𝑝 ) ≤ 𝐵 )
128 127 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 𝑝 ) ≤ 𝐵 )
129 31 59 80 97 128 elfzd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 𝑝 ) ∈ ( 1 ... 𝐵 ) )
130 93 recnd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 ∈ ℂ )
131 62 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ∈ ℕ )
132 131 nnzd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ∈ ℤ )
133 simplr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ∈ ℙ )
134 71 anasss ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 ∈ ℕ )
135 133 134 pccld ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 pCnt 𝑅 ) ∈ ℕ0 )
136 132 135 zexpcld ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ℤ )
137 136 zcnd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ℂ )
138 131 nncnd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ∈ ℂ )
139 65 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ≠ 0 )
140 135 nn0zd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 pCnt 𝑅 ) ∈ ℤ )
141 138 139 140 expne0d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ≠ 0 )
142 130 137 141 divcan1d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) = 𝑅 )
143 142 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 = ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
144 pcdvds ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑅 ∈ ℕ ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝑅 )
145 133 134 144 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝑅 )
146 134 nnzd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 ∈ ℤ )
147 dvdsval2 ⊢ ( ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ℤ ∧ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ≠ 0 ∧ 𝑅 ∈ ℤ ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝑅 ↔ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ ℤ ) )
148 136 141 146 147 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝑅 ↔ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ ℤ ) )
149 145 148 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ ℤ )
150 38 47 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
151 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
152 151 a1i ⊢ ( 𝜑 → ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) ) )
153 150 152 mpbird ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
154 153 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
155 34 36 107 117 52 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
156 155 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
157 34 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
158 40 36 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
159 logb1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 )
160 157 158 52 159 syl3anc ⊢ ( 𝜑 → ( 2 logb 1 ) = 0 )
161 160 eqcomd ⊢ ( 𝜑 → 0 = ( 2 logb 1 ) )
162 2z ⊢ 2 ∈ ℤ
163 162 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
164 34 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
165 0lt1 ⊢ 0 < 1
166 165 a1i ⊢ ( 𝜑 → 0 < 1 )
167 1lt9 ⊢ 1 < 9
168 167 a1i ⊢ ( 𝜑 → 1 < 9 )
169 48 109 107 168 116 lttrd ⊢ ( 𝜑 → 1 < 𝐵 )
170 48 107 169 ltled ⊢ ( 𝜑 → 1 ≤ 𝐵 )
171 163 164 48 166 107 117 170 logblebd ⊢ ( 𝜑 → ( 2 logb 1 ) ≤ ( 2 logb 𝐵 ) )
172 161 171 eqbrtrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝐵 ) )
173 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
174 flge ⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
175 155 173 174 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
176 172 175 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
177 156 176 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
178 elnn0z ⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
179 178 a1i ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
180 177 179 mpbird ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
181 154 180 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℤ )
182 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
183 154 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℤ )
184 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ )
185 184 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ )
186 185 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
187 183 186 zexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
188 1zzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℤ )
189 187 188 zsubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
190 182 189 fprodzcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
191 181 190 zmulcld ⊢ ( 𝜑 → ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℤ )
192 2 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
193 192 eleq1d ⊢ ( 𝜑 → ( 𝐴 ∈ ℤ ↔ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ∈ ℤ ) )
194 191 193 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
195 194 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝐴 ∈ ℤ )
196 simprl ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ∥ 𝑅 )
197 134 133 196 aks4d1p8d3 ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) gcd ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) = 1 )
198 138 exp0d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ 0 ) = 1 )
199 pcelnn ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑅 ∈ ℕ ) → ( ( 𝑝 pCnt 𝑅 ) ∈ ℕ ↔ 𝑝 ∥ 𝑅 ) )
200 133 134 199 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑝 pCnt 𝑅 ) ∈ ℕ ↔ 𝑝 ∥ 𝑅 ) )
201 196 200 mpbird ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 pCnt 𝑅 ) ∈ ℕ )
202 201 nngt0d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 0 < ( 𝑝 pCnt 𝑅 ) )
203 101 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ∈ ℝ )
204 173 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 0 ∈ ℤ )
205 prmgt1 ⊢ ( 𝑝 ∈ ℙ → 1 < 𝑝 )
206 205 adantl ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 1 < 𝑝 )
207 206 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 < 𝑝 )
208 203 204 140 207 ltexp2d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 0 < ( 𝑝 pCnt 𝑅 ) ↔ ( 𝑝 ↑ 0 ) < ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
209 202 208 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ 0 ) < ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
210 198 209 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 < ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
211 136 zred ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ℝ )
212 70 nnrpd ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
213 212 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ∈ ℝ+ )
214 213 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑅 ∈ ℝ+ )
215 214 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 ∈ ℝ+ )
216 211 215 ltmulgt11d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 1 < ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ↔ 𝑅 < ( 𝑅 · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ) )
217 210 216 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 < ( 𝑅 · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
218 124 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑝 ∈ ℝ+ )
219 218 140 rpexpcld ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ℝ+ )
220 93 93 219 ltdivmul2d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) < 𝑅 ↔ 𝑅 < ( 𝑅 · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ) )
221 217 220 mpbird ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) < 𝑅 )
222 93 211 141 redivcld ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ ℝ )
223 222 93 ltnled ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ) )
224 221 223 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ¬ 𝑅 ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
225 4 a1i ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) )
226 225 breq1d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ↔ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ) )
227 226 notbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ¬ 𝑅 ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ↔ ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ) )
228 224 227 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
229 elfznn ⊢ ( 𝑓 ∈ ( 1 ... 𝐵 ) → 𝑓 ∈ ℕ )
230 229 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 1 ... 𝐵 ) ) → 𝑓 ∈ ℕ )
231 230 nnred ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 1 ... 𝐵 ) ) → 𝑓 ∈ ℝ )
232 231 ex ⊢ ( 𝜑 → ( 𝑓 ∈ ( 1 ... 𝐵 ) → 𝑓 ∈ ℝ ) )
233 232 ssrdv ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ⊆ ℝ )
234 7 233 sstrd ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
235 234 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
236 235 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
237 236 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
238 19 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
239 238 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
240 239 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
241 infrefilb ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
242 241 3expa ⊢ ( ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ) ∧ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
243 242 ex ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ) )
244 243 con3d ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ) → ( ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) → ¬ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) )
245 237 240 244 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) → ¬ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) )
246 228 245 mpd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ¬ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
247 1zzd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 ∈ ℤ )
248 99 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝐵 ∈ ℤ )
249 137 mullidd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 1 · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) = ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
250 dvdsle ⊢ ( ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ℤ ∧ 𝑅 ∈ ℕ ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝑅 → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ≤ 𝑅 ) )
251 136 134 250 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝑅 → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ≤ 𝑅 ) )
252 145 251 mpd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ≤ 𝑅 )
253 249 252 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 1 · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ≤ 𝑅 )
254 48 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 1 ∈ ℝ )
255 254 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 ∈ ℝ )
256 255 93 219 lemuldivd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 1 · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ≤ 𝑅 ↔ 1 ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ) )
257 253 256 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 ≤ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
258 100 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝐵 ∈ ℝ )
259 121 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 ≤ 𝑝 )
260 203 135 259 expge1d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
261 nnledivrp ⊢ ( ( 𝑅 ∈ ℕ ∧ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ℝ+ ) → ( 1 ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ↔ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ≤ 𝑅 ) )
262 134 219 261 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 1 ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ↔ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ≤ 𝑅 ) )
263 260 262 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ≤ 𝑅 )
264 106 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 ≤ 𝐵 )
265 222 93 258 263 264 letrd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ≤ 𝐵 )
266 247 248 149 257 265 elfzd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ ( 1 ... 𝐵 ) )
267 breq1 ⊢ ( 𝑟 = ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) → ( 𝑟 ∥ 𝐴 ↔ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∥ 𝐴 ) )
268 267 notbid ⊢ ( 𝑟 = ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) → ( ¬ 𝑟 ∥ 𝐴 ↔ ¬ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∥ 𝐴 ) )
269 268 elrab3 ⊢ ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ ( 1 ... 𝐵 ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ↔ ¬ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∥ 𝐴 ) )
270 269 con2bid ⊢ ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ ( 1 ... 𝐵 ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∥ 𝐴 ↔ ¬ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) )
271 266 270 syl ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∥ 𝐴 ↔ ¬ ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) )
272 246 271 mpbird ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∥ 𝐴 )
273 134 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → 𝑅 ∈ ℕ )
274 153 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑁 ∈ ℕ )
275 274 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℕ )
276 275 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) → 𝑁 ∈ ℕ )
277 276 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) → 𝑁 ∈ ℕ )
278 74 277 sylbir ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑁 ∈ ℕ )
279 278 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → 𝑁 ∈ ℕ )
280 133 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → 𝑝 ∈ ℙ )
281 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → 𝑞 ∈ ℙ )
282 196 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → 𝑝 ∥ 𝑅 )
283 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → 𝑞 ∥ 𝑅 )
284 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) → ¬ 𝑝 ∥ 𝑁 )
285 284 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → ¬ 𝑝 ∥ 𝑁 )
286 simprl ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → 𝑞 ∥ 𝑁 )
287 273 279 280 281 282 283 285 286 aks4d1p8d2 ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ 𝑞 ∈ ℙ ) ∧ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) < 𝑅 )
288 simpr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 1 < ( 𝑁 gcd 𝑅 ) )
289 288 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 < ( 𝑁 gcd 𝑅 ) )
290 255 289 ltned ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 1 ≠ ( 𝑁 gcd 𝑅 ) )
291 290 necomd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑁 gcd 𝑅 ) ≠ 1 )
292 278 134 prmdvdsncoprmbd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ∃ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ↔ ( 𝑁 gcd 𝑅 ) ≠ 1 ) )
293 292 bicomd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑁 gcd 𝑅 ) ≠ 1 ↔ ∃ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) )
294 293 biimpd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑁 gcd 𝑅 ) ≠ 1 → ∃ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) ) )
295 291 294 mpd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ∃ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝑁 ∧ 𝑞 ∥ 𝑅 ) )
296 287 295 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) < 𝑅 )
297 211 93 ltnled ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
298 296 297 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ¬ 𝑅 ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
299 225 breq1d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ↔ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
300 299 notbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ¬ 𝑅 ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ↔ ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
301 298 300 mpbid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
302 infrefilb ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
303 302 3expa ⊢ ( ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ) ∧ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) )
304 303 ex ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) )
305 304 con3d ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ) → ( ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) → ¬ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) )
306 237 240 305 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ¬ inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) → ¬ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) )
307 301 306 mpd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ¬ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
308 211 93 258 252 264 letrd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ≤ 𝐵 )
309 247 248 136 260 308 elfzd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ( 1 ... 𝐵 ) )
310 breq1 ⊢ ( 𝑟 = ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) → ( 𝑟 ∥ 𝐴 ↔ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝐴 ) )
311 310 notbid ⊢ ( 𝑟 = ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) → ( ¬ 𝑟 ∥ 𝐴 ↔ ¬ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝐴 ) )
312 311 elrab3 ⊢ ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ ( 1 ... 𝐵 ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ↔ ¬ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝐴 ) )
313 309 312 syl ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ↔ ¬ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝐴 ) )
314 313 con2bid ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝐴 ↔ ¬ ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) )
315 307 314 mpbird ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ∥ 𝐴 )
316 149 136 195 197 272 315 coprmdvds2d ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( ( 𝑅 / ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt 𝑅 ) ) ) ∥ 𝐴 )
317 143 316 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → 𝑅 ∥ 𝐴 )
318 317 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∥ 𝐴 )
319 67 simprd ⊢ ( 𝜑 → ¬ 𝑅 ∥ 𝐴 )
320 319 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ 𝑝 ∥ 𝑅 ) ∧ ¬ 𝑝 ∥ 𝑁 ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ¬ 𝑅 ∥ 𝐴 )
321 75 320 sylbir ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ¬ 𝑅 ∥ 𝐴 )
322 318 321 pm2.21dd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ¬ ( 𝑅 / 𝑝 ) ∥ 𝐴 )
323 30 129 322 elrabd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 𝑝 ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
324 lbinfle ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 ∧ ( 𝑅 / 𝑝 ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / 𝑝 ) )
325 17 28 323 324 syl3anc ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / 𝑝 ) )
326 5 325 eqbrtrd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ≤ ( 𝑅 / 𝑝 ) )
327 207 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 1 < 𝑝 )
328 1rp ⊢ 1 ∈ ℝ+
329 328 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 1 ∈ ℝ+ )
330 215 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℝ+ )
331 329 95 330 ltdiv2d ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 1 < 𝑝 ↔ ( 𝑅 / 𝑝 ) < ( 𝑅 / 1 ) ) )
332 327 331 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 𝑝 ) < ( 𝑅 / 1 ) )
333 130 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → 𝑅 ∈ ℂ )
334 333 div1d ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 1 ) = 𝑅 )
335 332 334 breqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 𝑝 ) < 𝑅 )
336 98 101 65 redivcld ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑅 / 𝑝 ) ∈ ℝ )
337 336 adantr ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ( 𝑅 / 𝑝 ) ∈ ℝ )
338 337 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( 𝑅 / 𝑝 ) ∈ ℝ )
339 338 94 ltnled ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ( ( 𝑅 / 𝑝 ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝑅 / 𝑝 ) ) )
340 335 339 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ¬ 𝑅 ≤ ( 𝑅 / 𝑝 ) )
341 326 340 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑝 ∈ ℙ ) ∧ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 )
342 1 2 3 4 aks4d1p7 ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) )
343 342 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) )
344 341 343 r19.29a ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 )
345 344 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 )
346 1 2 3 4 345 aks4d1p5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )