bposlem6 - Intuitionistic Logic Explorer

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

Theorem bposlem6 16316

Description: Lemma for bpos 16320. 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 9479	. . . . 5 ⊢ 4 ∈ ℕ
2		5nn 9480	. . . . . . 7 ⊢ 5 ∈ ℕ
3		bpos.1	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘5))
4		eluznn 10016	. . . . . . 7 ⊢ ((5 ∈ ℕ ∧ 𝑁 ∈ (ℤ_≥‘5)) → 𝑁 ∈ ℕ)
5	2, 3, 4	sylancr 418	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
6	5	nnnn0d 9631	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
7		nnexpcl 11010	. . . . 5 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ₀) → (4↑𝑁) ∈ ℕ)
8	1, 6, 7	sylancr 418	. . . 4 ⊢ (𝜑 → (4↑𝑁) ∈ ℕ)
9	8	nnred 9326	. . 3 ⊢ (𝜑 → (4↑𝑁) ∈ ℝ)
10	9, 5	nndivred 9363	. 2 ⊢ (𝜑 → ((4↑𝑁) / 𝑁) ∈ ℝ)
11		fzctr 10557	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ (0...(2 · 𝑁)))
12	6, 11	syl 14	. . . 4 ⊢ (𝜑 → 𝑁 ∈ (0...(2 · 𝑁)))
13		bccl2 11228	. . . 4 ⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ)
14	12, 13	syl 14	. . 3 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ)
15	14	nnred 9326	. 2 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ)
16		2nn 9477	. . . . . . 7 ⊢ 2 ∈ ℕ
17		nnmulcl 9334	. . . . . . 7 ⊢ ((2 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (2 · 𝑁) ∈ ℕ)
18	16, 5, 17	sylancr 418	. . . . . 6 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ)
19	18	nnrpd 10112	. . . . 5 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ⁺)
20	18	nnred 9326	. . . . . . . 8 ⊢ (𝜑 → (2 · 𝑁) ∈ ℝ)
21	19	rpge0d 10118	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ (2 · 𝑁))
22	20, 21	resqrtcld 11952	. . . . . . 7 ⊢ (𝜑 → (√‘(2 · 𝑁)) ∈ ℝ)
23		3nn 9478	. . . . . . 7 ⊢ 3 ∈ ℕ
24		nndivre 9349	. . . . . . 7 ⊢ (((√‘(2 · 𝑁)) ∈ ℝ ∧ 3 ∈ ℕ) → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
25	22, 23, 24	sylancl 417	. . . . . 6 ⊢ (𝜑 → ((√‘(2 · 𝑁)) / 3) ∈ ℝ)
26		2re 9383	. . . . . 6 ⊢ 2 ∈ ℝ
27		readdcl 8311	. . . . . 6 ⊢ ((((√‘(2 · 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
28	25, 26, 27	sylancl 417	. . . . 5 ⊢ (𝜑 → (((√‘(2 · 𝑁)) / 3) + 2) ∈ ℝ)
29	19, 28	rpcxpcld 16168	. . . 4 ⊢ (𝜑 → ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ⁺)
30	29	rpred 10114	. . 3 ⊢ (𝜑 → ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) ∈ ℝ)
31		2rp 10076	. . . . 5 ⊢ 2 ∈ ℝ⁺
32		nnmulcl 9334	. . . . . . . . 9 ⊢ ((4 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (4 · 𝑁) ∈ ℕ)
33	1, 5, 32	sylancr 418	. . . . . . . 8 ⊢ (𝜑 → (4 · 𝑁) ∈ ℕ)
34	33	nnred 9326	. . . . . . 7 ⊢ (𝜑 → (4 · 𝑁) ∈ ℝ)
35		nndivre 9349	. . . . . . 7 ⊢ (((4 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((4 · 𝑁) / 3) ∈ ℝ)
36	34, 23, 35	sylancl 417	. . . . . 6 ⊢ (𝜑 → ((4 · 𝑁) / 3) ∈ ℝ)
37		5re 9392	. . . . . 6 ⊢ 5 ∈ ℝ
38		resubcl 8597	. . . . . 6 ⊢ ((((4 · 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
39	36, 37, 38	sylancl 417	. . . . 5 ⊢ (𝜑 → (((4 · 𝑁) / 3) − 5) ∈ ℝ)
40		rpcxpcl 16136	. . . . 5 ⊢ ((2 ∈ ℝ⁺ ∧ (((4 · 𝑁) / 3) − 5) ∈ ℝ) → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ⁺)
41	31, 39, 40	sylancr 418	. . . 4 ⊢ (𝜑 → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ⁺)
42	41	rpred 10114	. . 3 ⊢ (𝜑 → (2↑_𝑐(((4 · 𝑁) / 3) − 5)) ∈ ℝ)
43	30, 42	remulcld 8362	. 2 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))) ∈ ℝ)
44		df-5 9375	. . . . 5 ⊢ 5 = (4 + 1)
45		4z 9685	. . . . . 6 ⊢ 4 ∈ ℤ
46		uzid 9952	. . . . . 6 ⊢ (4 ∈ ℤ → 4 ∈ (ℤ_≥‘4))
47		peano2uz 9999	. . . . . 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 9956	. . . 4 ⊢ ((5 ∈ (ℤ_≥‘4) ∧ 𝑁 ∈ (ℤ_≥‘5)) → 𝑁 ∈ (ℤ_≥‘4))
52	49, 3, 51	sylancr 418	. . 3 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘4))
53		bclbnd 16307	. . 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 13107	. . . . . . . . . 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 13150	. . . . . . 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 16314	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (3...𝐾))
66		elfzuz 10441	. . . . . . . 8 ⊢ (𝑀 ∈ (3...𝐾) → 𝑀 ∈ (ℤ_≥‘3))
67	65, 66	syl 14	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘3))
68		eluznn 10016	. . . . . . 7 ⊢ ((3 ∈ ℕ ∧ 𝑀 ∈ (ℤ_≥‘3)) → 𝑀 ∈ ℕ)
69	23, 67, 68	sylancr 418	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℕ)
70	61, 69	ffvelcdmd 5847	. . . . 5 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℕ)
71	70	nnred 9326	. . . 4 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
72		2z 9683	. . . . . . . . 9 ⊢ 2 ∈ ℤ
73	18	nnzd 9778	. . . . . . . . . . . 12 ⊢ (𝜑 → (2 · 𝑁) ∈ ℤ)
74		znq 10040	. . . . . . . . . . . 12 ⊢ (((2 · 𝑁) ∈ ℤ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℚ)
75	73, 23, 74	sylancl 417	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℚ)
76	75	flqcld 10731	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((2 · 𝑁) / 3)) ∈ ℤ)
77	63, 76	eqeltrid 2325	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℤ)
78		zmulcl 9709	. . . . . . . . 9 ⊢ ((2 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (2 · 𝐾) ∈ ℤ)
79	72, 77, 78	sylancr 418	. . . . . . . 8 ⊢ (𝜑 → (2 · 𝐾) ∈ ℤ)
80	2	nnzi 9676	. . . . . . . 8 ⊢ 5 ∈ ℤ
81		zsubcl 9696	. . . . . . . 8 ⊢ (((2 · 𝐾) ∈ ℤ ∧ 5 ∈ ℤ) → ((2 · 𝐾) − 5) ∈ ℤ)
82	79, 80, 81	sylancl 417	. . . . . . 7 ⊢ (𝜑 → ((2 · 𝐾) − 5) ∈ ℤ)
83	82	zred 9779	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐾) − 5) ∈ ℝ)
84		rpcxpcl 16136	. . . . . 6 ⊢ ((2 ∈ ℝ⁺ ∧ ((2 · 𝐾) − 5) ∈ ℝ) → (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ⁺)
85	31, 83, 84	sylancr 418	. . . . 5 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ⁺)
86	85	rpred 10114	. . . 4 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 5)) ∈ ℝ)
87	71, 86	remulcld 8362	. . 3 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))) ∈ ℝ)
88	3, 62, 55, 63	bposlem3 16313	. . . 4 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) = ((2 · 𝑁)C𝑁))
89		elfzuz3 10442	. . . . . . . . . 10 ⊢ (𝑀 ∈ (3...𝐾) → 𝐾 ∈ (ℤ_≥‘𝑀))
90	65, 89	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘𝑀))
91	55, 59, 69, 90	pcmptdvds 13153	. . . . . . . 8 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∥ (seq1( · , 𝐹)‘𝐾))
92	70	nnzd 9778	. . . . . . . . 9 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ∈ ℤ)
93	70	nnne0d 9358	. . . . . . . . 9 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≠ 0)
94		uztrn 9955	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ (ℤ_≥‘𝑀) ∧ 𝑀 ∈ (ℤ_≥‘3)) → 𝐾 ∈ (ℤ_≥‘3))
95	90, 67, 94	syl2anc 415	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘3))
96		eluznn 10016	. . . . . . . . . . . 12 ⊢ ((3 ∈ ℕ ∧ 𝐾 ∈ (ℤ_≥‘3)) → 𝐾 ∈ ℕ)
97	23, 95, 96	sylancr 418	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ)
98	61, 97	ffvelcdmd 5847	. . . . . . . . . 10 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℕ)
99	98	nnzd 9778	. . . . . . . . 9 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℤ)
100		dvdsval2 12582	. . . . . . . . 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 9779	. . . . . 6 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) ∈ ℝ)
104		nnq 10049	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
105	69, 104	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℚ)
106		zq 10042	. . . . . . . . . 10 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℚ)
107	77, 106	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ∈ ℚ)
108		eluzle 9950	. . . . . . . . . 10 ⊢ (𝐾 ∈ (ℤ_≥‘𝑀) → 𝑀 ≤ 𝐾)
109	90, 108	syl 14	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
110		efchtqdvds 16265	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℚ ∧ 𝐾 ∈ ℚ ∧ 𝑀 ≤ 𝐾) → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
111	105, 107, 109, 110	syl3anc 1278	. . . . . . . 8 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∥ (exp‘(θ‘𝐾)))
112		efchtqcl 16246	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℚ → (exp‘(θ‘𝑀)) ∈ ℕ)
113	105, 112	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∈ ℕ)
114	113	nnzd 9778	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∈ ℤ)
115	113	nnne0d 9358	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ≠ 0)
116		efchtqcl 16246	. . . . . . . . . . 11 ⊢ (𝐾 ∈ ℚ → (exp‘(θ‘𝐾)) ∈ ℕ)
117	107, 116	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝐾)) ∈ ℕ)
118	117	nnzd 9778	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝐾)) ∈ ℤ)
119		dvdsval2 12582	. . . . . . . . 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 9779	. . . . . 6 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℝ)
123	18	nnnn0d 9631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ₀)
124		sqrtrirr 13014	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 · 𝑁) ∈ ℕ₀ → ((√‘(2 · 𝑁)) ∈ ℚ ∨ ((√‘(2 · 𝑁)) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (√‘(2 · 𝑁)) # 𝑞)))
125	123, 124	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((√‘(2 · 𝑁)) ∈ ℚ ∨ ((√‘(2 · 𝑁)) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (√‘(2 · 𝑁)) # 𝑞)))
126		prmz 12914	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
127		flaplt 10739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((√‘(2 · 𝑁)) ∈ ℚ ∨ ((√‘(2 · 𝑁)) ∈ ℝ ∧ ∀𝑞 ∈ ℚ (√‘(2 · 𝑁)) # 𝑞)) ∧ 𝑝 ∈ ℤ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
128	125, 126, 127	syl2an 289	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝))
129	64	breq1i 4138	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 < 𝑝 ↔ (⌊‘(√‘(2 · 𝑁))) < 𝑝)
130	128, 129	bitr4di 198	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ 𝑀 < 𝑝))
131	69	nnzd 9778	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
132		zltnle 9701	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ ℤ ∧ 𝑝 ∈ ℤ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀))
133	131, 126, 132	syl2an 289	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑀 < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀))
134	130, 133	bitrd 188	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ¬ 𝑝 ≤ 𝑀))
135		bposlem1 16311	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
136	5, 135	sylan 283	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁))
137	126	zred 9779	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ)
138	137	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℝ)
139		id 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℙ)
140		pccl 13107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ∈ ℙ ∧ ((2 · 𝑁)C𝑁) ∈ ℕ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
141	139, 14, 140	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ₀)
142	138, 141	reexpcld 11149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ)
143	20	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (2 · 𝑁) ∈ ℝ)
144	138	resqcld 11158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝↑2) ∈ ℝ)
145		lelttr 8420	. . . . . . . . . . . . . . . . . . . 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 11819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 0 ≤ (2 · 𝑁)) → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
149	20, 21, 148	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((√‘(2 · 𝑁))↑2) = (2 · 𝑁))
150	149	breq1d 4141	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
151	150	adantr 276	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (((√‘(2 · 𝑁))↑2) < (𝑝↑2) ↔ (2 · 𝑁) < (𝑝↑2)))
152	141	nn0zd 9777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ)
153	72	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈ ℤ)
154		prmgt1 12936	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℙ → 1 < 𝑝)
155	154	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 1 < 𝑝)
156	138, 152, 153, 155	ltexp2d 16178	. . . . . . . . . . . . . . . . . 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 9372	. . . . . . . . . . . . . . . . . 18 ⊢ 2 = (1 + 1)
159	158	breq2i 4139	. . . . . . . . . . . . . . . . 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 11955	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 0 ≤ (√‘(2 · 𝑁)))
163	162	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤ (√‘(2 · 𝑁)))
164		prmnn 12913	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℕ)
165	164	nnrpd 10112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℝ⁺)
166	165	rpge0d 10118	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℙ → 0 ≤ 𝑝)
167	166	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 0 ≤ 𝑝)
168	161, 138, 163, 167	lt2sqd 11163	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → ((√‘(2 · 𝑁)) < 𝑝 ↔ ((√‘(2 · 𝑁))↑2) < (𝑝↑2)))
169		1z 9681	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ ℤ
170		zleltp1 9711	. . . . . . . . . . . . . . . . 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 4163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑝 ∈ ℙ) ∧ (𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀)) → if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0) ≤ if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), 1, 0))
181		0le0 9402	. . . . . . . . . . . . 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 4144	. . . . . . . . . . . . 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 9732	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝑝 ≤ 𝐾)
188	126, 77, 187	syl2anr 290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → DECID 𝑝 ≤ 𝐾)
189		zdcle 9732	. . . . . . . . . . . . . . 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 6095	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑝 → (𝑛 pCnt ((2 · 𝑁)C𝑁)) = (𝑝 pCnt ((2 · 𝑁)C𝑁)))
201	90	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝐾 ∈ (ℤ_≥‘𝑀))
202	55, 197, 198, 199, 200, 201	pcmpt2 13152	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) = if((𝑝 ≤ 𝐾 ∧ ¬ 𝑝 ≤ 𝑀), (𝑝 pCnt ((2 · 𝑁)C𝑁)), 0))
203		eqid 2238	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
204	203	prmorcht 16282	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ ℕ → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
205	97, 204	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (exp‘(θ‘𝐾)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾))
206	203	prmorcht 16282	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℕ → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
207	69, 206	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (exp‘(θ‘𝑀)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))
208	205, 207	oveq12d 6106	. . . . . . . . . . . . 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 6104	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))) = (𝑝 pCnt ((seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝐾) / (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)))‘𝑀))))
211		nncn 9321	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
212	211	exp1d 11127	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
213	212	ifeq1d 3658	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → if(𝑛 ∈ ℙ, (𝑛↑1), 1) = if(𝑛 ∈ ℙ, 𝑛, 1))
214	213	mpteq2ia 4219	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1))
215	214	eqcomi 2242	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, 𝑛, 1)) = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑1), 1))
216		1nn0 9590	. . . . . . . . . . . . . . 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 13152	. . . . . . . . . . 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 4163	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
224	223	ralrimiva 2623	. . . . . . . 8 ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 pCnt ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀))) ≤ (𝑝 pCnt ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
225		pc2dvds 13138	. . . . . . . . 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 9326	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝐾)) ∈ ℝ)
229	113	nnred 9326	. . . . . . . . . 10 ⊢ (𝜑 → (exp‘(θ‘𝑀)) ∈ ℝ)
230	117	nngt0d 9357	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (exp‘(θ‘𝐾)))
231	113	nngt0d 9357	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (exp‘(θ‘𝑀)))
232	228, 229, 230, 231	divgt0d 9273	. . . . . . . . 9 ⊢ (𝜑 → 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))))
233		elnnz 9665	. . . . . . . . 9 ⊢ (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ ↔ (((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℤ ∧ 0 < ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀)))))
234	121, 232, 233	sylanbrc 421	. . . . . . . 8 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) ∈ ℕ)
235		dvdsle 12636	. . . . . . . 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 9349	. . . . . . . 8 ⊢ (((exp‘(θ‘𝐾)) ∈ ℝ ∧ 4 ∈ ℕ) → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
239	228, 1, 238	sylancl 417	. . . . . . 7 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / 4) ∈ ℝ)
240		4re 9390	. . . . . . . . . 10 ⊢ 4 ∈ ℝ
241	240	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 4 ∈ ℝ)
242		6re 9394	. . . . . . . . . 10 ⊢ 6 ∈ ℝ
243	242	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 6 ∈ ℝ)
244		4lt6 9496	. . . . . . . . . 10 ⊢ 4 < 6
245	244	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 4 < 6)
246		cht3 16277	. . . . . . . . . . . 12 ⊢ (θ‘3) = (log‘6)
247	246	fveq2i 5701	. . . . . . . . . . 11 ⊢ (exp‘(θ‘3)) = (exp‘(log‘6))
248		6pos 9414	. . . . . . . . . . . . 13 ⊢ 0 < 6
249	242, 248	elrpii 10074	. . . . . . . . . . . 12 ⊢ 6 ∈ ℝ⁺
250		reeflog 16092	. . . . . . . . . . . 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 9684	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℤ
254		zq 10042	. . . . . . . . . . . . . 14 ⊢ (3 ∈ ℤ → 3 ∈ ℚ)
255	253, 254	ax-mp 5	. . . . . . . . . . . . 13 ⊢ 3 ∈ ℚ
256	255	a1i 9	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ∈ ℚ)
257		eluzle 9950	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ (ℤ_≥‘3) → 3 ≤ 𝑀)
258	67, 257	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 3 ≤ 𝑀)
259		chtqwordi 16263	. . . . . . . . . . . 12 ⊢ ((3 ∈ ℚ ∧ 𝑀 ∈ ℚ ∧ 3 ≤ 𝑀) → (θ‘3) ≤ (θ‘𝑀))
260	256, 105, 258, 259	syl3anc 1278	. . . . . . . . . . 11 ⊢ (𝜑 → (θ‘3) ≤ (θ‘𝑀))
261		chtqcl 16244	. . . . . . . . . . . . 13 ⊢ (3 ∈ ℚ → (θ‘3) ∈ ℝ)
262	255, 261	ax-mp 5	. . . . . . . . . . . 12 ⊢ (θ‘3) ∈ ℝ
263		chtqcl 16244	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℚ → (θ‘𝑀) ∈ ℝ)
264	105, 263	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (θ‘𝑀) ∈ ℝ)
265		efle 16002	. . . . . . . . . . . 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 4167	. . . . . . . . 9 ⊢ (𝜑 → 6 ≤ (exp‘(θ‘𝑀)))
269	241, 243, 229, 245, 268	ltletrd 8758	. . . . . . . 8 ⊢ (𝜑 → 4 < (exp‘(θ‘𝑀)))
270		4pos 9410	. . . . . . . . . 10 ⊢ 0 < 4
271	270	a1i 9	. . . . . . . . 9 ⊢ (𝜑 → 0 < 4)
272		ltdiv2 9225	. . . . . . . . 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 9387	. . . . . . . . . . . . . 14 ⊢ 3 ∈ ℝ
277	276	a1i 9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 3 ∈ ℝ)
278	77	zred 9779	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ ℝ)
279		2lt3 9486	. . . . . . . . . . . . . 14 ⊢ 2 < 3
280	279	a1i 9	. . . . . . . . . . . . 13 ⊢ (𝜑 → 2 < 3)
281	69	nnred 9326	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑀 ∈ ℝ)
282	277, 281, 278, 258, 109	letrd 8457	. . . . . . . . . . . . 13 ⊢ (𝜑 → 3 ≤ 𝐾)
283	275, 277, 278, 280, 282	ltletrd 8758	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 < 𝐾)
284		chtqub 16296	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ ℚ ∧ 2 < 𝐾) → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
285	107, 283, 284	syl2anc 415	. . . . . . . . . . 11 ⊢ (𝜑 → (θ‘𝐾) < ((log‘2) · ((2 · 𝐾) − 3)))
286		chtqcl 16244	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ ℚ → (θ‘𝐾) ∈ ℝ)
287	107, 286	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (θ‘𝐾) ∈ ℝ)
288		relogcl 16091	. . . . . . . . . . . . . 14 ⊢ (2 ∈ ℝ⁺ → (log‘2) ∈ ℝ)
289	31, 288	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (log‘2) ∈ ℝ
290		zsubcl 9696	. . . . . . . . . . . . . . 15 ⊢ (((2 · 𝐾) ∈ ℤ ∧ 3 ∈ ℤ) → ((2 · 𝐾) − 3) ∈ ℤ)
291	79, 253, 290	sylancl 417	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · 𝐾) − 3) ∈ ℤ)
292	291	zred 9779	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐾) − 3) ∈ ℝ)
293		remulcl 8313	. . . . . . . . . . . . 13 ⊢ (((log‘2) ∈ ℝ ∧ ((2 · 𝐾) − 3) ∈ ℝ) → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
294	289, 292, 293	sylancr 418	. . . . . . . . . . . 12 ⊢ (𝜑 → ((log‘2) · ((2 · 𝐾) − 3)) ∈ ℝ)
295		eflt 16001	. . . . . . . . . . . 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 16101	. . . . . . . . . . . 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 9780	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((2 · 𝐾) − 3) ∈ ℂ)
301	289	recni 8344	. . . . . . . . . . . . 13 ⊢ (log‘2) ∈ ℂ
302		mulcom 8314	. . . . . . . . . . . . 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 5702	. . . . . . . . . . 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 4159	. . . . . . . . 9 ⊢ (𝜑 → (exp‘(θ‘𝐾)) < (2↑((2 · 𝐾) − 3)))
307		3p2e5 9455	. . . . . . . . . . . . . . . 16 ⊢ (3 + 2) = 5
308	307	oveq1i 6098	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 2) = (5 − 2)
309		3cn 9388	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℂ
310		2cn 9384	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℂ
311	309, 310	pncan3oi 8549	. . . . . . . . . . . . . . 15 ⊢ ((3 + 2) − 2) = 3
312	308, 311	eqtr3i 2261	. . . . . . . . . . . . . 14 ⊢ (5 − 2) = 3
313	312	oveq2i 6099	. . . . . . . . . . . . 13 ⊢ ((2 · 𝐾) − (5 − 2)) = ((2 · 𝐾) − 3)
314	79	zcnd 9780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (2 · 𝐾) ∈ ℂ)
315		5cn 9393	. . . . . . . . . . . . . . 15 ⊢ 5 ∈ ℂ
316		subsub 8563	. . . . . . . . . . . . . . 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 6104	. . . . . . . . . . 11 ⊢ (𝜑 → (2↑_𝑐((2 · 𝐾) − 3)) = (2↑_𝑐(((2 · 𝐾) − 5) + 2)))
321		cxpexpnn 16129	. . . . . . . . . . . 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 9780	. . . . . . . . . . . 12 ⊢ (𝜑 → ((2 · 𝐾) − 5) ∈ ℂ)
324		rpcxpadd 16138	. . . . . . . . . . . . 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 16129	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℕ ∧ 2 ∈ ℤ) → (2↑_𝑐2) = (2↑2))
329	16, 72, 328	mp2an 430	. . . . . . . . . . . 12 ⊢ (2↑_𝑐2) = (2↑2)
330		sq2 11093	. . . . . . . . . . . 12 ⊢ (2↑2) = 4
331	329, 330	eqtri 2259	. . . . . . . . . . 11 ⊢ (2↑_𝑐2) = 4
332	331	oveq2i 6099	. . . . . . . . . 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 4157	. . . . . . . 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 9216	. . . . . . . . 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 8459	. . . . . 6 ⊢ (𝜑 → ((exp‘(θ‘𝐾)) / (exp‘(θ‘𝑀))) < (2↑_𝑐((2 · 𝐾) − 5)))
341	103, 122, 86, 237, 340	lelttrd 8458	. . . . 5 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝐾) / (seq1( · , 𝐹)‘𝑀)) < (2↑_𝑐((2 · 𝐾) − 5)))
342	98	nnred 9326	. . . . . 6 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝐾) ∈ ℝ)
343		nnre 9320	. . . . . . . 8 ⊢ ((seq1( · , 𝐹)‘𝑀) ∈ ℕ → (seq1( · , 𝐹)‘𝑀) ∈ ℝ)
344		nngt0 9338	. . . . . . . 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 9214	. . . . . 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 4155	. . 3 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) < ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))))
351	30, 86	remulcld 8362	. . . 4 ⊢ (𝜑 → (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐((2 · 𝐾) − 5))) ∈ ℝ)
352	3, 62, 55, 63, 64	bposlem5 16315	. . . . 5 ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑀) ≤ ((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)))
353	71, 30, 85	lemul1d 10158	. . . . 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 9779	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐾) ∈ ℝ)
356	37	a1i 9	. . . . . . 7 ⊢ (𝜑 → 5 ∈ ℝ)
357		flqle 10732	. . . . . . . . . . 11 ⊢ (((2 · 𝑁) / 3) ∈ ℚ → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
358	75, 357	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (⌊‘((2 · 𝑁) / 3)) ≤ ((2 · 𝑁) / 3))
359	63, 358	eqbrtrid 4166	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 ≤ ((2 · 𝑁) / 3))
360		nndivre 9349	. . . . . . . . . . 11 ⊢ (((2 · 𝑁) ∈ ℝ ∧ 3 ∈ ℕ) → ((2 · 𝑁) / 3) ∈ ℝ)
361	20, 23, 360	sylancl 417	. . . . . . . . . 10 ⊢ (𝜑 → ((2 · 𝑁) / 3) ∈ ℝ)
362		2pos 9404	. . . . . . . . . . . 12 ⊢ 0 < 2
363	26, 362	pm3.2i 272	. . . . . . . . . . 11 ⊢ (2 ∈ ℝ ∧ 0 < 2)
364	363	a1i 9	. . . . . . . . . 10 ⊢ (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
365		lemul2 9195	. . . . . . . . . 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 9327	. . . . . . . . . 10 ⊢ (𝜑 → (2 · 𝑁) ∈ ℂ)
369		3ap0 9409	. . . . . . . . . . . 12 ⊢ 3 # 0
370	309, 369	pm3.2i 272	. . . . . . . . . . 11 ⊢ (3 ∈ ℂ ∧ 3 # 0)
371		divassap 9028	. . . . . . . . . . 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 9327	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℂ)
375		mulass 8316	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
376	310, 310, 374, 375	mp3an12i 1382	. . . . . . . . . . 11 ⊢ (𝜑 → ((2 · 2) · 𝑁) = (2 · (2 · 𝑁)))
377		2t2e4 9468	. . . . . . . . . . . 12 ⊢ (2 · 2) = 4
378	377	oveq1i 6098	. . . . . . . . . . 11 ⊢ ((2 · 2) · 𝑁) = (4 · 𝑁)
379	376, 378	eqtr3di 2286	. . . . . . . . . 10 ⊢ (𝜑 → (2 · (2 · 𝑁)) = (4 · 𝑁))
380	379	oveq1d 6103	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (2 · 𝑁)) / 3) = ((4 · 𝑁) / 3))
381	373, 380	eqtr3d 2273	. . . . . . . 8 ⊢ (𝜑 → (2 · ((2 · 𝑁) / 3)) = ((4 · 𝑁) / 3))
382	367, 381	breqtrd 4157	. . . . . . 7 ⊢ (𝜑 → (2 · 𝐾) ≤ ((4 · 𝑁) / 3))
383	355, 36, 356, 382	lesub1dd 8896	. . . . . 6 ⊢ (𝜑 → ((2 · 𝐾) − 5) ≤ (((4 · 𝑁) / 3) − 5))
384		1lt2 9485	. . . . . . . 8 ⊢ 1 < 2
385	384	a1i 9	. . . . . . 7 ⊢ (𝜑 → 1 < 2)
386	275, 385, 83, 39	cxpled 16164	. . . . . 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 10159	. . . . 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 8457	. . 3 ⊢ (𝜑 → ((seq1( · , 𝐹)‘𝑀) · (2↑_𝑐((2 · 𝐾) − 5))) ≤ (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
391	15, 87, 43, 350, 390	ltletrd 8758	. 2 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) < (((2 · 𝑁)↑_𝑐(((√‘(2 · 𝑁)) / 3) + 2)) · (2↑_𝑐(((4 · 𝑁) / 3) − 5))))
392	10, 15, 43, 54, 391	lttrd 8459	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 4131 ↦ cmpt 4193 ⟶wf 5376 ‘cfv 5380 (class class class)co 6088 ℂcc 8183 ℝcr 8184 0cc0 8185 1c1 8186 + caddc 8188 · cmul 8190 < clt 8366 ≤ cle 8367 − cmin 8504 # cap 8917 / cdiv 9010 ℕcn 9313 2c2 9364 3c3 9365 4c4 9366 5c5 9367 6c6 9368 ℕ₀cn0 9574 ℤcz 9655 ℤ_≥cuz 9937 ℚcq 10035 ℝ⁺crp 10071 ...cfz 10428 ⌊cfl 10720 seqcseq 10905 ↑cexp 10996 Ccbc 11207 √csqrt 11784 expce 12434 ∥ cdvds 12579 ℙcprime 12910 pCnt cpc 13092 logclog 16085 ↑_𝑐ccxp 16086 θccht 16233

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 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305 ax-pre-suploc 8306 ax-addf 8307 ax-mulf 8308

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 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-of 6305 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-2o 6692 df-oadd 6695 df-er 6811 df-map 6928 df-pm 6929 df-en 7027 df-dom 7028 df-fin 7029 df-sup 7330 df-inf 7331 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-5 9375 df-6 9376 df-7 9377 df-8 9378 df-9 9379 df-n0 9575 df-xnn0 9642 df-z 9656 df-dec 9789 df-uz 9938 df-q 10036 df-rp 10072 df-xneg 10191 df-xadd 10192 df-ioo 10311 df-ico 10313 df-icc 10314 df-fz 10429 df-fzo 10567 df-fl 10722 df-mod 10781 df-seqfrec 10906 df-exp 10997 df-fac 11186 df-bc 11208 df-ihash 11237 df-shft 11602 df-cj 11629 df-re 11630 df-im 11631 df-rsqrt 11786 df-abs 11787 df-clim 12070 df-sumdc 12145 df-ef 12440 df-e 12441 df-dvds 12580 df-gcd 12756 df-prm 12911 df-numer 12988 df-denom 12989 df-pc 13093 df-rest 13654 df-topgen 13673 df-psmet 14989 df-xmet 14990 df-met 14991 df-bl 14992 df-mopn 14993 df-top 15224 df-topon 15237 df-bases 15269 df-ntr 15322 df-cn 15414 df-cnp 15415 df-tx 15479 df-cncf 15797 df-limced 15882 df-dvap 15883 df-relog 16087 df-rpcxp 16088 df-logb 16180 df-cht 16236 df-ppi 16237

This theorem is used by: bposlem9 16319

W3C validator