elqaalem2

Description: Lemma for elqaa . (Contributed by Mario Carneiro, 23-Jul-2014) (Revised by AV, 3-Oct-2020)

	Ref	Expression
Hypotheses	elqaa.1	$⊢ φ \to A \in ℂ$
	elqaa.2	$⊢ φ \to F \in (Poly (ℚ) ∖ \{0_{𝑝}\})$
	elqaa.3	$⊢ φ \to F (A) = 0$
	elqaa.4	$⊢ B = coeff (F)$
	elqaa.5	$⊢ N = (k \in ℕ_{0} ⟼ inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <))$
	elqaa.6	$⊢ R = seq 0 (\times N) (\deg (F))$
	elqaa.7	$⊢ P = (x \in V, y \in V ⟼ x y \mod N (K))$
Assertion	elqaalem2	$⊢ (φ \land K \in (0 \dots \deg (F))) \to R \mod N (K) = 0$

Proof

Step	Hyp	Ref	Expression
1		elqaa.1	$⊢ φ \to A \in ℂ$
2		elqaa.2	$⊢ φ \to F \in (Poly (ℚ) ∖ \{0_{𝑝}\})$
3		elqaa.3	$⊢ φ \to F (A) = 0$
4		elqaa.4	$⊢ B = coeff (F)$
5		elqaa.5	$⊢ N = (k \in ℕ_{0} ⟼ inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <))$
6		elqaa.6	$⊢ R = seq 0 (\times N) (\deg (F))$
7		elqaa.7	$⊢ P = (x \in V, y \in V ⟼ x y \mod N (K))$
8		elfznn0	$⊢ K \in (0 \dots \deg (F)) \to K \in ℕ_{0}$
9	6	fveq2i	$⊢ (k \in ℕ ⟼ k \mod N (K)) (R) = (k \in ℕ ⟼ k \mod N (K)) (seq 0 (\times N) (\deg (F)))$
10		nnmulcl	$⊢ (i \in ℕ \land j \in ℕ) \to i j \in ℕ$
11	10	adantl	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to i j \in ℕ$
12		elfznn0	$⊢ i \in (0 \dots \deg (F)) \to i \in ℕ_{0}$
13	1 2 3 4 5 6	elqaalem1	$⊢ (φ \land i \in ℕ_{0}) \to (N (i) \in ℕ \land B (i) N (i) \in ℤ)$
14	13	simpld	$⊢ (φ \land i \in ℕ_{0}) \to N (i) \in ℕ$
15	14	adantlr	$⊢ ((φ \land K \in ℕ_{0}) \land i \in ℕ_{0}) \to N (i) \in ℕ$
16	12 15	sylan2	$⊢ ((φ \land K \in ℕ_{0}) \land i \in (0 \dots \deg (F))) \to N (i) \in ℕ$
17		eldifi	$⊢ F \in (Poly (ℚ) ∖ \{0_{𝑝}\}) \to F \in Poly (ℚ)$
18		dgrcl	$⊢ F \in Poly (ℚ) \to \deg (F) \in ℕ_{0}$
19	2 17 18	3syl	$⊢ φ \to \deg (F) \in ℕ_{0}$
20		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
21	19 20	eleqtrdi	$⊢ φ \to \deg (F) \in ℤ_{\geq 0}$
22	21	adantr	$⊢ (φ \land K \in ℕ_{0}) \to \deg (F) \in ℤ_{\geq 0}$
23		nnz	$⊢ i \in ℕ \to i \in ℤ$
24	23	ad2antrl	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to i \in ℤ$
25	1 2 3 4 5 6	elqaalem1	$⊢ (φ \land K \in ℕ_{0}) \to (N (K) \in ℕ \land B (K) N (K) \in ℤ)$
26	25	simpld	$⊢ (φ \land K \in ℕ_{0}) \to N (K) \in ℕ$
27	26	adantr	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to N (K) \in ℕ$
28	24 27	zmodcld	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to i \mod N (K) \in ℕ_{0}$
29	28	nn0zd	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to i \mod N (K) \in ℤ$
30		nnz	$⊢ j \in ℕ \to j \in ℤ$
31	30	ad2antll	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to j \in ℤ$
32	31 27	zmodcld	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to j \mod N (K) \in ℕ_{0}$
33	32	nn0zd	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to j \mod N (K) \in ℤ$
34	27	nnrpd	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to N (K) \in ℝ^{+}$
35		nnre	$⊢ i \in ℕ \to i \in ℝ$
36	35	ad2antrl	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to i \in ℝ$
37		modabs2	$⊢ (i \in ℝ \land N (K) \in ℝ^{+}) \to (i \mod N (K)) \mod N (K) = i \mod N (K)$
38	36 34 37	syl2anc	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (i \mod N (K)) \mod N (K) = i \mod N (K)$
39		nnre	$⊢ j \in ℕ \to j \in ℝ$
40	39	ad2antll	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to j \in ℝ$
41		modabs2	$⊢ (j \in ℝ \land N (K) \in ℝ^{+}) \to (j \mod N (K)) \mod N (K) = j \mod N (K)$
42	40 34 41	syl2anc	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (j \mod N (K)) \mod N (K) = j \mod N (K)$
43	29 24 33 31 34 38 42	modmul12d	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (i \mod N (K)) (j \mod N (K)) \mod N (K) = i j \mod N (K)$
44		oveq1	$⊢ k = i \to k \mod N (K) = i \mod N (K)$
45		eqid	$⊢ (k \in ℕ ⟼ k \mod N (K)) = (k \in ℕ ⟼ k \mod N (K))$
46		ovex	$⊢ i \mod N (K) \in V$
47	44 45 46	fvmpt	$⊢ i \in ℕ \to (k \in ℕ ⟼ k \mod N (K)) (i) = i \mod N (K)$
48	47	ad2antrl	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (k \in ℕ ⟼ k \mod N (K)) (i) = i \mod N (K)$
49		oveq1	$⊢ k = j \to k \mod N (K) = j \mod N (K)$
50		ovex	$⊢ j \mod N (K) \in V$
51	49 45 50	fvmpt	$⊢ j \in ℕ \to (k \in ℕ ⟼ k \mod N (K)) (j) = j \mod N (K)$
52	51	ad2antll	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (k \in ℕ ⟼ k \mod N (K)) (j) = j \mod N (K)$
53	48 52	oveq12d	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (k \in ℕ ⟼ k \mod N (K)) (i) P (k \in ℕ ⟼ k \mod N (K)) (j) = (i \mod N (K)) P (j \mod N (K))$
54		oveq12	$⊢ (x = i \mod N (K) \land y = j \mod N (K)) \to x y = (i \mod N (K)) (j \mod N (K))$
55	54	oveq1d	$⊢ (x = i \mod N (K) \land y = j \mod N (K)) \to x y \mod N (K) = (i \mod N (K)) (j \mod N (K)) \mod N (K)$
56		ovex	$⊢ (i \mod N (K)) (j \mod N (K)) \mod N (K) \in V$
57	55 7 56	ovmpoa	$⊢ (i \mod N (K) \in V \land j \mod N (K) \in V) \to (i \mod N (K)) P (j \mod N (K)) = (i \mod N (K)) (j \mod N (K)) \mod N (K)$
58	46 50 57	mp2an	$⊢ (i \mod N (K)) P (j \mod N (K)) = (i \mod N (K)) (j \mod N (K)) \mod N (K)$
59	53 58	eqtrdi	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (k \in ℕ ⟼ k \mod N (K)) (i) P (k \in ℕ ⟼ k \mod N (K)) (j) = (i \mod N (K)) (j \mod N (K)) \mod N (K)$
60		oveq1	$⊢ k = i j \to k \mod N (K) = i j \mod N (K)$
61		ovex	$⊢ i j \mod N (K) \in V$
62	60 45 61	fvmpt	$⊢ i j \in ℕ \to (k \in ℕ ⟼ k \mod N (K)) (i j) = i j \mod N (K)$
63	11 62	syl	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (k \in ℕ ⟼ k \mod N (K)) (i j) = i j \mod N (K)$
64	43 59 63	3eqtr4rd	$⊢ ((φ \land K \in ℕ_{0}) \land (i \in ℕ \land j \in ℕ)) \to (k \in ℕ ⟼ k \mod N (K)) (i j) = (k \in ℕ ⟼ k \mod N (K)) (i) P (k \in ℕ ⟼ k \mod N (K)) (j)$
65		oveq1	$⊢ k = N (i) \to k \mod N (K) = N (i) \mod N (K)$
66		ovex	$⊢ N (i) \mod N (K) \in V$
67	65 45 66	fvmpt	$⊢ N (i) \in ℕ \to (k \in ℕ ⟼ k \mod N (K)) (N (i)) = N (i) \mod N (K)$
68	15 67	syl	$⊢ ((φ \land K \in ℕ_{0}) \land i \in ℕ_{0}) \to (k \in ℕ ⟼ k \mod N (K)) (N (i)) = N (i) \mod N (K)$
69		fveq2	$⊢ k = i \to N (k) = N (i)$
70	69	oveq1d	$⊢ k = i \to N (k) \mod N (K) = N (i) \mod N (K)$
71		eqid	$⊢ (k \in ℕ_{0} ⟼ N (k) \mod N (K)) = (k \in ℕ_{0} ⟼ N (k) \mod N (K))$
72	70 71 66	fvmpt	$⊢ i \in ℕ_{0} \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (i) = N (i) \mod N (K)$
73	72	adantl	$⊢ ((φ \land K \in ℕ_{0}) \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (i) = N (i) \mod N (K)$
74	68 73	eqtr4d	$⊢ ((φ \land K \in ℕ_{0}) \land i \in ℕ_{0}) \to (k \in ℕ ⟼ k \mod N (K)) (N (i)) = (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (i)$
75	12 74	sylan2	$⊢ ((φ \land K \in ℕ_{0}) \land i \in (0 \dots \deg (F))) \to (k \in ℕ ⟼ k \mod N (K)) (N (i)) = (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (i)$
76	11 16 22 64 75	seqhomo	$⊢ (φ \land K \in ℕ_{0}) \to (k \in ℕ ⟼ k \mod N (K)) (seq 0 (\times N) (\deg (F))) = seq 0 (P, (k \in ℕ_{0} ⟼ N (k) \mod N (K))) (\deg (F))$
77	9 76	eqtrid	$⊢ (φ \land K \in ℕ_{0}) \to (k \in ℕ ⟼ k \mod N (K)) (R) = seq 0 (P, (k \in ℕ_{0} ⟼ N (k) \mod N (K))) (\deg (F))$
78	8 77	sylan2	$⊢ (φ \land K \in (0 \dots \deg (F))) \to (k \in ℕ ⟼ k \mod N (K)) (R) = seq 0 (P, (k \in ℕ_{0} ⟼ N (k) \mod N (K))) (\deg (F))$
79		0zd	$⊢ φ \to 0 \in ℤ$
80	10	adantl	$⊢ (φ \land (i \in ℕ \land j \in ℕ)) \to i j \in ℕ$
81	20 79 14 80	seqf	$⊢ φ \to seq 0 (\times N) : ℕ_{0} ⟶ ℕ$
82	81 19	ffvelcdmd	$⊢ φ \to seq 0 (\times N) (\deg (F)) \in ℕ$
83	6 82	eqeltrid	$⊢ φ \to R \in ℕ$
84	83	adantr	$⊢ (φ \land K \in ℕ_{0}) \to R \in ℕ$
85		oveq1	$⊢ k = R \to k \mod N (K) = R \mod N (K)$
86		ovex	$⊢ R \mod N (K) \in V$
87	85 45 86	fvmpt	$⊢ R \in ℕ \to (k \in ℕ ⟼ k \mod N (K)) (R) = R \mod N (K)$
88	84 87	syl	$⊢ (φ \land K \in ℕ_{0}) \to (k \in ℕ ⟼ k \mod N (K)) (R) = R \mod N (K)$
89	8 88	sylan2	$⊢ (φ \land K \in (0 \dots \deg (F))) \to (k \in ℕ ⟼ k \mod N (K)) (R) = R \mod N (K)$
90		oveq12	$⊢ (x = i \land y = j) \to x y = i j$
91	90	oveq1d	$⊢ (x = i \land y = j) \to x y \mod N (K) = i j \mod N (K)$
92	91 7 61	ovmpoa	$⊢ (i \in V \land j \in V) \to i P j = i j \mod N (K)$
93	92	el2v	$⊢ i P j = i j \mod N (K)$
94		nn0mulcl	$⊢ (i \in ℕ_{0} \land j \in ℕ_{0}) \to i j \in ℕ_{0}$
95	94	nn0zd	$⊢ (i \in ℕ_{0} \land j \in ℕ_{0}) \to i j \in ℤ$
96	8 26	sylan2	$⊢ (φ \land K \in (0 \dots \deg (F))) \to N (K) \in ℕ$
97		zmodcl	$⊢ (i j \in ℤ \land N (K) \in ℕ) \to i j \mod N (K) \in ℕ_{0}$
98	95 96 97	syl2anr	$⊢ ((φ \land K \in (0 \dots \deg (F))) \land (i \in ℕ_{0} \land j \in ℕ_{0})) \to i j \mod N (K) \in ℕ_{0}$
99	93 98	eqeltrid	$⊢ ((φ \land K \in (0 \dots \deg (F))) \land (i \in ℕ_{0} \land j \in ℕ_{0})) \to i P j \in ℕ_{0}$
100		fveq2	$⊢ k = m \to B (k) = B (m)$
101	100	oveq1d	$⊢ k = m \to B (k) n = B (m) n$
102	101	eleq1d	$⊢ k = m \to (B (k) n \in ℤ \leftrightarrow B (m) n \in ℤ)$
103	102	rabbidv	$⊢ k = m \to \{n \in ℕ \| B (k) n \in ℤ\} = \{n \in ℕ \| B (m) n \in ℤ\}$
104	103	infeq1d	$⊢ k = m \to inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <) = inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <)$
105	104	cbvmptv	$⊢ (k \in ℕ_{0} ⟼ inf (\{n \in ℕ \| B (k) n \in ℤ\} ℝ <)) = (m \in ℕ_{0} ⟼ inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <))$
106	5 105	eqtri	$⊢ N = (m \in ℕ_{0} ⟼ inf (\{n \in ℕ \| B (m) n \in ℤ\} ℝ <))$
107	1 2 3 4 106 6	elqaalem1	$⊢ (φ \land k \in ℕ_{0}) \to (N (k) \in ℕ \land B (k) N (k) \in ℤ)$
108	107	simpld	$⊢ (φ \land k \in ℕ_{0}) \to N (k) \in ℕ$
109	108	adantlr	$⊢ ((φ \land K \in ℕ_{0}) \land k \in ℕ_{0}) \to N (k) \in ℕ$
110	109	nnzd	$⊢ ((φ \land K \in ℕ_{0}) \land k \in ℕ_{0}) \to N (k) \in ℤ$
111	26	adantr	$⊢ ((φ \land K \in ℕ_{0}) \land k \in ℕ_{0}) \to N (K) \in ℕ$
112	110 111	zmodcld	$⊢ ((φ \land K \in ℕ_{0}) \land k \in ℕ_{0}) \to N (k) \mod N (K) \in ℕ_{0}$
113	112	fmpttd	$⊢ (φ \land K \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) : ℕ_{0} ⟶ ℕ_{0}$
114	8 113	sylan2	$⊢ (φ \land K \in (0 \dots \deg (F))) \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) : ℕ_{0} ⟶ ℕ_{0}$
115		ffvelcdm	$⊢ ((k \in ℕ_{0} ⟼ N (k) \mod N (K)) : ℕ_{0} ⟶ ℕ_{0} \land i \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (i) \in ℕ_{0}$
116	114 12 115	syl2an	$⊢ ((φ \land K \in (0 \dots \deg (F))) \land i \in (0 \dots \deg (F))) \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (i) \in ℕ_{0}$
117		c0ex	$⊢ 0 \in V$
118		vex	$⊢ i \in V$
119		oveq12	$⊢ (x = 0 \land y = i) \to x y = 0 \cdot i$
120	119	oveq1d	$⊢ (x = 0 \land y = i) \to x y \mod N (K) = 0 \cdot i \mod N (K)$
121		ovex	$⊢ 0 \cdot i \mod N (K) \in V$
122	120 7 121	ovmpoa	$⊢ (0 \in V \land i \in V) \to 0 P i = 0 \cdot i \mod N (K)$
123	117 118 122	mp2an	$⊢ 0 P i = 0 \cdot i \mod N (K)$
124		nn0cn	$⊢ i \in ℕ_{0} \to i \in ℂ$
125	124	mul02d	$⊢ i \in ℕ_{0} \to 0 \cdot i = 0$
126	125	oveq1d	$⊢ i \in ℕ_{0} \to 0 \cdot i \mod N (K) = 0 \mod N (K)$
127	96	nnrpd	$⊢ (φ \land K \in (0 \dots \deg (F))) \to N (K) \in ℝ^{+}$
128		0mod	$⊢ N (K) \in ℝ^{+} \to 0 \mod N (K) = 0$
129	127 128	syl	$⊢ (φ \land K \in (0 \dots \deg (F))) \to 0 \mod N (K) = 0$
130	126 129	sylan9eqr	$⊢ ((φ \land K \in (0 \dots \deg (F))) \land i \in ℕ_{0}) \to 0 \cdot i \mod N (K) = 0$
131	123 130	eqtrid	$⊢ ((φ \land K \in (0 \dots \deg (F))) \land i \in ℕ_{0}) \to 0 P i = 0$
132		oveq12	$⊢ (x = i \land y = 0) \to x y = i \cdot 0$
133	132	oveq1d	$⊢ (x = i \land y = 0) \to x y \mod N (K) = i \cdot 0 \mod N (K)$
134		ovex	$⊢ i \cdot 0 \mod N (K) \in V$
135	133 7 134	ovmpoa	$⊢ (i \in V \land 0 \in V) \to i P 0 = i \cdot 0 \mod N (K)$
136	118 117 135	mp2an	$⊢ i P 0 = i \cdot 0 \mod N (K)$
137	124	mul01d	$⊢ i \in ℕ_{0} \to i \cdot 0 = 0$
138	137	oveq1d	$⊢ i \in ℕ_{0} \to i \cdot 0 \mod N (K) = 0 \mod N (K)$
139	138 129	sylan9eqr	$⊢ ((φ \land K \in (0 \dots \deg (F))) \land i \in ℕ_{0}) \to i \cdot 0 \mod N (K) = 0$
140	136 139	eqtrid	$⊢ ((φ \land K \in (0 \dots \deg (F))) \land i \in ℕ_{0}) \to i P 0 = 0$
141		simpr	$⊢ (φ \land K \in (0 \dots \deg (F))) \to K \in (0 \dots \deg (F))$
142	19	adantr	$⊢ (φ \land K \in (0 \dots \deg (F))) \to \deg (F) \in ℕ_{0}$
143	8	adantl	$⊢ (φ \land K \in (0 \dots \deg (F))) \to K \in ℕ_{0}$
144		fveq2	$⊢ k = K \to N (k) = N (K)$
145	144	oveq1d	$⊢ k = K \to N (k) \mod N (K) = N (K) \mod N (K)$
146		ovex	$⊢ N (K) \mod N (K) \in V$
147	145 71 146	fvmpt	$⊢ K \in ℕ_{0} \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (K) = N (K) \mod N (K)$
148	143 147	syl	$⊢ (φ \land K \in (0 \dots \deg (F))) \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (K) = N (K) \mod N (K)$
149	96	nncnd	$⊢ (φ \land K \in (0 \dots \deg (F))) \to N (K) \in ℂ$
150	96	nnne0d	$⊢ (φ \land K \in (0 \dots \deg (F))) \to N (K) \neq 0$
151	149 150	dividd	$⊢ (φ \land K \in (0 \dots \deg (F))) \to \frac{N (K)}{N (K)} = 1$
152		1z	$⊢ 1 \in ℤ$
153	151 152	eqeltrdi	$⊢ (φ \land K \in (0 \dots \deg (F))) \to \frac{N (K)}{N (K)} \in ℤ$
154	96	nnred	$⊢ (φ \land K \in (0 \dots \deg (F))) \to N (K) \in ℝ$
155		mod0	$⊢ (N (K) \in ℝ \land N (K) \in ℝ^{+}) \to (N (K) \mod N (K) = 0 \leftrightarrow \frac{N (K)}{N (K)} \in ℤ)$
156	154 127 155	syl2anc	$⊢ (φ \land K \in (0 \dots \deg (F))) \to (N (K) \mod N (K) = 0 \leftrightarrow \frac{N (K)}{N (K)} \in ℤ)$
157	153 156	mpbird	$⊢ (φ \land K \in (0 \dots \deg (F))) \to N (K) \mod N (K) = 0$
158	148 157	eqtrd	$⊢ (φ \land K \in (0 \dots \deg (F))) \to (k \in ℕ_{0} ⟼ N (k) \mod N (K)) (K) = 0$
159	99 116 131 140 141 142 158	seqz	$⊢ (φ \land K \in (0 \dots \deg (F))) \to seq 0 (P, (k \in ℕ_{0} ⟼ N (k) \mod N (K))) (\deg (F)) = 0$
160	78 89 159	3eqtr3d	$⊢ (φ \land K \in (0 \dots \deg (F))) \to R \mod N (K) = 0$

Metamath Proof Explorer

Theorem elqaalem2

Proof