Metamath Proof Explorer

Theorem aks6d1c4

Description: Claim 4 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 12-May-2025)

Ref Expression
Hypotheses aks6d1c4.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c4.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c4.3 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c4.4 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c4.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c4.6 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
aks6d1c4.7 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
Assertion aks6d1c4 ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ϕ ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 aks6d1c4.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 aks6d1c4.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3 aks6d1c4.3 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
4 aks6d1c4.4 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
5 aks6d1c4.5 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
6 aks6d1c4.6 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
7 aks6d1c4.7 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
8 fvexd ⊢ ( 𝜑 → ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ∈ V )
9 4 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
10 eqid ⊢ ( ℤ/nℤ ‘ 𝑅 ) = ( ℤ/nℤ ‘ 𝑅 )
11 10 zncrng ⊢ ( 𝑅 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
12 9 11 syl ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
13 crngring ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing → ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring )
14 7 zrhrhm ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring → 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) )
15 zringbas ⊢ ℤ = ( Base ‘ ℤring )
16 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) )
17 15 16 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
18 12 13 14 17 4syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
19 18 ffund ⊢ ( 𝜑 → Fun 𝐿 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) → Fun 𝐿 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) → 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
22 fvelima ⊢ ( ( Fun 𝐿 ∧ 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) → ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 )
23 20 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) → ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 )
24 simpr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ( 𝐿 ‘ 𝑐 ) = 𝑎 ) → ( 𝐿 ‘ 𝑐 ) = 𝑎 )
25 24 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ( 𝐿 ‘ 𝑐 ) = 𝑎 ) → 𝑎 = ( 𝐿 ‘ 𝑐 ) )
26 simpll ⊢ ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → 𝜑 )
27 simpr ⊢ ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
28 26 27 jca ⊢ ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
29 ovexd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) ) ∈ V )
30 vex ⊢ 𝑘 ∈ V
31 vex ⊢ 𝑙 ∈ V
32 30 31 op1std ⊢ ( 𝑚 = ⟨ 𝑘 , 𝑙 ⟩ → ( 1st ‘ 𝑚 ) = 𝑘 )
33 32 oveq2d ⊢ ( 𝑚 = ⟨ 𝑘 , 𝑙 ⟩ → ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) = ( 𝑃 ↑ 𝑘 ) )
34 30 31 op2ndd ⊢ ( 𝑚 = ⟨ 𝑘 , 𝑙 ⟩ → ( 2nd ‘ 𝑚 ) = 𝑙 )
35 34 oveq2d ⊢ ( 𝑚 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
36 33 35 oveq12d ⊢ ( 𝑚 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) ) = ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
37 36 mpompt ⊢ ( 𝑚 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) ) ) = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
38 37 eqcomi ⊢ ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ) = ( 𝑚 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) ) )
39 6 38 eqtri ⊢ 𝐸 = ( 𝑚 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) ) )
40 29 39 fmptd ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ V )
41 40 ffund ⊢ ( 𝜑 → Fun 𝐸 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → Fun 𝐸 )
43 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
44 fvelima ⊢ ( ( Fun 𝐸 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 )
45 42 43 44 syl2anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 )
46 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → ( 𝐸 ‘ 𝑒 ) = 𝑐 )
47 46 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → 𝑐 = ( 𝐸 ‘ 𝑒 ) )
48 47 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → ( 𝑐 gcd 𝑅 ) = ( ( 𝐸 ‘ 𝑒 ) gcd 𝑅 ) )
49 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝜑 )
50 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝑒 ∈ ( ℕ0 × ℕ0 ) )
51 49 50 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) )
52 39 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝐸 = ( 𝑚 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) ) ) )
53 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑚 = 𝑒 ) → 𝑚 = 𝑒 )
54 53 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑚 = 𝑒 ) → ( 1st ‘ 𝑚 ) = ( 1st ‘ 𝑒 ) )
55 54 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑚 = 𝑒 ) → ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) = ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) )
56 53 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑚 = 𝑒 ) → ( 2nd ‘ 𝑚 ) = ( 2nd ‘ 𝑒 ) )
57 56 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑚 = 𝑒 ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) )
58 55 57 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ 𝑚 = 𝑒 ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑚 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑚 ) ) ) = ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) )
59 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝑒 ∈ ( ℕ0 × ℕ0 ) )
60 ovexd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) ∈ V )
61 52 58 59 60 fvmptd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑒 ) = ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) )
62 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
63 2 62 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
64 63 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝑃 ∈ ℤ )
66 xp1st ⊢ ( 𝑒 ∈ ( ℕ0 × ℕ0 ) → ( 1st ‘ 𝑒 ) ∈ ℕ0 )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 1st ‘ 𝑒 ) ∈ ℕ0 )
68 65 67 zexpcld ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ∈ ℤ )
69 63 nnne0d ⊢ ( 𝜑 → 𝑃 ≠ 0 )
70 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
71 dvdsval2 ⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℤ ) )
72 64 69 70 71 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℤ ) )
73 3 72 mpbid ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℤ )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑁 / 𝑃 ) ∈ ℤ )
75 xp2nd ⊢ ( 𝑒 ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ 𝑒 ) ∈ ℕ0 )
76 75 adantl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 2nd ‘ 𝑒 ) ∈ ℕ0 )
77 74 76 zexpcld ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ∈ ℤ )
78 68 77 zmulcld ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) ∈ ℤ )
79 61 78 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑒 ) ∈ ℤ )
80 61 oveq1d ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑒 ) gcd 𝑅 ) = ( ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) gcd 𝑅 ) )
81 4 nnzd ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
82 81 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝑅 ∈ ℤ )
83 78 82 gcdcomd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) gcd 𝑅 ) = ( 𝑅 gcd ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) ) )
84 81 64 70 3jca ⊢ ( 𝜑 → ( 𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
85 70 81 jca ⊢ ( 𝜑 → ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ) )
86 gcdcom ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑅 ∈ ℤ ) → ( 𝑁 gcd 𝑅 ) = ( 𝑅 gcd 𝑁 ) )
87 85 86 syl ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = ( 𝑅 gcd 𝑁 ) )
88 eqeq1 ⊢ ( ( 𝑁 gcd 𝑅 ) = ( 𝑅 gcd 𝑁 ) → ( ( 𝑁 gcd 𝑅 ) = 1 ↔ ( 𝑅 gcd 𝑁 ) = 1 ) )
89 87 88 syl ⊢ ( 𝜑 → ( ( 𝑁 gcd 𝑅 ) = 1 ↔ ( 𝑅 gcd 𝑁 ) = 1 ) )
90 89 pm5.74i ⊢ ( ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 ) ↔ ( 𝜑 → ( 𝑅 gcd 𝑁 ) = 1 ) )
91 5 90 mpbi ⊢ ( 𝜑 → ( 𝑅 gcd 𝑁 ) = 1 )
92 91 3 jca ⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑁 ) = 1 ∧ 𝑃 ∥ 𝑁 ) )
93 rpdvds ⊢ ( ( ( 𝑅 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑅 gcd 𝑁 ) = 1 ∧ 𝑃 ∥ 𝑁 ) ) → ( 𝑅 gcd 𝑃 ) = 1 )
94 84 92 93 syl2anc ⊢ ( 𝜑 → ( 𝑅 gcd 𝑃 ) = 1 )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑅 gcd 𝑃 ) = 1 )
96 95 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd 𝑃 ) = 1 )
97 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ∈ ℕ ) → 𝑅 ∈ ℕ )
98 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ∈ ℕ ) → 𝑃 ∈ ℕ )
99 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 1st ‘ 𝑒 ) ∈ ℕ )
100 rprpwr ⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑃 ∈ ℕ ∧ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( ( 𝑅 gcd 𝑃 ) = 1 → ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 ) )
101 97 98 99 100 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( ( 𝑅 gcd 𝑃 ) = 1 → ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 ) )
102 96 101 mpd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 )
103 67 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ≠ 0 ) → ( ( 1st ‘ 𝑒 ) ∈ ℕ0 ∧ ( 1st ‘ 𝑒 ) ≠ 0 ) )
104 elnnne0 ⊢ ( ( 1st ‘ 𝑒 ) ∈ ℕ ↔ ( ( 1st ‘ 𝑒 ) ∈ ℕ0 ∧ ( 1st ‘ 𝑒 ) ≠ 0 ) )
105 103 104 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 1st ‘ 𝑒 ) ≠ 0 ) → ( 1st ‘ 𝑒 ) ∈ ℕ )
106 105 ex ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 1st ‘ 𝑒 ) ≠ 0 → ( 1st ‘ 𝑒 ) ∈ ℕ ) )
107 106 necon1bd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ¬ ( 1st ‘ 𝑒 ) ∈ ℕ → ( 1st ‘ 𝑒 ) = 0 ) )
108 107 imp ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 1st ‘ 𝑒 ) = 0 )
109 108 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) = ( 𝑃 ↑ 0 ) )
110 109 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = ( 𝑅 gcd ( 𝑃 ↑ 0 ) ) )
111 65 zcnd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝑃 ∈ ℂ )
112 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → 𝑃 ∈ ℂ )
113 112 exp0d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑃 ↑ 0 ) = 1 )
114 113 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( 𝑃 ↑ 0 ) ) = ( 𝑅 gcd 1 ) )
115 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → 𝑅 ∈ ℤ )
116 gcd1 ⊢ ( 𝑅 ∈ ℤ → ( 𝑅 gcd 1 ) = 1 )
117 115 116 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd 1 ) = 1 )
118 114 117 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( 𝑃 ↑ 0 ) ) = 1 )
119 110 118 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 1st ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 )
120 102 119 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 )
121 81 73 70 3jca ⊢ ( 𝜑 → ( 𝑅 ∈ ℤ ∧ ( 𝑁 / 𝑃 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
122 1 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
123 122 recnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
124 63 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
125 124 recnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
126 1 nngt0d ⊢ ( 𝜑 → 0 < 𝑁 )
127 126 gt0ne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
128 123 125 127 69 ddcand ⊢ ( 𝜑 → ( 𝑁 / ( 𝑁 / 𝑃 ) ) = 𝑃 )
129 128 64 eqeltrd ⊢ ( 𝜑 → ( 𝑁 / ( 𝑁 / 𝑃 ) ) ∈ ℤ )
130 63 nngt0d ⊢ ( 𝜑 → 0 < 𝑃 )
131 122 124 126 130 divgt0d ⊢ ( 𝜑 → 0 < ( 𝑁 / 𝑃 ) )
132 131 gt0ne0d ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ≠ 0 )
133 dvdsval2 ⊢ ( ( ( 𝑁 / 𝑃 ) ∈ ℤ ∧ ( 𝑁 / 𝑃 ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 / 𝑃 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑁 / 𝑃 ) ) ∈ ℤ ) )
134 73 132 70 133 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 / 𝑃 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑁 / 𝑃 ) ) ∈ ℤ ) )
135 129 134 mpbird ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∥ 𝑁 )
136 91 135 jca ⊢ ( 𝜑 → ( ( 𝑅 gcd 𝑁 ) = 1 ∧ ( 𝑁 / 𝑃 ) ∥ 𝑁 ) )
137 rpdvds ⊢ ( ( ( 𝑅 ∈ ℤ ∧ ( 𝑁 / 𝑃 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑅 gcd 𝑁 ) = 1 ∧ ( 𝑁 / 𝑃 ) ∥ 𝑁 ) ) → ( 𝑅 gcd ( 𝑁 / 𝑃 ) ) = 1 )
138 121 136 137 syl2anc ⊢ ( 𝜑 → ( 𝑅 gcd ( 𝑁 / 𝑃 ) ) = 1 )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑅 gcd ( 𝑁 / 𝑃 ) ) = 1 )
140 139 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( 𝑁 / 𝑃 ) ) = 1 )
141 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → 𝑅 ∈ ℕ )
142 73 131 jca ⊢ ( 𝜑 → ( ( 𝑁 / 𝑃 ) ∈ ℤ ∧ 0 < ( 𝑁 / 𝑃 ) ) )
143 elnnz ⊢ ( ( 𝑁 / 𝑃 ) ∈ ℕ ↔ ( ( 𝑁 / 𝑃 ) ∈ ℤ ∧ 0 < ( 𝑁 / 𝑃 ) ) )
144 142 143 sylibr ⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℕ )
145 144 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
146 145 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑁 / 𝑃 ) ∈ ℕ )
147 simpr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 2nd ‘ 𝑒 ) ∈ ℕ )
148 rprpwr ⊢ ( ( 𝑅 ∈ ℕ ∧ ( 𝑁 / 𝑃 ) ∈ ℕ ∧ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( ( 𝑅 gcd ( 𝑁 / 𝑃 ) ) = 1 → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 ) )
149 141 146 147 148 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( ( 𝑅 gcd ( 𝑁 / 𝑃 ) ) = 1 → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 ) )
150 140 149 mpd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 )
151 76 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ≠ 0 ) → ( ( 2nd ‘ 𝑒 ) ∈ ℕ0 ∧ ( 2nd ‘ 𝑒 ) ≠ 0 ) )
152 elnnne0 ⊢ ( ( 2nd ‘ 𝑒 ) ∈ ℕ ↔ ( ( 2nd ‘ 𝑒 ) ∈ ℕ0 ∧ ( 2nd ‘ 𝑒 ) ≠ 0 ) )
153 151 152 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 2nd ‘ 𝑒 ) ≠ 0 ) → ( 2nd ‘ 𝑒 ) ∈ ℕ )
154 153 ex ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 2nd ‘ 𝑒 ) ≠ 0 → ( 2nd ‘ 𝑒 ) ∈ ℕ ) )
155 154 necon1bd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ → ( 2nd ‘ 𝑒 ) = 0 ) )
156 155 imp ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 2nd ‘ 𝑒 ) = 0 )
157 156 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 0 ) )
158 157 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ 0 ) ) )
159 123 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → 𝑁 ∈ ℂ )
160 159 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → 𝑁 ∈ ℂ )
161 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → 𝑃 ∈ ℂ )
162 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → 𝑃 ≠ 0 )
163 160 161 162 divcld ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑁 / 𝑃 ) ∈ ℂ )
164 163 exp0d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( ( 𝑁 / 𝑃 ) ↑ 0 ) = 1 )
165 164 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ 0 ) ) = ( 𝑅 gcd 1 ) )
166 158 165 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = ( 𝑅 gcd 1 ) )
167 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → 𝑅 ∈ ℤ )
168 167 116 syl ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd 1 ) = 1 )
169 166 168 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ¬ ( 2nd ‘ 𝑒 ) ∈ ℕ ) → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 )
170 150 169 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 )
171 120 170 jca ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 ∧ ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 ) )
172 rpmul ⊢ ( ( 𝑅 ∈ ℤ ∧ ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ∈ ℤ ∧ ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ∈ ℤ ) → ( ( ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 ∧ ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 ) → ( 𝑅 gcd ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) ) = 1 ) )
173 82 68 77 172 syl3anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( 𝑅 gcd ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) ) = 1 ∧ ( 𝑅 gcd ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) = 1 ) → ( 𝑅 gcd ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) ) = 1 ) )
174 171 173 mpd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝑅 gcd ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) ) = 1 )
175 83 174 eqtrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( ( 𝑃 ↑ ( 1st ‘ 𝑒 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑒 ) ) ) gcd 𝑅 ) = 1 )
176 80 175 eqtrd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑒 ) gcd 𝑅 ) = 1 )
177 79 176 jca ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑒 ) ∈ ℤ ∧ ( ( 𝐸 ‘ 𝑒 ) gcd 𝑅 ) = 1 ) )
178 51 177 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) → ( ( 𝐸 ‘ 𝑒 ) ∈ ℤ ∧ ( ( 𝐸 ‘ 𝑒 ) gcd 𝑅 ) = 1 ) )
179 178 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → ( ( 𝐸 ‘ 𝑒 ) ∈ ℤ ∧ ( ( 𝐸 ‘ 𝑒 ) gcd 𝑅 ) = 1 ) )
180 179 simprd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → ( ( 𝐸 ‘ 𝑒 ) gcd 𝑅 ) = 1 )
181 48 180 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → ( 𝑐 gcd 𝑅 ) = 1 )
182 179 simpld ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → ( 𝐸 ‘ 𝑒 ) ∈ ℤ )
183 47 182 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → 𝑐 ∈ ℤ )
184 181 183 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) ∧ 𝑒 ∈ ( ℕ0 × ℕ0 ) ) ∧ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) → ( ( 𝑐 gcd 𝑅 ) = 1 ∧ 𝑐 ∈ ℤ ) )
185 nfv ⊢ Ⅎ 𝑒 ( 𝐸 ‘ 𝑑 ) = 𝑐
186 nfv ⊢ Ⅎ 𝑑 ( 𝐸 ‘ 𝑒 ) = 𝑐
187 fveqeq2 ⊢ ( 𝑑 = 𝑒 → ( ( 𝐸 ‘ 𝑑 ) = 𝑐 ↔ ( 𝐸 ‘ 𝑒 ) = 𝑐 ) )
188 185 186 187 cbvrexw ⊢ ( ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ↔ ∃ 𝑒 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑒 ) = 𝑐 )
189 188 bilani ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) → ∃ 𝑒 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑒 ) = 𝑐 )
190 184 189 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 ) → ( ( 𝑐 gcd 𝑅 ) = 1 ∧ 𝑐 ∈ ℤ ) )
191 190 ex ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( ∃ 𝑑 ∈ ( ℕ0 × ℕ0 ) ( 𝐸 ‘ 𝑑 ) = 𝑐 → ( ( 𝑐 gcd 𝑅 ) = 1 ∧ 𝑐 ∈ ℤ ) ) )
192 45 191 mpd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( ( 𝑐 gcd 𝑅 ) = 1 ∧ 𝑐 ∈ ℤ ) )
193 192 simpld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( 𝑐 gcd 𝑅 ) = 1 )
194 9 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → 𝑅 ∈ ℕ0 )
195 192 simprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → 𝑐 ∈ ℤ )
196 eqid ⊢ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) = ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) )
197 10 196 7 znunit ⊢ ( ( 𝑅 ∈ ℕ0 ∧ 𝑐 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑐 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ↔ ( 𝑐 gcd 𝑅 ) = 1 ) )
198 194 195 197 syl2anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( ( 𝐿 ‘ 𝑐 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ↔ ( 𝑐 gcd 𝑅 ) = 1 ) )
199 193 198 mpbird ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( 𝐿 ‘ 𝑐 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
200 28 199 syl ⊢ ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( 𝐿 ‘ 𝑐 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
201 200 adantr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ( 𝐿 ‘ 𝑐 ) = 𝑎 ) → ( 𝐿 ‘ 𝑐 ) ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
202 25 201 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) ∧ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∧ ( 𝐿 ‘ 𝑐 ) = 𝑎 ) → 𝑎 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
203 nfv ⊢ Ⅎ 𝑐 ( 𝐿 ‘ 𝑏 ) = 𝑎
204 nfv ⊢ Ⅎ 𝑏 ( 𝐿 ‘ 𝑐 ) = 𝑎
205 fveqeq2 ⊢ ( 𝑏 = 𝑐 → ( ( 𝐿 ‘ 𝑏 ) = 𝑎 ↔ ( 𝐿 ‘ 𝑐 ) = 𝑎 ) )
206 203 204 205 cbvrexw ⊢ ( ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ↔ ∃ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑐 ) = 𝑎 )
207 206 bilani ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) → ∃ 𝑐 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑐 ) = 𝑎 )
208 202 207 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 ) → 𝑎 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
209 208 ex ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 → 𝑎 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) )
210 209 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) → ( ∃ 𝑏 ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ( 𝐿 ‘ 𝑏 ) = 𝑎 → 𝑎 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) )
211 23 210 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) → 𝑎 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
212 211 ex ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → 𝑎 ∈ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) )
213 212 ssrdv ⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ⊆ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
214 hashss ⊢ ( ( ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ∈ V ∧ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ⊆ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) )
215 8 213 214 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) )
216 10 196 znunithash ⊢ ( 𝑅 ∈ ℕ → ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) = ( ϕ ‘ 𝑅 ) )
217 4 216 syl ⊢ ( 𝜑 → ( ♯ ‘ ( Unit ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) = ( ϕ ‘ 𝑅 ) )
218 215 217 breqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ϕ ‘ 𝑅 ) )