aks6d1c5lem1 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > aks6d1c5lem1		Structured version Visualization version GIF version

Theorem aks6d1c5lem1 42506

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

**Hypotheses**
Ref	Expression
aks6d1p5.1	⊢ (𝜑 → 𝐾 ∈ Field)
aks6d1p5.2	⊢ (𝜑 → 𝑃 ∈ ℙ)
aks6d1c5.3	⊢ 𝑃 = (chr‘𝐾)
aks6d1c5.4	⊢ (𝜑 → 𝐴 ∈ ℕ₀)
aks6d1c5.5	⊢ (𝜑 → 𝐴 < 𝑃)
aks6d1c5.6	⊢ 𝑋 = (var₁‘𝐾)
aks6d1c5.7	⊢ ↑ = (._g‘(mulGrp‘(Poly₁‘𝐾)))
aks6d1c5.8	⊢ 𝐺 = (𝑔 ∈ (ℕ₀ ↑_m (0...𝐴)) ↦ ((mulGrp‘(Poly₁‘𝐾)) Σ_g (𝑖 ∈ (0...𝐴) ↦ ((𝑔‘𝑖) ↑ (𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝑖)))))))
aks6d1c5p1.1	⊢ (𝜑 → 𝐵 ∈ (0...𝐴))
aks6d1c5p1.2	⊢ (𝜑 → 𝐶 ∈ (0...𝐴))

