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 42750

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 21503	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
2	1	eqcomi 2771	. . . . . . . . . 10 ⊢ (+_g‘ℤ_ring) = +
3	2	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (+_g‘ℤ_ring) = + )
4	3	oveqd 7413	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = ((0 − 𝐶) + 𝐵))
5		0cnd 11172	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℂ)
6		aks6d1c5p1.2	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ (0...𝐴))
7	6	elfzelzd 13530	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐶 ∈ ℤ)
8	7	zcnd 12678	. . . . . . . . . 10 ⊢ (𝜑 → 𝐶 ∈ ℂ)
9		aks6d1c5p1.1	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ (0...𝐴))
10	9	elfzelzd 13530	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℤ)
11	10	zcnd 12678	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℂ)
12	5, 8, 11	subadd23d 11564	. . . . . . . . 9 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (0 + (𝐵 − 𝐶)))
13	11, 8	subcld 11542	. . . . . . . . . 10 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℂ)
14	13	addlidd 11384	. . . . . . . . 9 ⊢ (𝜑 → (0 + (𝐵 − 𝐶)) = (𝐵 − 𝐶))
15	12, 14	eqtrd 2797	. . . . . . . 8 ⊢ (𝜑 → ((0 − 𝐶) + 𝐵) = (𝐵 − 𝐶))
16	4, 15	eqtrd 2797	. . . . . . 7 ⊢ (𝜑 → ((0 − 𝐶)(+_g‘ℤ_ring)𝐵) = (𝐵 − 𝐶))
17	16	fveq2d 6871	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)))
18	17	eqeq1d 2764	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
19		aks6d1p5.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℙ)
20	19	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℙ)
21		prmnn 16708	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
22	20, 21	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
23	22	nnzd 12594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∈ ℤ)
24		dvds0 16305	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℤ → 𝑃 ∥ 0)
25	23, 24	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ 0)
26	11	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 ∈ ℂ)
27	26	subidd 11530	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = 0)
28	27	eqcomd 2768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐵))
29		simpr 488	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝐵 = 𝐶)
30	29	oveq2d 7412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → (𝐵 − 𝐵) = (𝐵 − 𝐶))
31	28, 30	eqtrd 2797	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 0 = (𝐵 − 𝐶))
32	25, 31	breqtrd 5126	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐵 = 𝐶) → 𝑃 ∥ (𝐵 − 𝐶))
33	32	ex 416	. . . . . . 7 ⊢ (𝜑 → (𝐵 = 𝐶 → 𝑃 ∥ (𝐵 − 𝐶)))
34	19, 21	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℕ)
35	34	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝑃 ∈ ℕ)
36	35	adantr 484	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℕ)
37		1zzd 12602	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ∈ ℤ)
38	36	nnzd 12594	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℤ)
39	38, 37	zsubcld 12682	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝑃 − 1) ∈ ℤ)
40	10, 7	zsubcld 12682	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ)
41	40	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℤ)
42		1e0p1 12735	. . . . . . . . . . . . . 14 ⊢ 1 = (0 + 1)
43	42	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 = (0 + 1))
44		simpr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 < 𝐵)
45	7	zred 12677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
46	45	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐶 ∈ ℝ)
47	46	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐶 ∈ ℝ)
48	10	zred 12677	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℝ)
49	48	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 ∈ ℝ)
50	49	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 ∈ ℝ)
51	47, 50	posdifd 11774	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐶 < 𝐵 ↔ 0 < (𝐵 − 𝐶)))
52	44, 51	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 < (𝐵 − 𝐶))
53		0zd 12580	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 ∈ ℤ)
54	53, 41	zltp1led 12626	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 < (𝐵 − 𝐶) ↔ (0 + 1) ≤ (𝐵 − 𝐶)))
55	52, 54	mpbid 234	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 + 1) ≤ (𝐵 − 𝐶))
56	43, 55	eqbrtrd 5122	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 1 ≤ (𝐵 − 𝐶))
57	41	zred 12677	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ ℝ)
58	36	nnred 12225	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝑃 ∈ ℝ)
59		elfzle1 13532	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ (0...𝐴) → 0 ≤ 𝐶)
60	6, 59	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝐶)
61	60	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 0 ≤ 𝐶)
62	61	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 0 ≤ 𝐶)
63	50, 47	subge02d 11779	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (0 ≤ 𝐶 ↔ (𝐵 − 𝐶) ≤ 𝐵))
64	62, 63	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ 𝐵)
65		aks6d1c5.4	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 ∈ ℕ₀)
66	65	nn0red 12543	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	34	nnred 12225	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑃 ∈ ℝ)
68		elfzle2 13533	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 𝐵 ≤ 𝐴)
69	9, 68	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ≤ 𝐴)
70		aks6d1c5.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 < 𝑃)
71	48, 66, 67, 69, 70	lelttrd 11341	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐵 < 𝑃)
72	71	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → 𝐵 < 𝑃)
73	72	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → 𝐵 < 𝑃)
74	57, 50, 58, 64, 73	lelttrd 11341	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) < 𝑃)
75	41, 38	zltlem1d 12625	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ((𝐵 − 𝐶) < 𝑃 ↔ (𝐵 − 𝐶) ≤ (𝑃 − 1)))
76	74, 75	mpbid 234	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ≤ (𝑃 − 1))
77	37, 39, 41, 56, 76	elfzd 13520	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → (𝐵 − 𝐶) ∈ (1...(𝑃 − 1)))
78		fzm1ndvds 16356	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℕ ∧ (𝐵 − 𝐶) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
79	36, 77, 78	syl2anc 593	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ 𝐶 < 𝐵) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
80		simpll 776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → 𝜑)
81		axlttri 11254	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
82	48, 45, 81	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵)))
83		ioran 997	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵) ↔ (¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵))
84	83	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (¬ (𝐵 = 𝐶 ∨ 𝐶 < 𝐵) ↔ (¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵)))
85	82, 84	bitr2d 282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵) ↔ 𝐵 < 𝐶))
86	85	biimpd 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵) → 𝐵 < 𝐶))
87	86	imp 410	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (¬ 𝐵 = 𝐶 ∧ ¬ 𝐶 < 𝐵)) → 𝐵 < 𝐶)
88	87	anassrs 471	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → 𝐵 < 𝐶)
89	80, 88	jca 519	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → (𝜑 ∧ 𝐵 < 𝐶))
90	34	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℕ)
91		1zzd 12602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ∈ ℤ)
92	34	nnzd 12594	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑃 ∈ ℤ)
93	92	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℤ)
94	93, 91	zsubcld 12682	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝑃 − 1) ∈ ℤ)
95	7	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℤ)
96	10	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℤ)
97	95, 96	zsubcld 12682	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℤ)
98	42	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 = (0 + 1))
99	48, 45	posdifd 11774	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵 < 𝐶 ↔ 0 < (𝐶 − 𝐵)))
100	99	biimpd 231	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵 < 𝐶 → 0 < (𝐶 − 𝐵)))
101	100	imp 410	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 < (𝐶 − 𝐵))
102		0zd 12580	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ∈ ℤ)
103	102, 97	zltp1led 12626	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 < (𝐶 − 𝐵) ↔ (0 + 1) ≤ (𝐶 − 𝐵)))
104	101, 103	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 + 1) ≤ (𝐶 − 𝐵))
105	98, 104	eqbrtrd 5122	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 1 ≤ (𝐶 − 𝐵))
106	97	zred 12677	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ ℝ)
107	45	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ∈ ℝ)
108	67	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝑃 ∈ ℝ)
109	9	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ (0...𝐴))
110		elfzle1 13532	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (0...𝐴) → 0 ≤ 𝐵)
111	109, 110	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 0 ≤ 𝐵)
112	48	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐵 ∈ ℝ)
113	107, 112	subge02d 11779	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (0 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ 𝐶))
114	111, 113	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ 𝐶)
115	66	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐴 ∈ ℝ)
116		elfzle2 13533	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 ∈ (0...𝐴) → 𝐶 ≤ 𝐴)
117	6, 116	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ≤ 𝐴)
118	117	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 ≤ 𝐴)
119	70	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐴 < 𝑃)
120	107, 115, 108, 118, 119	lelttrd 11341	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → 𝐶 < 𝑃)
121	106, 107, 108, 114, 120	lelttrd 11341	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) < 𝑃)
122	97, 93	zltlem1d 12625	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ((𝐶 − 𝐵) < 𝑃 ↔ (𝐶 − 𝐵) ≤ (𝑃 − 1)))
123	121, 122	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ≤ (𝑃 − 1))
124	91, 94, 97, 105, 123	elfzd 13520	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝐶 − 𝐵) ∈ (1...(𝑃 − 1)))
125		fzm1ndvds 16356	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ (𝐶 − 𝐵) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
126	90, 124, 125	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ¬ 𝑃 ∥ (𝐶 − 𝐵))
127		dvdsnegb 16307	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℤ ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
128	92, 40, 127	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ -(𝐵 − 𝐶)))
129	11, 8	negsubdi2d 11558	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → -(𝐵 − 𝐶) = (𝐶 − 𝐵))
130	129	breq2d 5112	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑃 ∥ -(𝐵 − 𝐶) ↔ 𝑃 ∥ (𝐶 − 𝐵)))
131	128, 130	bitrd 281	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ (𝐶 − 𝐵)))
132	131	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → (𝑃 ∥ (𝐵 − 𝐶) ↔ 𝑃 ∥ (𝐶 − 𝐵)))
133	126, 132	mtbird 327	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐵 < 𝐶) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
134	89, 133	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 𝐵 = 𝐶) ∧ ¬ 𝐶 < 𝐵) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
135	79, 134	pm2.61dan 822	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 𝐵 = 𝐶) → ¬ 𝑃 ∥ (𝐵 − 𝐶))
136	135	ex 416	. . . . . . . 8 ⊢ (𝜑 → (¬ 𝐵 = 𝐶 → ¬ 𝑃 ∥ (𝐵 − 𝐶)))
137	136	con4d 115	. . . . . . 7 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) → 𝐵 = 𝐶))
138	33, 137	impbid 214	. . . . . 6 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ 𝑃 ∥ (𝐵 − 𝐶)))
139		aks6d1p5.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ Field)
140	139	fldcrngd 20788	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ CRing)
141		crngring 20291	. . . . . . . 8 ⊢ (𝐾 ∈ CRing → 𝐾 ∈ Ring)
142	140, 141	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ Ring)
143		aks6d1c5.3	. . . . . . . 8 ⊢ 𝑃 = (chr‘𝐾)
144		eqid 2762	. . . . . . . 8 ⊢ (ℤRHom‘𝐾) = (ℤRHom‘𝐾)
145		eqid 2762	. . . . . . . 8 ⊢ (0_g‘𝐾) = (0_g‘𝐾)
146	143, 144, 145	chrdvds 21575	. . . . . . 7 ⊢ ((𝐾 ∈ Ring ∧ (𝐵 − 𝐶) ∈ ℤ) → (𝑃 ∥ (𝐵 − 𝐶) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
147	142, 40, 146	syl2anc 593	. . . . . 6 ⊢ (𝜑 → (𝑃 ∥ (𝐵 − 𝐶) ↔ ((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾)))
148	138, 147	bitr2d 282	. . . . 5 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘(𝐵 − 𝐶)) = (0_g‘𝐾) ↔ 𝐵 = 𝐶))
149	18, 148	bitrd 281	. . . 4 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ 𝐵 = 𝐶))
150	149	bicomd 225	. . 3 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾)))
151	144	zrhrhm 21560	. . . . . . 7 ⊢ (𝐾 ∈ Ring → (ℤRHom‘𝐾) ∈ (ℤ_ring RingHom 𝐾))
152		rhmghm 20528	. . . . . . 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 12580	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
156	155, 7	zsubcld 12682	. . . . . 6 ⊢ (𝜑 → (0 − 𝐶) ∈ ℤ)
157		zringbas 21502	. . . . . 6 ⊢ ℤ = (Base‘ℤ_ring)
158	156, 157	eleqtrdi 2872	. . . . 5 ⊢ (𝜑 → (0 − 𝐶) ∈ (Base‘ℤ_ring))
159	10, 157	eleqtrdi 2872	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (Base‘ℤ_ring))
160		eqid 2762	. . . . . 6 ⊢ (Base‘ℤ_ring) = (Base‘ℤ_ring)
161		eqid 2762	. . . . . 6 ⊢ (+_g‘ℤ_ring) = (+_g‘ℤ_ring)
162		eqid 2762	. . . . . 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 1390	. . . 4 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
165	164	eqeq1d 2764	. . 3 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘((0 − 𝐶)(+_g‘ℤ_ring)𝐵)) = (0_g‘𝐾) ↔ (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (0_g‘𝐾)))
166	150, 165	bitrd 281	. 2 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (0_g‘𝐾)))
167		eqid 2762	. . . . . 6 ⊢ (eval₁‘𝐾) = (eval₁‘𝐾)
168		eqid 2762	. . . . . 6 ⊢ (Poly₁‘𝐾) = (Poly₁‘𝐾)
169		eqid 2762	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
170		eqid 2762	. . . . . 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 7066	. . . . . 6 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘(0 − 𝐶)) ∈ (Base‘𝐾))
174		aks6d1c5.6	. . . . . . 7 ⊢ 𝑋 = (var₁‘𝐾)
175	167, 174, 169, 168, 170, 140, 173	evl1vard 22397	. . . . . 6 ⊢ (𝜑 → (𝑋 ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘𝑋)‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘(0 − 𝐶))))
176		eqid 2762	. . . . . . 7 ⊢ (algSc‘(Poly₁‘𝐾)) = (algSc‘(Poly₁‘𝐾))
177	172, 10	ffvelcdmd 7066	. . . . . . 7 ⊢ (𝜑 → ((ℤRHom‘𝐾)‘𝐵) ∈ (Base‘𝐾))
178	167, 168, 169, 176, 170, 140, 177, 173	evl1scad 22395	. . . . . 6 ⊢ (𝜑 → (((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵)))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = ((ℤRHom‘𝐾)‘𝐵)))
179		eqid 2762	. . . . . 6 ⊢ (+_g‘(Poly₁‘𝐾)) = (+_g‘(Poly₁‘𝐾))
180	167, 168, 169, 170, 140, 173, 175, 178, 179, 162	evl1addd 22401	. . . . 5 ⊢ (𝜑 → ((𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))) ∈ (Base‘(Poly₁‘𝐾)) ∧ (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵))))
181	180	simprd 499	. . . 4 ⊢ (𝜑 → (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)))
182	181	eqcomd 2768	. . 3 ⊢ (𝜑 → (((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))))
183	182	eqeq1d 2764	. 2 ⊢ (𝜑 → ((((ℤRHom‘𝐾)‘(0 − 𝐶))(+_g‘𝐾)((ℤRHom‘𝐾)‘𝐵)) = (0_g‘𝐾) ↔ (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (0_g‘𝐾)))
184	166, 183	bitrd 281	1 ⊢ (𝜑 → (𝐵 = 𝐶 ↔ (((eval₁‘𝐾)‘(𝑋(+_g‘(Poly₁‘𝐾))((algSc‘(Poly₁‘𝐾))‘((ℤRHom‘𝐾)‘𝐵))))‘((ℤRHom‘𝐾)‘(0 − 𝐶))) = (0_g‘𝐾)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1560 ∈ wcel 2142 class class class wbr 5100 ↦ cmpt 5181 ⟶wf 6517 ‘cfv 6521 (class class class)co 7396 ↑_m cmap 8808 ℂcc 11071 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 < clt 11216 ≤ cle 11217 − cmin 11414 -cneg 11415 ℕcn 12210 ℕ₀cn0 12481 ℤcz 12568 ...cfz 13512 ∥ cdvds 16286 ℙcprime 16705 Basecbs 17245 +_gcplusg 17286 0_gc0g 17468 Σ_g cgsu 17469 ._gcmg 19109 GrpHom cghm 19253 mulGrpcmgp 20186 Ringcrg 20279 CRingccrg 20280 RingHom crh 20514 Fieldcfield 20776 ℤ_ringczring 21495 ℤRHomczrh 21548 chrcchr 21550 algSccascl 21901 var₁cv1 22235 Poly₁cpl1 22236 eval₁ce1 22374

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151 ax-addf 11152 ax-mulf 11153

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-iin 4952 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-se 5601 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-isom 6530 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-of 7660 df-ofr 7661 df-om 7847 df-1st 7970 df-2nd 7971 df-supp 8141 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-er 8678 df-map 8810 df-pm 8811 df-ixp 8880 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-fsupp 9308 df-sup 9388 df-inf 9389 df-oi 9458 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-4 12282 df-5 12283 df-6 12284 df-7 12285 df-8 12286 df-9 12287 df-n0 12482 df-z 12569 df-dec 12689 df-uz 12840 df-rp 12994 df-fz 13513 df-fzo 13660 df-fl 13802 df-mod 13880 df-seq 14015 df-exp 14075 df-hash 14344 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-dvds 16287 df-prm 16706 df-struct 17183 df-sets 17200 df-slot 17218 df-ndx 17230 df-base 17246 df-ress 17267 df-plusg 17299 df-mulr 17300 df-starv 17301 df-sca 17302 df-vsca 17303 df-ip 17304 df-tset 17305 df-ple 17306 df-ds 17308 df-unif 17309 df-hom 17310 df-cco 17311 df-0g 17470 df-gsum 17471 df-prds 17476 df-pws 17478 df-mre 17614 df-mrc 17615 df-acs 17617 df-mgm 18674 df-sgrp 18753 df-mnd 18769 df-mhm 18817 df-submnd 18818 df-grp 18978 df-minusg 18979 df-sbg 18980 df-mulg 19110 df-subg 19165 df-ghm 19254 df-cntz 19357 df-od 19568 df-cmn 19822 df-abl 19823 df-mgp 20187 df-rng 20199 df-ur 20228 df-srg 20233 df-ring 20281 df-cring 20282 df-rhm 20517 df-subrng 20592 df-subrg 20616 df-field 20778 df-lmod 20926 df-lss 20996 df-lsp 21036 df-cnfld 21422 df-zring 21496 df-zrh 21552 df-chr 21554 df-assa 21902 df-asp 21903 df-ascl 21904 df-psr 21958 df-mvr 21959 df-mpl 21960 df-opsr 21962 df-evls 22124 df-evl 22125 df-psr1 22239 df-vr1 22240 df-ply1 22241 df-evl1 22376

This theorem is referenced by: aks6d1c5lem2 42752

W3C validator