Metamath Proof Explorer

Theorem aks4d1p5

Description: Show that N and R are coprime for AKS existence theorem. Precondition will be eliminated in further theorem. (Contributed by metakunt, 30-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 aks4d1p5.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 3 ) )
2 aks4d1p5.2 ⊢ 𝐴 = ( ( 𝑁 ↑ ( ⌊ ‘ ( 2 logb 𝐵 ) ) ) · ∏ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( 2 logb 𝑁 ) ↑ 2 ) ) ) ( ( 𝑁 ↑ 𝑘 ) − 1 ) )
3 aks4d1p5.3 ⊢ 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) )
4 aks4d1p5.4 ⊢ 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < )
5 aks4d1p5.5 ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 )
6 simpr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ) → 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
7 1 2 3 4 aks4d1p4 ⊢ ( 𝜑 → ( 𝑅 ∈ ( 1 ... 𝐵 ) ∧ ¬ 𝑅 ∥ 𝐴 ) )
8 7 simpld ⊢ ( 𝜑 → 𝑅 ∈ ( 1 ... 𝐵 ) )
9 elfznn ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ∈ ℕ )
10 8 9 syl ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
11 10 nnred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
12 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
13 1 12 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
14 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
15 3re ⊢ 3 ∈ ℝ
16 15 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
17 13 zred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
18 3pos ⊢ 0 < 3
19 18 a1i ⊢ ( 𝜑 → 0 < 3 )
20 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑁 )
21 1 20 syl ⊢ ( 𝜑 → 3 ≤ 𝑁 )
22 14 16 17 19 21 ltletrd ⊢ ( 𝜑 → 0 < 𝑁 )
23 13 22 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
24 elnnz ⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 0 < 𝑁 ) )
25 23 24 sylibr ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
26 gcdnncl ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑅 ∈ ℕ ) → ( 𝑁 gcd 𝑅 ) ∈ ℕ )
27 25 10 26 syl2anc ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) ∈ ℕ )
28 27 nnred ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) ∈ ℝ )
29 27 nnne0d ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) ≠ 0 )
30 11 28 29 redivcld ⊢ ( 𝜑 → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ℝ )
31 30 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ℝ )
32 11 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ∈ ℝ )
33 31 32 ltnled ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ) )
34 33 biimprd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 ) )
35 34 imp ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 )
36 4 a1i ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 = inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) )
37 ssrab2 ⊢ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 )
38 37 a1i ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ( 1 ... 𝐵 ) )
39 elfznn ⊢ ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℕ )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℕ )
41 40 nnred ⊢ ( ( 𝜑 ∧ 𝑜 ∈ ( 1 ... 𝐵 ) ) → 𝑜 ∈ ℝ )
42 41 ex ⊢ ( 𝜑 → ( 𝑜 ∈ ( 1 ... 𝐵 ) → 𝑜 ∈ ℝ ) )
43 42 ssrdv ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ⊆ ℝ )
44 38 43 sstrd ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
45 44 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ )
46 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐵 ) ∈ Fin )
47 46 38 ssfid ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
48 47 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin )
49 1 2 3 aks4d1p3 ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
50 rabn0 ⊢ ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ↔ ∃ 𝑟 ∈ ( 1 ... 𝐵 ) ¬ 𝑟 ∥ 𝐴 )
51 49 50 sylibr ⊢ ( 𝜑 → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ )
53 fiminre ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∈ Fin ∧ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ≠ ∅ ) → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
54 45 48 52 53 syl3anc ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 )
55 breq1 ⊢ ( 𝑟 = ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) → ( 𝑟 ∥ 𝐴 ↔ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) )
56 55 notbid ⊢ ( 𝑟 = ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) → ( ¬ 𝑟 ∥ 𝐴 ↔ ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) )
57 1zzd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 1 ∈ ℤ )
58 3 a1i ⊢ ( 𝜑 → 𝐵 = ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) )
59 2re ⊢ 2 ∈ ℝ
60 59 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
61 2pos ⊢ 0 < 2
62 61 a1i ⊢ ( 𝜑 → 0 < 2 )
63 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
64 1lt2 ⊢ 1 < 2
65 64 a1i ⊢ ( 𝜑 → 1 < 2 )
66 63 65 ltned ⊢ ( 𝜑 → 1 ≠ 2 )
67 66 necomd ⊢ ( 𝜑 → 2 ≠ 1 )
68 60 62 17 22 67 relogbcld ⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
69 5nn0 ⊢ 5 ∈ ℕ0
70 69 a1i ⊢ ( 𝜑 → 5 ∈ ℕ0 )
71 68 70 reexpcld ⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ )
72 ceilcl ⊢ ( ( ( 2 logb 𝑁 ) ↑ 5 ) ∈ ℝ → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
73 71 72 syl ⊢ ( 𝜑 → ( ⌈ ‘ ( ( 2 logb 𝑁 ) ↑ 5 ) ) ∈ ℤ )
74 58 73 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
75 74 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝐵 ∈ ℤ )
76 25 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
77 divgcdnnr ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ℕ )
78 10 76 77 syl2anc ⊢ ( 𝜑 → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ℕ )
79 78 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ℕ )
80 79 nnzd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ℤ )
81 79 nnge1d ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 1 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
82 75 zred ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝐵 ∈ ℝ )
83 10 nnrpd ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
84 83 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ∈ ℝ+ )
85 27 nnrpd ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) ∈ ℝ+ )
86 85 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) ∈ ℝ+ )
87 32 recnd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ∈ ℂ )
88 84 rpne0d ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ≠ 0 )
89 87 88 dividd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / 𝑅 ) = 1 )
90 simpr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 1 < ( 𝑁 gcd 𝑅 ) )
91 89 90 eqbrtrd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / 𝑅 ) < ( 𝑁 gcd 𝑅 ) )
92 32 84 86 91 ltdiv23d ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 )
93 31 32 92 ltled ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ≤ 𝑅 )
94 elfzle2 ⊢ ( 𝑅 ∈ ( 1 ... 𝐵 ) → 𝑅 ≤ 𝐵 )
95 8 94 syl ⊢ ( 𝜑 → 𝑅 ≤ 𝐵 )
96 95 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ≤ 𝐵 )
97 31 32 82 93 96 letrd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ≤ 𝐵 )
98 57 75 80 81 97 elfzd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ( 1 ... 𝐵 ) )
99 simpr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 )
100 exmidd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ∨ ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 ) )
101 5 99 100 mpjaodan ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∥ 𝐴 )
102 56 98 101 elrabd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } )
103 lbinfle ⊢ ( ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ⊆ ℝ ∧ ∃ 𝑥 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ∀ 𝑦 ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } 𝑥 ≤ 𝑦 ∧ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
104 45 54 102 103 syl3anc ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → inf ( { 𝑟 ∈ ( 1 ... 𝐵 ) ∣ ¬ 𝑟 ∥ 𝐴 } , ℝ , < ) ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
105 36 104 eqbrtrd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
106 32 31 lenltd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ↔ ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 ) )
107 105 106 mpbid ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 )
108 107 adantr ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ) → ¬ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 )
109 35 108 pm2.21dd ⊢ ( ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ) → 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
110 6 109 pm2.61dan ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
111 83 rpred ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
112 111 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ∈ ℝ )
113 92 107 pm2.21dd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) ∈ ℕ )
114 113 nnrpd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) ∈ ℝ+ )
115 112 recnd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → 𝑅 ∈ ℂ )
116 115 88 dividd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / 𝑅 ) = 1 )
117 116 90 eqbrtrd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / 𝑅 ) < ( 𝑁 gcd 𝑅 ) )
118 112 84 114 117 ltdiv23d ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 )
119 78 nnred ⊢ ( 𝜑 → ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ∈ ℝ )
120 119 111 ltnled ⊢ ( 𝜑 → ( ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ) )
121 120 adantr ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) ) )
122 118 121 mpbid ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ¬ 𝑅 ≤ ( 𝑅 / ( 𝑁 gcd 𝑅 ) ) )
123 110 122 pm2.21dd ⊢ ( ( 𝜑 ∧ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
124 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) = 1 ) → ( 𝑁 gcd 𝑅 ) = 1 )
125 27 adantr ⊢ ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) ∈ ℕ )
126 125 nnred ⊢ ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) ∈ ℝ )
127 126 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 gcd 𝑅 ) ∈ ℝ )
128 59 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → 2 ∈ ℝ )
129 1red ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 ∈ ℝ )
130 28 63 lenltd ⊢ ( 𝜑 → ( ( 𝑁 gcd 𝑅 ) ≤ 1 ↔ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) )
131 130 biimprd ⊢ ( 𝜑 → ( ¬ 1 < ( 𝑁 gcd 𝑅 ) → ( 𝑁 gcd 𝑅 ) ≤ 1 ) )
132 131 imp ⊢ ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) ≤ 1 )
133 132 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 gcd 𝑅 ) ≤ 1 )
134 64 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 2 )
135 127 129 128 133 134 lelttrd ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 gcd 𝑅 ) < 2 )
136 eluzle ⊢ ( ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( 𝑁 gcd 𝑅 ) )
137 136 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → 2 ≤ ( 𝑁 gcd 𝑅 ) )
138 127 128 127 135 137 ltletrd ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 gcd 𝑅 ) < ( 𝑁 gcd 𝑅 ) )
139 127 ltnrd ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( 𝑁 gcd 𝑅 ) < ( 𝑁 gcd 𝑅 ) )
140 138 139 pm2.21dd ⊢ ( ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) ∧ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
141 elnn1uz2 ⊢ ( ( 𝑁 gcd 𝑅 ) ∈ ℕ ↔ ( ( 𝑁 gcd 𝑅 ) = 1 ∨ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) )
142 125 141 sylib ⊢ ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) → ( ( 𝑁 gcd 𝑅 ) = 1 ∨ ( 𝑁 gcd 𝑅 ) ∈ ( ℤ≥ ‘ 2 ) ) )
143 124 140 142 mpjaodan ⊢ ( ( 𝜑 ∧ ¬ 1 < ( 𝑁 gcd 𝑅 ) ) → ( 𝑁 gcd 𝑅 ) = 1 )
144 123 143 pm2.61dan ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )