aks6d1c3

	Ref	Expression
Hypotheses	aks6d1c3.1	$⊢ φ \to N \in ℕ$
	aks6d1c3.2	$⊢ φ \to P \in ℙ$
	aks6d1c3.3	$⊢ φ \to P ∥ N$
	aks6d1c3.4	$⊢ φ \to R \in ℕ$
	aks6d1c3.5	$⊢ φ \to N \gcd R = 1$
	aks6d1c3.6	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
	aks6d1c3.7	$⊢ L = ℤRHom (Y)$
	aks6d1c3.8	$⊢ Y = ℤ / R ℤ$
	aks6d1c3.9	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
Assertion	aks6d1c3	$⊢ φ \to {\log_{2} N}^{2} < \|L [E [ℕ_{0} \times ℕ_{0}]]\|$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c3.1	$⊢ φ \to N \in ℕ$
2		aks6d1c3.2	$⊢ φ \to P \in ℙ$
3		aks6d1c3.3	$⊢ φ \to P ∥ N$
4		aks6d1c3.4	$⊢ φ \to R \in ℕ$
5		aks6d1c3.5	$⊢ φ \to N \gcd R = 1$
6		aks6d1c3.6	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
7		aks6d1c3.7	$⊢ L = ℤRHom (Y)$
8		aks6d1c3.8	$⊢ Y = ℤ / R ℤ$
9		aks6d1c3.9	$⊢ φ \to {\log_{2} N}^{2} < {od}_{ℤ} (R) (N)$
10		2re	$⊢ 2 \in ℝ$
11	10	a1i	$⊢ φ \to 2 \in ℝ$
12		2pos	$⊢ 0 < 2$
13	12	a1i	$⊢ φ \to 0 < 2$
14	1	nnred	$⊢ φ \to N \in ℝ$
15	1	nngt0d	$⊢ φ \to 0 < N$
16		1red	$⊢ φ \to 1 \in ℝ$
17		1lt2	$⊢ 1 < 2$
18	17	a1i	$⊢ φ \to 1 < 2$
19	16 18	ltned	$⊢ φ \to 1 \neq 2$
20	19	necomd	$⊢ φ \to 2 \neq 1$
21	11 13 14 15 20	relogbcld	$⊢ φ \to \log_{2} N \in ℝ$
22	21	resqcld	$⊢ φ \to {\log_{2} N}^{2} \in ℝ$
23	1	nnzd	$⊢ φ \to N \in ℤ$
24		odzcl	$⊢ (R \in ℕ \land N \in ℤ \land N \gcd R = 1) \to {od}_{ℤ} (R) (N) \in ℕ$
25	4 23 5 24	syl3anc	$⊢ φ \to {od}_{ℤ} (R) (N) \in ℕ$
26	25	nnred	$⊢ φ \to {od}_{ℤ} (R) (N) \in ℝ$
27	1 2 3 4 5 6 7 8	hashscontpowcl	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℕ_{0}$
28	27	nn0red	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ$
29		nfv	$⊢ Ⅎ x φ$
30		prmnn	$⊢ P \in ℙ \to P \in ℕ$
31	2 30	syl	$⊢ φ \to P \in ℕ$
32	31	nnzd	$⊢ φ \to P \in ℤ$
33	32	adantr	$⊢ (φ \land k \in ℕ_{0}) \to P \in ℤ$
34	33	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to P \in ℤ$
35		simplr	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to k \in ℕ_{0}$
36	34 35	zexpcld	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to P^{k} \in ℤ$
37	31	nnne0d	$⊢ φ \to P \neq 0$
38		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land N \in ℤ) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
39	32 37 23 38	syl3anc	$⊢ φ \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
40	3 39	mpbid	$⊢ φ \to \frac{N}{P} \in ℤ$
41	40	adantr	$⊢ (φ \land k \in ℕ_{0}) \to \frac{N}{P} \in ℤ$
42	41	adantr	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to \frac{N}{P} \in ℤ$
43		simpr	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to l \in ℕ_{0}$
44	42 43	zexpcld	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to {(\frac{N}{P})}^{l} \in ℤ$
45	36 44	zmulcld	$⊢ ((φ \land k \in ℕ_{0}) \land l \in ℕ_{0}) \to P^{k} {(\frac{N}{P})}^{l} \in ℤ$
46	45	ralrimiva	$⊢ (φ \land k \in ℕ_{0}) \to \forall l \in ℕ_{0} P^{k} {(\frac{N}{P})}^{l} \in ℤ$
47	46	ralrimiva	$⊢ φ \to \forall k \in ℕ_{0} \forall l \in ℕ_{0} P^{k} {(\frac{N}{P})}^{l} \in ℤ$
48	6	fmpo	$⊢ \forall k \in ℕ_{0} \forall l \in ℕ_{0} P^{k} {(\frac{N}{P})}^{l} \in ℤ \leftrightarrow E : ℕ_{0} \times ℕ_{0} ⟶ ℤ$
49	47 48	sylib	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} ⟶ ℤ$
50	49	ffund	$⊢ φ \to Fun E$
51	49	ffvelcdmda	$⊢ (φ \land x \in (ℕ_{0} \times ℕ_{0})) \to E (x) \in ℤ$
52	29 50 51	funimassd	$⊢ φ \to E [ℕ_{0} \times ℕ_{0}] \subseteq ℤ$
53	49	ffnd	$⊢ φ \to E Fn (ℕ_{0} \times ℕ_{0})$
54	53	adantr	$⊢ (φ \land i \in ℕ_{0}) \to E Fn (ℕ_{0} \times ℕ_{0})$
55		simpr	$⊢ (φ \land i \in ℕ_{0}) \to i \in ℕ_{0}$
56	55 55	opelxpd	$⊢ (φ \land i \in ℕ_{0}) \to ⟨i, i⟩ \in (ℕ_{0} \times ℕ_{0})$
57	54 56 56	fnfvimad	$⊢ (φ \land i \in ℕ_{0}) \to E (⟨i, i⟩) \in E [ℕ_{0} \times ℕ_{0}]$
58		vex	$⊢ k \in V$
59		vex	$⊢ l \in V$
60	58 59	op1std	$⊢ q = ⟨k, l⟩ \to 1^{st} (q) = k$
61	60	oveq2d	$⊢ q = ⟨k, l⟩ \to P^{1^{st} (q)} = P^{k}$
62	58 59	op2ndd	$⊢ q = ⟨k, l⟩ \to 2^{nd} (q) = l$
63	62	oveq2d	$⊢ q = ⟨k, l⟩ \to {(\frac{N}{P})}^{2^{nd} (q)} = {(\frac{N}{P})}^{l}$
64	61 63	oveq12d	$⊢ q = ⟨k, l⟩ \to P^{1^{st} (q)} {(\frac{N}{P})}^{2^{nd} (q)} = P^{k} {(\frac{N}{P})}^{l}$
65	64	mpompt	$⊢ (q \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (q)} {(\frac{N}{P})}^{2^{nd} (q)}) = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
66	6 65	eqtr4i	$⊢ E = (q \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (q)} {(\frac{N}{P})}^{2^{nd} (q)})$
67	66	a1i	$⊢ (φ \land i \in ℕ_{0}) \to E = (q \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (q)} {(\frac{N}{P})}^{2^{nd} (q)})$
68		simpr	$⊢ ((φ \land i \in ℕ_{0}) \land q = ⟨i, i⟩) \to q = ⟨i, i⟩$
69	68	fveq2d	$⊢ ((φ \land i \in ℕ_{0}) \land q = ⟨i, i⟩) \to 1^{st} (q) = 1^{st} (⟨i, i⟩)$
70	69	oveq2d	$⊢ ((φ \land i \in ℕ_{0}) \land q = ⟨i, i⟩) \to P^{1^{st} (q)} = P^{1^{st} (⟨i, i⟩)}$
71	68	fveq2d	$⊢ ((φ \land i \in ℕ_{0}) \land q = ⟨i, i⟩) \to 2^{nd} (q) = 2^{nd} (⟨i, i⟩)$
72	71	oveq2d	$⊢ ((φ \land i \in ℕ_{0}) \land q = ⟨i, i⟩) \to {(\frac{N}{P})}^{2^{nd} (q)} = {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)}$
73	70 72	oveq12d	$⊢ ((φ \land i \in ℕ_{0}) \land q = ⟨i, i⟩) \to P^{1^{st} (q)} {(\frac{N}{P})}^{2^{nd} (q)} = P^{1^{st} (⟨i, i⟩)} {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)}$
74		opelxp	$⊢ ⟨i, i⟩ \in (ℕ_{0} \times ℕ_{0}) \leftrightarrow (i \in ℕ_{0} \land i \in ℕ_{0})$
75	56 74	sylib	$⊢ (φ \land i \in ℕ_{0}) \to (i \in ℕ_{0} \land i \in ℕ_{0})$
76	75 74	sylibr	$⊢ (φ \land i \in ℕ_{0}) \to ⟨i, i⟩ \in (ℕ_{0} \times ℕ_{0})$
77	32	adantr	$⊢ (φ \land i \in ℕ_{0}) \to P \in ℤ$
78		xp1st	$⊢ ⟨i, i⟩ \in (ℕ_{0} \times ℕ_{0}) \to 1^{st} (⟨i, i⟩) \in ℕ_{0}$
79	56 78	syl	$⊢ (φ \land i \in ℕ_{0}) \to 1^{st} (⟨i, i⟩) \in ℕ_{0}$
80	77 79	zexpcld	$⊢ (φ \land i \in ℕ_{0}) \to P^{1^{st} (⟨i, i⟩)} \in ℤ$
81	40	adantr	$⊢ (φ \land i \in ℕ_{0}) \to \frac{N}{P} \in ℤ$
82		xp2nd	$⊢ ⟨i, i⟩ \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (⟨i, i⟩) \in ℕ_{0}$
83	56 82	syl	$⊢ (φ \land i \in ℕ_{0}) \to 2^{nd} (⟨i, i⟩) \in ℕ_{0}$
84	81 83	zexpcld	$⊢ (φ \land i \in ℕ_{0}) \to {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)} \in ℤ$
85	80 84	zmulcld	$⊢ (φ \land i \in ℕ_{0}) \to P^{1^{st} (⟨i, i⟩)} {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)} \in ℤ$
86	67 73 76 85	fvmptd	$⊢ (φ \land i \in ℕ_{0}) \to E (⟨i, i⟩) = P^{1^{st} (⟨i, i⟩)} {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)}$
87		vex	$⊢ i \in V$
88	87 87	op1st	$⊢ 1^{st} (⟨i, i⟩) = i$
89	88	a1i	$⊢ (φ \land i \in ℕ_{0}) \to 1^{st} (⟨i, i⟩) = i$
90	89	oveq2d	$⊢ (φ \land i \in ℕ_{0}) \to P^{1^{st} (⟨i, i⟩)} = P^{i}$
91	87 87	op2nd	$⊢ 2^{nd} (⟨i, i⟩) = i$
92	91	a1i	$⊢ (φ \land i \in ℕ_{0}) \to 2^{nd} (⟨i, i⟩) = i$
93	92	oveq2d	$⊢ (φ \land i \in ℕ_{0}) \to {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)} = {(\frac{N}{P})}^{i}$
94	90 93	oveq12d	$⊢ (φ \land i \in ℕ_{0}) \to P^{1^{st} (⟨i, i⟩)} {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)} = P^{i} {(\frac{N}{P})}^{i}$
95	14	recnd	$⊢ φ \to N \in ℂ$
96	95	adantr	$⊢ (φ \land i \in ℕ_{0}) \to N \in ℂ$
97	77	zcnd	$⊢ (φ \land i \in ℕ_{0}) \to P \in ℂ$
98	37	adantr	$⊢ (φ \land i \in ℕ_{0}) \to P \neq 0$
99	96 97 98	divcan2d	$⊢ (φ \land i \in ℕ_{0}) \to P (\frac{N}{P}) = N$
100	99	eqcomd	$⊢ (φ \land i \in ℕ_{0}) \to N = P (\frac{N}{P})$
101	100	oveq1d	$⊢ (φ \land i \in ℕ_{0}) \to N^{i} = {P (\frac{N}{P})}^{i}$
102	81	zcnd	$⊢ (φ \land i \in ℕ_{0}) \to \frac{N}{P} \in ℂ$
103	97 102 55	mulexpd	$⊢ (φ \land i \in ℕ_{0}) \to {P (\frac{N}{P})}^{i} = P^{i} {(\frac{N}{P})}^{i}$
104	101 103	eqtr2d	$⊢ (φ \land i \in ℕ_{0}) \to P^{i} {(\frac{N}{P})}^{i} = N^{i}$
105	94 104	eqtrd	$⊢ (φ \land i \in ℕ_{0}) \to P^{1^{st} (⟨i, i⟩)} {(\frac{N}{P})}^{2^{nd} (⟨i, i⟩)} = N^{i}$
106	86 105	eqtrd	$⊢ (φ \land i \in ℕ_{0}) \to E (⟨i, i⟩) = N^{i}$
107	106	eleq1d	$⊢ (φ \land i \in ℕ_{0}) \to (E (⟨i, i⟩) \in E [ℕ_{0} \times ℕ_{0}] \leftrightarrow N^{i} \in E [ℕ_{0} \times ℕ_{0}])$
108	57 107	mpbid	$⊢ (φ \land i \in ℕ_{0}) \to N^{i} \in E [ℕ_{0} \times ℕ_{0}]$
109	108	ralrimiva	$⊢ φ \to \forall i \in ℕ_{0} N^{i} \in E [ℕ_{0} \times ℕ_{0}]$
110	52 1 109 4 5 7 8	hashscontpow	$⊢ φ \to {od}_{ℤ} (R) (N) \leq \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
111	22 26 28 9 110	ltletrd	$⊢ φ \to {\log_{2} N}^{2} < \|L [E [ℕ_{0} \times ℕ_{0}]]\|$

Metamath Proof Explorer

Theorem aks6d1c3

Proof