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

Theorem bposlem9 27253
Description: Lemma for bpos 27254. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)
Hypotheses
Ref Expression
bposlem7.1 ๐น = (๐‘› โˆˆ โ„• โ†ฆ ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) + ((9 / 4) ยท (๐บโ€˜(๐‘› / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘›)))))
bposlem7.2 ๐บ = (๐‘ฅ โˆˆ โ„+ โ†ฆ ((logโ€˜๐‘ฅ) / ๐‘ฅ))
bposlem9.3 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
bposlem9.4 (๐œ‘ โ†’ 64 < ๐‘)
bposlem9.5 (๐œ‘ โ†’ ยฌ โˆƒ๐‘ โˆˆ โ„™ (๐‘ < ๐‘ โˆง ๐‘ โ‰ค (2 ยท ๐‘)))
Assertion
Ref Expression
bposlem9 (๐œ‘ โ†’ ๐œ“)
Distinct variable groups:   ๐‘›,๐‘   ๐‘›,๐บ   ๐œ‘,๐‘›   ๐‘,๐‘   ๐‘ฅ,๐‘
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘)   ๐œ“(๐‘ฅ,๐‘›,๐‘)   ๐น(๐‘ฅ,๐‘›,๐‘)   ๐บ(๐‘ฅ,๐‘)

