Metamath Proof Explorer

Theorem aks4d1p7

Description: Technical step in AKS lemma 4.1. (Contributed by metakunt, 31-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 aks4d1p7.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p7.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p7.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p7.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
5 1 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
6 breq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∥ 𝑅 ↔ 𝑞 ∥ 𝑅 ) )
7 breq1 ⊢ ( 𝑝 = 𝑞 → ( 𝑝 ∥ 𝑁 ↔ 𝑞 ∥ 𝑁 ) )
8 6 7 imbi12d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ↔ ( 𝑞 ∥ 𝑅 → 𝑞 ∥ 𝑁 ) ) )
9 8 cbvralvw ⊢ ( ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ↔ ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝑅 → 𝑞 ∥ 𝑁 ) )
10 9 bilani ⊢ ( ( 𝜑 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ) → ∀ 𝑞 ∈ ℙ ( 𝑞 ∥ 𝑅 → 𝑞 ∥ 𝑁 ) )
11 5 2 3 4 10 aks4d1p7d1 ⊢ ( ( 𝜑 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ) → 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
12 4 a1i ⊢ ( 𝜑 → 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) )
13 ltso ⊢ < Or ℝ
14 13 a1i ⊢ ( 𝜑 → < Or ℝ )
15 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ∈ Fin )
16 ssrab2 ⊢ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 )
17 16 a1i ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 ) )
18 15 17 ssfid ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
19 1 2 3 aks4d1p3 ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
20 rabn0 ⊢ ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ↔ ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
21 19 20 sylibr ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ )
22 elfznn ⊢ ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℕ )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℕ )
24 23 nnred ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℝ )
25 24 ex ⊢ ( 𝜑 → ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℝ ) )
26 25 ssrdv ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ⊆ ℝ )
27 17 26 sstrd ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
28 18 21 27 3jca ⊢ ( 𝜑 → ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ) )
29 fiinfcl ⊢ ( ( < Or ℝ ∧ ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ) ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
30 14 28 29 syl2anc ⊢ ( 𝜑 → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
31 12 30 eqeltrd ⊢ ( 𝜑 → 𝑅 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
32 breq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∥ 𝐴 ↔ 𝑅 ∥ 𝐴 ) )
33 32 notbid ⊢ ( 𝑟 = 𝑅 → ( ¬ 𝑟 ∥ 𝐴 ↔ ¬ 𝑅 ∥ 𝐴 ) )
34 33 elrab ⊢ ( 𝑅 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ↔ ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
35 31 34 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
36 35 simprd ⊢ ( 𝜑 → ¬ 𝑅 ∥ 𝐴 )
37 1 2 3 4 aks4d1p4 ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
38 37 simpld ⊢ ( 𝜑 → 𝑅 ∈ ( 1 ... 𝐵 ) )
39 38 elfzelzd ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
40 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
41 1 40 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
42 2re ⊢ 2 ∈ ℝ
43 42 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
44 2pos ⊢ 0 < 2
45 44 a1i ⊢ ( 𝜑 → 0 < 2 )
46 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
47 41 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
48 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
49 3re ⊢ 3 ∈ ℝ
50 49 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
51 3pos ⊢ 0 < 3
52 51 a1i ⊢ ( 𝜑 → 0 < 3 )
53 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
54 1 53 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
55 48 50 47 52 54 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
56 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
57 1lt2 ⊢ 1 < 2
58 57 a1i ⊢ ( 𝜑 → 1 < 2 )
59 56 58 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
60 59 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
61 43 45 47 55 60 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
62 5nn0 ⊢ 5 ∈ ℕ0
63 62 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
64 61 63 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
65 64 ceilcld ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
66 65 zred ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℝ )
67 46 66 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
68 9re ⊢ 9 ∈ ℝ
69 68 a1i ⊢ ( 𝜑 → 9 ∈ ℝ )
70 9pos ⊢ 0 < 9
71 70 a1i ⊢ ( 𝜑 → 0 < 9 )
72 47 54 3lexlogpow5ineq4 ⊢ ( 𝜑 → 9 < ( ( 2 logb 𝑁 ) ↑ 5 ) )
73 64 ceilged ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ≤ ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
74 69 64 66 72 73 ltletrd ⊢ ( 𝜑 → 9 < ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
75 74 46 breqtrrd ⊢ ( 𝜑 → 9 < 𝐵 )
76 48 69 67 71 75 lttrd ⊢ ( 𝜑 → 0 < 𝐵 )
77 43 45 67 76 60 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝐵 ) ∈ ℝ )
78 77 flcld ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ )
79 43 recnd ⊢ ( 𝜑 → 2 ∈ ℂ )
80 48 45 gtned ⊢ ( 𝜑 → 2 ≠ 0 )
81 logb1 ⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1 ) → ( 2 logb 1 ) = 0 )
82 79 80 60 81 syl3anc ⊢ ( 𝜑 → ( 2 logb 1 ) = 0 )
83 82 eqcomd ⊢ ( 𝜑 → 0 = ( 2 logb 1 ) )
84 2z ⊢ 2 ∈ ℤ
85 84 a1i ⊢ ( 𝜑 → 2 ∈ ℤ )
86 43 leidd ⊢ ( 𝜑 → 2 ≤ 2 )
87 0lt1 ⊢ 0 < 1
88 87 a1i ⊢ ( 𝜑 → 0 < 1 )
89 1lt9 ⊢ 1 < 9
90 89 a1i ⊢ ( 𝜑 → 1 < 9 )
91 56 69 90 ltled ⊢ ( 𝜑 → 1 ≤ 9 )
92 69 67 75 ltled ⊢ ( 𝜑 → 9 ≤ 𝐵 )
93 56 69 67 91 92 letrd ⊢ ( 𝜑 → 1 ≤ 𝐵 )
94 85 86 56 88 67 76 93 logblebd ⊢ ( 𝜑 → ( 2 logb 1 ) ≤ ( 2 logb 𝐵 ) )
95 83 94 eqbrtrd ⊢ ( 𝜑 → 0 ≤ ( 2 logb 𝐵 ) )
96 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
97 flge ⊢ ( ( ( 2 logb 𝐵 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
98 77 96 97 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( 2 logb 𝐵 ) ↔ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
99 95 98 mpbid ⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) )
100 78 99 jca ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
101 elnn0z ⊢ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 ↔ ( ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℤ ∧ 0 ≤ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
102 100 101 sylibr ⊢ ( 𝜑 → ( ⌊ ‘ ( 2 logb 𝐵 ) ) ∈ ℕ0 )
103 41 102 zexpcld ⊢ ( 𝜑 → ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℤ )
104 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ∈ Fin )
105 41 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑁 ∈ ℤ )
106 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) → 𝑘 ∈ ℕ )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ )
108 107 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 𝑘 ∈ ℕ0 )
109 105 108 zexpcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( 𝑁 ↑ 𝑘 ) ∈ ℤ )
110 1zzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → 1 ∈ ℤ )
111 109 110 zsubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ) → ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
112 104 111 fprodzcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ )
113 dvdsmultr1 ⊢ ( ( 𝑅 ∈ ℤ ∧ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ∈ ℤ ∧ ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ∈ ℤ ) → ( 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) → 𝑅 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ) )
114 39 103 112 113 syl3anc ⊢ ( 𝜑 → ( 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) → 𝑅 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ) )
115 114 imp ⊢ ( ( 𝜑 ∧ 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) → 𝑅 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
116 2 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) )
117 116 breq2d ⊢ ( 𝜑 → ( 𝑅 ∥ 𝐴 ↔ 𝑅 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ) )
118 117 adantr ⊢ ( ( 𝜑 ∧ 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) → ( 𝑅 ∥ 𝐴 ↔ 𝑅 ∥ ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) ) ) )
119 115 118 mpbird ⊢ ( ( 𝜑 ∧ 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) → 𝑅 ∥ 𝐴 )
120 119 ex ⊢ ( 𝜑 → ( 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) → 𝑅 ∥ 𝐴 ) )
121 120 con3d ⊢ ( 𝜑 → ( ¬ 𝑅 ∥ 𝐴 → ¬ 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) ) )
122 36 121 mpd ⊢ ( 𝜑 → ¬ 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
123 122 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ) → ¬ 𝑅 ∥ ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) )
124 11 123 pm2.65da ⊢ ( 𝜑 → ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
125 ianor ⊢ ( ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ( ¬ 𝑝 ∥ 𝑅 ∨ ¬ ¬ 𝑝 ∥ 𝑁 ) )
126 notnotb ⊢ ( 𝑝 ∥ 𝑁 ↔ ¬ ¬ 𝑝 ∥ 𝑁 )
127 126 orbi2i ⊢ ( ( ¬ 𝑝 ∥ 𝑅 ∨ 𝑝 ∥ 𝑁 ) ↔ ( ¬ 𝑝 ∥ 𝑅 ∨ ¬ ¬ 𝑝 ∥ 𝑁 ) )
128 127 bicomi ⊢ ( ( ¬ 𝑝 ∥ 𝑅 ∨ ¬ ¬ 𝑝 ∥ 𝑁 ) ↔ ( ¬ 𝑝 ∥ 𝑅 ∨ 𝑝 ∥ 𝑁 ) )
129 125 128 bitri ⊢ ( ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ( ¬ 𝑝 ∥ 𝑅 ∨ 𝑝 ∥ 𝑁 ) )
130 df-or ⊢ ( ( ¬ 𝑝 ∥ 𝑅 ∨ 𝑝 ∥ 𝑁 ) ↔ ( ¬ ¬ 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
131 129 130 bitri ⊢ ( ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ( ¬ ¬ 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
132 notnotb ⊢ ( 𝑝 ∥ 𝑅 ↔ ¬ ¬ 𝑝 ∥ 𝑅 )
133 132 imbi1i ⊢ ( ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ↔ ( ¬ ¬ 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
134 133 bicomi ⊢ ( ( ¬ ¬ 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) ↔ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
135 131 134 bitri ⊢ ( ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
136 135 ralbii ⊢ ( ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
137 136 notbii ⊢ ( ¬ ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ¬ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 → 𝑝 ∥ 𝑁 ) )
138 124 137 sylibr ⊢ ( 𝜑 → ¬ ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) )
139 ralnex ⊢ ( ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ¬ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) )
140 139 con2bii ⊢ ( ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ¬ ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) )
141 140 bicomi ⊢ ( ¬ ∀ 𝑝 ∈ ℙ ¬ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) ↔ ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) )
142 138 141 sylib ⊢ ( 𝜑 → ∃ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝑅 ∧ ¬ 𝑝 ∥ 𝑁 ) )