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