aks6d1c4

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

Proof

Step	Hyp	Ref	Expression
1		aks6d1c4.1	$⊢ φ \to N \in ℕ$
2		aks6d1c4.2	$⊢ φ \to P \in ℙ$
3		aks6d1c4.3	$⊢ φ \to P ∥ N$
4		aks6d1c4.4	$⊢ φ \to R \in ℕ$
5		aks6d1c4.5	$⊢ φ \to N \gcd R = 1$
6		aks6d1c4.6	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
7		aks6d1c4.7	$⊢ L = ℤRHom (ℤ / R ℤ)$
8		fvexd	$⊢ φ \to Unit (ℤ / R ℤ) \in V$
9	4	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
10		eqid	$⊢ ℤ / R ℤ = ℤ / R ℤ$
11	10	zncrng	$⊢ R \in ℕ_{0} \to ℤ / R ℤ \in CRing$
12	9 11	syl	$⊢ φ \to ℤ / R ℤ \in CRing$
13		crngring	$⊢ ℤ / R ℤ \in CRing \to ℤ / R ℤ \in Ring$
14	7	zrhrhm	$⊢ ℤ / R ℤ \in Ring \to L \in (ℤ_{ring} RingHom ℤ / R ℤ)$
15		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
16		eqid	$⊢ {Base}_{ℤ / R ℤ} = {Base}_{ℤ / R ℤ}$
17	15 16	rhmf	$⊢ L \in (ℤ_{ring} RingHom ℤ / R ℤ) \to L : ℤ ⟶ {Base}_{ℤ / R ℤ}$
18	12 13 14 17	4syl	$⊢ φ \to L : ℤ ⟶ {Base}_{ℤ / R ℤ}$
19	18	ffund	$⊢ φ \to Fun L$
20	19	adantr	$⊢ (φ \land a \in L [E [ℕ_{0} \times ℕ_{0}]]) \to Fun L$
21		simpr	$⊢ (φ \land a \in L [E [ℕ_{0} \times ℕ_{0}]]) \to a \in L [E [ℕ_{0} \times ℕ_{0}]]$
22		fvelima	$⊢ (Fun L \land a \in L [E [ℕ_{0} \times ℕ_{0}]]) \to \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a$
23	20 21 22	syl2anc	$⊢ (φ \land a \in L [E [ℕ_{0} \times ℕ_{0}]]) \to \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a$
24		simpr	$⊢ (((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \land L (c) = a) \to L (c) = a$
25	24	eqcomd	$⊢ (((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \land L (c) = a) \to a = L (c)$
26		simpll	$⊢ ((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \to φ$
27		simpr	$⊢ ((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \to c \in E [ℕ_{0} \times ℕ_{0}]$
28	26 27	jca	$⊢ ((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \to (φ \land c \in E [ℕ_{0} \times ℕ_{0}])$
29		ovexd	$⊢ (φ \land m \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (m)} {(\frac{N}{P})}^{2^{nd} (m)} \in V$
30		vex	$⊢ k \in V$
31		vex	$⊢ l \in V$
32	30 31	op1std	$⊢ m = ⟨k, l⟩ \to 1^{st} (m) = k$
33	32	oveq2d	$⊢ m = ⟨k, l⟩ \to P^{1^{st} (m)} = P^{k}$
34	30 31	op2ndd	$⊢ m = ⟨k, l⟩ \to 2^{nd} (m) = l$
35	34	oveq2d	$⊢ m = ⟨k, l⟩ \to {(\frac{N}{P})}^{2^{nd} (m)} = {(\frac{N}{P})}^{l}$
36	33 35	oveq12d	$⊢ m = ⟨k, l⟩ \to P^{1^{st} (m)} {(\frac{N}{P})}^{2^{nd} (m)} = P^{k} {(\frac{N}{P})}^{l}$
37	36	mpompt	$⊢ (m \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (m)} {(\frac{N}{P})}^{2^{nd} (m)}) = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
38	37	eqcomi	$⊢ (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l}) = (m \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (m)} {(\frac{N}{P})}^{2^{nd} (m)})$
39	6 38	eqtri	$⊢ E = (m \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (m)} {(\frac{N}{P})}^{2^{nd} (m)})$
40	29 39	fmptd	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} ⟶ V$
41	40	ffund	$⊢ φ \to Fun E$
42	41	adantr	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to Fun E$
43		simpr	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to c \in E [ℕ_{0} \times ℕ_{0}]$
44		fvelima	$⊢ (Fun E \land c \in E [ℕ_{0} \times ℕ_{0}]) \to \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c$
45	42 43 44	syl2anc	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c$
46		simpr	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to E (e) = c$
47	46	eqcomd	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to c = E (e)$
48	47	oveq1d	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to c \gcd R = E (e) \gcd R$
49		simplll	$⊢ (((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \to φ$
50		simpr	$⊢ (((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \to e \in (ℕ_{0} \times ℕ_{0})$
51	49 50	jca	$⊢ (((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \to (φ \land e \in (ℕ_{0} \times ℕ_{0}))$
52	39	a1i	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to E = (m \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (m)} {(\frac{N}{P})}^{2^{nd} (m)})$
53		simpr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land m = e) \to m = e$
54	53	fveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land m = e) \to 1^{st} (m) = 1^{st} (e)$
55	54	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land m = e) \to P^{1^{st} (m)} = P^{1^{st} (e)}$
56	53	fveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land m = e) \to 2^{nd} (m) = 2^{nd} (e)$
57	56	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land m = e) \to {(\frac{N}{P})}^{2^{nd} (m)} = {(\frac{N}{P})}^{2^{nd} (e)}$
58	55 57	oveq12d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land m = e) \to P^{1^{st} (m)} {(\frac{N}{P})}^{2^{nd} (m)} = P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)}$
59		simpr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to e \in (ℕ_{0} \times ℕ_{0})$
60		ovexd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} \in V$
61	52 58 59 60	fvmptd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to E (e) = P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)}$
62		prmnn	$⊢ P \in ℙ \to P \in ℕ$
63	2 62	syl	$⊢ φ \to P \in ℕ$
64	63	nnzd	$⊢ φ \to P \in ℤ$
65	64	adantr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to P \in ℤ$
66		xp1st	$⊢ e \in (ℕ_{0} \times ℕ_{0}) \to 1^{st} (e) \in ℕ_{0}$
67	66	adantl	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to 1^{st} (e) \in ℕ_{0}$
68	65 67	zexpcld	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (e)} \in ℤ$
69	63	nnne0d	$⊢ φ \to P \neq 0$
70	1	nnzd	$⊢ φ \to N \in ℤ$
71		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land N \in ℤ) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
72	64 69 70 71	syl3anc	$⊢ φ \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
73	3 72	mpbid	$⊢ φ \to \frac{N}{P} \in ℤ$
74	73	adantr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to \frac{N}{P} \in ℤ$
75		xp2nd	$⊢ e \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (e) \in ℕ_{0}$
76	75	adantl	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to 2^{nd} (e) \in ℕ_{0}$
77	74 76	zexpcld	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to {(\frac{N}{P})}^{2^{nd} (e)} \in ℤ$
78	68 77	zmulcld	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} \in ℤ$
79	61 78	eqeltrd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to E (e) \in ℤ$
80	61	oveq1d	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to E (e) \gcd R = P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} \gcd R$
81	4	nnzd	$⊢ φ \to R \in ℤ$
82	81	adantr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to R \in ℤ$
83	78 82	gcdcomd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} \gcd R = R \gcd P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)}$
84	81 64 70	3jca	$⊢ φ \to (R \in ℤ \land P \in ℤ \land N \in ℤ)$
85	70 81	jca	$⊢ φ \to (N \in ℤ \land R \in ℤ)$
86		gcdcom	$⊢ (N \in ℤ \land R \in ℤ) \to N \gcd R = R \gcd N$
87	85 86	syl	$⊢ φ \to N \gcd R = R \gcd N$
88		eqeq1	$⊢ N \gcd R = R \gcd N \to (N \gcd R = 1 \leftrightarrow R \gcd N = 1)$
89	87 88	syl	$⊢ φ \to (N \gcd R = 1 \leftrightarrow R \gcd N = 1)$
90	89	pm5.74i	$⊢ (φ \to N \gcd R = 1) \leftrightarrow (φ \to R \gcd N = 1)$
91	5 90	mpbi	$⊢ φ \to R \gcd N = 1$
92	91 3	jca	$⊢ φ \to (R \gcd N = 1 \land P ∥ N)$
93		rpdvds	$⊢ ((R \in ℤ \land P \in ℤ \land N \in ℤ) \land (R \gcd N = 1 \land P ∥ N)) \to R \gcd P = 1$
94	84 92 93	syl2anc	$⊢ φ \to R \gcd P = 1$
95	94	adantr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to R \gcd P = 1$
96	95	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \in ℕ) \to R \gcd P = 1$
97	4	ad2antrr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \in ℕ) \to R \in ℕ$
98	63	ad2antrr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \in ℕ) \to P \in ℕ$
99		simpr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \in ℕ) \to 1^{st} (e) \in ℕ$
100		rprpwr	$⊢ (R \in ℕ \land P \in ℕ \land 1^{st} (e) \in ℕ) \to (R \gcd P = 1 \to R \gcd P^{1^{st} (e)} = 1)$
101	97 98 99 100	syl3anc	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \in ℕ) \to (R \gcd P = 1 \to R \gcd P^{1^{st} (e)} = 1)$
102	96 101	mpd	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \in ℕ) \to R \gcd P^{1^{st} (e)} = 1$
103	67	anim1i	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \neq 0) \to (1^{st} (e) \in ℕ_{0} \land 1^{st} (e) \neq 0)$
104		elnnne0	$⊢ 1^{st} (e) \in ℕ \leftrightarrow (1^{st} (e) \in ℕ_{0} \land 1^{st} (e) \neq 0)$
105	103 104	sylibr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 1^{st} (e) \neq 0) \to 1^{st} (e) \in ℕ$
106	105	ex	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to (1^{st} (e) \neq 0 \to 1^{st} (e) \in ℕ)$
107	106	necon1bd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to (\neg 1^{st} (e) \in ℕ \to 1^{st} (e) = 0)$
108	107	imp	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to 1^{st} (e) = 0$
109	108	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to P^{1^{st} (e)} = P^{0}$
110	109	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to R \gcd P^{1^{st} (e)} = R \gcd P^{0}$
111	65	zcnd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to P \in ℂ$
112	111	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to P \in ℂ$
113	112	exp0d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to P^{0} = 1$
114	113	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to R \gcd P^{0} = R \gcd 1$
115	82	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to R \in ℤ$
116		gcd1	$⊢ R \in ℤ \to R \gcd 1 = 1$
117	115 116	syl	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to R \gcd 1 = 1$
118	114 117	eqtrd	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to R \gcd P^{0} = 1$
119	110 118	eqtrd	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 1^{st} (e) \in ℕ) \to R \gcd P^{1^{st} (e)} = 1$
120	102 119	pm2.61dan	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to R \gcd P^{1^{st} (e)} = 1$
121	81 73 70	3jca	$⊢ φ \to (R \in ℤ \land \frac{N}{P} \in ℤ \land N \in ℤ)$
122	1	nnred	$⊢ φ \to N \in ℝ$
123	122	recnd	$⊢ φ \to N \in ℂ$
124	63	nnred	$⊢ φ \to P \in ℝ$
125	124	recnd	$⊢ φ \to P \in ℂ$
126	1	nngt0d	$⊢ φ \to 0 < N$
127	126	gt0ne0d	$⊢ φ \to N \neq 0$
128	123 125 127 69	ddcand	$⊢ φ \to \frac{N}{\frac{N}{P}} = P$
129	128 64	eqeltrd	$⊢ φ \to \frac{N}{\frac{N}{P}} \in ℤ$
130	63	nngt0d	$⊢ φ \to 0 < P$
131	122 124 126 130	divgt0d	$⊢ φ \to 0 < \frac{N}{P}$
132	131	gt0ne0d	$⊢ φ \to \frac{N}{P} \neq 0$
133		dvdsval2	$⊢ (\frac{N}{P} \in ℤ \land \frac{N}{P} \neq 0 \land N \in ℤ) \to ((\frac{N}{P}) ∥ N \leftrightarrow \frac{N}{\frac{N}{P}} \in ℤ)$
134	73 132 70 133	syl3anc	$⊢ φ \to ((\frac{N}{P}) ∥ N \leftrightarrow \frac{N}{\frac{N}{P}} \in ℤ)$
135	129 134	mpbird	$⊢ φ \to (\frac{N}{P}) ∥ N$
136	91 135	jca	$⊢ φ \to (R \gcd N = 1 \land (\frac{N}{P}) ∥ N)$
137		rpdvds	$⊢ ((R \in ℤ \land \frac{N}{P} \in ℤ \land N \in ℤ) \land (R \gcd N = 1 \land (\frac{N}{P}) ∥ N)) \to R \gcd (\frac{N}{P}) = 1$
138	121 136 137	syl2anc	$⊢ φ \to R \gcd (\frac{N}{P}) = 1$
139	138	adantr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to R \gcd (\frac{N}{P}) = 1$
140	139	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \in ℕ) \to R \gcd (\frac{N}{P}) = 1$
141	4	ad2antrr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \in ℕ) \to R \in ℕ$
142	73 131	jca	$⊢ φ \to (\frac{N}{P} \in ℤ \land 0 < \frac{N}{P})$
143		elnnz	$⊢ \frac{N}{P} \in ℕ \leftrightarrow (\frac{N}{P} \in ℤ \land 0 < \frac{N}{P})$
144	142 143	sylibr	$⊢ φ \to \frac{N}{P} \in ℕ$
145	144	adantr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to \frac{N}{P} \in ℕ$
146	145	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \in ℕ) \to \frac{N}{P} \in ℕ$
147		simpr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \in ℕ) \to 2^{nd} (e) \in ℕ$
148		rprpwr	$⊢ (R \in ℕ \land \frac{N}{P} \in ℕ \land 2^{nd} (e) \in ℕ) \to (R \gcd (\frac{N}{P}) = 1 \to R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1)$
149	141 146 147 148	syl3anc	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \in ℕ) \to (R \gcd (\frac{N}{P}) = 1 \to R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1)$
150	140 149	mpd	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \in ℕ) \to R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1$
151	76	anim1i	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \neq 0) \to (2^{nd} (e) \in ℕ_{0} \land 2^{nd} (e) \neq 0)$
152		elnnne0	$⊢ 2^{nd} (e) \in ℕ \leftrightarrow (2^{nd} (e) \in ℕ_{0} \land 2^{nd} (e) \neq 0)$
153	151 152	sylibr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land 2^{nd} (e) \neq 0) \to 2^{nd} (e) \in ℕ$
154	153	ex	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to (2^{nd} (e) \neq 0 \to 2^{nd} (e) \in ℕ)$
155	154	necon1bd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to (\neg 2^{nd} (e) \in ℕ \to 2^{nd} (e) = 0)$
156	155	imp	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to 2^{nd} (e) = 0$
157	156	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to {(\frac{N}{P})}^{2^{nd} (e)} = {(\frac{N}{P})}^{0}$
158	157	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = R \gcd {(\frac{N}{P})}^{0}$
159	123	adantr	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to N \in ℂ$
160	159	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to N \in ℂ$
161	111	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to P \in ℂ$
162	69	ad2antrr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to P \neq 0$
163	160 161 162	divcld	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to \frac{N}{P} \in ℂ$
164	163	exp0d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to {(\frac{N}{P})}^{0} = 1$
165	164	oveq2d	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to R \gcd {(\frac{N}{P})}^{0} = R \gcd 1$
166	158 165	eqtrd	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = R \gcd 1$
167	82	adantr	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to R \in ℤ$
168	167 116	syl	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to R \gcd 1 = 1$
169	166 168	eqtrd	$⊢ ((φ \land e \in (ℕ_{0} \times ℕ_{0})) \land \neg 2^{nd} (e) \in ℕ) \to R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1$
170	150 169	pm2.61dan	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1$
171	120 170	jca	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to (R \gcd P^{1^{st} (e)} = 1 \land R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1)$
172		rpmul	$⊢ (R \in ℤ \land P^{1^{st} (e)} \in ℤ \land {(\frac{N}{P})}^{2^{nd} (e)} \in ℤ) \to ((R \gcd P^{1^{st} (e)} = 1 \land R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1) \to R \gcd P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} = 1)$
173	82 68 77 172	syl3anc	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to ((R \gcd P^{1^{st} (e)} = 1 \land R \gcd {(\frac{N}{P})}^{2^{nd} (e)} = 1) \to R \gcd P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} = 1)$
174	171 173	mpd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to R \gcd P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} = 1$
175	83 174	eqtrd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (e)} {(\frac{N}{P})}^{2^{nd} (e)} \gcd R = 1$
176	80 175	eqtrd	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to E (e) \gcd R = 1$
177	79 176	jca	$⊢ (φ \land e \in (ℕ_{0} \times ℕ_{0})) \to (E (e) \in ℤ \land E (e) \gcd R = 1)$
178	51 177	syl	$⊢ (((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \to (E (e) \in ℤ \land E (e) \gcd R = 1)$
179	178	adantr	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to (E (e) \in ℤ \land E (e) \gcd R = 1)$
180	179	simprd	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to E (e) \gcd R = 1$
181	48 180	eqtrd	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to c \gcd R = 1$
182	179	simpld	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to E (e) \in ℤ$
183	47 182	eqeltrd	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to c \in ℤ$
184	181 183	jca	$⊢ ((((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \land e \in (ℕ_{0} \times ℕ_{0})) \land E (e) = c) \to (c \gcd R = 1 \land c \in ℤ)$
185		nfv	$⊢ Ⅎ e E (d) = c$
186		nfv	$⊢ Ⅎ d E (e) = c$
187		fveqeq2	$⊢ d = e \to (E (d) = c \leftrightarrow E (e) = c)$
188	185 186 187	cbvrexw	$⊢ \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c \leftrightarrow \exists e \in (ℕ_{0} \times ℕ_{0}) E (e) = c$
189	188	biimpi	$⊢ \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c \to \exists e \in (ℕ_{0} \times ℕ_{0}) E (e) = c$
190	189	adantl	$⊢ ((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \to \exists e \in (ℕ_{0} \times ℕ_{0}) E (e) = c$
191	184 190	r19.29a	$⊢ ((φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \land \exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c) \to (c \gcd R = 1 \land c \in ℤ)$
192	191	ex	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to (\exists d \in (ℕ_{0} \times ℕ_{0}) E (d) = c \to (c \gcd R = 1 \land c \in ℤ))$
193	45 192	mpd	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to (c \gcd R = 1 \land c \in ℤ)$
194	193	simpld	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to c \gcd R = 1$
195	9	adantr	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to R \in ℕ_{0}$
196	193	simprd	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to c \in ℤ$
197		eqid	$⊢ Unit (ℤ / R ℤ) = Unit (ℤ / R ℤ)$
198	10 197 7	znunit	$⊢ (R \in ℕ_{0} \land c \in ℤ) \to (L (c) \in Unit (ℤ / R ℤ) \leftrightarrow c \gcd R = 1)$
199	195 196 198	syl2anc	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to (L (c) \in Unit (ℤ / R ℤ) \leftrightarrow c \gcd R = 1)$
200	194 199	mpbird	$⊢ (φ \land c \in E [ℕ_{0} \times ℕ_{0}]) \to L (c) \in Unit (ℤ / R ℤ)$
201	28 200	syl	$⊢ ((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \to L (c) \in Unit (ℤ / R ℤ)$
202	201	adantr	$⊢ (((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \land L (c) = a) \to L (c) \in Unit (ℤ / R ℤ)$
203	25 202	eqeltrd	$⊢ (((φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \land c \in E [ℕ_{0} \times ℕ_{0}]) \land L (c) = a) \to a \in Unit (ℤ / R ℤ)$
204		nfv	$⊢ Ⅎ c L (b) = a$
205		nfv	$⊢ Ⅎ b L (c) = a$
206		fveqeq2	$⊢ b = c \to (L (b) = a \leftrightarrow L (c) = a)$
207	204 205 206	cbvrexw	$⊢ \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a \leftrightarrow \exists c \in E [ℕ_{0} \times ℕ_{0}] L (c) = a$
208	207	biimpi	$⊢ \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a \to \exists c \in E [ℕ_{0} \times ℕ_{0}] L (c) = a$
209	208	adantl	$⊢ (φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \to \exists c \in E [ℕ_{0} \times ℕ_{0}] L (c) = a$
210	203 209	r19.29a	$⊢ (φ \land \exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a) \to a \in Unit (ℤ / R ℤ)$
211	210	ex	$⊢ φ \to (\exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a \to a \in Unit (ℤ / R ℤ))$
212	211	adantr	$⊢ (φ \land a \in L [E [ℕ_{0} \times ℕ_{0}]]) \to (\exists b \in E [ℕ_{0} \times ℕ_{0}] L (b) = a \to a \in Unit (ℤ / R ℤ))$
213	23 212	mpd	$⊢ (φ \land a \in L [E [ℕ_{0} \times ℕ_{0}]]) \to a \in Unit (ℤ / R ℤ)$
214	213	ex	$⊢ φ \to (a \in L [E [ℕ_{0} \times ℕ_{0}]] \to a \in Unit (ℤ / R ℤ))$
215	214	ssrdv	$⊢ φ \to L [E [ℕ_{0} \times ℕ_{0}]] \subseteq Unit (ℤ / R ℤ)$
216		hashss	$⊢ (Unit (ℤ / R ℤ) \in V \land L [E [ℕ_{0} \times ℕ_{0}]] \subseteq Unit (ℤ / R ℤ)) \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|Unit (ℤ / R ℤ)\|$
217	8 215 216	syl2anc	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|Unit (ℤ / R ℤ)\|$
218	10 197	znunithash	$⊢ R \in ℕ \to \|Unit (ℤ / R ℤ)\| = ϕ (R)$
219	4 218	syl	$⊢ φ \to \|Unit (ℤ / R ℤ)\| = ϕ (R)$
220	217 219	breqtrd	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq ϕ (R)$

Metamath Proof Explorer

Theorem aks6d1c4

Proof