bposlem6 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > bposlem6		GIF version

Theorem bposlem6 16245

Description: Lemma for bpos 16249. By using the various bounds at our disposal, arrive at an inequality that is false for 𝑁 large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)

**Hypotheses**
Ref	Expression
bpos.1	⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘5))
bpos.2	⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
bpos.3	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
bpos.4	⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))
bpos.5	⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))

**Assertion**
Ref	Expression
bposlem6	⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))

Distinct variable groups: 𝐹,𝑝 𝑛,𝑝,𝐾 𝑀,𝑝 𝑛,𝑁,𝑝 𝜑,𝑛,𝑝 Allowed substitution hints: 𝐹(𝑛) 𝑀(𝑛)

Proof of Theorem bposlem6 Dummy variable 𝑞 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4nn 9473	. . . . 5 ⊢ 4 ∈ ℕ
2		5nn 9474	. . . . . . 7 ⊢ 5 ∈ ℕ
3		bpos.1	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘5))
4		eluznn 10010	. . . . . . 7 ⊢ ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘5)) → 𝑁 ∈ ℕ)
5	2, 3, 4	sylancr 418	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnnn0d 9625	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
7		nnexpcl 11004	. . . . 5 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (4↑𝑁) ∈ ℕ)
8	1, 6, 7	sylancr 418	. . . 4 ⊢ (𝜑 → (4↑𝑁) ∈ ℕ)
9	8	nnred 9320	. . 3 ⊢ (𝜑 → (4↑𝑁) ∈ ℝ)
10	9, 5	nndivred 9357	. 2 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) ∈ ℝ)
11		fzctr 10551	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0...(2 · 𝑁)))
12	6, 11	syl 14	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (0...(2 · 𝑁)))
13		bccl2 11222	. . . 4 ⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
14	12, 13	syl 14	. . 3 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
15	14	nnred 9320	. 2 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ)
16		2nn 9471	. . . . . . 7 ⊢ 2 ∈ ℕ
17		nnmulcl 9328	. . . . . . 7 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
18	16, 5, 17	sylancr 418	. . . . . 6 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
19	18	nnrpd 10106	. . . . 5 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ⁺)
20	18	nnred 9320	. . . . . . . 8 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
21	19	rpge0d 10112	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
22	20, 21	resqrtcld 11946	. . . . . . 7 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
23		3nn 9472	. . . . . . 7 ⊢ 3 ∈ ℕ
24		nndivre 9343	. . . . . . 7 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
25	22, 23, 24	sylancl 417	. . . . . 6 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
26		2re 9377	. . . . . 6 ⊢ 2 ∈ ℝ
27		readdcl 8306	. . . . . 6 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
28	25, 26, 27	sylancl 417	. . . . 5 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
29	19, 28	rpcxpcld 16098	. . . 4 ⊢ (𝜑 → ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ⁺)
30	29	rpred 10108	. . 3 ⊢ (𝜑 → ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
31		2rp 10070	. . . . 5 ⊢ 2 ∈ ℝ⁺
32		nnmulcl 9328	. . . . . . . . 9 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (4 · 𝑁) ∈ ℕ)
33	1, 5, 32	sylancr 418	. . . . . . . 8 ⊢ (𝜑 → (4 · 𝑁) ∈ ℕ)
34	33	nnred 9320	. . . . . . 7 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
35		nndivre 9343	. . . . . . 7 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
36	34, 23, 35	sylancl 417	. . . . . 6 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
37		5re 9386	. . . . . 6 ⊢ 5 ∈ ℝ
38		resubcl 8592	. . . . . 6 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
39	36, 37, 38	sylancl 417	. . . . 5 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
40		rpcxpcl 16068	. . . . 5 ⊢ ((2 ∈ ℝ⁺ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℝ) → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ⁺)
41	31, 39, 40	sylancr 418	. . . 4 ⊢ (𝜑 → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ⁺)
42	41	rpred 10108	. . 3 ⊢ (𝜑 → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ)
43	30, 42	remulcld 8357	. 2 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))) ∈ ℝ)
44		df-5 9369	. . . . 5 ⊢ 5 = (4 + 1)
45		4z 9679	. . . . . 6 ⊢ 4 ∈ ℤ
46		uzid 9946	. . . . . 6 ⊢ (4 ∈ ℤ → 4 ∈ (ℤ_≥‘4))
47		peano2uz 9993	. . . . . 6 ⊢ (4 ∈ (ℤ_≥‘4) → (4 + 1) ∈ (ℤ_≥‘4))
48	45, 46, 47	mp2b 8	. . . . 5 ⊢ (4 + 1) ∈ (ℤ_≥‘4)
49	44, 48	eqeltri 2311	. . . 4 ⊢ 5 ∈ (ℤ_≥‘4)
50		eqid 2238	. . . . 5 ⊢ (ℤ_≥‘4) = (ℤ_≥‘4)
51	50	uztrn2 9950	. . . 4 ⊢ ((5 ∈ (ℤ_≥‘4) ∧ 𝑁 ∈ (ℤ_≥‘5)) → 𝑁 ∈ (ℤ_≥‘4))
52	49, 3, 51	sylancr 418	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘4))
53		bclbnd 16236	. . 3 ⊢ (𝑁 ∈ (ℤ_≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
54	52, 53	syl 14	. 2 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁))
55		bpos.3	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt ((2 · 𝑁)C𝑁))), 1))
56		id 19	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℙ → 𝑛 ∈ ℙ)
57		pccl 13101	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
58	56, 14, 57	syl2anr 290	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
59	58	ralrimiva 2623	. . . . . . . 8 ⊢ (𝜑 → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
60	55, 59	pcmptcl 13144	. . . . . . 7 ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
61	60	simprd 114	. . . . . 6 ⊢ (𝜑 → seq1( · , 𝐹):ℕ⟶ℕ)
62		bpos.2	. . . . . . . . 9 ⊢ (𝜑 → ¬ ∃𝑝 ∈ ℙ (𝑁 < 𝑝 ∧ 𝑝 ≤ (2 · 𝑁)))
63		bpos.4	. . . . . . . . 9 ⊢ 𝐾 = (⌊‘((2 · 𝑁) / 3))
64		bpos.5	. . . . . . . . 9 ⊢ 𝑀 = (⌊‘(√‘(2 · 𝑁)))
65	3, 62, 55, 63, 64	bposlem4 16243	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (3...𝐾))
66		elfzuz 10435	. . . . . . . 8 ⊢ (𝑀 ∈ (3...𝐾) → 𝑀 ∈ (ℤ_≥‘3))
67	65, 66	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘3))
68		eluznn 10010	. . . . . . 7 ⊢ ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ_≥‘3)) → 𝑀 ∈ ℕ)
69	23, 67, 68	sylancr 418	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
70	61, 69	ffvelcdmd 5844	. . . . 5 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
71	70	nnred 9320	. . . 4 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
72		2z 9677	. . . . . . . . 9 ⊢ 2 ∈ ℤ
73	18	nnzd 9772	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℤ)
74		znq 10034	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℤ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℚ)
75	73, 23, 74	sylancl 417	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℚ)
76	75	flqcld 10725	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((2 · 𝑁) / 3)) ∈ ℤ)
77	63, 76	eqeltrid 2325	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℤ)
78		zmulcl 9703	. . . . . . . . 9 ⊢ ((2 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (2 · 𝐾) ∈ ℤ)
79	72, 77, 78	sylancr 418	. . . . . . . 8 ⊢ (𝜑 → (2 · 𝐾) ∈ ℤ)
80	2	nnzi 9670	. . . . . . . 8 ⊢ 5 ∈ ℤ
81		zsubcl 9690	. . . . . . . 8 ⊢ (((2 · 𝐾) ∈ ℤ ∧ 5 ∈ ℤ) → ((2 · 𝐾) − 5) ∈ ℤ)
82	79, 80, 81	sylancl 417	. . . . . . 7 ⊢ (𝜑 → ((2 · 𝐾) − 5) ∈ ℤ)
83	82	zred 9773	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐾) − 5) ∈ ℝ)
84		rpcxpcl 16068	. . . . . 6 ⊢ ((2 ∈ ℝ⁺ ∧ ((2 · 𝐾) − 5) ∈ ℝ) → (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ⁺)
85	31, 83, 84	sylancr 418	. . . . 5 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ⁺)
86	85	rpred 10108	. . . 4 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ)
87	71, 86	remulcld 8357	. . 3 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))) ∈ ℝ)
88	3, 62, 55, 63	bposlem3 16242	. . . 4 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
89		elfzuz3 10436	. . . . . . . . . 10 ⊢ (𝑀 ∈ (3...𝐾) → 𝐾 ∈ (ℤ_≥‘𝑀))
90	65, 89	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘𝑀))
91	55, 59, 69, 90	pcmptdvds 13147	. . . . . . . 8 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾))
92	70	nnzd 9772	. . . . . . . . 9 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ)
93	70	nnne0d 9352	. . . . . . . . 9 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0)
94		uztrn 9949	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ (ℤ_≥‘𝑀) ∧ 𝑀 ∈ (ℤ_≥‘3)) → 𝐾 ∈ (ℤ_≥‘3))
95	90, 67, 94	syl2anc 415	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘3))
96		eluznn 10010	. . . . . . . . . . . 12 ⊢ ((3 ∈ ℕ ∧ 𝐾 ∈ (ℤ_≥‘3)) → 𝐾 ∈ ℕ)
97	23, 95, 96	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ)
98	61, 97	ffvelcdmd 5844	. . . . . . . . . 10 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ)
99	98	nnzd 9772	. . . . . . . . 9 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℤ)
100		dvdsval2 12576	. . . . . . . . 9 ⊢ (((seq1( · , 𝐹)‘𝑀) ∈ ℤ ∧ (seq1( · , 𝐹)‘𝑀) ≠ 0 ∧ (seq1( · , 𝐹)‘𝐾) ∈ ℤ) → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
101	92, 93, 99, 100	syl3anc 1278	. . . . . . . 8 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾) ↔ ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ))
102	91, 101	mpbid 147	. . . . . . 7 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ)
103	102	zred 9773	. . . . . 6 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℝ)
104		nnq 10043	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
105	69, 104	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℚ)
106		zq 10036	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℚ)
107	77, 106	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℚ)
108		eluzle 9944	. . . . . . . . . 10 ⊢ (𝐾 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝐾)
109	90, 108	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
110		efchtqdvds 16194	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℚ ∧ 𝐾 ∈ ℚ ∧ 𝑀 ≤ 𝐾) → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
111	105, 107, 109, 110	syl3anc 1278	. . . . . . . 8 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
112		efchtqcl 16175	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℚ → (exp‘(θ‘𝑀)) ∈ ℕ)
113	105, 112	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∈ ℕ)
114	113	nnzd 9772	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∈ ℤ)
115	113	nnne0d 9352	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ≠ 0)
116		efchtqcl 16175	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℚ → (exp‘(θ‘𝐾)) ∈ ℕ)
117	107, 116	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝐾)) ∈ ℕ)
118	117	nnzd 9772	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝐾)) ∈ ℤ)
119		dvdsval2 12576	. . . . . . . . 9 ⊢ (((exp‘(θ‘𝑀)) ∈ ℤ ∧ (exp‘(θ‘𝑀)) ≠ 0 ∧ (exp‘(θ‘𝐾)) ∈ ℤ) → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
120	114, 115, 118, 119	syl3anc 1278	. . . . . . . 8 ⊢ (𝜑 → ((exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ))
121	111, 120	mpbid 147	. . . . . . 7 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ)
122	121	zred 9773	. . . . . 6 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℝ)
123	18	nnnn0d 9625	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ₀)
124		sqrtrirr 13008	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 𝑁) ∈ ℕ₀ → ((√‘(2 · 𝑁)) ∈ ℚ ∨ ((√‘(2 · 𝑁)) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (√‘(2 · 𝑁)) # 𝑞)))
125	123, 124	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘(2 · 𝑁)) ∈ ℚ ∨ ((√‘(2 · 𝑁)) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (√‘(2 · 𝑁)) # 𝑞)))
126		prmz 12908	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
127		flaplt 10733	. . . . . . . . . . . . . . . . . 18 ⊢ ((((√‘(2 · 𝑁)) ∈ ℚ ∨ ((√‘(2 · 𝑁)) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (√‘(2 · 𝑁)) # 𝑞)) ∧ 𝑝 ∈ ℤ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
128	125, 126, 127	syl2an 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
129	64	breq1i 4137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝)
130	128, 129	bitr4di 198	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ 𝑀 < 𝑝))
131	69	nnzd 9772	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
132		zltnle 9695	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀))
133	131, 126, 132	syl2an 289	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀))
134	130, 133	bitrd 188	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀))
135		bposlem1 16240	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
136	5, 135	sylan 283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
137	126	zred 9773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
138	137	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
139		id 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
140		pccl 13101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
141	139, 14, 140	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
142	138, 141	reexpcld 11143	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
143	20	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
144	138	resqcld 11152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑2) ∈ ℝ)
145		lelttr 8415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ ∧ (2 · 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
146	142, 143, 144, 145	syl3anc 1278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁) ∧ (2 · 𝑁) < (𝑝↑2)) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
147	136, 146	mpand 433	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((2 · 𝑁) < (𝑝↑2) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
148		resqrtth 11813	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
149	20, 21, 148	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
150	149	breq1d 4140	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
151	150	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
152	141	nn0zd 9771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
153	72	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈ ℤ)
154		prmgt1 12930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℙ → 1 < 𝑝)
155	154	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
156	138, 152, 153, 155	ltexp2d 16107	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) < (𝑝↑2)))
157	147, 151, 156	3imtr4d 203	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2))
158		df-2 9366	. . . . . . . . . . . . . . . . . 18 ⊢ 2 = (1 + 1)
159	158	breq2i 4138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 pCnt ((2 · 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1))
160	157, 159	imbitrdi 161	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
161	22	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (√‘(2 · 𝑁)) ∈ ℝ)
162	20, 21	sqrtge0d 11949	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (√‘(2 · 𝑁)))
163	162	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤ (√‘(2 · 𝑁)))
164		prmnn 12907	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
165	164	nnrpd 10106	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ⁺)
166	165	rpge0d 10112	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℙ → 0 ≤ 𝑝)
167	166	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤ 𝑝)
168	161, 138, 163, 167	lt2sqd 11157	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ((√‘(2 · 𝑁))↑2) < (𝑝↑2)))
169		1z 9675	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
170		zleltp1 9705	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ ∧ 1 ∈ ℤ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
171	152, 169, 170	sylancl 417	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1 ↔ (𝑝 pCnt ((2 · 𝑁)C𝑁)) < (1 + 1)))
172	160, 168, 171	3imtr4d 203	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
173	134, 172	sylbird 170	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (¬ 𝑝 ≤ 𝑀 → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1))
174	173	imp 124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ 𝑝 ≤ 𝑀) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
175	174	adantrl 482	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ≤ 1)
176		iftrue 3645	. . . . . . . . . . . . 13 ⊢ ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
177	176	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
178		iftrue 3645	. . . . . . . . . . . . 13 ⊢ ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 1)
179	178	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 1)
180	175, 177, 179	3brtr4d 4162	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0))
181		0le0 9396	. . . . . . . . . . . . 13 ⊢ 0 ≤ 0
182		iffalse 3648	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) = 0)
183		iffalse 3648	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) = 0)
184	182, 183	breq12d 4143	. . . . . . . . . . . . 13 ⊢ (¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → (if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0) ↔ 0 ≤ 0))
185	181, 184	mpbiri 168	. . . . . . . . . . . 12 ⊢ (¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0))
186	185	adantl 277	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ ¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0))
187		zdcle 9726	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝑝 ≤ 𝐾)
188	126, 77, 187	syl2anr 290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → DECID 𝑝 ≤ 𝐾)
189		zdcle 9726	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑝 ≤ 𝑀)
190	126, 131, 189	syl2anr 290	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → DECID 𝑝 ≤ 𝑀)
191		dcn 854	. . . . . . . . . . . . . 14 ⊢ (DECID 𝑝 ≤ 𝑀 → DECID ¬ 𝑝 ≤ 𝑀)
192	190, 191	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → DECID ¬ 𝑝 ≤ 𝑀)
193	188, 192	dcand 945	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → DECID (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀))
194		exmiddc 848	. . . . . . . . . . . 12 ⊢ (DECID (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) → ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) ∨ ¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)))
195	193, 194	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀) ∨ ¬ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)))
196	180, 186, 195	mpjaodan 810	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0))
197	59	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ (𝑛 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
198	69	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑀 ∈ ℕ)
199		simpr 110	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ)
200		oveq1 6092	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
201	90	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐾 ∈ (ℤ_≥‘𝑀))
202	55, 197, 198, 199, 200, 201	pcmpt2 13146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0))
203		eqid 2238	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
204	203	prmorcht 16211	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
205	97, 204	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
206	203	prmorcht 16211	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
207	69, 206	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
208	205, 207	oveq12d 6103	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
209	208	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) = ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀)))
210	209	oveq2d 6101	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))))
211		nncn 9315	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
212	211	exp1d 11121	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
213	212	ifeq1d 3658	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1))
214	213	mpteq2ia 4217	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
215	214	eqcomi 2242	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1))
216		1nn0 9584	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℕ₀
217	216	a1i 9	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ ℙ) → 1 ∈ ℕ₀)
218	217	ralrimiva 2623	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑛 ∈ ℙ 1 ∈ ℕ₀)
219	218	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ∀𝑛 ∈ ℙ 1 ∈ ℕ₀)
220		eqidd 2239	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑝 → 1 = 1)
221	215, 219, 198, 199, 220, 201	pcmpt2 13146	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0))
222	210, 221	eqtrd 2271	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0))
223	196, 202, 222	3brtr4d 4162	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
224	223	ralrimiva 2623	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
225		pc2dvds 13132	. . . . . . . . 9 ⊢ ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
226	102, 121, 225	syl2anc 415	. . . . . . . 8 ⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))))
227	224, 226	mpbird 167	. . . . . . 7 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
228	117	nnred 9320	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝐾)) ∈ ℝ)
229	113	nnred 9320	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∈ ℝ)
230	117	nngt0d 9351	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (exp‘(θ‘𝐾)))
231	113	nngt0d 9351	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (exp‘(θ‘𝑀)))
232	228, 229, 230, 231	divgt0d 9268	. . . . . . . . 9 ⊢ (𝜑 → 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
233		elnnz 9659	. . . . . . . . 9 ⊢ (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ ↔ (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ ∧ 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
234	121, 232, 233	sylanbrc 421	. . . . . . . 8 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ)
235		dvdsle 12630	. . . . . . . 8 ⊢ ((((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℤ ∧ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
236	102, 234, 235	syl2anc 415	. . . . . . 7 ⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∥ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
237	227, 236	mpd 13	. . . . . 6 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ≤ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
238		nndivre 9343	. . . . . . . 8 ⊢ (((exp‘(θ‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
239	228, 1, 238	sylancl 417	. . . . . . 7 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
240		4re 9384	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
241	240	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 4 ∈ ℝ)
242		6re 9388	. . . . . . . . . 10 ⊢ 6 ∈ ℝ
243	242	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 6 ∈ ℝ)
244		4lt6 9490	. . . . . . . . . 10 ⊢ 4 < 6
245	244	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 4 < 6)
246		cht3 16206	. . . . . . . . . . . 12 ⊢ (θ‘3) = (log‘6)
247	246	fveq2i 5698	. . . . . . . . . . 11 ⊢ (exp‘(θ‘3)) = (exp‘(log‘6))
248		6pos 9408	. . . . . . . . . . . . 13 ⊢ 0 < 6
249	242, 248	elrpii 10068	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ⁺
250		reeflog 16024	. . . . . . . . . . . 12 ⊢ (6 ∈ ℝ⁺ → (exp‘(log‘6)) = 6)
251	249, 250	ax-mp 5	. . . . . . . . . . 11 ⊢ (exp‘(log‘6)) = 6
252	247, 251	eqtri 2259	. . . . . . . . . 10 ⊢ (exp‘(θ‘3)) = 6
253		3z 9678	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℤ
254		zq 10036	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℤ → 3 ∈ ℚ)
255	253, 254	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℚ
256	255	a1i 9	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ∈ ℚ)
257		eluzle 9944	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (ℤ_≥‘3) → 3 ≤ 𝑀)
258	67, 257	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ 𝑀)
259		chtqwordi 16192	. . . . . . . . . . . 12 ⊢ ((3 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 3 ≤ 𝑀) → (θ‘3) ≤ (θ‘𝑀))
260	256, 105, 258, 259	syl3anc 1278	. . . . . . . . . . 11 ⊢ (𝜑 → (θ‘3) ≤ (θ‘𝑀))
261		chtqcl 16173	. . . . . . . . . . . . 13 ⊢ (3 ∈ ℚ → (θ‘3) ∈ ℝ)
262	255, 261	ax-mp 5	. . . . . . . . . . . 12 ⊢ (θ‘3) ∈ ℝ
263		chtqcl 16173	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℚ → (θ‘𝑀) ∈ ℝ)
264	105, 263	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (θ‘𝑀) ∈ ℝ)
265		efle 15936	. . . . . . . . . . . 12 ⊢ (((θ‘3) ∈ ℝ ∧ (θ‘𝑀) ∈ ℝ) → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
266	262, 264, 265	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → ((θ‘3) ≤ (θ‘𝑀) ↔ (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀))))
267	260, 266	mpbid 147	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘3)) ≤ (exp‘(θ‘𝑀)))
268	252, 267	eqbrtrrid 4166	. . . . . . . . 9 ⊢ (𝜑 → 6 ≤ (exp‘(θ‘𝑀)))
269	241, 243, 229, 245, 268	ltletrd 8753	. . . . . . . 8 ⊢ (𝜑 → 4 < (exp‘(θ‘𝑀)))
270		4pos 9404	. . . . . . . . . 10 ⊢ 0 < 4
271	270	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 0 < 4)
272		ltdiv2 9220	. . . . . . . . 9 ⊢ (((4 ∈ ℝ ∧ 0 < 4) ∧ ((exp‘(θ‘𝑀)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝑀))) ∧ ((exp‘(θ‘𝐾)) ∈ ℝ ∧ 0 < (exp‘(θ‘𝐾)))) → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
273	241, 271, 229, 231, 228, 230, 272	syl222anc 1294	. . . . . . . 8 ⊢ (𝜑 → (4 < (exp‘(θ‘𝑀)) ↔ ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4)))
274	269, 273	mpbid 147	. . . . . . 7 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < ((exp‘(θ‘𝐾)) / 4))
275	26	a1i 9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 ∈ ℝ)
276		3re 9381	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℝ
277	276	a1i 9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 3 ∈ ℝ)
278	77	zred 9773	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ ℝ)
279		2lt3 9480	. . . . . . . . . . . . . 14 ⊢ 2 < 3
280	279	a1i 9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 < 3)
281	69	nnred 9320	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ)
282	277, 281, 278, 258, 109	letrd 8452	. . . . . . . . . . . . 13 ⊢ (𝜑 → 3 ≤ 𝐾)
283	275, 277, 278, 280, 282	ltletrd 8753	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 < 𝐾)
284		chtqub 16225	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℚ ∧ 2 < 𝐾) → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
285	107, 283, 284	syl2anc 415	. . . . . . . . . . 11 ⊢ (𝜑 → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
286		chtqcl 16173	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℚ → (θ‘𝐾) ∈ ℝ)
287	107, 286	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (θ‘𝐾) ∈ ℝ)
288		relogcl 16023	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
289	31, 288	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (log‘2) ∈ ℝ
290		zsubcl 9690	. . . . . . . . . . . . . . 15 ⊢ (((2 · 𝐾) ∈ ℤ ∧ 3 ∈ ℤ) → ((2 · 𝐾) − 3) ∈ ℤ)
291	79, 253, 290	sylancl 417	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 𝐾) − 3) ∈ ℤ)
292	291	zred 9773	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐾) − 3) ∈ ℝ)
293		remulcl 8308	. . . . . . . . . . . . 13 ⊢ (((log‘2) ∈ ℝ ∧ ((2 · 𝐾) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
294	289, 292, 293	sylancr 418	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
295		eflt 15935	. . . . . . . . . . . 12 ⊢ (((θ‘𝐾) ∈ ℝ ∧ ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ) → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
296	287, 294, 295	syl2anc 415	. . . . . . . . . . 11 ⊢ (𝜑 → ((θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)) ↔ (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3)))))
297	285, 296	mpbid 147	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝐾)) < (exp‘((log‘2) · ((2 · 𝐾) − 3))))
298		reexplog 16033	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℝ⁺ ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
299	31, 291, 298	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘(((2 · 𝐾) − 3) · (log‘2))))
300	291	zcnd 9774	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐾) − 3) ∈ ℂ)
301	289	recni 8339	. . . . . . . . . . . . 13 ⊢ (log‘2) ∈ ℂ
302		mulcom 8309	. . . . . . . . . . . . 13 ⊢ ((((2 · 𝐾) − 3) ∈ ℂ ∧ (log‘2) ∈ ℂ) → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
303	300, 301, 302	sylancl 417	. . . . . . . . . . . 12 ⊢ (𝜑 → (((2 · 𝐾) − 3) · (log‘2)) = ((log‘2) · ((2 · 𝐾) − 3)))
304	303	fveq2d 5699	. . . . . . . . . . 11 ⊢ (𝜑 → (exp‘(((2 · 𝐾) − 3) · (log‘2))) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
305	299, 304	eqtrd 2271	. . . . . . . . . 10 ⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) = (exp‘((log‘2) · ((2 · 𝐾) − 3))))
306	297, 305	breqtrrd 4158	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝐾)) < (2↑((2 · 𝐾) − 3)))
307		3p2e5 9449	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
308	307	oveq1i 6095	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 2) = (5 − 2)
309		3cn 9382	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
310		2cn 9378	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
311	309, 310	pncan3oi 8544	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 2) = 3
312	308, 311	eqtr3i 2261	. . . . . . . . . . . . . 14 ⊢ (5 − 2) = 3
313	312	oveq2i 6096	. . . . . . . . . . . . 13 ⊢ ((2 · 𝐾) − (5 − 2)) = ((2 · 𝐾) − 3)
314	79	zcnd 9774	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝐾) ∈ ℂ)
315		5cn 9387	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℂ
316		subsub 8558	. . . . . . . . . . . . . . 15 ⊢ (((2 · 𝐾) ∈ ℂ ∧ 5 ∈ ℂ ∧ 2 ∈ ℂ) → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
317	315, 310, 316	mp3an23 1370	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝐾) ∈ ℂ → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
318	314, 317	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐾) − (5 − 2)) = (((2 · 𝐾) − 5) + 2))
319	313, 318	eqtr3id 2285	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝐾) − 3) = (((2 · 𝐾) − 5) + 2))
320	319	oveq2d 6101	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 3)) = (2↑_𝑐(((2 · 𝐾) − 5) + 2)))
321		cxpexpnn 16061	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℕ ∧ ((2 · 𝐾) − 3) ∈ ℤ) → (2↑_𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
322	16, 291, 321	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 3)) = (2↑((2 · 𝐾) − 3)))
323	82	zcnd 9774	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝐾) − 5) ∈ ℂ)
324		rpcxpadd 16070	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ⁺ ∧ ((2 · 𝐾) − 5) ∈ ℂ ∧ 2 ∈ ℂ) → (2↑_𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑_𝑐((2 · 𝐾) − 5)) · (2↑_𝑐2)))
325	31, 310, 324	mp3an13 1369	. . . . . . . . . . . 12 ⊢ (((2 · 𝐾) − 5) ∈ ℂ → (2↑_𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑_𝑐((2 · 𝐾) − 5)) · (2↑_𝑐2)))
326	323, 325	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑_𝑐(((2 · 𝐾) − 5) + 2)) = ((2↑_𝑐((2 · 𝐾) − 5)) · (2↑_𝑐2)))
327	320, 322, 326	3eqtr3d 2279	. . . . . . . . . 10 ⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑_𝑐((2 · 𝐾) − 5)) · (2↑_𝑐2)))
328		cxpexpnn 16061	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ ∧ 2 ∈ ℤ) → (2↑_𝑐2) = (2↑2))
329	16, 72, 328	mp2an 430	. . . . . . . . . . . 12 ⊢ (2↑_𝑐2) = (2↑2)
330		sq2 11087	. . . . . . . . . . . 12 ⊢ (2↑2) = 4
331	329, 330	eqtri 2259	. . . . . . . . . . 11 ⊢ (2↑_𝑐2) = 4
332	331	oveq2i 6096	. . . . . . . . . 10 ⊢ ((2↑_𝑐((2 · 𝐾) − 5)) · (2↑_𝑐2)) = ((2↑_𝑐((2 · 𝐾) − 5)) · 4)
333	327, 332	eqtrdi 2287	. . . . . . . . 9 ⊢ (𝜑 → (2↑((2 · 𝐾) − 3)) = ((2↑_𝑐((2 · 𝐾) − 5)) · 4))
334	306, 333	breqtrd 4156	. . . . . . . 8 ⊢ (𝜑 → (exp‘(θ‘𝐾)) < ((2↑_𝑐((2 · 𝐾) − 5)) · 4))
335	240, 270	pm3.2i 272	. . . . . . . . . 10 ⊢ (4 ∈ ℝ ∧ 0 < 4)
336	335	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → (4 ∈ ℝ ∧ 0 < 4))
337		ltdivmul2 9211	. . . . . . . . 9 ⊢ (((exp‘(θ‘𝐾)) ∈ ℝ ∧ (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → (((exp‘(θ‘𝐾)) / 4) < (2↑_𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑_𝑐((2 · 𝐾) − 5)) · 4)))
338	228, 86, 336, 337	syl3anc 1278	. . . . . . . 8 ⊢ (𝜑 → (((exp‘(θ‘𝐾)) / 4) < (2↑_𝑐((2 · 𝐾) − 5)) ↔ (exp‘(θ‘𝐾)) < ((2↑_𝑐((2 · 𝐾) − 5)) · 4)))
339	334, 338	mpbird 167	. . . . . . 7 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / 4) < (2↑_𝑐((2 · 𝐾) − 5)))
340	122, 239, 86, 274, 339	lttrd 8454	. . . . . 6 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < (2↑_𝑐((2 · 𝐾) − 5)))
341	103, 122, 86, 237, 340	lelttrd 8453	. . . . 5 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑_𝑐((2 · 𝐾) − 5)))
342	98	nnred 9320	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℝ)
343		nnre 9314	. . . . . . . 8 ⊢ ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
344		nngt0 9332	. . . . . . . 8 ⊢ ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → 0 < (seq1( · , 𝐹)‘𝑀))
345	343, 344	jca 306	. . . . . . 7 ⊢ ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
346	70, 345	syl 14	. . . . . 6 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀)))
347		ltdivmul 9209	. . . . . 6 ⊢ (((seq1( · , 𝐹)‘𝐾) ∈ ℝ ∧ (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ ∧ ((seq1( · , 𝐹)‘𝑀) ∈ ℝ ∧ 0 < (seq1( · , 𝐹)‘𝑀))) → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑_𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5)))))
348	342, 86, 346, 347	syl3anc 1278	. . . . 5 ⊢ (𝜑 → (((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑_𝑐((2 · 𝐾) − 5)) ↔ (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5)))))
349	341, 348	mpbid 147	. . . 4 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) < ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))))
350	88, 349	eqbrtrrd 4154	. . 3 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) < ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))))
351	30, 86	remulcld 8357	. . . 4 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐((2 · 𝐾) − 5))) ∈ ℝ)
352	3, 62, 55, 63, 64	bposlem5 16244	. . . . 5 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
353	71, 30, 85	lemul1d 10152	. . . . 5 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ↔ ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐((2 · 𝐾) − 5)))))
354	352, 353	mpbid 147	. . . 4 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐((2 · 𝐾) − 5))))
355	79	zred 9773	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐾) ∈ ℝ)
356	37	a1i 9	. . . . . . 7 ⊢ (𝜑 → 5 ∈ ℝ)
357		flqle 10726	. . . . . . . . . . 11 ⊢ (((2 · 𝑁) / 3) ∈ ℚ → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
358	75, 357	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
359	63, 358	eqbrtrid 4165	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ ((2 · 𝑁) / 3))
360		nndivre 9343	. . . . . . . . . . 11 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ)
361	20, 23, 360	sylancl 417	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ)
362		2pos 9398	. . . . . . . . . . . 12 ⊢ 0 < 2
363	26, 362	pm3.2i 272	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 < 2)
364	363	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
365		lemul2 9190	. . . . . . . . . 10 ⊢ ((𝐾 ∈ ℝ ∧ ((2 · 𝑁) / 3) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
366	278, 361, 364, 365	syl3anc 1278	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ≤ ((2 · 𝑁) / 3) ↔ (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3))))
367	359, 366	mpbid 147	. . . . . . . 8 ⊢ (𝜑 → (2 · 𝐾) ≤ (2 · ((2 · 𝑁) / 3)))
368	18	nncnd 9321	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
369		3ap0 9403	. . . . . . . . . . . 12 ⊢ 3 # 0
370	309, 369	pm3.2i 272	. . . . . . . . . . 11 ⊢ (3 ∈ ℂ ∧ 3 # 0)
371		divassap 9023	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ (2 · 𝑁) ∈ ℂ ∧ (3 ∈ ℂ ∧ 3 # 0)) → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
372	310, 370, 371	mp3an13 1369	. . . . . . . . . 10 ⊢ ((2 · 𝑁) ∈ ℂ → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
373	368, 372	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (2 · 𝑁)) / 3) = (2 · ((2 · 𝑁) / 3)))
374	5	nncnd 9321	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
375		mulass 8311	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
376	310, 310, 374, 375	mp3an12i 1382	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
377		2t2e4 9462	. . . . . . . . . . . 12 ⊢ (2 · 2) = 4
378	377	oveq1i 6095	. . . . . . . . . . 11 ⊢ ((2 · 2) · 𝑁) = (4 · 𝑁)
379	376, 378	eqtr3di 2286	. . . . . . . . . 10 ⊢ (𝜑 → (2 · (2 · 𝑁)) = (4 · 𝑁))
380	379	oveq1d 6100	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (2 · 𝑁)) / 3) = ((4 · 𝑁) / 3))
381	373, 380	eqtr3d 2273	. . . . . . . 8 ⊢ (𝜑 → (2 · ((2 · 𝑁) / 3)) = ((4 · 𝑁) / 3))
382	367, 381	breqtrd 4156	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐾) ≤ ((4 · 𝑁) / 3))
383	355, 36, 356, 382	lesub1dd 8891	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5))
384		1lt2 9479	. . . . . . . 8 ⊢ 1 < 2
385	384	a1i 9	. . . . . . 7 ⊢ (𝜑 → 1 < 2)
386	275, 385, 83, 39	cxpled 16094	. . . . . 6 ⊢ (𝜑 → (((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5) ↔ (2↑_𝑐((2 · 𝐾) − 5)) ≤ (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
387	383, 386	mpbid 147	. . . . 5 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 5)) ≤ (2↑_𝑐(((4 · 𝑁) / 3) − 5)))
388	86, 42, 29	lemul2d 10153	. . . . 5 ⊢ (𝜑 → ((2↑_𝑐((2 · 𝐾) − 5)) ≤ (2↑_𝑐(((4 · 𝑁) / 3) − 5)) ↔ (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5)))))
389	387, 388	mpbid 147	. . . 4 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
390	87, 351, 43, 354, 389	letrd 8452	. . 3 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
391	15, 87, 43, 350, 390	ltletrd 8753	. 2 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) < (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
392	10, 15, 43, 54, 391	lttrd 8454	1 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) < (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))