**Assertion**
Ref	Expression
aks6d1c5lem1	⊢ (𝜑 → (𝐵 = 𝐶 ↔ (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (0_g‘𝐾)))

**Proof of Theorem aks6d1c5lem1**
Step	Hyp	Ref	Expression
1		zringplusg 21421	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
2	1	eqcomi 2746	. . . . . . . . . 10 ⊢ (+_g‘ℤ_ring) = +
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘ℤ_ring) = + )
4	3	oveqd 7385	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = ((0 − 𝐶) + 𝐵))
5		0cnd 11137	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℂ)
6		aks6d1c5p1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (0...𝐴))
7	6	elfzelzd 13453	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ)
8	7	zcnd 12609	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
9		aks6d1c5p1.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (0...𝐴))
10	9	elfzelzd 13453	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ)
11	10	zcnd 12609	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
12	5, 8, 11	subadd23d 11526	. . . . . . . . 9 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (0 + (𝐵 − 𝐶)))
13	11, 8	subcld 11504	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
14	13	addlidd 11346	. . . . . . . . 9 ⊢ (𝜑 → (0 + (𝐵 − 𝐶)) = (𝐵 − 𝐶))
15	12, 14	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (𝐵 − 𝐶))
16	4, 15	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = (𝐵 − 𝐶))
17	16	fveq2d 6846	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)))
18	17	eqeq1d 2739	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
19		aks6d1p5.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℙ)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℙ)
21		prmnn 16613	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
23	22	nnzd 12526	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℤ)
24		dvds0 16210	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0)
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ 0)
26	11	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ)
27	26	subidd 11492	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = 0)
28	27	eqcomd 2743	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐵))
29		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
30	29	oveq2d 7384	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = (𝐵 − 𝐶))
31	28, 30	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐶))
32	25, 31	breqtrd 5126	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ (𝐵 − 𝐶))
33	32	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → 𝑃 ∥ (𝐵 − 𝐶)))
34	19, 21	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
35	34	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
36	35	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℕ)
37		1zzd 12534	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ∈ ℤ)
38	36	nnzd 12526	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℤ)
39	38, 37	zsubcld 12613	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝑃 − 1) ∈ ℤ)
40	10, 7	zsubcld 12613	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ)
41	40	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℤ)
42		1e0p1 12661	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
43	42	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 = (0 + 1))
44		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 < 𝐵)
45	7	zred 12608	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
46	45	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐶 ∈ ℝ)
47	46	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 ∈ ℝ)
48	10	zred 12608	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
49	48	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 ∈ ℝ)
50	49	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 ∈ ℝ)
51	47, 50	posdifd 11736	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐶 < 𝐵 ↔ 0 < (𝐵 − 𝐶)))
52	44, 51	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 < (𝐵 − 𝐶))
53		0zd 12512	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 ∈ ℤ)
54	53, 41	zltp1led 42349	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 < (𝐵 − 𝐶) ↔ (0 + 1) ≤ (𝐵 − 𝐶)))
55	52, 54	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 + 1) ≤ (𝐵 − 𝐶))
56	43, 55	eqbrtrd 5122	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ≤ (𝐵 − 𝐶))
57	41	zred 12608	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℝ)
58	36	nnred 12172	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℝ)
59		elfzle1 13455	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ (0...𝐴) → 0 ≤ 𝐶)
60	6, 59	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝐶)
61	60	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 0 ≤ 𝐶)
62	61	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 ≤ 𝐶)
63	50, 47	subge02d 11741	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 ≤ 𝐶 ↔ (𝐵 − 𝐶) ≤ 𝐵))
64	62, 63	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ 𝐵)
65		aks6d1c5.4	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
66	65	nn0red 12475	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	34	nnred 12172	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
68		elfzle2 13456	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 𝐵 ≤ 𝐴)
69	9, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ≤ 𝐴)
70		aks6d1c5.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 < 𝑃)
71	48, 66, 67, 69, 70	lelttrd 11303	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 < 𝑃)
72	71	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 < 𝑃)
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 < 𝑃)
74	57, 50, 58, 64, 73	lelttrd 11303	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) < 𝑃)
75	41, 38	zltlem1d 12557	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ((𝐵 − 𝐶) < 𝑃 ↔ (𝐵 − 𝐶) ≤ (𝑃 − 1)))
76	74, 75	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ (𝑃 − 1))
77	37, 39, 41, 56, 76	elfzd 13443	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ (1...(𝑃 − 1)))
78		fzm1ndvds 16261	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ ∧ (𝐵 − 𝐶) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
79	36, 77, 78	syl2anc 585	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
80		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → 𝜑)
81		axlttri 11216	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
82	48, 45, 81	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
83		ioran 986	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵) ↔ (¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵))
84	83	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵) ↔ (¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵)))
85	82, 84	bitr2d 280	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵) ↔ 𝐵 < 𝐶))
86	85	biimpd 229	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵) → 𝐵 < 𝐶))
87	86	imp 406	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵)) → 𝐵 < 𝐶)
88	87	anassrs 467	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → 𝐵 < 𝐶)
89	80, 88	jca 511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → (𝜑 ∧ 𝐵 < 𝐶))
90	34	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℕ)
91		1zzd 12534	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ∈ ℤ)
92	34	nnzd 12526	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
93	92	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℤ)
94	93, 91	zsubcld 12613	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝑃 − 1) ∈ ℤ)
95	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℤ)
96	10	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℤ)
97	95, 96	zsubcld 12613	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℤ)
98	42	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 = (0 + 1))
99	48, 45	posdifd 11736	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ 0 < (𝐶 − 𝐵)))
100	99	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 < 𝐶 → 0 < (𝐶 − 𝐵)))
101	100	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 < (𝐶 − 𝐵))
102		0zd 12512	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ∈ ℤ)
103	102, 97	zltp1led 42349	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 < (𝐶 − 𝐵) ↔ (0 + 1) ≤ (𝐶 − 𝐵)))
104	101, 103	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 + 1) ≤ (𝐶 − 𝐵))
105	98, 104	eqbrtrd 5122	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ≤ (𝐶 − 𝐵))
106	97	zred 12608	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℝ)
107	45	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℝ)
108	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℝ)
109	9	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ (0...𝐴))
110		elfzle1 13455	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 0 ≤ 𝐵)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ≤ 𝐵)
112	48	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℝ)
113	107, 112	subge02d 11741	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ 𝐶))
114	111, 113	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ 𝐶)
115	66	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐴 ∈ ℝ)
116		elfzle2 13456	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ (0...𝐴) → 𝐶 ≤ 𝐴)
117	6, 116	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ≤ 𝐴)
118	117	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ≤ 𝐴)
119	70	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐴 < 𝑃)
120	107, 115, 108, 118, 119	lelttrd 11303	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 < 𝑃)
121	106, 107, 108, 114, 120	lelttrd 11303	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) < 𝑃)
122	97, 93	zltlem1d 12557	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ((𝐶 − 𝐵) < 𝑃 ↔ (𝐶 − 𝐵) ≤ (𝑃 − 1)))
123	121, 122	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ (𝑃 − 1))
124	91, 94, 97, 105, 123	elfzd 13443	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ (1...(𝑃 − 1)))
125		fzm1ndvds 16261	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ (𝐶 − 𝐵) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
126	90, 124, 125	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
127		dvdsnegb 16212	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℤ ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
128	92, 40, 127	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
129	11, 8	negsubdi2d 11520	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -(𝐵 − 𝐶) = (𝐶 − 𝐵))
130	129	breq2d 5112	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 ∥ -(𝐵 − 𝐶) ↔ 𝑃 ∥ (𝐶 − 𝐵)))
131	128, 130	bitrd 279	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ (𝐶 − 𝐵)))
132	131	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ (𝐶 − 𝐵)))
133	126, 132	mtbird 325	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
134	89, 133	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
135	79, 134	pm2.61dan 813	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
136	135	ex 412	. . . . . . . 8 ⊢ (𝜑 → (¬ 𝐵 = 𝐶 → ¬ 𝑃 ∥ (𝐵 − 𝐶)))
137	136	con4d 115	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) → 𝐵 = 𝐶))
138	33, 137	impbid 212	. . . . . 6 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ 𝑃 ∥ (𝐵 − 𝐶)))
139		aks6d1p5.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Field)
140	139	fldcrngd 20687	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
141		crngring 20192	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Ring)
143		aks6d1c5.3	. . . . . . . 8 ⊢ 𝑃 = (chr‘𝐾)
144		eqid 2737	. . . . . . . 8 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
145		eqid 2737	. . . . . . . 8 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
146	143, 144, 145	chrdvds 21493	. . . . . . 7 ⊢ ((𝐾 ∈ Ring ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
147	142, 40, 146	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
148	138, 147	bitr2d 280	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾) ↔ 𝐵 = 𝐶))
149	18, 148	bitrd 279	. . . 4 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ 𝐵 = 𝐶))
150	149	bicomd 223	. . 3 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾)))
151	144	zrhrhm 21478	. . . . . . 7 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
152		rhmghm 20431	. . . . . . 7 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾) → (ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾))
153	151, 152	syl 17	. . . . . 6 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾))
154	142, 153	syl 17	. . . . 5 ⊢ (𝜑 → (ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾))
155		0zd 12512	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
156	155, 7	zsubcld 12613	. . . . . 6 ⊢ (𝜑 → (0 − 𝐶) ∈ ℤ)
157		zringbas 21420	. . . . . 6 ⊢ ℤ = (Base‘ℤ_ring)
158	156, 157	eleqtrdi 2847	. . . . 5 ⊢ (𝜑 → (0 − 𝐶) ∈ (Base‘ℤ_ring))
159	10, 157	eleqtrdi 2847	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (Base‘ℤ_ring))
160		eqid 2737	. . . . . 6 ⊢ (Base‘ℤ_ring) = (Base‘ℤ_ring)
161		eqid 2737	. . . . . 6 ⊢ (+_g‘ℤ_ring) = (+_g‘ℤ_ring)
162		eqid 2737	. . . . . 6 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
163	160, 161, 162	ghmlin 19162	. . . . 5 ⊢ (((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) ∧ (0 − 𝐶) ∈ (Base‘ℤ_ring) ∧ 𝐵 ∈ (Base‘ℤ_ring)) → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
164	154, 158, 159, 163	syl3anc 1374	. . . 4 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
165	164	eqeq1d 2739	. . 3 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (0_g‘𝐾)))
166	150, 165	bitrd 279	. 2 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (0_g‘𝐾)))
167		eqid 2737	. . . . . 6 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
168		eqid 2737	. . . . . 6 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
169		eqid 2737	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
170		eqid 2737	. . . . . 6 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
171	157, 169	ghmf 19161	. . . . . . . 8 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
172	154, 171	syl 17	. . . . . . 7 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
173	172, 156	ffvelcdmd 7039	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘(0 − 𝐶)) ∈ (Base‘𝐾))
174		aks6d1c5.6	. . . . . . 7 ⊢ 𝑋 = (var₁‘𝐾)
175	167, 174, 169, 168, 170, 140, 173	evl1vard 22293	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘𝑋)‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘(0 − 𝐶))))
176		eqid 2737	. . . . . . 7 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
177	172, 10	ffvelcdmd 7039	. . . . . . 7 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐵) ∈ (Base‘𝐾))
178	167, 168, 169, 176, 170, 140, 177, 173	evl1scad 22291	. . . . . 6 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘𝐵)))
179		eqid 2737	. . . . . 6 ⊢ (+_g‘(Poly₁‘𝐾)) = (+_g‘(Poly₁‘𝐾))
180	167, 168, 169, 170, 140, 173, 175, 178, 179, 162	evl1addd 22297	. . . . 5 ⊢ (𝜑 → ((𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵))))
181	180	simprd 495	. . . 4 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
182	181	eqcomd 2743	. . 3 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))))
183	182	eqeq1d 2739	. 2 ⊢ (𝜑 → ((((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (0_g‘𝐾) ↔ (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (0_g‘𝐾)))
184	166, 183	bitrd 279	1 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (0_g‘𝐾)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 class class class wbr 5100 ↦ cmpt 5181 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ↑_m cmap 8775 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 < clt 11178 ≤ cle 11179 − cmin 11376 -cneg 11377 ℕcn 12157 ℕ₀cn0 12413 ℤcz 12500 ...cfz 13435 ∥ cdvds 16191 ℙcprime 16610 Basecbs 17148 +_gcplusg 17189 0_gc0g 17371 Σ_g cgsu 17372 ._gcmg 19009 GrpHom cghm 19153 mulGrpcmgp 20087 Ringcrg 20180 CRingccrg 20181 RingHom crh 20417 Fieldcfield 20675 ℤ_ringczring 21413 ℤRHomczrh 21466 chrcchr 21468 algSccascl 21819 var₁cv1 22128 Poly₁cpl1 22129 eval₁ce1 22270

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117 ax-mulf 11118

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-se 5586 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-isom 6509 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-ofr 7633 df-om 7819 df-1st 7943 df-2nd 7944 df-supp 8113 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-2o 8408 df-er 8645 df-map 8777 df-pm 8778 df-ixp 8848 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-fsupp 9277 df-sup 9357 df-inf 9358 df-oi 9427 df-card 9863 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-div 11807 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-7 12225 df-8 12226 df-9 12227 df-n0 12414 df-z 12501 df-dec 12620 df-uz 12764 df-rp 12918 df-fz 13436 df-fzo 13583 df-fl 13724 df-mod 13802 df-seq 13937 df-exp 13997 df-hash 14266 df-cj 15034 df-re 15035 df-im 15036 df-sqrt 15170 df-abs 15171 df-dvds 16192 df-prm 16611 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-starv 17204 df-sca 17205 df-vsca 17206 df-ip 17207 df-tset 17208 df-ple 17209 df-ds 17211 df-unif 17212 df-hom 17213 df-cco 17214 df-0g 17373 df-gsum 17374 df-prds 17379 df-pws 17381 df-mre 17517 df-mrc 17518 df-acs 17520 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-mhm 18720 df-submnd 18721 df-grp 18878 df-minusg 18879 df-sbg 18880 df-mulg 19010 df-subg 19065 df-ghm 19154 df-cntz 19258 df-od 19469 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-srg 20134 df-ring 20182 df-cring 20183 df-rhm 20420 df-subrng 20491 df-subrg 20515 df-field 20677 df-lmod 20825 df-lss 20895 df-lsp 20935 df-cnfld 21322 df-zring 21414 df-zrh 21470 df-chr 21472 df-assa 21820 df-asp 21821 df-ascl 21822 df-psr 21877 df-mvr 21878 df-mpl 21879 df-opsr 21881 df-evls 22041 df-evl 22042 df-psr1 22132 df-vr1 22133 df-ply1 22134 df-evl1 22272

This theorem is referenced by: aks6d1c5lem2 42508

W3C validator