MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem6 Structured version   Visualization version   GIF version

Theorem bposlem6 27028
Description: Lemma for bpos 27032. 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
StepHypRef Expression
1 4nn 12299 . . . . 5 4 ∈ β„•
2 5nn 12302 . . . . . . 7 5 ∈ β„•
3 bpos.1 . . . . . . 7 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜5))
4 eluznn 12906 . . . . . . 7 ((5 ∈ β„• ∧ 𝑁 ∈ (β„€β‰₯β€˜5)) β†’ 𝑁 ∈ β„•)
52, 3, 4sylancr 585 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•)
65nnnn0d 12536 . . . . 5 (πœ‘ β†’ 𝑁 ∈ β„•0)
7 nnexpcl 14044 . . . . 5 ((4 ∈ β„• ∧ 𝑁 ∈ β„•0) β†’ (4↑𝑁) ∈ β„•)
81, 6, 7sylancr 585 . . . 4 (πœ‘ β†’ (4↑𝑁) ∈ β„•)
98nnred 12231 . . 3 (πœ‘ β†’ (4↑𝑁) ∈ ℝ)
109, 5nndivred 12270 . 2 (πœ‘ β†’ ((4↑𝑁) / 𝑁) ∈ ℝ)
11 fzctr 13617 . . . . 5 (𝑁 ∈ β„•0 β†’ 𝑁 ∈ (0...(2 Β· 𝑁)))
126, 11syl 17 . . . 4 (πœ‘ β†’ 𝑁 ∈ (0...(2 Β· 𝑁)))
13 bccl2 14287 . . . 4 (𝑁 ∈ (0...(2 Β· 𝑁)) β†’ ((2 Β· 𝑁)C𝑁) ∈ β„•)
1412, 13syl 17 . . 3 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) ∈ β„•)
1514nnred 12231 . 2 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) ∈ ℝ)
16 2nn 12289 . . . . . . 7 2 ∈ β„•
17 nnmulcl 12240 . . . . . . 7 ((2 ∈ β„• ∧ 𝑁 ∈ β„•) β†’ (2 Β· 𝑁) ∈ β„•)
1816, 5, 17sylancr 585 . . . . . 6 (πœ‘ β†’ (2 Β· 𝑁) ∈ β„•)
1918nnrpd 13018 . . . . 5 (πœ‘ β†’ (2 Β· 𝑁) ∈ ℝ+)
2018nnred 12231 . . . . . . . 8 (πœ‘ β†’ (2 Β· 𝑁) ∈ ℝ)
2119rpge0d 13024 . . . . . . . 8 (πœ‘ β†’ 0 ≀ (2 Β· 𝑁))
2220, 21resqrtcld 15368 . . . . . . 7 (πœ‘ β†’ (βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ)
23 3nn 12295 . . . . . . 7 3 ∈ β„•
24 nndivre 12257 . . . . . . 7 (((βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ ∧ 3 ∈ β„•) β†’ ((βˆšβ€˜(2 Β· 𝑁)) / 3) ∈ ℝ)
2522, 23, 24sylancl 584 . . . . . 6 (πœ‘ β†’ ((βˆšβ€˜(2 Β· 𝑁)) / 3) ∈ ℝ)
26 2re 12290 . . . . . 6 2 ∈ ℝ
27 readdcl 11195 . . . . . 6 ((((βˆšβ€˜(2 Β· 𝑁)) / 3) ∈ ℝ ∧ 2 ∈ ℝ) β†’ (((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2) ∈ ℝ)
2825, 26, 27sylancl 584 . . . . 5 (πœ‘ β†’ (((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2) ∈ ℝ)
2919, 28rpcxpcld 26477 . . . 4 (πœ‘ β†’ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) ∈ ℝ+)
3029rpred 13020 . . 3 (πœ‘ β†’ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) ∈ ℝ)
31 2rp 12983 . . . . 5 2 ∈ ℝ+
32 nnmulcl 12240 . . . . . . . . 9 ((4 ∈ β„• ∧ 𝑁 ∈ β„•) β†’ (4 Β· 𝑁) ∈ β„•)
331, 5, 32sylancr 585 . . . . . . . 8 (πœ‘ β†’ (4 Β· 𝑁) ∈ β„•)
3433nnred 12231 . . . . . . 7 (πœ‘ β†’ (4 Β· 𝑁) ∈ ℝ)
35 nndivre 12257 . . . . . . 7 (((4 Β· 𝑁) ∈ ℝ ∧ 3 ∈ β„•) β†’ ((4 Β· 𝑁) / 3) ∈ ℝ)
3634, 23, 35sylancl 584 . . . . . 6 (πœ‘ β†’ ((4 Β· 𝑁) / 3) ∈ ℝ)
37 5re 12303 . . . . . 6 5 ∈ ℝ
38 resubcl 11528 . . . . . 6 ((((4 Β· 𝑁) / 3) ∈ ℝ ∧ 5 ∈ ℝ) β†’ (((4 Β· 𝑁) / 3) βˆ’ 5) ∈ ℝ)
3936, 37, 38sylancl 584 . . . . 5 (πœ‘ β†’ (((4 Β· 𝑁) / 3) βˆ’ 5) ∈ ℝ)
40 rpcxpcl 26420 . . . . 5 ((2 ∈ ℝ+ ∧ (((4 Β· 𝑁) / 3) βˆ’ 5) ∈ ℝ) β†’ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ∈ ℝ+)
4131, 39, 40sylancr 585 . . . 4 (πœ‘ β†’ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ∈ ℝ+)
4241rpred 13020 . . 3 (πœ‘ β†’ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ∈ ℝ)
4330, 42remulcld 11248 . 2 (πœ‘ β†’ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))) ∈ ℝ)
44 df-5 12282 . . . . 5 5 = (4 + 1)
45 4z 12600 . . . . . 6 4 ∈ β„€
46 uzid 12841 . . . . . 6 (4 ∈ β„€ β†’ 4 ∈ (β„€β‰₯β€˜4))
47 peano2uz 12889 . . . . . 6 (4 ∈ (β„€β‰₯β€˜4) β†’ (4 + 1) ∈ (β„€β‰₯β€˜4))
4845, 46, 47mp2b 10 . . . . 5 (4 + 1) ∈ (β„€β‰₯β€˜4)
4944, 48eqeltri 2827 . . . 4 5 ∈ (β„€β‰₯β€˜4)
50 eqid 2730 . . . . 5 (β„€β‰₯β€˜4) = (β„€β‰₯β€˜4)
5150uztrn2 12845 . . . 4 ((5 ∈ (β„€β‰₯β€˜4) ∧ 𝑁 ∈ (β„€β‰₯β€˜5)) β†’ 𝑁 ∈ (β„€β‰₯β€˜4))
5249, 3, 51sylancr 585 . . 3 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜4))
53 bclbnd 27019 . . 3 (𝑁 ∈ (β„€β‰₯β€˜4) β†’ ((4↑𝑁) / 𝑁) < ((2 Β· 𝑁)C𝑁))
5452, 53syl 17 . 2 (πœ‘ β†’ ((4↑𝑁) / 𝑁) < ((2 Β· 𝑁)C𝑁))
55 bpos.3 . . . . . . . 8 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑(𝑛 pCnt ((2 Β· 𝑁)C𝑁))), 1))
56 id 22 . . . . . . . . . 10 (𝑛 ∈ β„™ β†’ 𝑛 ∈ β„™)
57 pccl 16786 . . . . . . . . . 10 ((𝑛 ∈ β„™ ∧ ((2 Β· 𝑁)C𝑁) ∈ β„•) β†’ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
5856, 14, 57syl2anr 595 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ β„™) β†’ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
5958ralrimiva 3144 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘› ∈ β„™ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
6055, 59pcmptcl 16828 . . . . . . 7 (πœ‘ β†’ (𝐹:β„•βŸΆβ„• ∧ seq1( Β· , 𝐹):β„•βŸΆβ„•))
6160simprd 494 . . . . . 6 (πœ‘ β†’ seq1( Β· , 𝐹):β„•βŸΆβ„•)
62 bpos.2 . . . . . . . . 9 (πœ‘ β†’ Β¬ βˆƒπ‘ ∈ β„™ (𝑁 < 𝑝 ∧ 𝑝 ≀ (2 Β· 𝑁)))
63 bpos.4 . . . . . . . . 9 𝐾 = (βŒŠβ€˜((2 Β· 𝑁) / 3))
64 bpos.5 . . . . . . . . 9 𝑀 = (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁)))
653, 62, 55, 63, 64bposlem4 27026 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ (3...𝐾))
66 elfzuz 13501 . . . . . . . 8 (𝑀 ∈ (3...𝐾) β†’ 𝑀 ∈ (β„€β‰₯β€˜3))
6765, 66syl 17 . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ (β„€β‰₯β€˜3))
68 eluznn 12906 . . . . . . 7 ((3 ∈ β„• ∧ 𝑀 ∈ (β„€β‰₯β€˜3)) β†’ 𝑀 ∈ β„•)
6923, 67, 68sylancr 585 . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„•)
7061, 69ffvelcdmd 7086 . . . . 5 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ β„•)
7170nnred 12231 . . . 4 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ)
72 2z 12598 . . . . . . . . 9 2 ∈ β„€
73 nndivre 12257 . . . . . . . . . . . 12 (((2 Β· 𝑁) ∈ ℝ ∧ 3 ∈ β„•) β†’ ((2 Β· 𝑁) / 3) ∈ ℝ)
7420, 23, 73sylancl 584 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· 𝑁) / 3) ∈ ℝ)
7574flcld 13767 . . . . . . . . . 10 (πœ‘ β†’ (βŒŠβ€˜((2 Β· 𝑁) / 3)) ∈ β„€)
7663, 75eqeltrid 2835 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ β„€)
77 zmulcl 12615 . . . . . . . . 9 ((2 ∈ β„€ ∧ 𝐾 ∈ β„€) β†’ (2 Β· 𝐾) ∈ β„€)
7872, 76, 77sylancr 585 . . . . . . . 8 (πœ‘ β†’ (2 Β· 𝐾) ∈ β„€)
792nnzi 12590 . . . . . . . 8 5 ∈ β„€
80 zsubcl 12608 . . . . . . . 8 (((2 Β· 𝐾) ∈ β„€ ∧ 5 ∈ β„€) β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ β„€)
8178, 79, 80sylancl 584 . . . . . . 7 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ β„€)
8281zred 12670 . . . . . 6 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ ℝ)
83 rpcxpcl 26420 . . . . . 6 ((2 ∈ ℝ+ ∧ ((2 Β· 𝐾) βˆ’ 5) ∈ ℝ) β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ+)
8431, 82, 83sylancr 585 . . . . 5 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ+)
8584rpred 13020 . . . 4 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ)
8671, 85remulcld 11248 . . 3 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ∈ ℝ)
873, 62, 55, 63bposlem3 27025 . . . 4 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) = ((2 Β· 𝑁)C𝑁))
88 elfzuz3 13502 . . . . . . . . . 10 (𝑀 ∈ (3...𝐾) β†’ 𝐾 ∈ (β„€β‰₯β€˜π‘€))
8965, 88syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ (β„€β‰₯β€˜π‘€))
9055, 59, 69, 89pcmptdvds 16831 . . . . . . . 8 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) βˆ₯ (seq1( Β· , 𝐹)β€˜πΎ))
9170nnzd 12589 . . . . . . . . 9 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ β„€)
9270nnne0d 12266 . . . . . . . . 9 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) β‰  0)
93 uztrn 12844 . . . . . . . . . . . . 13 ((𝐾 ∈ (β„€β‰₯β€˜π‘€) ∧ 𝑀 ∈ (β„€β‰₯β€˜3)) β†’ 𝐾 ∈ (β„€β‰₯β€˜3))
9489, 67, 93syl2anc 582 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐾 ∈ (β„€β‰₯β€˜3))
95 eluznn 12906 . . . . . . . . . . . 12 ((3 ∈ β„• ∧ 𝐾 ∈ (β„€β‰₯β€˜3)) β†’ 𝐾 ∈ β„•)
9623, 94, 95sylancr 585 . . . . . . . . . . 11 (πœ‘ β†’ 𝐾 ∈ β„•)
9761, 96ffvelcdmd 7086 . . . . . . . . . 10 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) ∈ β„•)
9897nnzd 12589 . . . . . . . . 9 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) ∈ β„€)
99 dvdsval2 16204 . . . . . . . . 9 (((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„€ ∧ (seq1( Β· , 𝐹)β€˜π‘€) β‰  0 ∧ (seq1( Β· , 𝐹)β€˜πΎ) ∈ β„€) β†’ ((seq1( Β· , 𝐹)β€˜π‘€) βˆ₯ (seq1( Β· , 𝐹)β€˜πΎ) ↔ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€))
10091, 92, 98, 99syl3anc 1369 . . . . . . . 8 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) βˆ₯ (seq1( Β· , 𝐹)β€˜πΎ) ↔ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€))
10190, 100mpbid 231 . . . . . . 7 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€)
102101zred 12670 . . . . . 6 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ ℝ)
10369nnred 12231 . . . . . . . . 9 (πœ‘ β†’ 𝑀 ∈ ℝ)
10476zred 12670 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ ℝ)
105 eluzle 12839 . . . . . . . . . 10 (𝐾 ∈ (β„€β‰₯β€˜π‘€) β†’ 𝑀 ≀ 𝐾)
10689, 105syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝑀 ≀ 𝐾)
107 efchtdvds 26899 . . . . . . . . 9 ((𝑀 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑀 ≀ 𝐾) β†’ (expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)))
108103, 104, 106, 107syl3anc 1369 . . . . . . . 8 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)))
109 efchtcl 26851 . . . . . . . . . . 11 (𝑀 ∈ ℝ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ β„•)
110103, 109syl 17 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ β„•)
111110nnzd 12589 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ β„€)
112110nnne0d 12266 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) β‰  0)
113 efchtcl 26851 . . . . . . . . . . 11 (𝐾 ∈ ℝ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„•)
114104, 113syl 17 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„•)
115114nnzd 12589 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„€)
116 dvdsval2 16204 . . . . . . . . 9 (((expβ€˜(ΞΈβ€˜π‘€)) ∈ β„€ ∧ (expβ€˜(ΞΈβ€˜π‘€)) β‰  0 ∧ (expβ€˜(ΞΈβ€˜πΎ)) ∈ β„€) β†’ ((expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€))
117111, 112, 115, 116syl3anc 1369 . . . . . . . 8 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜π‘€)) βˆ₯ (expβ€˜(ΞΈβ€˜πΎ)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€))
118108, 117mpbid 231 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€)
119118zred 12670 . . . . . 6 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ ℝ)
120 prmz 16616 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„€)
121 fllt 13775 . . . . . . . . . . . . . . . . . 18 (((βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ ∧ 𝑝 ∈ β„€) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁))) < 𝑝))
12222, 120, 121syl2an 594 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁))) < 𝑝))
12364breq1i 5154 . . . . . . . . . . . . . . . . 17 (𝑀 < 𝑝 ↔ (βŒŠβ€˜(βˆšβ€˜(2 Β· 𝑁))) < 𝑝)
124122, 123bitr4di 288 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ 𝑀 < 𝑝))
125120zred 12670 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ β„™ β†’ 𝑝 ∈ ℝ)
126 ltnle 11297 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℝ ∧ 𝑝 ∈ ℝ) β†’ (𝑀 < 𝑝 ↔ Β¬ 𝑝 ≀ 𝑀))
127103, 125, 126syl2an 594 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑀 < 𝑝 ↔ Β¬ 𝑝 ≀ 𝑀))
128124, 127bitrd 278 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ Β¬ 𝑝 ≀ 𝑀))
129 bposlem1 27023 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ β„• ∧ 𝑝 ∈ β„™) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁))
1305, 129sylan 578 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁))
131125adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝑝 ∈ ℝ)
132 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„™)
133 pccl 16786 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ∈ β„™ ∧ ((2 Β· 𝑁)C𝑁) ∈ β„•) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
134132, 14, 133syl2anr 595 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
135131, 134reexpcld 14132 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ∈ ℝ)
13620adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (2 Β· 𝑁) ∈ ℝ)
137131resqcld 14094 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝↑2) ∈ ℝ)
138 lelttr 11308 . . . . . . . . . . . . . . . . . . . 20 (((𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ∈ ℝ ∧ (2 Β· 𝑁) ∈ ℝ ∧ (𝑝↑2) ∈ ℝ) β†’ (((𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁) ∧ (2 Β· 𝑁) < (𝑝↑2)) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
139135, 136, 137, 138syl3anc 1369 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) ≀ (2 Β· 𝑁) ∧ (2 Β· 𝑁) < (𝑝↑2)) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
140130, 139mpand 691 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((2 Β· 𝑁) < (𝑝↑2) β†’ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
141 resqrtth 15206 . . . . . . . . . . . . . . . . . . . . 21 (((2 Β· 𝑁) ∈ ℝ ∧ 0 ≀ (2 Β· 𝑁)) β†’ ((βˆšβ€˜(2 Β· 𝑁))↑2) = (2 Β· 𝑁))
14220, 21, 141syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((βˆšβ€˜(2 Β· 𝑁))↑2) = (2 Β· 𝑁))
143142breq1d 5157 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) ↔ (2 Β· 𝑁) < (𝑝↑2)))
144143adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) ↔ (2 Β· 𝑁) < (𝑝↑2)))
145134nn0zd 12588 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„€)
14672a1i 11 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 2 ∈ β„€)
147 prmgt1 16638 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ β„™ β†’ 1 < 𝑝)
148147adantl 480 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 1 < 𝑝)
149131, 145, 146, 148ltexp2d 14218 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < 2 ↔ (𝑝↑(𝑝 pCnt ((2 Β· 𝑁)C𝑁))) < (𝑝↑2)))
150140, 144, 1493imtr4d 293 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < 2))
151 df-2 12279 . . . . . . . . . . . . . . . . . 18 2 = (1 + 1)
152151breq2i 5155 . . . . . . . . . . . . . . . . 17 ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < 2 ↔ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1))
153150, 152imbitrdi 250 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1)))
15422adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (βˆšβ€˜(2 Β· 𝑁)) ∈ ℝ)
15520, 21sqrtge0d 15371 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 0 ≀ (βˆšβ€˜(2 Β· 𝑁)))
156155adantr 479 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 0 ≀ (βˆšβ€˜(2 Β· 𝑁)))
157 prmnn 16615 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ β„™ β†’ 𝑝 ∈ β„•)
158157nnrpd 13018 . . . . . . . . . . . . . . . . . . 19 (𝑝 ∈ β„™ β†’ 𝑝 ∈ ℝ+)
159158rpge0d 13024 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ β„™ β†’ 0 ≀ 𝑝)
160159adantl 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 0 ≀ 𝑝)
161154, 131, 156, 160lt2sqd 14223 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 ↔ ((βˆšβ€˜(2 Β· 𝑁))↑2) < (𝑝↑2)))
162 1z 12596 . . . . . . . . . . . . . . . . 17 1 ∈ β„€
163 zleltp1 12617 . . . . . . . . . . . . . . . . 17 (((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„€ ∧ 1 ∈ β„€) β†’ ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1 ↔ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1)))
164145, 162, 163sylancl 584 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1 ↔ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) < (1 + 1)))
165153, 161, 1643imtr4d 293 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((βˆšβ€˜(2 Β· 𝑁)) < 𝑝 β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1))
166128, 165sylbird 259 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (Β¬ 𝑝 ≀ 𝑀 β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1))
167166imp 405 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ Β¬ 𝑝 ≀ 𝑀) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1)
168167adantrl 712 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ (𝑝 pCnt ((2 Β· 𝑁)C𝑁)) ≀ 1)
169 iftrue 4533 . . . . . . . . . . . . 13 ((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 Β· 𝑁)C𝑁)))
170169adantl 480 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) = (𝑝 pCnt ((2 Β· 𝑁)C𝑁)))
171 iftrue 4533 . . . . . . . . . . . . 13 ((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) = 1)
172171adantl 480 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) = 1)
173168, 170, 1723brtr4d 5179 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
174 0le0 12317 . . . . . . . . . . . . 13 0 ≀ 0
175 iffalse 4536 . . . . . . . . . . . . . 14 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) = 0)
176 iffalse 4536 . . . . . . . . . . . . . 14 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) = 0)
177175, 176breq12d 5160 . . . . . . . . . . . . 13 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ (if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0) ↔ 0 ≀ 0))
178174, 177mpbiri 257 . . . . . . . . . . . 12 (Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
179178adantl 480 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑝 ∈ β„™) ∧ Β¬ (𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀)) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
180173, 179pm2.61dan 809 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0) ≀ if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
18159adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ βˆ€π‘› ∈ β„™ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) ∈ β„•0)
18269adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝑀 ∈ β„•)
183 simpr 483 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝑝 ∈ β„™)
184 oveq1 7418 . . . . . . . . . . 11 (𝑛 = 𝑝 β†’ (𝑛 pCnt ((2 Β· 𝑁)C𝑁)) = (𝑝 pCnt ((2 Β· 𝑁)C𝑁)))
18589adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ 𝐾 ∈ (β„€β‰₯β€˜π‘€))
18655, 181, 182, 183, 184, 185pcmpt2 16830 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) = if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), (𝑝 pCnt ((2 Β· 𝑁)C𝑁)), 0))
187 eqid 2730 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1))
188187prmorcht 26918 . . . . . . . . . . . . . . 15 (𝐾 ∈ β„• β†’ (expβ€˜(ΞΈβ€˜πΎ)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ))
18996, 188syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ))
190187prmorcht 26918 . . . . . . . . . . . . . . 15 (𝑀 ∈ β„• β†’ (expβ€˜(ΞΈβ€˜π‘€)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))
19169, 190syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) = (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))
192189, 191oveq12d 7429 . . . . . . . . . . . . 13 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) = ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€)))
193192adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) = ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€)))
194193oveq2d 7427 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))) = (𝑝 pCnt ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))))
195 nncn 12224 . . . . . . . . . . . . . . . 16 (𝑛 ∈ β„• β†’ 𝑛 ∈ β„‚)
196195exp1d 14110 . . . . . . . . . . . . . . 15 (𝑛 ∈ β„• β†’ (𝑛↑1) = 𝑛)
197196ifeq1d 4546 . . . . . . . . . . . . . 14 (𝑛 ∈ β„• β†’ if(𝑛 ∈ β„™, (𝑛↑1), 1) = if(𝑛 ∈ β„™, 𝑛, 1))
198197mpteq2ia 5250 . . . . . . . . . . . . 13 (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑1), 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1))
199198eqcomi 2739 . . . . . . . . . . . 12 (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)) = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (𝑛↑1), 1))
200 1nn0 12492 . . . . . . . . . . . . . . 15 1 ∈ β„•0
201200a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ β„™) β†’ 1 ∈ β„•0)
202201ralrimiva 3144 . . . . . . . . . . . . 13 (πœ‘ β†’ βˆ€π‘› ∈ β„™ 1 ∈ β„•0)
203202adantr 479 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ βˆ€π‘› ∈ β„™ 1 ∈ β„•0)
204 eqidd 2731 . . . . . . . . . . . 12 (𝑛 = 𝑝 β†’ 1 = 1)
205199, 203, 182, 183, 204, 185pcmpt2 16830 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜πΎ) / (seq1( Β· , (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, 𝑛, 1)))β€˜π‘€))) = if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
206194, 205eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))) = if((𝑝 ≀ 𝐾 ∧ Β¬ 𝑝 ≀ 𝑀), 1, 0))
207180, 186, 2063brtr4d 5179 . . . . . . . . 9 ((πœ‘ ∧ 𝑝 ∈ β„™) β†’ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
208207ralrimiva 3144 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
209 pc2dvds 16816 . . . . . . . . 9 ((((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€ ∧ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€) β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ↔ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))))
210101, 118, 209syl2anc 582 . . . . . . . 8 (πœ‘ β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ↔ βˆ€π‘ ∈ β„™ (𝑝 pCnt ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€))) ≀ (𝑝 pCnt ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))))
211208, 210mpbird 256 . . . . . . 7 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))
212114nnred 12231 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ)
213110nnred 12231 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜π‘€)) ∈ ℝ)
214114nngt0d 12265 . . . . . . . . . 10 (πœ‘ β†’ 0 < (expβ€˜(ΞΈβ€˜πΎ)))
215110nngt0d 12265 . . . . . . . . . 10 (πœ‘ β†’ 0 < (expβ€˜(ΞΈβ€˜π‘€)))
216212, 213, 214, 215divgt0d 12153 . . . . . . . . 9 (πœ‘ β†’ 0 < ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))
217 elnnz 12572 . . . . . . . . 9 (((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„• ↔ (((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„€ ∧ 0 < ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
218118, 216, 217sylanbrc 581 . . . . . . . 8 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„•)
219 dvdsle 16257 . . . . . . . 8 ((((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ∈ β„€ ∧ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) ∈ β„•) β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ≀ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
220101, 218, 219syl2anc 582 . . . . . . 7 (πœ‘ β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) βˆ₯ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ≀ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€)))))
221211, 220mpd 15 . . . . . 6 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) ≀ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))))
222 nndivre 12257 . . . . . . . 8 (((expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ ∧ 4 ∈ β„•) β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / 4) ∈ ℝ)
223212, 1, 222sylancl 584 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / 4) ∈ ℝ)
224 4re 12300 . . . . . . . . . 10 4 ∈ ℝ
225224a1i 11 . . . . . . . . 9 (πœ‘ β†’ 4 ∈ ℝ)
226 6re 12306 . . . . . . . . . 10 6 ∈ ℝ
227226a1i 11 . . . . . . . . 9 (πœ‘ β†’ 6 ∈ ℝ)
228 4lt6 12398 . . . . . . . . . 10 4 < 6
229228a1i 11 . . . . . . . . 9 (πœ‘ β†’ 4 < 6)
230 cht3 26913 . . . . . . . . . . . 12 (ΞΈβ€˜3) = (logβ€˜6)
231230fveq2i 6893 . . . . . . . . . . 11 (expβ€˜(ΞΈβ€˜3)) = (expβ€˜(logβ€˜6))
232 6pos 12326 . . . . . . . . . . . . 13 0 < 6
233226, 232elrpii 12981 . . . . . . . . . . . 12 6 ∈ ℝ+
234 reeflog 26325 . . . . . . . . . . . 12 (6 ∈ ℝ+ β†’ (expβ€˜(logβ€˜6)) = 6)
235233, 234ax-mp 5 . . . . . . . . . . 11 (expβ€˜(logβ€˜6)) = 6
236231, 235eqtri 2758 . . . . . . . . . 10 (expβ€˜(ΞΈβ€˜3)) = 6
237 3re 12296 . . . . . . . . . . . . 13 3 ∈ ℝ
238237a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ 3 ∈ ℝ)
239 eluzle 12839 . . . . . . . . . . . . 13 (𝑀 ∈ (β„€β‰₯β€˜3) β†’ 3 ≀ 𝑀)
24067, 239syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 3 ≀ 𝑀)
241 chtwordi 26896 . . . . . . . . . . . 12 ((3 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 3 ≀ 𝑀) β†’ (ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€))
242238, 103, 240, 241syl3anc 1369 . . . . . . . . . . 11 (πœ‘ β†’ (ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€))
243 chtcl 26849 . . . . . . . . . . . . 13 (3 ∈ ℝ β†’ (ΞΈβ€˜3) ∈ ℝ)
244237, 243ax-mp 5 . . . . . . . . . . . 12 (ΞΈβ€˜3) ∈ ℝ
245 chtcl 26849 . . . . . . . . . . . . 13 (𝑀 ∈ ℝ β†’ (ΞΈβ€˜π‘€) ∈ ℝ)
246103, 245syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (ΞΈβ€˜π‘€) ∈ ℝ)
247 efle 16065 . . . . . . . . . . . 12 (((ΞΈβ€˜3) ∈ ℝ ∧ (ΞΈβ€˜π‘€) ∈ ℝ) β†’ ((ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€) ↔ (expβ€˜(ΞΈβ€˜3)) ≀ (expβ€˜(ΞΈβ€˜π‘€))))
248244, 246, 247sylancr 585 . . . . . . . . . . 11 (πœ‘ β†’ ((ΞΈβ€˜3) ≀ (ΞΈβ€˜π‘€) ↔ (expβ€˜(ΞΈβ€˜3)) ≀ (expβ€˜(ΞΈβ€˜π‘€))))
249242, 248mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜3)) ≀ (expβ€˜(ΞΈβ€˜π‘€)))
250236, 249eqbrtrrid 5183 . . . . . . . . 9 (πœ‘ β†’ 6 ≀ (expβ€˜(ΞΈβ€˜π‘€)))
251225, 227, 213, 229, 250ltletrd 11378 . . . . . . . 8 (πœ‘ β†’ 4 < (expβ€˜(ΞΈβ€˜π‘€)))
252 4pos 12323 . . . . . . . . . 10 0 < 4
253252a1i 11 . . . . . . . . 9 (πœ‘ β†’ 0 < 4)
254 ltdiv2 12104 . . . . . . . . 9 (((4 ∈ ℝ ∧ 0 < 4) ∧ ((expβ€˜(ΞΈβ€˜π‘€)) ∈ ℝ ∧ 0 < (expβ€˜(ΞΈβ€˜π‘€))) ∧ ((expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ ∧ 0 < (expβ€˜(ΞΈβ€˜πΎ)))) β†’ (4 < (expβ€˜(ΞΈβ€˜π‘€)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < ((expβ€˜(ΞΈβ€˜πΎ)) / 4)))
255225, 253, 213, 215, 212, 214, 254syl222anc 1384 . . . . . . . 8 (πœ‘ β†’ (4 < (expβ€˜(ΞΈβ€˜π‘€)) ↔ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < ((expβ€˜(ΞΈβ€˜πΎ)) / 4)))
256251, 255mpbid 231 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < ((expβ€˜(ΞΈβ€˜πΎ)) / 4))
25726a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 2 ∈ ℝ)
258 2lt3 12388 . . . . . . . . . . . . . 14 2 < 3
259258a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ 2 < 3)
260238, 103, 104, 240, 106letrd 11375 . . . . . . . . . . . . 13 (πœ‘ β†’ 3 ≀ 𝐾)
261257, 238, 104, 259, 260ltletrd 11378 . . . . . . . . . . . 12 (πœ‘ β†’ 2 < 𝐾)
262 chtub 26951 . . . . . . . . . . . 12 ((𝐾 ∈ ℝ ∧ 2 < 𝐾) β†’ (ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
263104, 261, 262syl2anc 582 . . . . . . . . . . 11 (πœ‘ β†’ (ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
264 chtcl 26849 . . . . . . . . . . . . 13 (𝐾 ∈ ℝ β†’ (ΞΈβ€˜πΎ) ∈ ℝ)
265104, 264syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (ΞΈβ€˜πΎ) ∈ ℝ)
266 relogcl 26320 . . . . . . . . . . . . . 14 (2 ∈ ℝ+ β†’ (logβ€˜2) ∈ ℝ)
26731, 266ax-mp 5 . . . . . . . . . . . . 13 (logβ€˜2) ∈ ℝ
268 3z 12599 . . . . . . . . . . . . . . 15 3 ∈ β„€
269 zsubcl 12608 . . . . . . . . . . . . . . 15 (((2 Β· 𝐾) ∈ β„€ ∧ 3 ∈ β„€) β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€)
27078, 268, 269sylancl 584 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€)
271270zred 12670 . . . . . . . . . . . . 13 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ ℝ)
272 remulcl 11197 . . . . . . . . . . . . 13 (((logβ€˜2) ∈ ℝ ∧ ((2 Β· 𝐾) βˆ’ 3) ∈ ℝ) β†’ ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ∈ ℝ)
273267, 271, 272sylancr 585 . . . . . . . . . . . 12 (πœ‘ β†’ ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ∈ ℝ)
274 eflt 16064 . . . . . . . . . . . 12 (((ΞΈβ€˜πΎ) ∈ ℝ ∧ ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ∈ ℝ) β†’ ((ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))))
275265, 273, 274syl2anc 582 . . . . . . . . . . 11 (πœ‘ β†’ ((ΞΈβ€˜πΎ) < ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))))
276263, 275mpbid 231 . . . . . . . . . 10 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) < (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3))))
277 reexplog 26339 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€) β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = (expβ€˜(((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2))))
27831, 270, 277sylancr 585 . . . . . . . . . . 11 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = (expβ€˜(((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2))))
279270zcnd 12671 . . . . . . . . . . . . 13 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) ∈ β„‚)
280267recni 11232 . . . . . . . . . . . . 13 (logβ€˜2) ∈ β„‚
281 mulcom 11198 . . . . . . . . . . . . 13 ((((2 Β· 𝐾) βˆ’ 3) ∈ β„‚ ∧ (logβ€˜2) ∈ β„‚) β†’ (((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2)) = ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
282279, 280, 281sylancl 584 . . . . . . . . . . . 12 (πœ‘ β†’ (((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2)) = ((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3)))
283282fveq2d 6894 . . . . . . . . . . 11 (πœ‘ β†’ (expβ€˜(((2 Β· 𝐾) βˆ’ 3) Β· (logβ€˜2))) = (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3))))
284278, 283eqtrd 2770 . . . . . . . . . 10 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = (expβ€˜((logβ€˜2) Β· ((2 Β· 𝐾) βˆ’ 3))))
285276, 284breqtrrd 5175 . . . . . . . . 9 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) < (2↑((2 Β· 𝐾) βˆ’ 3)))
286 3p2e5 12367 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
287286oveq1i 7421 . . . . . . . . . . . . . . 15 ((3 + 2) βˆ’ 2) = (5 βˆ’ 2)
288 3cn 12297 . . . . . . . . . . . . . . . 16 3 ∈ β„‚
289 2cn 12291 . . . . . . . . . . . . . . . 16 2 ∈ β„‚
290288, 289pncan3oi 11480 . . . . . . . . . . . . . . 15 ((3 + 2) βˆ’ 2) = 3
291287, 290eqtr3i 2760 . . . . . . . . . . . . . 14 (5 βˆ’ 2) = 3
292291oveq2i 7422 . . . . . . . . . . . . 13 ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = ((2 Β· 𝐾) βˆ’ 3)
29378zcnd 12671 . . . . . . . . . . . . . 14 (πœ‘ β†’ (2 Β· 𝐾) ∈ β„‚)
294 5cn 12304 . . . . . . . . . . . . . . 15 5 ∈ β„‚
295 subsub 11494 . . . . . . . . . . . . . . 15 (((2 Β· 𝐾) ∈ β„‚ ∧ 5 ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = (((2 Β· 𝐾) βˆ’ 5) + 2))
296294, 289, 295mp3an23 1451 . . . . . . . . . . . . . 14 ((2 Β· 𝐾) ∈ β„‚ β†’ ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = (((2 Β· 𝐾) βˆ’ 5) + 2))
297293, 296syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ (5 βˆ’ 2)) = (((2 Β· 𝐾) βˆ’ 5) + 2))
298292, 297eqtr3id 2784 . . . . . . . . . . . 12 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 3) = (((2 Β· 𝐾) βˆ’ 5) + 2))
299298oveq2d 7427 . . . . . . . . . . 11 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 3)) = (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)))
300 2ne0 12320 . . . . . . . . . . . 12 2 β‰  0
301 cxpexpz 26411 . . . . . . . . . . . 12 ((2 ∈ β„‚ ∧ 2 β‰  0 ∧ ((2 Β· 𝐾) βˆ’ 3) ∈ β„€) β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 3)) = (2↑((2 Β· 𝐾) βˆ’ 3)))
302289, 300, 270, 301mp3an12i 1463 . . . . . . . . . . 11 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 3)) = (2↑((2 Β· 𝐾) βˆ’ 3)))
30381zcnd 12671 . . . . . . . . . . . 12 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ∈ β„‚)
304 2cnne0 12426 . . . . . . . . . . . . 13 (2 ∈ β„‚ ∧ 2 β‰  0)
305 cxpadd 26423 . . . . . . . . . . . . 13 (((2 ∈ β„‚ ∧ 2 β‰  0) ∧ ((2 Β· 𝐾) βˆ’ 5) ∈ β„‚ ∧ 2 ∈ β„‚) β†’ (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
306304, 289, 305mp3an13 1450 . . . . . . . . . . . 12 (((2 Β· 𝐾) βˆ’ 5) ∈ β„‚ β†’ (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
307303, 306syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (2↑𝑐(((2 Β· 𝐾) βˆ’ 5) + 2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
308299, 302, 3073eqtr3d 2778 . . . . . . . . . 10 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)))
309 2nn0 12493 . . . . . . . . . . . . 13 2 ∈ β„•0
310 cxpexp 26412 . . . . . . . . . . . . 13 ((2 ∈ β„‚ ∧ 2 ∈ β„•0) β†’ (2↑𝑐2) = (2↑2))
311289, 309, 310mp2an 688 . . . . . . . . . . . 12 (2↑𝑐2) = (2↑2)
312 sq2 14165 . . . . . . . . . . . 12 (2↑2) = 4
313311, 312eqtri 2758 . . . . . . . . . . 11 (2↑𝑐2) = 4
314313oveq2i 7422 . . . . . . . . . 10 ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· (2↑𝑐2)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4)
315308, 314eqtrdi 2786 . . . . . . . . 9 (πœ‘ β†’ (2↑((2 Β· 𝐾) βˆ’ 3)) = ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4))
316285, 315breqtrd 5173 . . . . . . . 8 (πœ‘ β†’ (expβ€˜(ΞΈβ€˜πΎ)) < ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4))
317224, 252pm3.2i 469 . . . . . . . . . 10 (4 ∈ ℝ ∧ 0 < 4)
318317a1i 11 . . . . . . . . 9 (πœ‘ β†’ (4 ∈ ℝ ∧ 0 < 4))
319 ltdivmul2 12095 . . . . . . . . 9 (((expβ€˜(ΞΈβ€˜πΎ)) ∈ ℝ ∧ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) β†’ (((expβ€˜(ΞΈβ€˜πΎ)) / 4) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4)))
320212, 85, 318, 319syl3anc 1369 . . . . . . . 8 (πœ‘ β†’ (((expβ€˜(ΞΈβ€˜πΎ)) / 4) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (expβ€˜(ΞΈβ€˜πΎ)) < ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) Β· 4)))
321316, 320mpbird 256 . . . . . . 7 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / 4) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))
322119, 223, 85, 256, 321lttrd 11379 . . . . . 6 (πœ‘ β†’ ((expβ€˜(ΞΈβ€˜πΎ)) / (expβ€˜(ΞΈβ€˜π‘€))) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))
323102, 119, 85, 221, 322lelttrd 11376 . . . . 5 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))
32497nnred 12231 . . . . . 6 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) ∈ ℝ)
325 nnre 12223 . . . . . . . 8 ((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„• β†’ (seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ)
326 nngt0 12247 . . . . . . . 8 ((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„• β†’ 0 < (seq1( Β· , 𝐹)β€˜π‘€))
327325, 326jca 510 . . . . . . 7 ((seq1( Β· , 𝐹)β€˜π‘€) ∈ β„• β†’ ((seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ ∧ 0 < (seq1( Β· , 𝐹)β€˜π‘€)))
32870, 327syl 17 . . . . . 6 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ ∧ 0 < (seq1( Β· , 𝐹)β€˜π‘€)))
329 ltdivmul 12093 . . . . . 6 (((seq1( Β· , 𝐹)β€˜πΎ) ∈ ℝ ∧ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ∈ ℝ ∧ ((seq1( Β· , 𝐹)β€˜π‘€) ∈ ℝ ∧ 0 < (seq1( Β· , 𝐹)β€˜π‘€))) β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (seq1( Β· , 𝐹)β€˜πΎ) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))))
330324, 85, 328, 329syl3anc 1369 . . . . 5 (πœ‘ β†’ (((seq1( Β· , 𝐹)β€˜πΎ) / (seq1( Β· , 𝐹)β€˜π‘€)) < (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ↔ (seq1( Β· , 𝐹)β€˜πΎ) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))))
331323, 330mpbid 231 . . . 4 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜πΎ) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))))
33287, 331eqbrtrrd 5171 . . 3 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) < ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))))
33330, 85remulcld 11248 . . . 4 (πœ‘ β†’ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ∈ ℝ)
3343, 62, 55, 63, 64bposlem5 27027 . . . . 5 (πœ‘ β†’ (seq1( Β· , 𝐹)β€˜π‘€) ≀ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)))
33571, 30, 84lemul1d 13063 . . . . 5 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) ≀ ((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) ↔ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5)))))
336334, 335mpbid 231 . . . 4 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))))
33778zred 12670 . . . . . . 7 (πœ‘ β†’ (2 Β· 𝐾) ∈ ℝ)
33837a1i 11 . . . . . . 7 (πœ‘ β†’ 5 ∈ ℝ)
339 flle 13768 . . . . . . . . . . 11 (((2 Β· 𝑁) / 3) ∈ ℝ β†’ (βŒŠβ€˜((2 Β· 𝑁) / 3)) ≀ ((2 Β· 𝑁) / 3))
34074, 339syl 17 . . . . . . . . . 10 (πœ‘ β†’ (βŒŠβ€˜((2 Β· 𝑁) / 3)) ≀ ((2 Β· 𝑁) / 3))
34163, 340eqbrtrid 5182 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ≀ ((2 Β· 𝑁) / 3))
342 2pos 12319 . . . . . . . . . . . 12 0 < 2
34326, 342pm3.2i 469 . . . . . . . . . . 11 (2 ∈ ℝ ∧ 0 < 2)
344343a1i 11 . . . . . . . . . 10 (πœ‘ β†’ (2 ∈ ℝ ∧ 0 < 2))
345 lemul2 12071 . . . . . . . . . 10 ((𝐾 ∈ ℝ ∧ ((2 Β· 𝑁) / 3) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) β†’ (𝐾 ≀ ((2 Β· 𝑁) / 3) ↔ (2 Β· 𝐾) ≀ (2 Β· ((2 Β· 𝑁) / 3))))
346104, 74, 344, 345syl3anc 1369 . . . . . . . . 9 (πœ‘ β†’ (𝐾 ≀ ((2 Β· 𝑁) / 3) ↔ (2 Β· 𝐾) ≀ (2 Β· ((2 Β· 𝑁) / 3))))
347341, 346mpbid 231 . . . . . . . 8 (πœ‘ β†’ (2 Β· 𝐾) ≀ (2 Β· ((2 Β· 𝑁) / 3)))
34818nncnd 12232 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· 𝑁) ∈ β„‚)
349 3ne0 12322 . . . . . . . . . . . 12 3 β‰  0
350288, 349pm3.2i 469 . . . . . . . . . . 11 (3 ∈ β„‚ ∧ 3 β‰  0)
351 divass 11894 . . . . . . . . . . 11 ((2 ∈ β„‚ ∧ (2 Β· 𝑁) ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((2 Β· (2 Β· 𝑁)) / 3) = (2 Β· ((2 Β· 𝑁) / 3)))
352289, 350, 351mp3an13 1450 . . . . . . . . . 10 ((2 Β· 𝑁) ∈ β„‚ β†’ ((2 Β· (2 Β· 𝑁)) / 3) = (2 Β· ((2 Β· 𝑁) / 3)))
353348, 352syl 17 . . . . . . . . 9 (πœ‘ β†’ ((2 Β· (2 Β· 𝑁)) / 3) = (2 Β· ((2 Β· 𝑁) / 3)))
3545nncnd 12232 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑁 ∈ β„‚)
355 mulass 11200 . . . . . . . . . . . 12 ((2 ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 𝑁 ∈ β„‚) β†’ ((2 Β· 2) Β· 𝑁) = (2 Β· (2 Β· 𝑁)))
356289, 289, 354, 355mp3an12i 1463 . . . . . . . . . . 11 (πœ‘ β†’ ((2 Β· 2) Β· 𝑁) = (2 Β· (2 Β· 𝑁)))
357 2t2e4 12380 . . . . . . . . . . . 12 (2 Β· 2) = 4
358357oveq1i 7421 . . . . . . . . . . 11 ((2 Β· 2) Β· 𝑁) = (4 Β· 𝑁)
359356, 358eqtr3di 2785 . . . . . . . . . 10 (πœ‘ β†’ (2 Β· (2 Β· 𝑁)) = (4 Β· 𝑁))
360359oveq1d 7426 . . . . . . . . 9 (πœ‘ β†’ ((2 Β· (2 Β· 𝑁)) / 3) = ((4 Β· 𝑁) / 3))
361353, 360eqtr3d 2772 . . . . . . . 8 (πœ‘ β†’ (2 Β· ((2 Β· 𝑁) / 3)) = ((4 Β· 𝑁) / 3))
362347, 361breqtrd 5173 . . . . . . 7 (πœ‘ β†’ (2 Β· 𝐾) ≀ ((4 Β· 𝑁) / 3))
363337, 36, 338, 362lesub1dd 11834 . . . . . 6 (πœ‘ β†’ ((2 Β· 𝐾) βˆ’ 5) ≀ (((4 Β· 𝑁) / 3) βˆ’ 5))
364 1lt2 12387 . . . . . . . 8 1 < 2
365364a1i 11 . . . . . . 7 (πœ‘ β†’ 1 < 2)
366257, 365, 82, 39cxpled 26464 . . . . . 6 (πœ‘ β†’ (((2 Β· 𝐾) βˆ’ 5) ≀ (((4 Β· 𝑁) / 3) βˆ’ 5) ↔ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ≀ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
367363, 366mpbid 231 . . . . 5 (πœ‘ β†’ (2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ≀ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)))
36885, 42, 29lemul2d 13064 . . . . 5 (πœ‘ β†’ ((2↑𝑐((2 Β· 𝐾) βˆ’ 5)) ≀ (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)) ↔ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5)))))
369367, 368mpbid 231 . . . 4 (πœ‘ β†’ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
37086, 333, 43, 336, 369letrd 11375 . . 3 (πœ‘ β†’ ((seq1( Β· , 𝐹)β€˜π‘€) Β· (2↑𝑐((2 Β· 𝐾) βˆ’ 5))) ≀ (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
37115, 86, 43, 332, 370ltletrd 11378 . 2 (πœ‘ β†’ ((2 Β· 𝑁)C𝑁) < (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
37210, 15, 43, 54, 371lttrd 11379 1 (πœ‘ β†’ ((4↑𝑁) / 𝑁) < (((2 Β· 𝑁)↑𝑐(((βˆšβ€˜(2 Β· 𝑁)) / 3) + 2)) Β· (2↑𝑐(((4 Β· 𝑁) / 3) βˆ’ 5))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  ifcif 4527   class class class wbr 5147   ↦ cmpt 5230  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448   / cdiv 11875  β„•cn 12216  2c2 12271  3c3 12272  4c4 12273  5c5 12274  6c6 12275  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  β„+crp 12978  ...cfz 13488  βŒŠcfl 13759  seqcseq 13970  β†‘cexp 14031  Ccbc 14266  βˆšcsqrt 15184  expce 16009   βˆ₯ cdvds 16201  β„™cprime 16612   pCnt cpc 16773  logclog 26299  β†‘𝑐ccxp 26300  ΞΈccht 26831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190  ax-addf 11191
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-xnn0 12549  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ioc 13333  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-fac 14238  df-bc 14267  df-hash 14295  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637  df-ef 16015  df-sin 16017  df-cos 16018  df-pi 16020  df-dvds 16202  df-gcd 16440  df-prm 16613  df-pc 16774  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-hom 17225  df-cco 17226  df-rest 17372  df-topn 17373  df-0g 17391  df-gsum 17392  df-topgen 17393  df-pt 17394  df-prds 17397  df-xrs 17452  df-qtop 17457  df-imas 17458  df-xps 17460  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-mulg 18987  df-cntz 19222  df-cmn 19691  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-cnfld 21145  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-lp 22860  df-perf 22861  df-cn 22951  df-cnp 22952  df-haus 23039  df-tx 23286  df-hmeo 23479  df-fil 23570  df-fm 23662  df-flim 23663  df-flf 23664  df-xms 24046  df-ms 24047  df-tms 24048  df-cncf 24618  df-limc 25615  df-dv 25616  df-log 26301  df-cxp 26302  df-cht 26837  df-ppi 26840
This theorem is referenced by:  bposlem9  27031
  Copyright terms: Public domain W3C validator