Colors of variables: wff set class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 = wceq 1402 ∈ wcel 2209 ≠ wne 2420 ∀wral 2528 ∃wrex 2529 ifcif 3638 class class class wbr 4130 ↦ cmpt 4192 ⟶wf 5373 ‘cfv 5377 (class class class)co 6085 ℂcc 8178 ℝcr 8179 0cc0 8180 1c1 8181 + caddc 8183 · cmul 8185 < clt 8361 ≤ cle 8362 − cmin 8499 # cap 8912 / cdiv 9005 ℕcn 9307 2c2 9358 3c3 9359 4c4 9360 5c5 9361 6c6 9362 ℕ₀cn0 9568 ℤcz 9649 ℤ_≥cuz 9931 ℚcq 10029 ℝ⁺crp 10065 ...cfz 10422 ⌊cfl 10714 seqcseq 10899 ↑cexp 10990 Ccbc 11201 √csqrt 11778 expce 12428 ∥ cdvds 12573 ℙcprime 12904 pCnt cpc 13086 logclog 16017 ↑_𝑐ccxp 16018 θccht 16162

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4246 ax-sep 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578 ax-setind 4684 ax-iinf 4735 ax-cnex 8271 ax-resscn 8272 ax-1cn 8273 ax-1re 8274 ax-icn 8275 ax-addcl 8276 ax-addrcl 8277 ax-mulcl 8278 ax-mulrcl 8279 ax-addcom 8280 ax-mulcom 8281 ax-addass 8282 ax-mulass 8283 ax-distr 8284 ax-i2m1 8285 ax-0lt1 8286 ax-1rid 8287 ax-0id 8288 ax-rnegex 8289 ax-precex 8290 ax-cnre 8291 ax-pre-ltirr 8292 ax-pre-ltwlin 8293 ax-pre-lttrn 8294 ax-pre-apti 8295 ax-pre-ltadd 8296 ax-pre-mulgt0 8297 ax-pre-mulext 8298 ax-arch 8299 ax-caucvg 8300 ax-pre-suploc 8301 ax-addf 8302 ax-mulf 8303

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-disj 4107 df-br 4131 df-opab 4193 df-mpt 4194 df-tr 4230 df-id 4438 df-po 4441 df-iso 4442 df-iord 4511 df-on 4513 df-ilim 4514 df-suc 4516 df-iom 4738 df-xp 4780 df-rel 4781 df-cnv 4782 df-co 4783 df-dm 4784 df-rn 4785 df-res 4786 df-ima 4787 df-iota 5337 df-fun 5379 df-fn 5380 df-f 5381 df-f1 5382 df-fo 5383 df-f1o 5384 df-fv 5385 df-isom 5386 df-riota 6038 df-ov 6088 df-oprab 6089 df-mpo 6090 df-of 6302 df-1st 6374 df-2nd 6375 df-recs 6576 df-irdg 6641 df-frec 6662 df-1o 6687 df-2o 6688 df-oadd 6691 df-er 6807 df-map 6924 df-pm 6925 df-en 7023 df-dom 7024 df-fin 7025 df-sup 7325 df-inf 7326 df-pnf 8363 df-mnf 8364 df-xr 8365 df-ltxr 8366 df-le 8367 df-sub 8501 df-neg 8502 df-reap 8906 df-ap 8913 df-div 9006 df-inn 9308 df-2 9366 df-3 9367 df-4 9368 df-5 9369 df-6 9370 df-7 9371 df-8 9372 df-9 9373 df-n0 9569 df-xnn0 9636 df-z 9650 df-dec 9783 df-uz 9932 df-q 10030 df-rp 10066 df-xneg 10185 df-xadd 10186 df-ioo 10305 df-ico 10307 df-icc 10308 df-fz 10423 df-fzo 10561 df-fl 10716 df-mod 10775 df-seqfrec 10900 df-exp 10991 df-fac 11180 df-bc 11202 df-ihash 11231 df-shft 11596 df-cj 11623 df-re 11624 df-im 11625 df-rsqrt 11780 df-abs 11781 df-clim 12064 df-sumdc 12139 df-ef 12434 df-e 12435 df-dvds 12574 df-gcd 12750 df-prm 12905 df-numer 12982 df-denom 12983 df-pc 13087 df-rest 13647 df-topgen 13666 df-psmet 14932 df-xmet 14933 df-met 14934 df-bl 14935 df-mopn 14936 df-top 15158 df-topon 15171 df-bases 15203 df-ntr 15256 df-cn 15348 df-cnp 15349 df-tx 15413 df-cncf 15731 df-limced 15816 df-dvap 15817 df-relog 16019 df-rpcxp 16020 df-logb 16109 df-cht 16165 df-ppi 16166

This theorem is used by: bposlem9 16248

W3C validator