lgsdilem2

	Ref	Expression
Hypotheses	lgsdilem2.1	$⊢ φ \to A \in ℤ$
	lgsdilem2.2	$⊢ φ \to M \in ℤ$
	lgsdilem2.3	$⊢ φ \to N \in ℤ$
	lgsdilem2.4	$⊢ φ \to M \neq 0$
	lgsdilem2.5	$⊢ φ \to N \neq 0$
	lgsdilem2.6	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))$
Assertion	lgsdilem2	$⊢ φ \to seq 1 (\times F) (\|M\|) = seq 1 (\times F) (\|M \cdot N\|)$

Proof

Step	Hyp	Ref	Expression
1		lgsdilem2.1	$⊢ φ \to A \in ℤ$
2		lgsdilem2.2	$⊢ φ \to M \in ℤ$
3		lgsdilem2.3	$⊢ φ \to N \in ℤ$
4		lgsdilem2.4	$⊢ φ \to M \neq 0$
5		lgsdilem2.5	$⊢ φ \to N \neq 0$
6		lgsdilem2.6	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1))$
7		mulid1	$⊢ k \in ℂ \to k \cdot 1 = k$
8	7	adantl	$⊢ (φ \land k \in ℂ) \to k \cdot 1 = k$
9		nnabscl	$⊢ (M \in ℤ \land M \neq 0) \to \|M\| \in ℕ$
10	2 4 9	syl2anc	$⊢ φ \to \|M\| \in ℕ$
11		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
12	10 11	eleqtrdi	$⊢ φ \to \|M\| \in ℤ_{\geq 1}$
13	10	nnzd	$⊢ φ \to \|M\| \in ℤ$
14	2 3	zmulcld	$⊢ φ \to M \cdot N \in ℤ$
15	2	zcnd	$⊢ φ \to M \in ℂ$
16	3	zcnd	$⊢ φ \to N \in ℂ$
17	15 16 4 5	mulne0d	$⊢ φ \to M \cdot N \neq 0$
18		nnabscl	$⊢ (M \cdot N \in ℤ \land M \cdot N \neq 0) \to \|M \cdot N\| \in ℕ$
19	14 17 18	syl2anc	$⊢ φ \to \|M \cdot N\| \in ℕ$
20	19	nnzd	$⊢ φ \to \|M \cdot N\| \in ℤ$
21	15	abscld	$⊢ φ \to \|M\| \in ℝ$
22	16	abscld	$⊢ φ \to \|N\| \in ℝ$
23	15	absge0d	$⊢ φ \to 0 \leq \|M\|$
24		nnabscl	$⊢ (N \in ℤ \land N \neq 0) \to \|N\| \in ℕ$
25	3 5 24	syl2anc	$⊢ φ \to \|N\| \in ℕ$
26	25	nnge1d	$⊢ φ \to 1 \leq \|N\|$
27	21 22 23 26	lemulge11d	$⊢ φ \to \|M\| \leq \|M\| \|N\|$
28	15 16	absmuld	$⊢ φ \to \|M \cdot N\| = \|M\| \|N\|$
29	27 28	breqtrrd	$⊢ φ \to \|M\| \leq \|M \cdot N\|$
30		eluz2	$⊢ \|M \cdot N\| \in ℤ_{\geq \|M\|} \leftrightarrow (\|M\| \in ℤ \land \|M \cdot N\| \in ℤ \land \|M\| \leq \|M \cdot N\|)$
31	13 20 29 30	syl3anbrc	$⊢ φ \to \|M \cdot N\| \in ℤ_{\geq \|M\|}$
32	6	lgsfcl3	$⊢ (A \in ℤ \land M \in ℤ \land M \neq 0) \to F : ℕ ⟶ ℤ$
33	1 2 4 32	syl3anc	$⊢ φ \to F : ℕ ⟶ ℤ$
34		elfznn	$⊢ k \in (1 \dots \|M\|) \to k \in ℕ$
35		ffvelrn	$⊢ (F : ℕ ⟶ ℤ \land k \in ℕ) \to F (k) \in ℤ$
36	33 34 35	syl2an	$⊢ (φ \land k \in (1 \dots \|M\|)) \to F (k) \in ℤ$
37	36	zcnd	$⊢ (φ \land k \in (1 \dots \|M\|)) \to F (k) \in ℂ$
38		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
39	38	adantl	$⊢ (φ \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
40	12 37 39	seqcl	$⊢ φ \to seq 1 (\times F) (\|M\|) \in ℂ$
41	10	peano2nnd	$⊢ φ \to \|M\| + 1 \in ℕ$
42		elfzuz	$⊢ k \in (\|M\| + 1 \dots \|M \cdot N\|) \to k \in ℤ_{\geq (\|M\| + 1)}$
43		eluznn	$⊢ (\|M\| + 1 \in ℕ \land k \in ℤ_{\geq (\|M\| + 1)}) \to k \in ℕ$
44	41 42 43	syl2an	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to k \in ℕ$
45		eleq1w	$⊢ n = k \to (n \in ℙ \leftrightarrow k \in ℙ)$
46		oveq2	$⊢ n = k \to A /_{L} n = A /_{L} k$
47		oveq1	$⊢ n = k \to n pCnt M = k pCnt M$
48	46 47	oveq12d	$⊢ n = k \to {(A /_{L} n)}^{n pCnt M} = {(A /_{L} k)}^{k pCnt M}$
49	45 48	ifbieq1d	$⊢ n = k \to if (n \in ℙ, {(A /_{L} n)}^{n pCnt M}, 1) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1)$
50		ovex	$⊢ {(A /_{L} k)}^{k pCnt M} \in V$
51		1ex	$⊢ 1 \in V$
52	50 51	ifex	$⊢ if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) \in V$
53	49 6 52	fvmpt	$⊢ k \in ℕ \to F (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1)$
54	44 53	syl	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to F (k) = if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1)$
55		simpr	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k \in ℙ$
56	2	ad2antrr	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to M \in ℤ$
57		zq	$⊢ M \in ℤ \to M \in ℚ$
58	56 57	syl	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to M \in ℚ$
59		pcabs	$⊢ (k \in ℙ \land M \in ℚ) \to k pCnt \|M\| = k pCnt M$
60	55 58 59	syl2anc	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k pCnt \|M\| = k pCnt M$
61		elfzle1	$⊢ k \in (\|M\| + 1 \dots \|M \cdot N\|) \to \|M\| + 1 \leq k$
62	61	adantl	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to \|M\| + 1 \leq k$
63		elfzelz	$⊢ k \in (\|M\| + 1 \dots \|M \cdot N\|) \to k \in ℤ$
64		zltp1le	$⊢ (\|M\| \in ℤ \land k \in ℤ) \to (\|M\| < k \leftrightarrow \|M\| + 1 \leq k)$
65	13 63 64	syl2an	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to (\|M\| < k \leftrightarrow \|M\| + 1 \leq k)$
66	62 65	mpbird	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to \|M\| < k$
67	21	adantr	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to \|M\| \in ℝ$
68	63	adantl	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to k \in ℤ$
69	68	zred	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to k \in ℝ$
70	67 69	ltnled	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to (\|M\| < k \leftrightarrow \neg k \leq \|M\|)$
71	66 70	mpbid	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to \neg k \leq \|M\|$
72	71	adantr	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to \neg k \leq \|M\|$
73		prmz	$⊢ k \in ℙ \to k \in ℤ$
74	73	adantl	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k \in ℤ$
75	4	ad2antrr	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to M \neq 0$
76	56 75 9	syl2anc	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to \|M\| \in ℕ$
77		dvdsle	$⊢ (k \in ℤ \land \|M\| \in ℕ) \to (k ∥ \|M\| \to k \leq \|M\|)$
78	74 76 77	syl2anc	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to (k ∥ \|M\| \to k \leq \|M\|)$
79	72 78	mtod	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to \neg k ∥ \|M\|$
80		pceq0	$⊢ (k \in ℙ \land \|M\| \in ℕ) \to (k pCnt \|M\| = 0 \leftrightarrow \neg k ∥ \|M\|)$
81	55 76 80	syl2anc	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to (k pCnt \|M\| = 0 \leftrightarrow \neg k ∥ \|M\|)$
82	79 81	mpbird	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k pCnt \|M\| = 0$
83	60 82	eqtr3d	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to k pCnt M = 0$
84	83	oveq2d	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to {(A /_{L} k)}^{k pCnt M} = {(A /_{L} k)}^{0}$
85	1	ad2antrr	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to A \in ℤ$
86		lgscl	$⊢ (A \in ℤ \land k \in ℤ) \to A /_{L} k \in ℤ$
87	85 74 86	syl2anc	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to A /_{L} k \in ℤ$
88	87	zcnd	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to A /_{L} k \in ℂ$
89	88	exp0d	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to {(A /_{L} k)}^{0} = 1$
90	84 89	eqtrd	$⊢ ((φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \land k \in ℙ) \to {(A /_{L} k)}^{k pCnt M} = 1$
91	90	ifeq1da	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) = if (k \in ℙ, 1, 1)$
92		ifid	$⊢ if (k \in ℙ, 1, 1) = 1$
93	91 92	syl6eq	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to if (k \in ℙ, {(A /_{L} k)}^{k pCnt M}, 1) = 1$
94	54 93	eqtrd	$⊢ (φ \land k \in (\|M\| + 1 \dots \|M \cdot N\|)) \to F (k) = 1$
95	8 12 31 40 94	seqid2	$⊢ φ \to seq 1 (\times F) (\|M\|) = seq 1 (\times F) (\|M \cdot N\|)$

Metamath Proof Explorer

Theorem lgsdilem2

Proof