Metamath Proof Explorer

Theorem aks6d1c5lem1

Description: Lemma for claim 5, evaluate the linear factor at -c to get a root. (Contributed by metakunt, 5-May-2025)

Ref Expression
Hypotheses aks6d1p5.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c5p1.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 0 ... 𝐴 ) )
aks6d1c5p1.2 ⊢ ( 𝜑 → 𝐶 ∈ ( 0 ... 𝐴 ) )
Assertion aks6d1c5lem1 ( 𝜑 → ( 𝐵 = 𝐶 ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) = ( 0g ‘ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1p5.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
2 aks6d1p5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3 aks6d1c5.3 ⊢ 𝑃 = ( chr ‘ 𝐾 )
4 aks6d1c5.4 ⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
5 aks6d1c5.5 ⊢ ( 𝜑 → 𝐴 < 𝑃 )
6 aks6d1c5.6 ⊢ 𝑋 = ( var1 ‘ 𝐾 )
7 aks6d1c5.7 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
8 aks6d1c5.8 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ↑ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
9 aks6d1c5p1.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 0 ... 𝐴 ) )
10 aks6d1c5p1.2 ⊢ ( 𝜑 → 𝐶 ∈ ( 0 ... 𝐴 ) )
11 zringplusg ⊢ + = ( +g ‘ ℤring )
12 11 eqcomi ⊢ ( +g ‘ ℤring ) = +
13 12 a1i ⊢ ( 𝜑 → ( +g ‘ ℤring ) = + )
14 13 oveqd ⊢ ( 𝜑 → ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) = ( ( 0 − 𝐶 ) + 𝐵 ) )
15 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
16 10 elfzelzd ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
17 16 zcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
18 9 elfzelzd ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
19 18 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
20 15 17 19 subadd23d ⊢ ( 𝜑 → ( ( 0 − 𝐶 ) + 𝐵 ) = ( 0 + ( 𝐵 − 𝐶 ) ) )
21 19 17 subcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℂ )
22 21 addlidd ⊢ ( 𝜑 → ( 0 + ( 𝐵 − 𝐶 ) ) = ( 𝐵 − 𝐶 ) )
23 20 22 eqtrd ⊢ ( 𝜑 → ( ( 0 − 𝐶 ) + 𝐵 ) = ( 𝐵 − 𝐶 ) )
24 14 23 eqtrd ⊢ ( 𝜑 → ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) = ( 𝐵 − 𝐶 ) )
25 24 fveq2d ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ ( 𝐵 − 𝐶 ) ) )
26 25 eqeq1d ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) ) = ( 0g ‘ 𝐾 ) ↔ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 𝐵 − 𝐶 ) ) = ( 0g ‘ 𝐾 ) ) )
27 2 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑃 ∈ ℙ )
28 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑃 ∈ ℕ )
30 29 nnzd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑃 ∈ ℤ )
31 dvds0 ⊢ ( 𝑃 ∈ ℤ → 𝑃 ∥ 0 )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑃 ∥ 0 )
33 19 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 ∈ ℂ )
34 33 subidd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐵 ) = 0 )
35 34 eqcomd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 0 = ( 𝐵 − 𝐵 ) )
36 simpr ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
37 36 oveq2d ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → ( 𝐵 − 𝐵 ) = ( 𝐵 − 𝐶 ) )
38 35 37 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 0 = ( 𝐵 − 𝐶 ) )
39 32 38 breqtrd ⊢ ( ( 𝜑 ∧ 𝐵 = 𝐶 ) → 𝑃 ∥ ( 𝐵 − 𝐶 ) )
40 39 ex ⊢ ( 𝜑 → ( 𝐵 = 𝐶 → 𝑃 ∥ ( 𝐵 − 𝐶 ) ) )
41 2 28 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
42 41 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) → 𝑃 ∈ ℕ )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 𝑃 ∈ ℕ )
44 1zzd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 1 ∈ ℤ )
45 43 nnzd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 𝑃 ∈ ℤ )
46 45 44 zsubcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝑃 − 1 ) ∈ ℤ )
47 18 16 zsubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) ∈ ℤ )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝐵 − 𝐶 ) ∈ ℤ )
49 1e0p1 ⊢ 1 = ( 0 + 1 )
50 49 a1i ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 1 = ( 0 + 1 ) )
51 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 𝐶 < 𝐵 )
52 16 zred ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
53 52 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) → 𝐶 ∈ ℝ )
54 53 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 𝐶 ∈ ℝ )
55 18 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
56 55 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) → 𝐵 ∈ ℝ )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 𝐵 ∈ ℝ )
58 54 57 posdifd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝐶 < 𝐵 ↔ 0 < ( 𝐵 − 𝐶 ) ) )
59 51 58 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 0 < ( 𝐵 − 𝐶 ) )
60 0zd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 0 ∈ ℤ )
61 60 48 zltp1led ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 0 < ( 𝐵 − 𝐶 ) ↔ ( 0 + 1 ) ≤ ( 𝐵 − 𝐶 ) ) )
62 59 61 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 0 + 1 ) ≤ ( 𝐵 − 𝐶 ) )
63 50 62 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 1 ≤ ( 𝐵 − 𝐶 ) )
64 48 zred ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝐵 − 𝐶 ) ∈ ℝ )
65 43 nnred ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 𝑃 ∈ ℝ )
66 elfzle1 ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → 0 ≤ 𝐶 )
67 10 66 syl ⊢ ( 𝜑 → 0 ≤ 𝐶 )
68 67 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) → 0 ≤ 𝐶 )
69 68 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 0 ≤ 𝐶 )
70 57 54 subge02d ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 0 ≤ 𝐶 ↔ ( 𝐵 − 𝐶 ) ≤ 𝐵 ) )
71 69 70 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝐵 − 𝐶 ) ≤ 𝐵 )
72 4 nn0red ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
73 41 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
74 elfzle2 ⊢ ( 𝐵 ∈ ( 0 ... 𝐴 ) → 𝐵 ≤ 𝐴 )
75 9 74 syl ⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
76 55 72 73 75 5 lelttrd ⊢ ( 𝜑 → 𝐵 < 𝑃 )
77 76 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) → 𝐵 < 𝑃 )
78 77 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → 𝐵 < 𝑃 )
79 64 57 65 71 78 lelttrd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝐵 − 𝐶 ) < 𝑃 )
80 48 45 zltlem1d ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( ( 𝐵 − 𝐶 ) < 𝑃 ↔ ( 𝐵 − 𝐶 ) ≤ ( 𝑃 − 1 ) ) )
81 79 80 mpbid ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝐵 − 𝐶 ) ≤ ( 𝑃 − 1 ) )
82 44 46 48 63 81 elfzd ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ( 𝐵 − 𝐶 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
83 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝐵 − 𝐶 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( 𝐵 − 𝐶 ) )
84 43 82 83 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ 𝐶 < 𝐵 ) → ¬ 𝑃 ∥ ( 𝐵 − 𝐶 ) )
85 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ ¬ 𝐶 < 𝐵 ) → 𝜑 )
86 axlttri ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 < 𝐵 ) ) )
87 55 52 86 syl2anc ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ ¬ ( 𝐵 = 𝐶 ∨ 𝐶 < 𝐵 ) ) )
88 ioran ⊢ ( ¬ ( 𝐵 = 𝐶 ∨ 𝐶 < 𝐵 ) ↔ ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵 ) )
89 88 a1i ⊢ ( 𝜑 → ( ¬ ( 𝐵 = 𝐶 ∨ 𝐶 < 𝐵 ) ↔ ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵 ) ) )
90 87 89 bitr2d ⊢ ( 𝜑 → ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵 ) ↔ 𝐵 < 𝐶 ) )
91 90 biimpd ⊢ ( 𝜑 → ( ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵 ) → 𝐵 < 𝐶 ) )
92 91 imp ⊢ ( ( 𝜑 ∧ ( ¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵 ) ) → 𝐵 < 𝐶 )
93 92 anassrs ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ ¬ 𝐶 < 𝐵 ) → 𝐵 < 𝐶 )
94 85 93 jca ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ ¬ 𝐶 < 𝐵 ) → ( 𝜑 ∧ 𝐵 < 𝐶 ) )
95 41 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝑃 ∈ ℕ )
96 1zzd ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 1 ∈ ℤ )
97 41 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝑃 ∈ ℤ )
99 98 96 zsubcld ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝑃 − 1 ) ∈ ℤ )
100 16 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐶 ∈ ℤ )
101 18 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐵 ∈ ℤ )
102 100 101 zsubcld ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝐶 − 𝐵 ) ∈ ℤ )
103 49 a1i ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 1 = ( 0 + 1 ) )
104 55 52 posdifd ⊢ ( 𝜑 → ( 𝐵 < 𝐶 ↔ 0 < ( 𝐶 − 𝐵 ) ) )
105 104 biimpd ⊢ ( 𝜑 → ( 𝐵 < 𝐶 → 0 < ( 𝐶 − 𝐵 ) ) )
106 105 imp ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 0 < ( 𝐶 − 𝐵 ) )
107 0zd ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 0 ∈ ℤ )
108 107 102 zltp1led ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 0 < ( 𝐶 − 𝐵 ) ↔ ( 0 + 1 ) ≤ ( 𝐶 − 𝐵 ) ) )
109 106 108 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 0 + 1 ) ≤ ( 𝐶 − 𝐵 ) )
110 103 109 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 1 ≤ ( 𝐶 − 𝐵 ) )
111 102 zred ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
112 52 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐶 ∈ ℝ )
113 73 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝑃 ∈ ℝ )
114 9 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐵 ∈ ( 0 ... 𝐴 ) )
115 elfzle1 ⊢ ( 𝐵 ∈ ( 0 ... 𝐴 ) → 0 ≤ 𝐵 )
116 114 115 syl ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 0 ≤ 𝐵 )
117 55 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐵 ∈ ℝ )
118 112 117 subge02d ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 0 ≤ 𝐵 ↔ ( 𝐶 − 𝐵 ) ≤ 𝐶 ) )
119 116 118 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝐶 − 𝐵 ) ≤ 𝐶 )
120 72 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐴 ∈ ℝ )
121 elfzle2 ⊢ ( 𝐶 ∈ ( 0 ... 𝐴 ) → 𝐶 ≤ 𝐴 )
122 10 121 syl ⊢ ( 𝜑 → 𝐶 ≤ 𝐴 )
123 122 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐶 ≤ 𝐴 )
124 5 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐴 < 𝑃 )
125 112 120 113 123 124 lelttrd ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → 𝐶 < 𝑃 )
126 111 112 113 119 125 lelttrd ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝐶 − 𝐵 ) < 𝑃 )
127 102 98 zltlem1d ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( ( 𝐶 − 𝐵 ) < 𝑃 ↔ ( 𝐶 − 𝐵 ) ≤ ( 𝑃 − 1 ) ) )
128 126 127 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝐶 − 𝐵 ) ≤ ( 𝑃 − 1 ) )
129 96 99 102 110 128 elfzd ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝐶 − 𝐵 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
130 fzm1ndvds ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝐶 − 𝐵 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ ( 𝐶 − 𝐵 ) )
131 95 129 130 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ¬ 𝑃 ∥ ( 𝐶 − 𝐵 ) )
132 dvdsnegb ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝐵 − 𝐶 ) ∈ ℤ ) → ( 𝑃 ∥ ( 𝐵 − 𝐶 ) ↔ 𝑃 ∥ - ( 𝐵 − 𝐶 ) ) )
133 97 47 132 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( 𝐵 − 𝐶 ) ↔ 𝑃 ∥ - ( 𝐵 − 𝐶 ) ) )
134 19 17 negsubdi2d ⊢ ( 𝜑 → - ( 𝐵 − 𝐶 ) = ( 𝐶 − 𝐵 ) )
135 134 breq2d ⊢ ( 𝜑 → ( 𝑃 ∥ - ( 𝐵 − 𝐶 ) ↔ 𝑃 ∥ ( 𝐶 − 𝐵 ) ) )
136 133 135 bitrd ⊢ ( 𝜑 → ( 𝑃 ∥ ( 𝐵 − 𝐶 ) ↔ 𝑃 ∥ ( 𝐶 − 𝐵 ) ) )
137 136 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ( 𝑃 ∥ ( 𝐵 − 𝐶 ) ↔ 𝑃 ∥ ( 𝐶 − 𝐵 ) ) )
138 131 137 mtbird ⊢ ( ( 𝜑 ∧ 𝐵 < 𝐶 ) → ¬ 𝑃 ∥ ( 𝐵 − 𝐶 ) )
139 94 138 syl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) ∧ ¬ 𝐶 < 𝐵 ) → ¬ 𝑃 ∥ ( 𝐵 − 𝐶 ) )
140 84 139 pm2.61dan ⊢ ( ( 𝜑 ∧ ¬ 𝐵 = 𝐶 ) → ¬ 𝑃 ∥ ( 𝐵 − 𝐶 ) )
141 140 ex ⊢ ( 𝜑 → ( ¬ 𝐵 = 𝐶 → ¬ 𝑃 ∥ ( 𝐵 − 𝐶 ) ) )
142 141 con4d ⊢ ( 𝜑 → ( 𝑃 ∥ ( 𝐵 − 𝐶 ) → 𝐵 = 𝐶 ) )
143 40 142 impbid ⊢ ( 𝜑 → ( 𝐵 = 𝐶 ↔ 𝑃 ∥ ( 𝐵 − 𝐶 ) ) )
144 1 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
145 crngring ⊢ ( 𝐾 ∈ CRing → 𝐾 ∈ Ring )
146 144 145 syl ⊢ ( 𝜑 → 𝐾 ∈ Ring )
147 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
148 eqid ⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
149 3 147 148 chrdvds ⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝐵 − 𝐶 ) ∈ ℤ ) → ( 𝑃 ∥ ( 𝐵 − 𝐶 ) ↔ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 𝐵 − 𝐶 ) ) = ( 0g ‘ 𝐾 ) ) )
150 146 47 149 syl2anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( 𝐵 − 𝐶 ) ↔ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 𝐵 − 𝐶 ) ) = ( 0g ‘ 𝐾 ) ) )
151 143 150 bitr2d ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 𝐵 − 𝐶 ) ) = ( 0g ‘ 𝐾 ) ↔ 𝐵 = 𝐶 ) )
152 26 151 bitrd ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) ) = ( 0g ‘ 𝐾 ) ↔ 𝐵 = 𝐶 ) )
153 152 bicomd ⊢ ( 𝜑 → ( 𝐵 = 𝐶 ↔ ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) ) = ( 0g ‘ 𝐾 ) ) )
154 147 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
155 rhmghm ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) )
156 154 155 syl ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) )
157 146 156 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) )
158 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
159 158 16 zsubcld ⊢ ( 𝜑 → ( 0 − 𝐶 ) ∈ ℤ )
160 zringbas ⊢ ℤ = ( Base ‘ ℤring )
161 159 160 eleqtrdi ⊢ ( 𝜑 → ( 0 − 𝐶 ) ∈ ( Base ‘ ℤring ) )
162 18 160 eleqtrdi ⊢ ( 𝜑 → 𝐵 ∈ ( Base ‘ ℤring ) )
163 eqid ⊢ ( Base ‘ ℤring ) = ( Base ‘ ℤring )
164 eqid ⊢ ( +g ‘ ℤring ) = ( +g ‘ ℤring )
165 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
166 163 164 165 ghmlin ⊢ ( ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) ∧ ( 0 − 𝐶 ) ∈ ( Base ‘ ℤring ) ∧ 𝐵 ∈ ( Base ‘ ℤring ) ) → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) ) = ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) )
167 157 161 162 166 syl3anc ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) ) = ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) )
168 167 eqeq1d ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( ( 0 − 𝐶 ) ( +g ‘ ℤring ) 𝐵 ) ) = ( 0g ‘ 𝐾 ) ↔ ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) = ( 0g ‘ 𝐾 ) ) )
169 153 168 bitrd ⊢ ( 𝜑 → ( 𝐵 = 𝐶 ↔ ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) = ( 0g ‘ 𝐾 ) ) )
170 eqid ⊢ ( eval1 ‘ 𝐾 ) = ( eval1 ‘ 𝐾 )
171 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
172 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
173 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
174 160 172 ghmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring GrpHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
175 157 174 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
176 175 159 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ∈ ( Base ‘ 𝐾 ) )
177 170 6 172 171 173 144 176 evl1vard ⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑋 ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) )
178 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
179 175 18 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ∈ ( Base ‘ 𝐾 ) )
180 170 171 172 178 173 144 179 176 evl1scad ⊢ ( 𝜑 → ( ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) )
181 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
182 170 171 172 173 144 176 177 180 181 165 evl1addd ⊢ ( 𝜑 → ( ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) = ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) )
183 182 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) = ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) )
184 183 eqcomd ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) )
185 184 eqeq1d ⊢ ( 𝜑 → ( ( ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) = ( 0g ‘ 𝐾 ) ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) = ( 0g ‘ 𝐾 ) ) )
186 169 185 bitrd ⊢ ( 𝜑 → ( 𝐵 = 𝐶 ↔ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑋 ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐵 ) ) ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ ( 0 − 𝐶 ) ) ) = ( 0g ‘ 𝐾 ) ) )