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 42093

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 21488	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
2	1	eqcomi 2749	. . . . . . . . . 10 ⊢ (+_g‘ℤ_ring) = +
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘ℤ_ring) = + )
4	3	oveqd 7465	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = ((0 − 𝐶) + 𝐵))
5		0cnd 11283	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℂ)
6		aks6d1c5p1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (0...𝐴))
7	6	elfzelzd 13585	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ)
8	7	zcnd 12748	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
9		aks6d1c5p1.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (0...𝐴))
10	9	elfzelzd 13585	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ)
11	10	zcnd 12748	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
12	5, 8, 11	subadd23d 11669	. . . . . . . . 9 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (0 + (𝐵 − 𝐶)))
13	11, 8	subcld 11647	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
14	13	addlidd 11491	. . . . . . . . 9 ⊢ (𝜑 → (0 + (𝐵 − 𝐶)) = (𝐵 − 𝐶))
15	12, 14	eqtrd 2780	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (𝐵 − 𝐶))
16	4, 15	eqtrd 2780	. . . . . . 7 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = (𝐵 − 𝐶))
17	16	fveq2d 6924	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)))
18	17	eqeq1d 2742	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
19		aks6d1p5.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℙ)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℙ)
21		prmnn 16721	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
23	22	nnzd 12666	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℤ)
24		dvds0 16320	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0)
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ 0)
26	11	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ)
27	26	subidd 11635	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = 0)
28	27	eqcomd 2746	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐵))
29		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
30	29	oveq2d 7464	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = (𝐵 − 𝐶))
31	28, 30	eqtrd 2780	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐶))
32	25, 31	breqtrd 5192	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ (𝐵 − 𝐶))
33	32	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → 𝑃 ∥ (𝐵 − 𝐶)))
34	19, 21	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
35	34	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
36	35	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℕ)
37		1zzd 12674	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ∈ ℤ)
38	36	nnzd 12666	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℤ)
39	38, 37	zsubcld 12752	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝑃 − 1) ∈ ℤ)
40	10, 7	zsubcld 12752	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ)
41	40	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℤ)
42		1e0p1 12800	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
43	42	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 = (0 + 1))
44		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 < 𝐵)
45	7	zred 12747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
46	45	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐶 ∈ ℝ)
47	46	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 ∈ ℝ)
48	10	zred 12747	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
49	48	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 ∈ ℝ)
50	49	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 ∈ ℝ)
51	47, 50	posdifd 11877	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐶 < 𝐵 ↔ 0 < (𝐵 − 𝐶)))
52	44, 51	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 < (𝐵 − 𝐶))
53		0zd 12651	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 ∈ ℤ)
54	53, 41	zltp1led 41936	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 < (𝐵 − 𝐶) ↔ (0 + 1) ≤ (𝐵 − 𝐶)))
55	52, 54	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 + 1) ≤ (𝐵 − 𝐶))
56	43, 55	eqbrtrd 5188	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ≤ (𝐵 − 𝐶))
57	41	zred 12747	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℝ)
58	36	nnred 12308	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℝ)
59		elfzle1 13587	. . . . . . . . . . . . . . . . . 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 11882	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 ≤ 𝐶 ↔ (𝐵 − 𝐶) ≤ 𝐵))
64	62, 63	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ 𝐵)
65		aks6d1c5.4	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
66	65	nn0red 12614	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	34	nnred 12308	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
68		elfzle2 13588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 𝐵 ≤ 𝐴)
69	9, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ≤ 𝐴)
70		aks6d1c5.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 < 𝑃)
71	48, 66, 67, 69, 70	lelttrd 11448	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 < 𝑃)
72	71	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 < 𝑃)
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 < 𝑃)
74	57, 50, 58, 64, 73	lelttrd 11448	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) < 𝑃)
75	41, 38	zltlem1d 41935	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ((𝐵 − 𝐶) < 𝑃 ↔ (𝐵 − 𝐶) ≤ (𝑃 − 1)))
76	74, 75	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ (𝑃 − 1))
77	37, 39, 41, 56, 76	elfzd 13575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ (1...(𝑃 − 1)))
78		fzm1ndvds 16370	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ ∧ (𝐵 − 𝐶) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
79	36, 77, 78	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
80		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → 𝜑)
81		axlttri 11361	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
82	48, 45, 81	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
83		ioran 984	. . . . . . . . . . . . . . . . 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 12674	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ∈ ℤ)
92	34	nnzd 12666	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
93	92	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℤ)
94	93, 91	zsubcld 12752	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝑃 − 1) ∈ ℤ)
95	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℤ)
96	10	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℤ)
97	95, 96	zsubcld 12752	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℤ)
98	42	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 = (0 + 1))
99	48, 45	posdifd 11877	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ 0 < (𝐶 − 𝐵)))
100	99	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 < 𝐶 → 0 < (𝐶 − 𝐵)))
101	100	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 < (𝐶 − 𝐵))
102		0zd 12651	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ∈ ℤ)
103	102, 97	zltp1led 41936	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 < (𝐶 − 𝐵) ↔ (0 + 1) ≤ (𝐶 − 𝐵)))
104	101, 103	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 + 1) ≤ (𝐶 − 𝐵))
105	98, 104	eqbrtrd 5188	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ≤ (𝐶 − 𝐵))
106	97	zred 12747	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℝ)
107	45	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℝ)
108	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℝ)
109	9	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ (0...𝐴))
110		elfzle1 13587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 0 ≤ 𝐵)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ≤ 𝐵)
112	48	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℝ)
113	107, 112	subge02d 11882	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ 𝐶))
114	111, 113	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ 𝐶)
115	66	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐴 ∈ ℝ)
116		elfzle2 13588	. . . . . . . . . . . . . . . . . . 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 11448	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 < 𝑃)
121	106, 107, 108, 114, 120	lelttrd 11448	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) < 𝑃)
122	97, 93	zltlem1d 41935	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ((𝐶 − 𝐵) < 𝑃 ↔ (𝐶 − 𝐵) ≤ (𝑃 − 1)))
123	121, 122	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ (𝑃 − 1))
124	91, 94, 97, 105, 123	elfzd 13575	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ (1...(𝑃 − 1)))
125		fzm1ndvds 16370	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ (𝐶 − 𝐵) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
126	90, 124, 125	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
127		dvdsnegb 16322	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℤ ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
128	92, 40, 127	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
129	11, 8	negsubdi2d 11663	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -(𝐵 − 𝐶) = (𝐶 − 𝐵))
130	129	breq2d 5178	. . . . . . . . . . . . . 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 812	. . . . . . . . 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 20764	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
141		crngring 20272	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Ring)
143		aks6d1c5.3	. . . . . . . 8 ⊢ 𝑃 = (chr‘𝐾)
144		eqid 2740	. . . . . . . 8 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
145		eqid 2740	. . . . . . . 8 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
146	143, 144, 145	chrdvds 21564	. . . . . . 7 ⊢ ((𝐾 ∈ Ring ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
147	142, 40, 146	syl2anc 583	. . . . . 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 21545	. . . . . . 7 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
152		rhmghm 20510	. . . . . . 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 12651	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
156	155, 7	zsubcld 12752	. . . . . 6 ⊢ (𝜑 → (0 − 𝐶) ∈ ℤ)
157		zringbas 21487	. . . . . 6 ⊢ ℤ = (Base‘ℤ_ring)
158	156, 157	eleqtrdi 2854	. . . . 5 ⊢ (𝜑 → (0 − 𝐶) ∈ (Base‘ℤ_ring))
159	10, 157	eleqtrdi 2854	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (Base‘ℤ_ring))
160		eqid 2740	. . . . . 6 ⊢ (Base‘ℤ_ring) = (Base‘ℤ_ring)
161		eqid 2740	. . . . . 6 ⊢ (+_g‘ℤ_ring) = (+_g‘ℤ_ring)
162		eqid 2740	. . . . . 6 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
163	160, 161, 162	ghmlin 19261	. . . . 5 ⊢ (((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) ∧ (0 − 𝐶) ∈ (Base‘ℤ_ring) ∧ 𝐵 ∈ (Base‘ℤ_ring)) → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
164	154, 158, 159, 163	syl3anc 1371	. . . 4 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
165	164	eqeq1d 2742	. . 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 2740	. . . . . 6 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
168		eqid 2740	. . . . . 6 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
169		eqid 2740	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
170		eqid 2740	. . . . . 6 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
171	157, 169	ghmf 19260	. . . . . . . 8 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
172	154, 171	syl 17	. . . . . . 7 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
173	172, 156	ffvelcdmd 7119	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘(0 − 𝐶)) ∈ (Base‘𝐾))
174		aks6d1c5.6	. . . . . . 7 ⊢ 𝑋 = (var₁‘𝐾)
175	167, 174, 169, 168, 170, 140, 173	evl1vard 22362	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘𝑋)‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘(0 − 𝐶))))
176		eqid 2740	. . . . . . 7 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
177	172, 10	ffvelcdmd 7119	. . . . . . 7 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐵) ∈ (Base‘𝐾))
178	167, 168, 169, 176, 170, 140, 177, 173	evl1scad 22360	. . . . . 6 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘𝐵)))
179		eqid 2740	. . . . . 6 ⊢ (+_g‘(Poly₁‘𝐾)) = (+_g‘(Poly₁‘𝐾))
180	167, 168, 169, 170, 140, 173, 175, 178, 179, 162	evl1addd 22366	. . . . 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 2746	. . 3 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))))
183	182	eqeq1d 2742	. 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 846 = wceq 1537 ∈ wcel 2108 class class class wbr 5166 ↦ cmpt 5249 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 ↑_m cmap 8884 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 < clt 11324 ≤ cle 11325 − cmin 11520 -cneg 11521 ℕcn 12293 ℕ₀cn0 12553 ℤcz 12639 ...cfz 13567 ∥ cdvds 16302 ℙcprime 16718 Basecbs 17258 +_gcplusg 17311 0_gc0g 17499 Σ_g cgsu 17500 ._gcmg 19107 GrpHom cghm 19252 mulGrpcmgp 20161 Ringcrg 20260 CRingccrg 20261 RingHom crh 20495 Fieldcfield 20752 ℤ_ringczring 21480 ℤRHomczrh 21533 chrcchr 21535 algSccascl 21895 var₁cv1 22198 Poly₁cpl1 22199 eval₁ce1 22339

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262 ax-addf 11263 ax-mulf 11264

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-iin 5018 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-of 7714 df-ofr 7715 df-om 7904 df-1st 8030 df-2nd 8031 df-supp 8202 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-2o 8523 df-er 8763 df-map 8886 df-pm 8887 df-ixp 8956 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-fsupp 9432 df-sup 9511 df-inf 9512 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-5 12359 df-6 12360 df-7 12361 df-8 12362 df-9 12363 df-n0 12554 df-z 12640 df-dec 12759 df-uz 12904 df-rp 13058 df-fz 13568 df-fzo 13712 df-fl 13843 df-mod 13921 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-dvds 16303 df-prm 16719 df-struct 17194 df-sets 17211 df-slot 17229 df-ndx 17241 df-base 17259 df-ress 17288 df-plusg 17324 df-mulr 17325 df-starv 17326 df-sca 17327 df-vsca 17328 df-ip 17329 df-tset 17330 df-ple 17331 df-ds 17333 df-unif 17334 df-hom 17335 df-cco 17336 df-0g 17501 df-gsum 17502 df-prds 17507 df-pws 17509 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18678 df-sgrp 18757 df-mnd 18773 df-mhm 18818 df-submnd 18819 df-grp 18976 df-minusg 18977 df-sbg 18978 df-mulg 19108 df-subg 19163 df-ghm 19253 df-cntz 19357 df-od 19570 df-cmn 19824 df-abl 19825 df-mgp 20162 df-rng 20180 df-ur 20209 df-srg 20214 df-ring 20262 df-cring 20263 df-rhm 20498 df-subrng 20572 df-subrg 20597 df-field 20754 df-lmod 20882 df-lss 20953 df-lsp 20993 df-cnfld 21388 df-zring 21481 df-zrh 21537 df-chr 21539 df-assa 21896 df-asp 21897 df-ascl 21898 df-psr 21952 df-mvr 21953 df-mpl 21954 df-opsr 21956 df-evls 22121 df-evl 22122 df-psr1 22202 df-vr1 22203 df-ply1 22204 df-evl1 22341

This theorem is referenced by: aks6d1c5lem2 42095

W3C validator