Proof of Theorem bposlem9
Dummy variable ๐‘ž is distinct from all other variables.
StepHypRef Expression
1 bposlem9.4 . . 3 (๐œ‘ โ†’ 64 < ๐‘)
2 bposlem7.1 . . . 4 ๐น = (๐‘› โˆˆ โ„• โ†ฆ ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) + ((9 / 4) ยท (๐บโ€˜(๐‘› / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘›)))))
3 bposlem7.2 . . . 4 ๐บ = (๐‘ฅ โˆˆ โ„+ โ†ฆ ((logโ€˜๐‘ฅ) / ๐‘ฅ))
4 6nn0 12533 . . . . . 6 6 โˆˆ โ„•0
5 4nn 12335 . . . . . 6 4 โˆˆ โ„•
64, 5decnncl 12737 . . . . 5 64 โˆˆ โ„•
76a1i 11 . . . 4 (๐œ‘ โ†’ 64 โˆˆ โ„•)
8 bposlem9.3 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
9 ere 16075 . . . . . . . 8 e โˆˆ โ„
10 8re 12348 . . . . . . . 8 8 โˆˆ โ„
11 egt2lt3 16192 . . . . . . . . . 10 (2 < e โˆง e < 3)
1211simpri 484 . . . . . . . . 9 e < 3
13 3lt8 12448 . . . . . . . . 9 3 < 8
14 3re 12332 . . . . . . . . . 10 3 โˆˆ โ„
159, 14, 10lttri 11380 . . . . . . . . 9 ((e < 3 โˆง 3 < 8) โ†’ e < 8)
1612, 13, 15mp2an 690 . . . . . . . 8 e < 8
179, 10, 16ltleii 11377 . . . . . . 7 e โ‰ค 8
18 0re 11256 . . . . . . . . 9 0 โˆˆ โ„
19 epos 16193 . . . . . . . . 9 0 < e
2018, 9, 19ltleii 11377 . . . . . . . 8 0 โ‰ค e
21 8pos 12364 . . . . . . . . 9 0 < 8
2218, 10, 21ltleii 11377 . . . . . . . 8 0 โ‰ค 8
23 le2sq 14140 . . . . . . . 8 (((e โˆˆ โ„ โˆง 0 โ‰ค e) โˆง (8 โˆˆ โ„ โˆง 0 โ‰ค 8)) โ†’ (e โ‰ค 8 โ†” (eโ†‘2) โ‰ค (8โ†‘2)))
249, 20, 10, 22, 23mp4an 691 . . . . . . 7 (e โ‰ค 8 โ†” (eโ†‘2) โ‰ค (8โ†‘2))
2517, 24mpbi 229 . . . . . 6 (eโ†‘2) โ‰ค (8โ†‘2)
2610recni 11268 . . . . . . . 8 8 โˆˆ โ„‚
2726sqvali 14185 . . . . . . 7 (8โ†‘2) = (8 ยท 8)
28 8t8e64 12838 . . . . . . 7 (8 ยท 8) = 64
2927, 28eqtri 2756 . . . . . 6 (8โ†‘2) = 64
3025, 29breqtri 5177 . . . . 5 (eโ†‘2) โ‰ค 64
3130a1i 11 . . . 4 (๐œ‘ โ†’ (eโ†‘2) โ‰ค 64)
329resqcli 14191 . . . . . 6 (eโ†‘2) โˆˆ โ„
3332a1i 11 . . . . 5 (๐œ‘ โ†’ (eโ†‘2) โˆˆ โ„)
346nnrei 12261 . . . . . 6 64 โˆˆ โ„
3534a1i 11 . . . . 5 (๐œ‘ โ†’ 64 โˆˆ โ„)
368nnred 12267 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
37 ltle 11342 . . . . . . 7 ((64 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (64 < ๐‘ โ†’ 64 โ‰ค ๐‘))
3834, 36, 37sylancr 585 . . . . . 6 (๐œ‘ โ†’ (64 < ๐‘ โ†’ 64 โ‰ค ๐‘))
391, 38mpd 15 . . . . 5 (๐œ‘ โ†’ 64 โ‰ค ๐‘)
4033, 35, 36, 31, 39letrd 11411 . . . 4 (๐œ‘ โ†’ (eโ†‘2) โ‰ค ๐‘)
412, 3, 7, 8, 31, 40bposlem7 27251 . . 3 (๐œ‘ โ†’ (64 < ๐‘ โ†’ (๐นโ€˜๐‘) < (๐นโ€˜64)))
421, 41mpd 15 . 2 (๐œ‘ โ†’ (๐นโ€˜๐‘) < (๐นโ€˜64))
432, 3bposlem8 27252 . . . . 5 ((๐นโ€˜64) โˆˆ โ„ โˆง (๐นโ€˜64) < (logโ€˜2))
4443a1i 11 . . . 4 (๐œ‘ โ†’ ((๐นโ€˜64) โˆˆ โ„ โˆง (๐นโ€˜64) < (logโ€˜2)))
4544simpld 493 . . 3 (๐œ‘ โ†’ (๐นโ€˜64) โˆˆ โ„)
46 2fveq3 6907 . . . . . . . . 9 (๐‘› = ๐‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘›)) = (๐บโ€˜(โˆšโ€˜๐‘)))
4746oveq2d 7442 . . . . . . . 8 (๐‘› = ๐‘ โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) = ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))))
48 fvoveq1 7449 . . . . . . . . 9 (๐‘› = ๐‘ โ†’ (๐บโ€˜(๐‘› / 2)) = (๐บโ€˜(๐‘ / 2)))
4948oveq2d 7442 . . . . . . . 8 (๐‘› = ๐‘ โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘› / 2))) = ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))
5047, 49oveq12d 7444 . . . . . . 7 (๐‘› = ๐‘ โ†’ (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) + ((9 / 4) ยท (๐บโ€˜(๐‘› / 2)))) = (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))
51 oveq2 7434 . . . . . . . . 9 (๐‘› = ๐‘ โ†’ (2 ยท ๐‘›) = (2 ยท ๐‘))
5251fveq2d 6906 . . . . . . . 8 (๐‘› = ๐‘ โ†’ (โˆšโ€˜(2 ยท ๐‘›)) = (โˆšโ€˜(2 ยท ๐‘)))
5352oveq2d 7442 . . . . . . 7 (๐‘› = ๐‘ โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘›))) = ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))
5450, 53oveq12d 7444 . . . . . 6 (๐‘› = ๐‘ โ†’ ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) + ((9 / 4) ยท (๐บโ€˜(๐‘› / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘›)))) = ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
55 ovex 7459 . . . . . 6 ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) โˆˆ V
5654, 2, 55fvmpt 7010 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (๐นโ€˜๐‘) = ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
578, 56syl 17 . . . 4 (๐œ‘ โ†’ (๐นโ€˜๐‘) = ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
58 sqrt2re 16236 . . . . . . 7 (โˆšโ€˜2) โˆˆ โ„
598nnrpd 13056 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ โ„+)
6059rpsqrtcld 15400 . . . . . . . . 9 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„+)
61 fveq2 6902 . . . . . . . . . . 11 (๐‘ฅ = (โˆšโ€˜๐‘) โ†’ (logโ€˜๐‘ฅ) = (logโ€˜(โˆšโ€˜๐‘)))
62 id 22 . . . . . . . . . . 11 (๐‘ฅ = (โˆšโ€˜๐‘) โ†’ ๐‘ฅ = (โˆšโ€˜๐‘))
6361, 62oveq12d 7444 . . . . . . . . . 10 (๐‘ฅ = (โˆšโ€˜๐‘) โ†’ ((logโ€˜๐‘ฅ) / ๐‘ฅ) = ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)))
64 ovex 7459 . . . . . . . . . 10 ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)) โˆˆ V
6563, 3, 64fvmpt 7010 . . . . . . . . 9 ((โˆšโ€˜๐‘) โˆˆ โ„+ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) = ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)))
6660, 65syl 17 . . . . . . . 8 (๐œ‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) = ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)))
6760relogcld 26585 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„)
6867, 60rerpdivcld 13089 . . . . . . . 8 (๐œ‘ โ†’ ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)) โˆˆ โ„)
6966, 68eqeltrd 2829 . . . . . . 7 (๐œ‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„)
70 remulcl 11233 . . . . . . 7 (((โˆšโ€˜2) โˆˆ โ„ โˆง (๐บโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„) โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) โˆˆ โ„)
7158, 69, 70sylancr 585 . . . . . 6 (๐œ‘ โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) โˆˆ โ„)
72 9re 12351 . . . . . . . 8 9 โˆˆ โ„
73 4re 12336 . . . . . . . 8 4 โˆˆ โ„
74 4ne0 12360 . . . . . . . 8 4 โ‰  0
7572, 73, 74redivcli 12021 . . . . . . 7 (9 / 4) โˆˆ โ„
7659rphalfcld 13070 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ / 2) โˆˆ โ„+)
77 fveq2 6902 . . . . . . . . . . 11 (๐‘ฅ = (๐‘ / 2) โ†’ (logโ€˜๐‘ฅ) = (logโ€˜(๐‘ / 2)))
78 id 22 . . . . . . . . . . 11 (๐‘ฅ = (๐‘ / 2) โ†’ ๐‘ฅ = (๐‘ / 2))
7977, 78oveq12d 7444 . . . . . . . . . 10 (๐‘ฅ = (๐‘ / 2) โ†’ ((logโ€˜๐‘ฅ) / ๐‘ฅ) = ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))
80 ovex 7459 . . . . . . . . . 10 ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)) โˆˆ V
8179, 3, 80fvmpt 7010 . . . . . . . . 9 ((๐‘ / 2) โˆˆ โ„+ โ†’ (๐บโ€˜(๐‘ / 2)) = ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))
8276, 81syl 17 . . . . . . . 8 (๐œ‘ โ†’ (๐บโ€˜(๐‘ / 2)) = ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))
8376relogcld 26585 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜(๐‘ / 2)) โˆˆ โ„)
8483, 76rerpdivcld 13089 . . . . . . . 8 (๐œ‘ โ†’ ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)) โˆˆ โ„)
8582, 84eqeltrd 2829 . . . . . . 7 (๐œ‘ โ†’ (๐บโ€˜(๐‘ / 2)) โˆˆ โ„)
86 remulcl 11233 . . . . . . 7 (((9 / 4) โˆˆ โ„ โˆง (๐บโ€˜(๐‘ / 2)) โˆˆ โ„) โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))) โˆˆ โ„)
8775, 85, 86sylancr 585 . . . . . 6 (๐œ‘ โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))) โˆˆ โ„)
8871, 87readdcld 11283 . . . . 5 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) โˆˆ โ„)
89 2rp 13021 . . . . . . 7 2 โˆˆ โ„+
90 relogcl 26537 . . . . . . 7 (2 โˆˆ โ„+ โ†’ (logโ€˜2) โˆˆ โ„)
9189, 90ax-mp 5 . . . . . 6 (logโ€˜2) โˆˆ โ„
92 rpmulcl 13039 . . . . . . . 8 ((2 โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„+) โ†’ (2 ยท ๐‘) โˆˆ โ„+)
9389, 59, 92sylancr 585 . . . . . . 7 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„+)
9493rpsqrtcld 15400 . . . . . 6 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„+)
95 rerpdivcl 13046 . . . . . 6 (((logโ€˜2) โˆˆ โ„ โˆง (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„+) โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))) โˆˆ โ„)
9691, 94, 95sylancr 585 . . . . 5 (๐œ‘ โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))) โˆˆ โ„)
9788, 96readdcld 11283 . . . 4 (๐œ‘ โ†’ ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) โˆˆ โ„)
9857, 97eqeltrd 2829 . . 3 (๐œ‘ โ†’ (๐นโ€˜๐‘) โˆˆ โ„)
9991a1i 11 . . . 4 (๐œ‘ โ†’ (logโ€˜2) โˆˆ โ„)
10044simprd 494 . . . 4 (๐œ‘ โ†’ (๐นโ€˜64) < (logโ€˜2))
101 nnrp 13027 . . . . . . . . . . 11 (4 โˆˆ โ„• โ†’ 4 โˆˆ โ„+)
1025, 101ax-mp 5 . . . . . . . . . 10 4 โˆˆ โ„+
103 relogcl 26537 . . . . . . . . . 10 (4 โˆˆ โ„+ โ†’ (logโ€˜4) โˆˆ โ„)
104102, 103ax-mp 5 . . . . . . . . 9 (logโ€˜4) โˆˆ โ„
105 remulcl 11233 . . . . . . . . 9 ((๐‘ โˆˆ โ„ โˆง (logโ€˜4) โˆˆ โ„) โ†’ (๐‘ ยท (logโ€˜4)) โˆˆ โ„)
10636, 104, 105sylancl 584 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ ยท (logโ€˜4)) โˆˆ โ„)
10759relogcld 26585 . . . . . . . 8 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„)
108106, 107resubcld 11682 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆˆ โ„)
109 rpre 13024 . . . . . . . . . . . . 13 ((2 ยท ๐‘) โˆˆ โ„+ โ†’ (2 ยท ๐‘) โˆˆ โ„)
110 rpge0 13029 . . . . . . . . . . . . 13 ((2 ยท ๐‘) โˆˆ โ„+ โ†’ 0 โ‰ค (2 ยท ๐‘))
111109, 110resqrtcld 15406 . . . . . . . . . . . 12 ((2 ยท ๐‘) โˆˆ โ„+ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„)
11293, 111syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„)
113 3nn 12331 . . . . . . . . . . 11 3 โˆˆ โ„•
114 nndivre 12293 . . . . . . . . . . 11 (((โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„ โˆง 3 โˆˆ โ„•) โ†’ ((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„)
115112, 113, 114sylancl 584 . . . . . . . . . 10 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„)
116 2re 12326 . . . . . . . . . 10 2 โˆˆ โ„
117 readdcl 11231 . . . . . . . . . 10 ((((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„ โˆง 2 โˆˆ โ„) โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) โˆˆ โ„)
118115, 116, 117sylancl 584 . . . . . . . . 9 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) โˆˆ โ„)
11993relogcld 26585 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜(2 ยท ๐‘)) โˆˆ โ„)
120118, 119remulcld 11284 . . . . . . . 8 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) โˆˆ โ„)
121 remulcl 11233 . . . . . . . . . . . 12 ((4 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (4 ยท ๐‘) โˆˆ โ„)
12273, 36, 121sylancr 585 . . . . . . . . . . 11 (๐œ‘ โ†’ (4 ยท ๐‘) โˆˆ โ„)
123 nndivre 12293 . . . . . . . . . . 11 (((4 ยท ๐‘) โˆˆ โ„ โˆง 3 โˆˆ โ„•) โ†’ ((4 ยท ๐‘) / 3) โˆˆ โ„)
124122, 113, 123sylancl 584 . . . . . . . . . 10 (๐œ‘ โ†’ ((4 ยท ๐‘) / 3) โˆˆ โ„)
125 5re 12339 . . . . . . . . . 10 5 โˆˆ โ„
126 resubcl 11564 . . . . . . . . . 10 ((((4 ยท ๐‘) / 3) โˆˆ โ„ โˆง 5 โˆˆ โ„) โ†’ (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„)
127124, 125, 126sylancl 584 . . . . . . . . 9 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„)
128 remulcl 11233 . . . . . . . . 9 (((((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„ โˆง (logโ€˜2) โˆˆ โ„) โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆˆ โ„)
129127, 91, 128sylancl 584 . . . . . . . 8 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆˆ โ„)
130120, 129readdcld 11283 . . . . . . 7 (๐œ‘ โ†’ (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โˆˆ โ„)
131 remulcl 11233 . . . . . . . . 9 ((((4 ยท ๐‘) / 3) โˆˆ โ„ โˆง (logโ€˜2) โˆˆ โ„) โ†’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆˆ โ„)
132124, 91, 131sylancl 584 . . . . . . . 8 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆˆ โ„)
133132, 107resubcld 11682 . . . . . . 7 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘)) โˆˆ โ„)
1348nnzd 12625 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
135 df-5 12318 . . . . . . . . . . . 12 5 = (4 + 1)
13673a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 4 โˆˆ โ„)
137 6nn 12341 . . . . . . . . . . . . . . . 16 6 โˆˆ โ„•
138 4nn0 12531 . . . . . . . . . . . . . . . 16 4 โˆˆ โ„•0
139 4lt10 12853 . . . . . . . . . . . . . . . 16 4 < 10
140137, 138, 138, 139declti 12755 . . . . . . . . . . . . . . 15 4 < 64
141140a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 4 < 64)
142136, 35, 36, 141, 1lttrd 11415 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 4 < ๐‘)
143 4z 12636 . . . . . . . . . . . . . 14 4 โˆˆ โ„ค
144 zltp1le 12652 . . . . . . . . . . . . . 14 ((4 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (4 < ๐‘ โ†” (4 + 1) โ‰ค ๐‘))
145143, 134, 144sylancr 585 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (4 < ๐‘ โ†” (4 + 1) โ‰ค ๐‘))
146142, 145mpbid 231 . . . . . . . . . . . 12 (๐œ‘ โ†’ (4 + 1) โ‰ค ๐‘)
147135, 146eqbrtrid 5187 . . . . . . . . . . 11 (๐œ‘ โ†’ 5 โ‰ค ๐‘)
148 5nn 12338 . . . . . . . . . . . . 13 5 โˆˆ โ„•
149148nnzi 12626 . . . . . . . . . . . 12 5 โˆˆ โ„ค
150149eluz1i 12870 . . . . . . . . . . 11 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜5) โ†” (๐‘ โˆˆ โ„ค โˆง 5 โ‰ค ๐‘))
151134, 147, 150sylanbrc 581 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜5))
152 bposlem9.5 . . . . . . . . . . 11 (๐œ‘ โ†’ ยฌ โˆƒ๐‘ โˆˆ โ„™ (๐‘ < ๐‘ โˆง ๐‘ โ‰ค (2 ยท ๐‘)))
153 breq2 5156 . . . . . . . . . . . . 13 (๐‘ = ๐‘ž โ†’ (๐‘ < ๐‘ โ†” ๐‘ < ๐‘ž))
154 breq1 5155 . . . . . . . . . . . . 13 (๐‘ = ๐‘ž โ†’ (๐‘ โ‰ค (2 ยท ๐‘) โ†” ๐‘ž โ‰ค (2 ยท ๐‘)))
155153, 154anbi12d 630 . . . . . . . . . . . 12 (๐‘ = ๐‘ž โ†’ ((๐‘ < ๐‘ โˆง ๐‘ โ‰ค (2 ยท ๐‘)) โ†” (๐‘ < ๐‘ž โˆง ๐‘ž โ‰ค (2 ยท ๐‘))))
156155cbvrexvw 3233 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ โ„™ (๐‘ < ๐‘ โˆง ๐‘ โ‰ค (2 ยท ๐‘)) โ†” โˆƒ๐‘ž โˆˆ โ„™ (๐‘ < ๐‘ž โˆง ๐‘ž โ‰ค (2 ยท ๐‘)))
157152, 156sylnib 327 . . . . . . . . . 10 (๐œ‘ โ†’ ยฌ โˆƒ๐‘ž โˆˆ โ„™ (๐‘ < ๐‘ž โˆง ๐‘ž โ‰ค (2 ยท ๐‘)))
158 eqid 2728 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (๐‘›โ†‘(๐‘› pCnt ((2 ยท ๐‘)C๐‘))), 1)) = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (๐‘›โ†‘(๐‘› pCnt ((2 ยท ๐‘)C๐‘))), 1))
159 eqid 2728 . . . . . . . . . 10 (โŒŠโ€˜((2 ยท ๐‘) / 3)) = (โŒŠโ€˜((2 ยท ๐‘) / 3))
160 eqid 2728 . . . . . . . . . 10 (โŒŠโ€˜(โˆšโ€˜(2 ยท ๐‘))) = (โŒŠโ€˜(โˆšโ€˜(2 ยท ๐‘)))
161151, 157, 158, 159, 160bposlem6 27250 . . . . . . . . 9 (๐œ‘ โ†’ ((4โ†‘๐‘) / ๐‘) < (((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) ยท (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5))))
162 reexplog 26557 . . . . . . . . . . . 12 ((4 โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„ค) โ†’ (4โ†‘๐‘) = (expโ€˜(๐‘ ยท (logโ€˜4))))
163102, 134, 162sylancr 585 . . . . . . . . . . 11 (๐œ‘ โ†’ (4โ†‘๐‘) = (expโ€˜(๐‘ ยท (logโ€˜4))))
16459reeflogd 26586 . . . . . . . . . . . 12 (๐œ‘ โ†’ (expโ€˜(logโ€˜๐‘)) = ๐‘)
165164eqcomd 2734 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ = (expโ€˜(logโ€˜๐‘)))
166163, 165oveq12d 7444 . . . . . . . . . 10 (๐œ‘ โ†’ ((4โ†‘๐‘) / ๐‘) = ((expโ€˜(๐‘ ยท (logโ€˜4))) / (expโ€˜(logโ€˜๐‘))))
167106recnd 11282 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ ยท (logโ€˜4)) โˆˆ โ„‚)
168107recnd 11282 . . . . . . . . . . 11 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„‚)
169 efsub 16086 . . . . . . . . . . 11 (((๐‘ ยท (logโ€˜4)) โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚) โ†’ (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) = ((expโ€˜(๐‘ ยท (logโ€˜4))) / (expโ€˜(logโ€˜๐‘))))
170167, 168, 169syl2anc 582 . . . . . . . . . 10 (๐œ‘ โ†’ (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) = ((expโ€˜(๐‘ ยท (logโ€˜4))) / (expโ€˜(logโ€˜๐‘))))
171166, 170eqtr4d 2771 . . . . . . . . 9 (๐œ‘ โ†’ ((4โ†‘๐‘) / ๐‘) = (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))))
17293rpcnd 13060 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
17393rpne0d 13063 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘) โ‰  0)
174118recnd 11282 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) โˆˆ โ„‚)
175172, 173, 174cxpefd 26674 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) = (expโ€˜((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘)))))
176 2cn 12327 . . . . . . . . . . . 12 2 โˆˆ โ„‚
177 2ne0 12356 . . . . . . . . . . . 12 2 โ‰  0
178127recnd 11282 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„‚)
179 cxpef 26627 . . . . . . . . . . . 12 ((2 โˆˆ โ„‚ โˆง 2 โ‰  0 โˆง (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„‚) โ†’ (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5)) = (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))
180176, 177, 178, 179mp3an12i 1461 . . . . . . . . . . 11 (๐œ‘ โ†’ (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5)) = (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))
181175, 180oveq12d 7444 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) ยท (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5))) = ((expโ€˜((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘)))) ยท (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
182120recnd 11282 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) โˆˆ โ„‚)
183129recnd 11282 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆˆ โ„‚)
184 efadd 16080 . . . . . . . . . . 11 ((((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) โˆˆ โ„‚ โˆง ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆˆ โ„‚) โ†’ (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))) = ((expโ€˜((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘)))) ยท (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
185182, 183, 184syl2anc 582 . . . . . . . . . 10 (๐œ‘ โ†’ (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))) = ((expโ€˜((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘)))) ยท (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
186181, 185eqtr4d 2771 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) ยท (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5))) = (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
187161, 171, 1863brtr3d 5183 . . . . . . . 8 (๐œ‘ โ†’ (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) < (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
188 eflt 16103 . . . . . . . . 9 ((((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆˆ โ„ โˆง (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โˆˆ โ„) โ†’ (((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) < (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โ†” (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) < (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))))
189108, 130, 188syl2anc 582 . . . . . . . 8 (๐œ‘ โ†’ (((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) < (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โ†” (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) < (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))))
190187, 189mpbird 256 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) < (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))
191108, 130, 133, 190ltsub1dd 11866 . . . . . 6 (๐œ‘ โ†’ (((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) < ((((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))))
19236recnd 11282 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
193 mulcom 11234 . . . . . . . . . . 11 ((2 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (2 ยท ๐‘) = (๐‘ ยท 2))
194176, 192, 193sylancr 585 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท ๐‘) = (๐‘ ยท 2))
195194oveq1d 7441 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘) ยท (logโ€˜2)) = ((๐‘ ยท 2) ยท (logโ€˜2)))
19691recni 11268 . . . . . . . . . . . 12 (logโ€˜2) โˆˆ โ„‚
197 mulass 11236 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง (logโ€˜2) โˆˆ โ„‚) โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (2 ยท (logโ€˜2))))
198176, 196, 197mp3an23 1449 . . . . . . . . . . 11 (๐‘ โˆˆ โ„‚ โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (2 ยท (logโ€˜2))))
199192, 198syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (2 ยท (logโ€˜2))))
2001962timesi 12390 . . . . . . . . . . . 12 (2 ยท (logโ€˜2)) = ((logโ€˜2) + (logโ€˜2))
201 relogmul 26554 . . . . . . . . . . . . 13 ((2 โˆˆ โ„+ โˆง 2 โˆˆ โ„+) โ†’ (logโ€˜(2 ยท 2)) = ((logโ€˜2) + (logโ€˜2)))
20289, 89, 201mp2an 690 . . . . . . . . . . . 12 (logโ€˜(2 ยท 2)) = ((logโ€˜2) + (logโ€˜2))
203 2t2e4 12416 . . . . . . . . . . . . 13 (2 ยท 2) = 4
204203fveq2i 6905 . . . . . . . . . . . 12 (logโ€˜(2 ยท 2)) = (logโ€˜4)
205200, 202, 2043eqtr2i 2762 . . . . . . . . . . 11 (2 ยท (logโ€˜2)) = (logโ€˜4)
206205oveq2i 7437 . . . . . . . . . 10 (๐‘ ยท (2 ยท (logโ€˜2))) = (๐‘ ยท (logโ€˜4))
207199, 206eqtrdi 2784 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (logโ€˜4)))
208195, 207eqtrd 2768 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘) ยท (logโ€˜2)) = (๐‘ ยท (logโ€˜4)))
209208oveq1d 7441 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (logโ€˜2)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))) = ((๐‘ ยท (logโ€˜4)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
210124recnd 11282 . . . . . . . . . 10 (๐œ‘ โ†’ ((4 ยท ๐‘) / 3) โˆˆ โ„‚)
211 3rp 13022 . . . . . . . . . . . 12 3 โˆˆ โ„+
212 rpdivcl 13041 . . . . . . . . . . . 12 (((2 ยท ๐‘) โˆˆ โ„+ โˆง 3 โˆˆ โ„+) โ†’ ((2 ยท ๐‘) / 3) โˆˆ โ„+)
21393, 211, 212sylancl 584 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) โˆˆ โ„+)
214213rpcnd 13060 . . . . . . . . . 10 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) โˆˆ โ„‚)
215 4p2e6 12405 . . . . . . . . . . . . . 14 (4 + 2) = 6
216215oveq1i 7436 . . . . . . . . . . . . 13 ((4 + 2) ยท ๐‘) = (6 ยท ๐‘)
217 4cn 12337 . . . . . . . . . . . . . 14 4 โˆˆ โ„‚
218 adddir 11245 . . . . . . . . . . . . . 14 ((4 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ ((4 + 2) ยท ๐‘) = ((4 ยท ๐‘) + (2 ยท ๐‘)))
219217, 176, 192, 218mp3an12i 1461 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((4 + 2) ยท ๐‘) = ((4 ยท ๐‘) + (2 ยท ๐‘)))
220216, 219eqtr3id 2782 . . . . . . . . . . . 12 (๐œ‘ โ†’ (6 ยท ๐‘) = ((4 ยท ๐‘) + (2 ยท ๐‘)))
221220oveq1d 7441 . . . . . . . . . . 11 (๐œ‘ โ†’ ((6 ยท ๐‘) / 3) = (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3))
222 6cn 12343 . . . . . . . . . . . . . 14 6 โˆˆ โ„‚
223 3cn 12333 . . . . . . . . . . . . . . 15 3 โˆˆ โ„‚
224 3ne0 12358 . . . . . . . . . . . . . . 15 3 โ‰  0
225223, 224pm3.2i 469 . . . . . . . . . . . . . 14 (3 โˆˆ โ„‚ โˆง 3 โ‰  0)
226 div23 11931 . . . . . . . . . . . . . 14 ((6 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ ((6 ยท ๐‘) / 3) = ((6 / 3) ยท ๐‘))
227222, 225, 226mp3an13 1448 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„‚ โ†’ ((6 ยท ๐‘) / 3) = ((6 / 3) ยท ๐‘))
228192, 227syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((6 ยท ๐‘) / 3) = ((6 / 3) ยท ๐‘))
229 3t2e6 12418 . . . . . . . . . . . . . . 15 (3 ยท 2) = 6
230229oveq1i 7436 . . . . . . . . . . . . . 14 ((3 ยท 2) / 3) = (6 / 3)
231176, 223, 224divcan3i 12000 . . . . . . . . . . . . . 14 ((3 ยท 2) / 3) = 2
232230, 231eqtr3i 2758 . . . . . . . . . . . . 13 (6 / 3) = 2
233232oveq1i 7436 . . . . . . . . . . . 12 ((6 / 3) ยท ๐‘) = (2 ยท ๐‘)
234228, 233eqtrdi 2784 . . . . . . . . . . 11 (๐œ‘ โ†’ ((6 ยท ๐‘) / 3) = (2 ยท ๐‘))
235122recnd 11282 . . . . . . . . . . . 12 (๐œ‘ โ†’ (4 ยท ๐‘) โˆˆ โ„‚)
236 remulcl 11233 . . . . . . . . . . . . . 14 ((2 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (2 ยท ๐‘) โˆˆ โ„)
237116, 36, 236sylancr 585 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„)
238237recnd 11282 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
239 divdir 11937 . . . . . . . . . . . . 13 (((4 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
240225, 239mp3an3 1446 . . . . . . . . . . . 12 (((4 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โˆˆ โ„‚) โ†’ (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
241235, 238, 240syl2anc 582 . . . . . . . . . . 11 (๐œ‘ โ†’ (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
242221, 234, 2413eqtr3d 2776 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท ๐‘) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
243210, 214, 242mvrladdd 11667 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆ’ ((4 ยท ๐‘) / 3)) = ((2 ยท ๐‘) / 3))
244243oveq1d 7441 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘) โˆ’ ((4 ยท ๐‘) / 3)) ยท (logโ€˜2)) = (((2 ยท ๐‘) / 3) ยท (logโ€˜2)))
24599recnd 11282 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜2) โˆˆ โ„‚)
246238, 210, 245subdird 11711 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘) โˆ’ ((4 ยท ๐‘) / 3)) ยท (logโ€˜2)) = (((2 ยท ๐‘) ยท (logโ€˜2)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
247244, 246eqtr3d 2770 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) = (((2 ยท ๐‘) ยท (logโ€˜2)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
248132recnd 11282 . . . . . . . 8 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆˆ โ„‚)
249167, 248, 168nnncan2d 11646 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = ((๐‘ ยท (logโ€˜4)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
250209, 247, 2493eqtr4d 2778 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) = (((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))))
251115recnd 11282 . . . . . . . . . 10 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„‚)
252176a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
253119recnd 11282 . . . . . . . . . 10 (๐œ‘ โ†’ (logโ€˜(2 ยท ๐‘)) โˆˆ โ„‚)
254251, 252, 253adddird 11279 . . . . . . . . 9 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (2 ยท (logโ€˜(2 ยท ๐‘)))))
255 relogmul 26554 . . . . . . . . . . . . 13 ((2 โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„+) โ†’ (logโ€˜(2 ยท ๐‘)) = ((logโ€˜2) + (logโ€˜๐‘)))
25689, 59, 255sylancr 585 . . . . . . . . . . . 12 (๐œ‘ โ†’ (logโ€˜(2 ยท ๐‘)) = ((logโ€˜2) + (logโ€˜๐‘)))
257256oveq2d 7442 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท (logโ€˜(2 ยท ๐‘))) = (2 ยท ((logโ€˜2) + (logโ€˜๐‘))))
258252, 245, 168adddid 11278 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท ((logโ€˜2) + (logโ€˜๐‘))) = ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))))
259257, 258eqtrd 2768 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท (logโ€˜(2 ยท ๐‘))) = ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))))
260259oveq2d 7442 . . . . . . . . 9 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (2 ยท (logโ€˜(2 ยท ๐‘)))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))))
261254, 260eqtrd 2768 . . . . . . . 8 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))))
262 5cn 12340 . . . . . . . . . . . 12 5 โˆˆ โ„‚
263262a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 5 โˆˆ โ„‚)
264210, 263, 245subdird 11711 . . . . . . . . . 10 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) = ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (5 ยท (logโ€˜2))))
265264oveq1d 7441 . . . . . . . . 9 (๐œ‘ โ†’ (((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = (((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (5 ยท (logโ€˜2))) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))))
266262, 196mulcli 11261 . . . . . . . . . . 11 (5 ยท (logโ€˜2)) โˆˆ โ„‚
267266a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ (5 ยท (logโ€˜2)) โˆˆ โ„‚)
268248, 267, 168nnncan1d 11645 . . . . . . . . 9 (๐œ‘ โ†’ (((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (5 ยท (logโ€˜2))) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))
269265, 268eqtrd 2768 . . . . . . . 8 (๐œ‘ โ†’ (((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))
270261, 269oveq12d 7444 . . . . . . 7 (๐œ‘ โ†’ (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + (((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘)))) = (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))))
271133recnd 11282 . . . . . . . 8 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘)) โˆˆ โ„‚)
272182, 183, 271addsubassd 11631 . . . . . . 7 (๐œ‘ โ†’ ((((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + (((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘)))))
273262, 223, 196subdiri 11704 . . . . . . . . . . . . 13 ((5 โˆ’ 3) ยท (logโ€˜2)) = ((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2)))
274 3p2e5 12403 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
275274oveq1i 7436 . . . . . . . . . . . . . . 15 ((3 + 2) โˆ’ 3) = (5 โˆ’ 3)
276 pncan2 11507 . . . . . . . . . . . . . . . 16 ((3 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚) โ†’ ((3 + 2) โˆ’ 3) = 2)
277223, 176, 276mp2an 690 . . . . . . . . . . . . . . 15 ((3 + 2) โˆ’ 3) = 2
278275, 277eqtr3i 2758 . . . . . . . . . . . . . 14 (5 โˆ’ 3) = 2
279278oveq1i 7436 . . . . . . . . . . . . 13 ((5 โˆ’ 3) ยท (logโ€˜2)) = (2 ยท (logโ€˜2))
280273, 279eqtr3i 2758 . . . . . . . . . . . 12 ((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) = (2 ยท (logโ€˜2))
281280a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ ((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) = (2 ยท (logโ€˜2)))
282 mulcl 11232 . . . . . . . . . . . . 13 ((2 โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚) โ†’ (2 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
283176, 168, 282sylancr 585 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
284 df-3 12316 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
285284oveq1i 7436 . . . . . . . . . . . . . . 15 (3 ยท (logโ€˜๐‘)) = ((2 + 1) ยท (logโ€˜๐‘))
286 1cnd 11249 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
287252, 286, 168adddird 11279 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 + 1) ยท (logโ€˜๐‘)) = ((2 ยท (logโ€˜๐‘)) + (1 ยท (logโ€˜๐‘))))
288285, 287eqtrid 2780 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3 ยท (logโ€˜๐‘)) = ((2 ยท (logโ€˜๐‘)) + (1 ยท (logโ€˜๐‘))))
289168mullidd 11272 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (1 ยท (logโ€˜๐‘)) = (logโ€˜๐‘))
290289oveq2d 7442 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 ยท (logโ€˜๐‘)) + (1 ยท (logโ€˜๐‘))) = ((2 ยท (logโ€˜๐‘)) + (logโ€˜๐‘)))
291288, 290eqtrd 2768 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (3 ยท (logโ€˜๐‘)) = ((2 ยท (logโ€˜๐‘)) + (logโ€˜๐‘)))
292291oveq1d 7441 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2))) = (((2 ยท (logโ€˜๐‘)) + (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2))))
293283, 168, 267, 292assraddsubd 11668 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2))) = ((2 ยท (logโ€˜๐‘)) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))))
294281, 293oveq12d 7444 . . . . . . . . . 10 (๐œ‘ โ†’ (((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) + ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2)))) = ((2 ยท (logโ€˜2)) + ((2 ยท (logโ€˜๐‘)) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))))
295 relogdiv 26555 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„+ โˆง 2 โˆˆ โ„+) โ†’ (logโ€˜(๐‘ / 2)) = ((logโ€˜๐‘) โˆ’ (logโ€˜2)))
29659, 89, 295sylancl 584 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (logโ€˜(๐‘ / 2)) = ((logโ€˜๐‘) โˆ’ (logโ€˜2)))
297296oveq2d 7442 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท (logโ€˜(๐‘ / 2))) = (3 ยท ((logโ€˜๐‘) โˆ’ (logโ€˜2))))
298 subdi 11687 . . . . . . . . . . . . . 14 ((3 โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚ โˆง (logโ€˜2) โˆˆ โ„‚) โ†’ (3 ยท ((logโ€˜๐‘) โˆ’ (logโ€˜2))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
299223, 196, 298mp3an13 1448 . . . . . . . . . . . . 13 ((logโ€˜๐‘) โˆˆ โ„‚ โ†’ (3 ยท ((logโ€˜๐‘) โˆ’ (logโ€˜2))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
300168, 299syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท ((logโ€˜๐‘) โˆ’ (logโ€˜2))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
301297, 300eqtrd 2768 . . . . . . . . . . 11 (๐œ‘ โ†’ (3 ยท (logโ€˜(๐‘ / 2))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
302 div23 11931 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ ((2 ยท ๐‘) / 3) = ((2 / 3) ยท ๐‘))
303176, 225, 302mp3an13 1448 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ โ„‚ โ†’ ((2 ยท ๐‘) / 3) = ((2 / 3) ยท ๐‘))
304192, 303syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) = ((2 / 3) ยท ๐‘))
305223, 176, 223, 176, 177, 177divmuldivi 12014 . . . . . . . . . . . . . . . . 17 ((3 / 2) ยท (3 / 2)) = ((3 ยท 3) / (2 ยท 2))
306 3t3e9 12419 . . . . . . . . . . . . . . . . . 18 (3 ยท 3) = 9
307306, 203oveq12i 7438 . . . . . . . . . . . . . . . . 17 ((3 ยท 3) / (2 ยท 2)) = (9 / 4)
308305, 307eqtr2i 2757 . . . . . . . . . . . . . . . 16 (9 / 4) = ((3 / 2) ยท (3 / 2))
309308a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (9 / 4) = ((3 / 2) ยท (3 / 2)))
310304, 309oveq12d 7444 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (9 / 4)) = (((2 / 3) ยท ๐‘) ยท ((3 / 2) ยท (3 / 2))))
311176, 223, 224divcli 11996 . . . . . . . . . . . . . . 15 (2 / 3) โˆˆ โ„‚
312223, 176, 177divcli 11996 . . . . . . . . . . . . . . . 16 (3 / 2) โˆˆ โ„‚
313 mul4 11422 . . . . . . . . . . . . . . . 16 ((((2 / 3) โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โˆง ((3 / 2) โˆˆ โ„‚ โˆง (3 / 2) โˆˆ โ„‚)) โ†’ (((2 / 3) ยท ๐‘) ยท ((3 / 2) ยท (3 / 2))) = (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))))
314312, 312, 313mpanr12 703 . . . . . . . . . . . . . . 15 (((2 / 3) โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (((2 / 3) ยท ๐‘) ยท ((3 / 2) ยท (3 / 2))) = (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))))
315311, 192, 314sylancr 585 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 / 3) ยท ๐‘) ยท ((3 / 2) ยท (3 / 2))) = (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))))
316 divcan6 11961 . . . . . . . . . . . . . . . . . 18 (((2 โˆˆ โ„‚ โˆง 2 โ‰  0) โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ ((2 / 3) ยท (3 / 2)) = 1)
317176, 177, 223, 224, 316mp4an 691 . . . . . . . . . . . . . . . . 17 ((2 / 3) ยท (3 / 2)) = 1
318317oveq1i 7436 . . . . . . . . . . . . . . . 16 (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))) = (1 ยท (๐‘ ยท (3 / 2)))
319 mulcl 11232 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆˆ โ„‚ โˆง (3 / 2) โˆˆ โ„‚) โ†’ (๐‘ ยท (3 / 2)) โˆˆ โ„‚)
320192, 312, 319sylancl 584 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐‘ ยท (3 / 2)) โˆˆ โ„‚)
321320mullidd 11272 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 ยท (๐‘ ยท (3 / 2))) = (๐‘ ยท (3 / 2)))
322318, 321eqtrid 2780 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))) = (๐‘ ยท (3 / 2)))
323 2cnne0 12462 . . . . . . . . . . . . . . . . 17 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
324 div12 11934 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„‚ โˆง 3 โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (๐‘ ยท (3 / 2)) = (3 ยท (๐‘ / 2)))
325223, 323, 324mp3an23 1449 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ โ„‚ โ†’ (๐‘ ยท (3 / 2)) = (3 ยท (๐‘ / 2)))
326192, 325syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘ ยท (3 / 2)) = (3 ยท (๐‘ / 2)))
327322, 326eqtrd 2768 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))) = (3 ยท (๐‘ / 2)))
328310, 315, 3273eqtrd 2772 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (9 / 4)) = (3 ยท (๐‘ / 2)))
329328, 82oveq12d 7444 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((2 ยท ๐‘) / 3) ยท (9 / 4)) ยท (๐บโ€˜(๐‘ / 2))) = ((3 ยท (๐‘ / 2)) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))))
33075recni 11268 . . . . . . . . . . . . . 14 (9 / 4) โˆˆ โ„‚
331330a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (9 / 4) โˆˆ โ„‚)
33285recnd 11282 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐บโ€˜(๐‘ / 2)) โˆˆ โ„‚)
333214, 331, 332mulassd 11277 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((2 ยท ๐‘) / 3) ยท (9 / 4)) ยท (๐บโ€˜(๐‘ / 2))) = (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))
334223a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
33576rpcnd 13060 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ / 2) โˆˆ โ„‚)
33683recnd 11282 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (logโ€˜(๐‘ / 2)) โˆˆ โ„‚)
33776rpne0d 13063 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘ / 2) โ‰  0)
338336, 335, 337divcld 12030 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)) โˆˆ โ„‚)
339334, 335, 338mulassd 11277 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3 ยท (๐‘ / 2)) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))) = (3 ยท ((๐‘ / 2) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))))
340336, 335, 337divcan2d 12032 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐‘ / 2) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))) = (logโ€˜(๐‘ / 2)))
341340oveq2d 7442 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (3 ยท ((๐‘ / 2) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))) = (3 ยท (logโ€˜(๐‘ / 2))))
342339, 341eqtrd 2768 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((3 ยท (๐‘ / 2)) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))) = (3 ยท (logโ€˜(๐‘ / 2))))
343329, 333, 3423eqtr3d 2776 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) = (3 ยท (logโ€˜(๐‘ / 2))))
344223, 196mulcli 11261 . . . . . . . . . . . . 13 (3 ยท (logโ€˜2)) โˆˆ โ„‚
345344a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท (logโ€˜2)) โˆˆ โ„‚)
346 mulcl 11232 . . . . . . . . . . . . 13 ((3 โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚) โ†’ (3 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
347223, 168, 346sylancr 585 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
348267, 345, 347npncan3d 11647 . . . . . . . . . . 11 (๐œ‘ โ†’ (((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) + ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2)))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
349301, 343, 3483eqtr4d 2778 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) = (((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) + ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2)))))
350116, 91remulcli 11270 . . . . . . . . . . . . 13 (2 ยท (logโ€˜2)) โˆˆ โ„
351350recni 11268 . . . . . . . . . . . 12 (2 ยท (logโ€˜2)) โˆˆ โ„‚
352351a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท (logโ€˜2)) โˆˆ โ„‚)
353 subcl 11499 . . . . . . . . . . . 12 (((logโ€˜๐‘) โˆˆ โ„‚ โˆง (5 ยท (logโ€˜2)) โˆˆ โ„‚) โ†’ ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))) โˆˆ โ„‚)
354168, 266, 353sylancl 584 . . . . . . . . . . 11 (๐œ‘ โ†’ ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))) โˆˆ โ„‚)
355352, 283, 354addassd 11276 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))) = ((2 ยท (logโ€˜2)) + ((2 ยท (logโ€˜๐‘)) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))))
356294, 349, 3553eqtr4d 2778 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) = (((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))))
357356oveq2d 7442 . . . . . . . 8 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))))
358 mulcl 11232 . . . . . . . . . . 11 ((((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„‚ โˆง (logโ€˜2) โˆˆ โ„‚) โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) โˆˆ โ„‚)
359251, 196, 358sylancl 584 . . . . . . . . . 10 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) โˆˆ โ„‚)
360251, 168mulcld 11274 . . . . . . . . . 10 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) โˆˆ โ„‚)
36187recnd 11282 . . . . . . . . . . 11 (๐œ‘ โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))) โˆˆ โ„‚)
362214, 361mulcld 11274 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) โˆˆ โ„‚)
363359, 360, 362addassd 11276 . . . . . . . . 9 (๐œ‘ โ†’ (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))))
364256oveq2d 7442 . . . . . . . . . . 11 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((logโ€˜2) + (logโ€˜๐‘))))
365251, 245, 168adddid 11278 . . . . . . . . . . 11 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((logโ€˜2) + (logโ€˜๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘))))
366364, 365eqtrd 2768 . . . . . . . . . 10 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘))))
367366oveq1d 7441 . . . . . . . . 9 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
36857oveq2d 7442 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = (((2 ยท ๐‘) / 3) ยท ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
36988recnd 11282 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) โˆˆ โ„‚)
37096recnd 11282 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))) โˆˆ โ„‚)
371214, 369, 370adddid 11278 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))) = ((((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) + (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
372368, 371eqtrd 2768 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) + (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
37371recnd 11282 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) โˆˆ โ„‚)
374214, 373, 361adddid 11278 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
37593rpge0d 13062 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 โ‰ค (2 ยท ๐‘))
376 remsqsqrt 15245 . . . . . . . . . . . . . . . . . 18 (((2 ยท ๐‘) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘)) โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) = (2 ยท ๐‘))
377237, 375, 376syl2anc 582 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) = (2 ยท ๐‘))
378377oveq1d 7441 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) / 3) = ((2 ยท ๐‘) / 3))
379112recnd 11282 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„‚)
380224a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 3 โ‰  0)
381379, 379, 334, 380div23d 12067 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) / 3) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))))
382378, 381eqtr3d 2770 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))))
383382oveq1d 7441 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))))
384251, 379, 373mulassd 11277 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))))))
385 0le2 12354 . . . . . . . . . . . . . . . . . . 19 0 โ‰ค 2
386116, 385pm3.2i 469 . . . . . . . . . . . . . . . . . 18 (2 โˆˆ โ„ โˆง 0 โ‰ค 2)
38759rprege0d 13065 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘))
388 sqrtmul 15248 . . . . . . . . . . . . . . . . . 18 (((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โˆง (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘)) โ†’ (โˆšโ€˜(2 ยท ๐‘)) = ((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)))
389386, 387, 388sylancr 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) = ((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)))
390389oveq1d 7441 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))))
39158recni 11268 . . . . . . . . . . . . . . . . . 18 (โˆšโ€˜2) โˆˆ โ„‚
392391a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜2) โˆˆ โ„‚)
39360rpcnd 13060 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„‚)
39469recnd 11282 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„‚)
395392, 393, 392, 394mul4d 11466 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜2) ยท (โˆšโ€˜2)) ยท ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘)))))
396 remsqsqrt 15245 . . . . . . . . . . . . . . . . . . . 20 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
397116, 385, 396mp2an 690 . . . . . . . . . . . . . . . . . . 19 ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2
398397a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
39966oveq2d 7442 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘))) = ((โˆšโ€˜๐‘) ยท ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘))))
40067recnd 11282 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (logโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„‚)
40160rpne0d 13063 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โ‰  0)
402400, 393, 401divcan2d 12032 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘))) = (logโ€˜(โˆšโ€˜๐‘)))
403399, 402eqtrd 2768 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘))) = (logโ€˜(โˆšโ€˜๐‘)))
404398, 403oveq12d 7444 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (โˆšโ€˜2)) ยท ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (2 ยท (logโ€˜(โˆšโ€˜๐‘))))
4054002timesd 12495 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 ยท (logโ€˜(โˆšโ€˜๐‘))) = ((logโ€˜(โˆšโ€˜๐‘)) + (logโ€˜(โˆšโ€˜๐‘))))
40660, 60relogmuld 26587 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (logโ€˜((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))) = ((logโ€˜(โˆšโ€˜๐‘)) + (logโ€˜(โˆšโ€˜๐‘))))
407 remsqsqrt 15245 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘) โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
408387, 407syl 17 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
409408fveq2d 6906 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (logโ€˜((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))) = (logโ€˜๐‘))
410406, 409eqtr3d 2770 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((logโ€˜(โˆšโ€˜๐‘)) + (logโ€˜(โˆšโ€˜๐‘))) = (logโ€˜๐‘))
411404, 405, 4103eqtrd 2772 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (โˆšโ€˜2)) ยท ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (logโ€˜๐‘))
412390, 395, 4113eqtrd 2772 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (logโ€˜๐‘))
413412oveq2d 7442 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)))
414383, 384, 4133eqtrd 2772 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)))
415414oveq1d 7441 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
416374, 415eqtrd 2768 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
417382oveq1d 7441 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
418251, 379, 370mulassd 11277 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
41994rpne0d 13063 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โ‰  0)
420245, 379, 419divcan2d 12032 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = (logโ€˜2))
421420oveq2d 7442 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)))
422417, 418, 4213eqtrd 2772 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)))
423416, 422oveq12d 7444 . . . . . . . . . 10 (๐œ‘ โ†’ ((((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) + (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))) = (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2))))
424360, 362addcld 11273 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) โˆˆ โ„‚)
425424, 359addcomd 11456 . . . . . . . . . 10 (๐œ‘ โ†’ (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))))
426372, 423, 4253eqtrd 2772 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))))
427363, 367, 4263eqtr4rd 2779 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
428251, 253mulcld 11274 . . . . . . . . 9 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) โˆˆ โ„‚)
429 addcl 11230 . . . . . . . . . 10 (((2 ยท (logโ€˜2)) โˆˆ โ„‚ โˆง (2 ยท (logโ€˜๐‘)) โˆˆ โ„‚) โ†’ ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) โˆˆ โ„‚)
430351, 283, 429sylancr 585 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) โˆˆ โ„‚)
431428, 430, 354addassd 11276 . . . . . . . 8 (๐œ‘ โ†’ (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))))
432357, 427, 4313eqtr4d 2778 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))))
433270, 272, 4323eqtr4rd 2779 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))))
434191, 250, 4333brtr4d 5184 . . . . 5 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) < (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)))
43599, 98, 213ltmul2d 13100 . . . . 5 (๐œ‘ โ†’ ((logโ€˜2) < (๐นโ€˜๐‘) โ†” (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) < (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘))))
436434, 435mpbird 256 . . . 4 (๐œ‘ โ†’ (logโ€˜2) < (๐นโ€˜๐‘))
43745, 99, 98, 100, 436lttrd 11415 . . 3 (๐œ‘ โ†’ (๐นโ€˜64) < (๐นโ€˜๐‘))
43845, 98, 437ltnsymd 11403 . 2 (๐œ‘ โ†’ ยฌ (๐นโ€˜๐‘) < (๐นโ€˜64))
43942, 438pm2.21dd 194 1 (๐œ‘ โ†’ ๐œ“)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2937  โˆƒwrex 3067  ifcif 4532   class class class wbr 5152   โ†ฆ cmpt 5235  โ€˜cfv 6553  (class class class)co 7426  โ„‚cc 11146  โ„cr 11147  0cc0 11148  1c1 11149   + caddc 11151   ยท cmul 11153   < clt 11288   โ‰ค cle 11289   โˆ’ cmin 11484   / cdiv 11911  โ„•cn 12252  2c2 12307  3c3 12308  4c4 12309  5c5 12310  6c6 12311  8c8 12313  9c9 12314  โ„คcz 12598  cdc 12717  โ„คโ‰ฅcuz 12862  โ„+crp 13016  โŒŠcfl 13797  โ†‘cexp 14068  Ccbc 14303  โˆšcsqrt 15222  expce 16047  eceu 16048  โ„™cprime 16651   pCnt cpc 16814  logclog 26516  โ†‘๐‘ccxp 26517
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-inf2 9674  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226  ax-addf 11227
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7692  df-om 7879  df-1st 8001  df-2nd 8002  df-supp 8174  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-oadd 8499  df-er 8733  df-map 8855  df-pm 8856  df-ixp 8925  df-en 8973  df-dom 8974  df-sdom 8975  df-fin 8976  df-fsupp 9396  df-fi 9444  df-sup 9475  df-inf 9476  df-oi 9543  df-dju 9934  df-card 9972  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-xnn0 12585  df-z 12599  df-dec 12718  df-uz 12863  df-q 12973  df-rp 13017  df-xneg 13134  df-xadd 13135  df-xmul 13136  df-ioo 13370  df-ioc 13371  df-ico 13372  df-icc 13373  df-fz 13527  df-fzo 13670  df-fl 13799  df-mod 13877  df-seq 14009  df-exp 14069  df-fac 14275  df-bc 14304  df-hash 14332  df-shft 15056  df-cj 15088  df-re 15089  df-im 15090  df-sqrt 15224  df-abs 15225  df-limsup 15457  df-clim 15474  df-rlim 15475  df-sum 15675  df-ef 16053  df-e 16054  df-sin 16055  df-cos 16056  df-pi 16058  df-dvds 16241  df-gcd 16479  df-prm 16652  df-pc 16815  df-struct 17125  df-sets 17142  df-slot 17160  df-ndx 17172  df-base 17190  df-ress 17219  df-plusg 17255  df-mulr 17256  df-starv 17257  df-sca 17258  df-vsca 17259  df-ip 17260  df-tset 17261  df-ple 17262  df-ds 17264  df-unif 17265  df-hom 17266  df-cco 17267  df-rest 17413  df-topn 17414  df-0g 17432  df-gsum 17433  df-topgen 17434  df-pt 17435  df-prds 17438  df-xrs 17493  df-qtop 17498  df-imas 17499  df-xps 17501  df-mre 17575  df-mrc 17576  df-acs 17578  df-mgm 18609  df-sgrp 18688  df-mnd 18704  df-submnd 18750  df-mulg 19038  df-cntz 19282  df-cmn 19751  df-psmet 21285  df-xmet 21286  df-met 21287  df-bl 21288  df-mopn 21289  df-fbas 21290  df-fg 21291  df-cnfld 21294  df-top 22824  df-topon 22841  df-topsp 22863  df-bases 22877  df-cld 22951  df-ntr 22952  df-cls 22953  df-nei 23030  df-lp 23068  df-perf 23069  df-cn 23159  df-cnp 23160  df-haus 23247  df-tx 23494  df-hmeo 23687  df-fil 23778  df-fm 23870  df-flim 23871  df-flf 23872  df-xms 24254  df-ms 24255  df-tms 24256  df-cncf 24826  df-limc 25823  df-dv 25824  df-log 26518  df-cxp 26519  df-cht 27057  df-ppi 27060
This theorem is referenced by:  bpos  27254
  Copyright terms: Public domain W3C validator