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 42138

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 21466	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
2	1	eqcomi 2745	. . . . . . . . . 10 ⊢ (+_g‘ℤ_ring) = +
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘ℤ_ring) = + )
4	3	oveqd 7449	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = ((0 − 𝐶) + 𝐵))
5		0cnd 11255	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℂ)
6		aks6d1c5p1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (0...𝐴))
7	6	elfzelzd 13566	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ)
8	7	zcnd 12725	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
9		aks6d1c5p1.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (0...𝐴))
10	9	elfzelzd 13566	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ)
11	10	zcnd 12725	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
12	5, 8, 11	subadd23d 11643	. . . . . . . . 9 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (0 + (𝐵 − 𝐶)))
13	11, 8	subcld 11621	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
14	13	addlidd 11463	. . . . . . . . 9 ⊢ (𝜑 → (0 + (𝐵 − 𝐶)) = (𝐵 − 𝐶))
15	12, 14	eqtrd 2776	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (𝐵 − 𝐶))
16	4, 15	eqtrd 2776	. . . . . . 7 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = (𝐵 − 𝐶))
17	16	fveq2d 6909	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)))
18	17	eqeq1d 2738	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
19		aks6d1p5.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℙ)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℙ)
21		prmnn 16712	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
23	22	nnzd 12642	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℤ)
24		dvds0 16310	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0)
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ 0)
26	11	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ)
27	26	subidd 11609	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = 0)
28	27	eqcomd 2742	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐵))
29		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
30	29	oveq2d 7448	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = (𝐵 − 𝐶))
31	28, 30	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐶))
32	25, 31	breqtrd 5168	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ (𝐵 − 𝐶))
33	32	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → 𝑃 ∥ (𝐵 − 𝐶)))
34	19, 21	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
35	34	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
36	35	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℕ)
37		1zzd 12650	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ∈ ℤ)
38	36	nnzd 12642	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℤ)
39	38, 37	zsubcld 12729	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝑃 − 1) ∈ ℤ)
40	10, 7	zsubcld 12729	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ)
41	40	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℤ)
42		1e0p1 12777	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
43	42	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 = (0 + 1))
44		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 < 𝐵)
45	7	zred 12724	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
46	45	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐶 ∈ ℝ)
47	46	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 ∈ ℝ)
48	10	zred 12724	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
49	48	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 ∈ ℝ)
50	49	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 ∈ ℝ)
51	47, 50	posdifd 11851	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐶 < 𝐵 ↔ 0 < (𝐵 − 𝐶)))
52	44, 51	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 < (𝐵 − 𝐶))
53		0zd 12627	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 ∈ ℤ)
54	53, 41	zltp1led 41981	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 < (𝐵 − 𝐶) ↔ (0 + 1) ≤ (𝐵 − 𝐶)))
55	52, 54	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 + 1) ≤ (𝐵 − 𝐶))
56	43, 55	eqbrtrd 5164	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ≤ (𝐵 − 𝐶))
57	41	zred 12724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℝ)
58	36	nnred 12282	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℝ)
59		elfzle1 13568	. . . . . . . . . . . . . . . . . 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 11856	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 ≤ 𝐶 ↔ (𝐵 − 𝐶) ≤ 𝐵))
64	62, 63	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ 𝐵)
65		aks6d1c5.4	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
66	65	nn0red 12590	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	34	nnred 12282	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
68		elfzle2 13569	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 𝐵 ≤ 𝐴)
69	9, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ≤ 𝐴)
70		aks6d1c5.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 < 𝑃)
71	48, 66, 67, 69, 70	lelttrd 11420	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 < 𝑃)
72	71	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 < 𝑃)
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 < 𝑃)
74	57, 50, 58, 64, 73	lelttrd 11420	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) < 𝑃)
75	41, 38	zltlem1d 12673	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ((𝐵 − 𝐶) < 𝑃 ↔ (𝐵 − 𝐶) ≤ (𝑃 − 1)))
76	74, 75	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ (𝑃 − 1))
77	37, 39, 41, 56, 76	elfzd 13556	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ (1...(𝑃 − 1)))
78		fzm1ndvds 16360	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ ∧ (𝐵 − 𝐶) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
79	36, 77, 78	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
80		simpll 766	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → 𝜑)
81		axlttri 11333	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
82	48, 45, 81	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
83		ioran 985	. . . . . . . . . . . . . . . . 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 12650	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ∈ ℤ)
92	34	nnzd 12642	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
93	92	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℤ)
94	93, 91	zsubcld 12729	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝑃 − 1) ∈ ℤ)
95	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℤ)
96	10	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℤ)
97	95, 96	zsubcld 12729	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℤ)
98	42	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 = (0 + 1))
99	48, 45	posdifd 11851	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ 0 < (𝐶 − 𝐵)))
100	99	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 < 𝐶 → 0 < (𝐶 − 𝐵)))
101	100	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 < (𝐶 − 𝐵))
102		0zd 12627	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ∈ ℤ)
103	102, 97	zltp1led 41981	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 < (𝐶 − 𝐵) ↔ (0 + 1) ≤ (𝐶 − 𝐵)))
104	101, 103	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 + 1) ≤ (𝐶 − 𝐵))
105	98, 104	eqbrtrd 5164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ≤ (𝐶 − 𝐵))
106	97	zred 12724	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℝ)
107	45	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℝ)
108	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℝ)
109	9	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ (0...𝐴))
110		elfzle1 13568	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 0 ≤ 𝐵)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ≤ 𝐵)
112	48	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℝ)
113	107, 112	subge02d 11856	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ 𝐶))
114	111, 113	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ 𝐶)
115	66	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐴 ∈ ℝ)
116		elfzle2 13569	. . . . . . . . . . . . . . . . . . 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 11420	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 < 𝑃)
121	106, 107, 108, 114, 120	lelttrd 11420	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) < 𝑃)
122	97, 93	zltlem1d 12673	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ((𝐶 − 𝐵) < 𝑃 ↔ (𝐶 − 𝐵) ≤ (𝑃 − 1)))
123	121, 122	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ (𝑃 − 1))
124	91, 94, 97, 105, 123	elfzd 13556	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ (1...(𝑃 − 1)))
125		fzm1ndvds 16360	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ (𝐶 − 𝐵) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
126	90, 124, 125	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
127		dvdsnegb 16312	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℤ ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
128	92, 40, 127	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
129	11, 8	negsubdi2d 11637	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -(𝐵 − 𝐶) = (𝐶 − 𝐵))
130	129	breq2d 5154	. . . . . . . . . . . . . 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 20743	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
141		crngring 20243	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Ring)
143		aks6d1c5.3	. . . . . . . 8 ⊢ 𝑃 = (chr‘𝐾)
144		eqid 2736	. . . . . . . 8 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
145		eqid 2736	. . . . . . . 8 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
146	143, 144, 145	chrdvds 21542	. . . . . . 7 ⊢ ((𝐾 ∈ Ring ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
147	142, 40, 146	syl2anc 584	. . . . . 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 21523	. . . . . . 7 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
152		rhmghm 20485	. . . . . . 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 12627	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
156	155, 7	zsubcld 12729	. . . . . 6 ⊢ (𝜑 → (0 − 𝐶) ∈ ℤ)
157		zringbas 21465	. . . . . 6 ⊢ ℤ = (Base‘ℤ_ring)
158	156, 157	eleqtrdi 2850	. . . . 5 ⊢ (𝜑 → (0 − 𝐶) ∈ (Base‘ℤ_ring))
159	10, 157	eleqtrdi 2850	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (Base‘ℤ_ring))
160		eqid 2736	. . . . . 6 ⊢ (Base‘ℤ_ring) = (Base‘ℤ_ring)
161		eqid 2736	. . . . . 6 ⊢ (+_g‘ℤ_ring) = (+_g‘ℤ_ring)
162		eqid 2736	. . . . . 6 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
163	160, 161, 162	ghmlin 19240	. . . . 5 ⊢ (((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) ∧ (0 − 𝐶) ∈ (Base‘ℤ_ring) ∧ 𝐵 ∈ (Base‘ℤ_ring)) → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
164	154, 158, 159, 163	syl3anc 1372	. . . 4 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
165	164	eqeq1d 2738	. . 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 2736	. . . . . 6 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
168		eqid 2736	. . . . . 6 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
169		eqid 2736	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
170		eqid 2736	. . . . . 6 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
171	157, 169	ghmf 19239	. . . . . . . 8 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
172	154, 171	syl 17	. . . . . . 7 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
173	172, 156	ffvelcdmd 7104	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘(0 − 𝐶)) ∈ (Base‘𝐾))
174		aks6d1c5.6	. . . . . . 7 ⊢ 𝑋 = (var₁‘𝐾)
175	167, 174, 169, 168, 170, 140, 173	evl1vard 22342	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘𝑋)‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘(0 − 𝐶))))
176		eqid 2736	. . . . . . 7 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
177	172, 10	ffvelcdmd 7104	. . . . . . 7 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐵) ∈ (Base‘𝐾))
178	167, 168, 169, 176, 170, 140, 177, 173	evl1scad 22340	. . . . . 6 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘𝐵)))
179		eqid 2736	. . . . . 6 ⊢ (+_g‘(Poly₁‘𝐾)) = (+_g‘(Poly₁‘𝐾))
180	167, 168, 169, 170, 140, 173, 175, 178, 179, 162	evl1addd 22346	. . . . 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 2742	. . 3 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))))
183	182	eqeq1d 2738	. 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 847 = wceq 1539 ∈ wcel 2107 class class class wbr 5142 ↦ cmpt 5224 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 ↑_m cmap 8867 ℂcc 11154 ℝcr 11155 0cc0 11156 1c1 11157 + caddc 11159 < clt 11296 ≤ cle 11297 − cmin 11493 -cneg 11494 ℕcn 12267 ℕ₀cn0 12528 ℤcz 12615 ...cfz 13548 ∥ cdvds 16291 ℙcprime 16709 Basecbs 17248 +_gcplusg 17298 0_gc0g 17485 Σ_g cgsu 17486 ._gcmg 19086 GrpHom cghm 19231 mulGrpcmgp 20138 Ringcrg 20231 CRingccrg 20232 RingHom crh 20470 Fieldcfield 20731 ℤ_ringczring 21458 ℤRHomczrh 21511 chrcchr 21513 algSccascl 21873 var₁cv1 22178 Poly₁cpl1 22179 eval₁ce1 22319

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234 ax-addf 11235 ax-mulf 11236

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-iin 4993 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-of 7698 df-ofr 7699 df-om 7889 df-1st 8015 df-2nd 8016 df-supp 8187 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-er 8746 df-map 8869 df-pm 8870 df-ixp 8939 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-fsupp 9403 df-sup 9483 df-inf 9484 df-oi 9551 df-card 9980 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12529 df-z 12616 df-dec 12736 df-uz 12880 df-rp 13036 df-fz 13549 df-fzo 13696 df-fl 13833 df-mod 13911 df-seq 14044 df-exp 14104 df-hash 14371 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-dvds 16292 df-prm 16710 df-struct 17185 df-sets 17202 df-slot 17220 df-ndx 17232 df-base 17249 df-ress 17276 df-plusg 17311 df-mulr 17312 df-starv 17313 df-sca 17314 df-vsca 17315 df-ip 17316 df-tset 17317 df-ple 17318 df-ds 17320 df-unif 17321 df-hom 17322 df-cco 17323 df-0g 17487 df-gsum 17488 df-prds 17493 df-pws 17495 df-mre 17630 df-mrc 17631 df-acs 17633 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-mhm 18797 df-submnd 18798 df-grp 18955 df-minusg 18956 df-sbg 18957 df-mulg 19087 df-subg 19142 df-ghm 19232 df-cntz 19336 df-od 19547 df-cmn 19801 df-abl 19802 df-mgp 20139 df-rng 20151 df-ur 20180 df-srg 20185 df-ring 20233 df-cring 20234 df-rhm 20473 df-subrng 20547 df-subrg 20571 df-field 20733 df-lmod 20861 df-lss 20931 df-lsp 20971 df-cnfld 21366 df-zring 21459 df-zrh 21515 df-chr 21517 df-assa 21874 df-asp 21875 df-ascl 21876 df-psr 21930 df-mvr 21931 df-mpl 21932 df-opsr 21934 df-evls 22099 df-evl 22100 df-psr1 22182 df-vr1 22183 df-ply1 22184 df-evl1 22321

This theorem is referenced by: aks6d1c5lem2 42140

W3C validator