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 42118

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 21483	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
2	1	eqcomi 2744	. . . . . . . . . 10 ⊢ (+_g‘ℤ_ring) = +
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘ℤ_ring) = + )
4	3	oveqd 7448	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = ((0 − 𝐶) + 𝐵))
5		0cnd 11252	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℂ)
6		aks6d1c5p1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (0...𝐴))
7	6	elfzelzd 13562	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ)
8	7	zcnd 12721	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
9		aks6d1c5p1.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (0...𝐴))
10	9	elfzelzd 13562	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ)
11	10	zcnd 12721	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
12	5, 8, 11	subadd23d 11640	. . . . . . . . 9 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (0 + (𝐵 − 𝐶)))
13	11, 8	subcld 11618	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
14	13	addlidd 11460	. . . . . . . . 9 ⊢ (𝜑 → (0 + (𝐵 − 𝐶)) = (𝐵 − 𝐶))
15	12, 14	eqtrd 2775	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (𝐵 − 𝐶))
16	4, 15	eqtrd 2775	. . . . . . 7 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = (𝐵 − 𝐶))
17	16	fveq2d 6911	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)))
18	17	eqeq1d 2737	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
19		aks6d1p5.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℙ)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℙ)
21		prmnn 16708	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
23	22	nnzd 12638	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℤ)
24		dvds0 16306	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0)
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ 0)
26	11	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ)
27	26	subidd 11606	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = 0)
28	27	eqcomd 2741	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐵))
29		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
30	29	oveq2d 7447	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = (𝐵 − 𝐶))
31	28, 30	eqtrd 2775	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐶))
32	25, 31	breqtrd 5174	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ (𝐵 − 𝐶))
33	32	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → 𝑃 ∥ (𝐵 − 𝐶)))
34	19, 21	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
35	34	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
36	35	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℕ)
37		1zzd 12646	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ∈ ℤ)
38	36	nnzd 12638	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℤ)
39	38, 37	zsubcld 12725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝑃 − 1) ∈ ℤ)
40	10, 7	zsubcld 12725	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ)
41	40	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℤ)
42		1e0p1 12773	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
43	42	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 = (0 + 1))
44		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 < 𝐵)
45	7	zred 12720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
46	45	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐶 ∈ ℝ)
47	46	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 ∈ ℝ)
48	10	zred 12720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
49	48	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 ∈ ℝ)
50	49	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 ∈ ℝ)
51	47, 50	posdifd 11848	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐶 < 𝐵 ↔ 0 < (𝐵 − 𝐶)))
52	44, 51	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 < (𝐵 − 𝐶))
53		0zd 12623	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 ∈ ℤ)
54	53, 41	zltp1led 41961	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 < (𝐵 − 𝐶) ↔ (0 + 1) ≤ (𝐵 − 𝐶)))
55	52, 54	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 + 1) ≤ (𝐵 − 𝐶))
56	43, 55	eqbrtrd 5170	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ≤ (𝐵 − 𝐶))
57	41	zred 12720	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℝ)
58	36	nnred 12279	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℝ)
59		elfzle1 13564	. . . . . . . . . . . . . . . . . 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 11853	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 ≤ 𝐶 ↔ (𝐵 − 𝐶) ≤ 𝐵))
64	62, 63	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ 𝐵)
65		aks6d1c5.4	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
66	65	nn0red 12586	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	34	nnred 12279	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
68		elfzle2 13565	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 𝐵 ≤ 𝐴)
69	9, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ≤ 𝐴)
70		aks6d1c5.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 < 𝑃)
71	48, 66, 67, 69, 70	lelttrd 11417	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 < 𝑃)
72	71	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 < 𝑃)
73	72	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 < 𝑃)
74	57, 50, 58, 64, 73	lelttrd 11417	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) < 𝑃)
75	41, 38	zltlem1d 12669	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ((𝐵 − 𝐶) < 𝑃 ↔ (𝐵 − 𝐶) ≤ (𝑃 − 1)))
76	74, 75	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ (𝑃 − 1))
77	37, 39, 41, 56, 76	elfzd 13552	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ (1...(𝑃 − 1)))
78		fzm1ndvds 16356	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ ∧ (𝐵 − 𝐶) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
79	36, 77, 78	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
80		simpll 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → 𝜑)
81		axlttri 11330	. . . . . . . . . . . . . . . . 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 12646	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ∈ ℤ)
92	34	nnzd 12638	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
93	92	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℤ)
94	93, 91	zsubcld 12725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝑃 − 1) ∈ ℤ)
95	7	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℤ)
96	10	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℤ)
97	95, 96	zsubcld 12725	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℤ)
98	42	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 = (0 + 1))
99	48, 45	posdifd 11848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ 0 < (𝐶 − 𝐵)))
100	99	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 < 𝐶 → 0 < (𝐶 − 𝐵)))
101	100	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 < (𝐶 − 𝐵))
102		0zd 12623	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ∈ ℤ)
103	102, 97	zltp1led 41961	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 < (𝐶 − 𝐵) ↔ (0 + 1) ≤ (𝐶 − 𝐵)))
104	101, 103	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 + 1) ≤ (𝐶 − 𝐵))
105	98, 104	eqbrtrd 5170	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ≤ (𝐶 − 𝐵))
106	97	zred 12720	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℝ)
107	45	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℝ)
108	67	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℝ)
109	9	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ (0...𝐴))
110		elfzle1 13564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 0 ≤ 𝐵)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ≤ 𝐵)
112	48	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℝ)
113	107, 112	subge02d 11853	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ 𝐶))
114	111, 113	mpbid 232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ 𝐶)
115	66	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐴 ∈ ℝ)
116		elfzle2 13565	. . . . . . . . . . . . . . . . . . 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 11417	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 < 𝑃)
121	106, 107, 108, 114, 120	lelttrd 11417	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) < 𝑃)
122	97, 93	zltlem1d 12669	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ((𝐶 − 𝐵) < 𝑃 ↔ (𝐶 − 𝐵) ≤ (𝑃 − 1)))
123	121, 122	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ (𝑃 − 1))
124	91, 94, 97, 105, 123	elfzd 13552	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ (1...(𝑃 − 1)))
125		fzm1ndvds 16356	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ (𝐶 − 𝐵) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
126	90, 124, 125	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
127		dvdsnegb 16308	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℤ ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
128	92, 40, 127	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
129	11, 8	negsubdi2d 11634	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -(𝐵 − 𝐶) = (𝐶 − 𝐵))
130	129	breq2d 5160	. . . . . . . . . . . . . 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 20759	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
141		crngring 20263	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Ring)
143		aks6d1c5.3	. . . . . . . 8 ⊢ 𝑃 = (chr‘𝐾)
144		eqid 2735	. . . . . . . 8 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
145		eqid 2735	. . . . . . . 8 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
146	143, 144, 145	chrdvds 21559	. . . . . . 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 21540	. . . . . . 7 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
152		rhmghm 20501	. . . . . . 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 12623	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
156	155, 7	zsubcld 12725	. . . . . 6 ⊢ (𝜑 → (0 − 𝐶) ∈ ℤ)
157		zringbas 21482	. . . . . 6 ⊢ ℤ = (Base‘ℤ_ring)
158	156, 157	eleqtrdi 2849	. . . . 5 ⊢ (𝜑 → (0 − 𝐶) ∈ (Base‘ℤ_ring))
159	10, 157	eleqtrdi 2849	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (Base‘ℤ_ring))
160		eqid 2735	. . . . . 6 ⊢ (Base‘ℤ_ring) = (Base‘ℤ_ring)
161		eqid 2735	. . . . . 6 ⊢ (+_g‘ℤ_ring) = (+_g‘ℤ_ring)
162		eqid 2735	. . . . . 6 ⊢ (+_g‘𝐾) = (+_g‘𝐾)
163	160, 161, 162	ghmlin 19252	. . . . 5 ⊢ (((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) ∧ (0 − 𝐶) ∈ (Base‘ℤ_ring) ∧ 𝐵 ∈ (Base‘ℤ_ring)) → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
164	154, 158, 159, 163	syl3anc 1370	. . . 4 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
165	164	eqeq1d 2737	. . 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 2735	. . . . . 6 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
168		eqid 2735	. . . . . 6 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
169		eqid 2735	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
170		eqid 2735	. . . . . 6 ⊢ (Base‘(Poly₁‘𝐾)) = (Base‘(Poly₁‘𝐾))
171	157, 169	ghmf 19251	. . . . . . . 8 ⊢ ((ℤRHom‘𝐾) ∈ (ℤ_ring GrpHom 𝐾) → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
172	154, 171	syl 17	. . . . . . 7 ⊢ (𝜑 → (ℤRHom‘𝐾):ℤ⟶(Base‘𝐾))
173	172, 156	ffvelcdmd 7105	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘(0 − 𝐶)) ∈ (Base‘𝐾))
174		aks6d1c5.6	. . . . . . 7 ⊢ 𝑋 = (var₁‘𝐾)
175	167, 174, 169, 168, 170, 140, 173	evl1vard 22357	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘𝑋)‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘(0 − 𝐶))))
176		eqid 2735	. . . . . . 7 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
177	172, 10	ffvelcdmd 7105	. . . . . . 7 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐵) ∈ (Base‘𝐾))
178	167, 168, 169, 176, 170, 140, 177, 173	evl1scad 22355	. . . . . 6 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘𝐵)))
179		eqid 2735	. . . . . 6 ⊢ (+_g‘(Poly₁‘𝐾)) = (+_g‘(Poly₁‘𝐾))
180	167, 168, 169, 170, 140, 173, 175, 178, 179, 162	evl1addd 22361	. . . . 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 2741	. . 3 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))))
183	182	eqeq1d 2737	. 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 1537 ∈ wcel 2106 class class class wbr 5148 ↦ cmpt 5231 ⟶wf 6559 ‘cfv 6563 (class class class)co 7431 ↑_m cmap 8865 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 < clt 11293 ≤ cle 11294 − cmin 11490 -cneg 11491 ℕcn 12264 ℕ₀cn0 12524 ℤcz 12611 ...cfz 13544 ∥ cdvds 16287 ℙcprime 16705 Basecbs 17245 +_gcplusg 17298 0_gc0g 17486 Σ_g cgsu 17487 ._gcmg 19098 GrpHom cghm 19243 mulGrpcmgp 20152 Ringcrg 20251 CRingccrg 20252 RingHom crh 20486 Fieldcfield 20747 ℤ_ringczring 21475 ℤRHomczrh 21528 chrcchr 21530 algSccascl 21890 var₁cv1 22193 Poly₁cpl1 22194 eval₁ce1 22334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231 ax-addf 11232 ax-mulf 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-tp 4636 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-iin 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-ofr 7698 df-om 7888 df-1st 8013 df-2nd 8014 df-supp 8185 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-2o 8506 df-er 8744 df-map 8867 df-pm 8868 df-ixp 8937 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-fsupp 9400 df-sup 9480 df-inf 9481 df-oi 9548 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 df-n0 12525 df-z 12612 df-dec 12732 df-uz 12877 df-rp 13033 df-fz 13545 df-fzo 13692 df-fl 13829 df-mod 13907 df-seq 14040 df-exp 14100 df-hash 14367 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-dvds 16288 df-prm 16706 df-struct 17181 df-sets 17198 df-slot 17216 df-ndx 17228 df-base 17246 df-ress 17275 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 17488 df-gsum 17489 df-prds 17494 df-pws 17496 df-mre 17631 df-mrc 17632 df-acs 17634 df-mgm 18666 df-sgrp 18745 df-mnd 18761 df-mhm 18809 df-submnd 18810 df-grp 18967 df-minusg 18968 df-sbg 18969 df-mulg 19099 df-subg 19154 df-ghm 19244 df-cntz 19348 df-od 19561 df-cmn 19815 df-abl 19816 df-mgp 20153 df-rng 20171 df-ur 20200 df-srg 20205 df-ring 20253 df-cring 20254 df-rhm 20489 df-subrng 20563 df-subrg 20587 df-field 20749 df-lmod 20877 df-lss 20948 df-lsp 20988 df-cnfld 21383 df-zring 21476 df-zrh 21532 df-chr 21534 df-assa 21891 df-asp 21892 df-ascl 21893 df-psr 21947 df-mvr 21948 df-mpl 21949 df-opsr 21951 df-evls 22116 df-evl 22117 df-psr1 22197 df-vr1 22198 df-ply1 22199 df-evl1 22336

This theorem is referenced by: aks6d1c5lem2 42120

W3C validator