Theorem aks6d1c3

Description: Claim 3 of Theorem 6.1 of the AKS inequality lemma. https://www3.nd.edu/%7eandyp/notes/AKS.pdf (Contributed by metakunt, 28-Apr-2025)

	Ref	Expression
Hypotheses	aks6d1c3.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	aks6d1c3.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	aks6d1c3.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
	aks6d1c3.4	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
	aks6d1c3.5	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
	aks6d1c3.6	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
	aks6d1c3.7	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
	aks6d1c3.8	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
	aks6d1c3.9	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
Assertion	aks6d1c3	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		aks6d1c3.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		aks6d1c3.2	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3		aks6d1c3.3	⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
4		aks6d1c3.4	⊢ ( 𝜑 → 𝑅 ∈ ℕ )
5		aks6d1c3.5	⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
6		aks6d1c3.6	⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
7		aks6d1c3.7	⊢ 𝐿 = ( ℤRHom ‘ 𝑌 )
8		aks6d1c3.8	⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑅 )
9		aks6d1c3.9	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) )
10		2re	⊢ 2 ∈ ℝ
11	10	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
12		2pos	⊢ 0 < 2
13	12	a1i	⊢ ( 𝜑 → 0 < 2 )
14	1	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
15	1	nngt0d	⊢ ( 𝜑 → 0 < 𝑁 )
16		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
17		1lt2	⊢ 1 < 2
18	17	a1i	⊢ ( 𝜑 → 1 < 2 )
19	16 18	ltned	⊢ ( 𝜑 → 1 ≠ 2 )
20	19	necomd	⊢ ( 𝜑 → 2 ≠ 1 )
21	11 13 14 15 20	relogbcld	⊢ ( 𝜑 → ( 2 logb 𝑁 ) ∈ ℝ )
22	21	resqcld	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) ∈ ℝ )
23	1	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
24		odzcl	⊢ ( ( 𝑅 ∈ ℕ ∧ 𝑁 ∈ ℤ ∧ ( 𝑁 gcd 𝑅 ) = 1 ) → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
25	4 23 5 24	syl3anc	⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℕ )
26	25	nnred	⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ∈ ℝ )
27	1 2 3 4 5 6 7 8	hashscontpowcl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℕ0 )
28	27	nn0red	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ∈ ℝ )
29		nfv	⊢ Ⅎ 𝑥 𝜑
30		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
31	2 30	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
32	31	nnzd	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ ℤ )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ℕ0 ) → 𝑃 ∈ ℤ )
35		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
36	34 35	zexpcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑃 ↑ 𝑘 ) ∈ ℤ )
37	31	nnne0d	⊢ ( 𝜑 → 𝑃 ≠ 0 )
38		dvdsval2	⊢ ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℤ ) )
39	32 37 23 38	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∥ 𝑁 ↔ ( 𝑁 / 𝑃 ) ∈ ℤ ) )
40	3 39	mpbid	⊢ ( 𝜑 → ( 𝑁 / 𝑃 ) ∈ ℤ )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℤ )
42	41	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℤ )
43		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ℕ0 ) → 𝑙 ∈ ℕ0 )
44	42 43	zexpcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ∈ ℤ )
45	36 44	zmulcld	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ∈ ℤ )
46	45	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑙 ∈ ℕ0 ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ∈ ℤ )
47	46	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 ∀ 𝑙 ∈ ℕ0 ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ∈ ℤ )
48	6	fmpo	⊢ ( ∀ 𝑘 ∈ ℕ0 ∀ 𝑙 ∈ ℕ0 ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) ∈ ℤ ↔ 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℤ )
49	47 48	sylib	⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℤ )
50	49	ffund	⊢ ( 𝜑 → Fun 𝐸 )
51	49	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ℕ0 × ℕ0 ) ) → ( 𝐸 ‘ 𝑥 ) ∈ ℤ )
52	29 50 51	funimassd	⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ )
53	49	ffnd	⊢ ( 𝜑 → 𝐸 Fn ( ℕ0 × ℕ0 ) )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐸 Fn ( ℕ0 × ℕ0 ) )
55		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑖 ∈ ℕ0 )
56	55 55	opelxpd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⟨ 𝑖 , 𝑖 ⟩ ∈ ( ℕ0 × ℕ0 ) )
57	54 56 56	fnfvimad	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝐸 ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
58		vex	⊢ 𝑘 ∈ V
59		vex	⊢ 𝑙 ∈ V
60	58 59	op1std	⊢ ( 𝑞 = ⟨ 𝑘 , 𝑙 ⟩ → ( 1st ‘ 𝑞 ) = 𝑘 )
61	60	oveq2d	⊢ ( 𝑞 = ⟨ 𝑘 , 𝑙 ⟩ → ( 𝑃 ↑ ( 1st ‘ 𝑞 ) ) = ( 𝑃 ↑ 𝑘 ) )
62	58 59	op2ndd	⊢ ( 𝑞 = ⟨ 𝑘 , 𝑙 ⟩ → ( 2nd ‘ 𝑞 ) = 𝑙 )
63	62	oveq2d	⊢ ( 𝑞 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑞 ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) )
64	61 63	oveq12d	⊢ ( 𝑞 = ⟨ 𝑘 , 𝑙 ⟩ → ( ( 𝑃 ↑ ( 1st ‘ 𝑞 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑞 ) ) ) = ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
65	64	mpompt	⊢ ( 𝑞 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑞 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑞 ) ) ) ) = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
66	6 65	eqtr4i	⊢ 𝐸 = ( 𝑞 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑞 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑞 ) ) ) )
67	66	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝐸 = ( 𝑞 ∈ ( ℕ0 × ℕ0 ) ↦ ( ( 𝑃 ↑ ( 1st ‘ 𝑞 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑞 ) ) ) ) )
68		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑞 = ⟨ 𝑖 , 𝑖 ⟩ ) → 𝑞 = ⟨ 𝑖 , 𝑖 ⟩ )
69	68	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑞 = ⟨ 𝑖 , 𝑖 ⟩ ) → ( 1st ‘ 𝑞 ) = ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) )
70	69	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑞 = ⟨ 𝑖 , 𝑖 ⟩ ) → ( 𝑃 ↑ ( 1st ‘ 𝑞 ) ) = ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) )
71	68	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑞 = ⟨ 𝑖 , 𝑖 ⟩ ) → ( 2nd ‘ 𝑞 ) = ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) )
72	71	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑞 = ⟨ 𝑖 , 𝑖 ⟩ ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑞 ) ) = ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) )
73	70 72	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) ∧ 𝑞 = ⟨ 𝑖 , 𝑖 ⟩ ) → ( ( 𝑃 ↑ ( 1st ‘ 𝑞 ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ 𝑞 ) ) ) = ( ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) ) )
74		opelxp	⊢ ( ⟨ 𝑖 , 𝑖 ⟩ ∈ ( ℕ0 × ℕ0 ) ↔ ( 𝑖 ∈ ℕ0 ∧ 𝑖 ∈ ℕ0 ) )
75	56 74	sylib	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑖 ∈ ℕ0 ∧ 𝑖 ∈ ℕ0 ) )
76	75 74	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ⟨ 𝑖 , 𝑖 ⟩ ∈ ( ℕ0 × ℕ0 ) )
77	32	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑃 ∈ ℤ )
78		xp1st	⊢ ( ⟨ 𝑖 , 𝑖 ⟩ ∈ ( ℕ0 × ℕ0 ) → ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ∈ ℕ0 )
79	56 78	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ∈ ℕ0 )
80	77 79	zexpcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) ∈ ℤ )
81	40	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℤ )
82		xp2nd	⊢ ( ⟨ 𝑖 , 𝑖 ⟩ ∈ ( ℕ0 × ℕ0 ) → ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ∈ ℕ0 )
83	56 82	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ∈ ℕ0 )
84	81 83	zexpcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) ∈ ℤ )
85	80 84	zmulcld	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) ) ∈ ℤ )
86	67 73 76 85	fvmptd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝐸 ‘ ⟨ 𝑖 , 𝑖 ⟩ ) = ( ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) ) )
87		vex	⊢ 𝑖 ∈ V
88	87 87	op1st	⊢ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) = 𝑖
89	88	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) = 𝑖 )
90	89	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) = ( 𝑃 ↑ 𝑖 ) )
91	87 87	op2nd	⊢ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) = 𝑖
92	91	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) = 𝑖 )
93	92	oveq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) = ( ( 𝑁 / 𝑃 ) ↑ 𝑖 ) )
94	90 93	oveq12d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) ) = ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑖 ) ) )
95	14	recnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
96	95	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑁 ∈ ℂ )
97	77	zcnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑃 ∈ ℂ )
98	37	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑃 ≠ 0 )
99	96 97 98	divcan2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑃 · ( 𝑁 / 𝑃 ) ) = 𝑁 )
100	99	eqcomd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → 𝑁 = ( 𝑃 · ( 𝑁 / 𝑃 ) ) )
101	100	oveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑖 ) = ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑖 ) )
102	81	zcnd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 / 𝑃 ) ∈ ℂ )
103	97 102 55	mulexpd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑃 · ( 𝑁 / 𝑃 ) ) ↑ 𝑖 ) = ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑖 ) ) )
104	101 103	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑃 ↑ 𝑖 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑖 ) ) = ( 𝑁 ↑ 𝑖 ) )
105	94 104	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝑃 ↑ ( 1st ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) · ( ( 𝑁 / 𝑃 ) ↑ ( 2nd ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ) ) = ( 𝑁 ↑ 𝑖 ) )
106	86 105	eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝐸 ‘ ⟨ 𝑖 , 𝑖 ⟩ ) = ( 𝑁 ↑ 𝑖 ) )
107	106	eleq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( ( 𝐸 ‘ ⟨ 𝑖 , 𝑖 ⟩ ) ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ↔ ( 𝑁 ↑ 𝑖 ) ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
108	57 107	mpbid	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑖 ) ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
109	108	ralrimiva	⊢ ( 𝜑 → ∀ 𝑖 ∈ ℕ0 ( 𝑁 ↑ 𝑖 ) ∈ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) )
110	52 1 109 4 5 7 8	hashscontpow	⊢ ( 𝜑 → ( ( odℤ ‘ 𝑅 ) ‘ 𝑁 ) ≤ ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
111	22 26 28 9 110	ltletrd	⊢ ( 𝜑 → ( ( 2 logb 𝑁 ) ↑ 2 ) < ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )