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

Theorem bposlem9 26481
Description: Lemma for bpos 26482. 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 12296 . . . . . 6 6 โˆˆ โ„•0
5 4nn 12098 . . . . . 6 4 โˆˆ โ„•
64, 5decnncl 12499 . . . . 5 64 โˆˆ โ„•
76a1i 11 . . . 4 (๐œ‘ โ†’ 64 โˆˆ โ„•)
8 bposlem9.3 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
9 ere 15839 . . . . . . . 8 e โˆˆ โ„
10 8re 12111 . . . . . . . 8 8 โˆˆ โ„
11 egt2lt3 15956 . . . . . . . . . 10 (2 < e โˆง e < 3)
1211simpri 487 . . . . . . . . 9 e < 3
13 3lt8 12211 . . . . . . . . 9 3 < 8
14 3re 12095 . . . . . . . . . 10 3 โˆˆ โ„
159, 14, 10lttri 11143 . . . . . . . . 9 ((e < 3 โˆง 3 < 8) โ†’ e < 8)
1612, 13, 15mp2an 690 . . . . . . . 8 e < 8
179, 10, 16ltleii 11140 . . . . . . 7 e โ‰ค 8
18 0re 11019 . . . . . . . . 9 0 โˆˆ โ„
19 epos 15957 . . . . . . . . 9 0 < e
2018, 9, 19ltleii 11140 . . . . . . . 8 0 โ‰ค e
21 8pos 12127 . . . . . . . . 9 0 < 8
2218, 10, 21ltleii 11140 . . . . . . . 8 0 โ‰ค 8
23 le2sq 13895 . . . . . . . 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 230 . . . . . 6 (eโ†‘2) โ‰ค (8โ†‘2)
2610recni 11031 . . . . . . . 8 8 โˆˆ โ„‚
2726sqvali 13939 . . . . . . 7 (8โ†‘2) = (8 ยท 8)
28 8t8e64 12600 . . . . . . 7 (8 ยท 8) = 64
2927, 28eqtri 2764 . . . . . 6 (8โ†‘2) = 64
3025, 29breqtri 5106 . . . . 5 (eโ†‘2) โ‰ค 64
3130a1i 11 . . . 4 (๐œ‘ โ†’ (eโ†‘2) โ‰ค 64)
329resqcli 13945 . . . . . 6 (eโ†‘2) โˆˆ โ„
3332a1i 11 . . . . 5 (๐œ‘ โ†’ (eโ†‘2) โˆˆ โ„)
346nnrei 12024 . . . . . 6 64 โˆˆ โ„
3534a1i 11 . . . . 5 (๐œ‘ โ†’ 64 โˆˆ โ„)
368nnred 12030 . . . . 5 (๐œ‘ โ†’ ๐‘ โˆˆ โ„)
37 ltle 11105 . . . . . . 7 ((64 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (64 < ๐‘ โ†’ 64 โ‰ค ๐‘))
3834, 36, 37sylancr 588 . . . . . 6 (๐œ‘ โ†’ (64 < ๐‘ โ†’ 64 โ‰ค ๐‘))
391, 38mpd 15 . . . . 5 (๐œ‘ โ†’ 64 โ‰ค ๐‘)
4033, 35, 36, 31, 39letrd 11174 . . . 4 (๐œ‘ โ†’ (eโ†‘2) โ‰ค ๐‘)
412, 3, 7, 8, 31, 40bposlem7 26479 . . 3 (๐œ‘ โ†’ (64 < ๐‘ โ†’ (๐นโ€˜๐‘) < (๐นโ€˜64)))
421, 41mpd 15 . 2 (๐œ‘ โ†’ (๐นโ€˜๐‘) < (๐นโ€˜64))
432, 3bposlem8 26480 . . . . 5 ((๐นโ€˜64) โˆˆ โ„ โˆง (๐นโ€˜64) < (logโ€˜2))
4443a1i 11 . . . 4 (๐œ‘ โ†’ ((๐นโ€˜64) โˆˆ โ„ โˆง (๐นโ€˜64) < (logโ€˜2)))
4544simpld 496 . . 3 (๐œ‘ โ†’ (๐นโ€˜64) โˆˆ โ„)
46 2fveq3 6805 . . . . . . . . 9 (๐‘› = ๐‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘›)) = (๐บโ€˜(โˆšโ€˜๐‘)))
4746oveq2d 7319 . . . . . . . 8 (๐‘› = ๐‘ โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) = ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))))
48 fvoveq1 7326 . . . . . . . . 9 (๐‘› = ๐‘ โ†’ (๐บโ€˜(๐‘› / 2)) = (๐บโ€˜(๐‘ / 2)))
4948oveq2d 7319 . . . . . . . 8 (๐‘› = ๐‘ โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘› / 2))) = ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))
5047, 49oveq12d 7321 . . . . . . 7 (๐‘› = ๐‘ โ†’ (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) + ((9 / 4) ยท (๐บโ€˜(๐‘› / 2)))) = (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))
51 oveq2 7311 . . . . . . . . 9 (๐‘› = ๐‘ โ†’ (2 ยท ๐‘›) = (2 ยท ๐‘))
5251fveq2d 6804 . . . . . . . 8 (๐‘› = ๐‘ โ†’ (โˆšโ€˜(2 ยท ๐‘›)) = (โˆšโ€˜(2 ยท ๐‘)))
5352oveq2d 7319 . . . . . . 7 (๐‘› = ๐‘ โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘›))) = ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))
5450, 53oveq12d 7321 . . . . . 6 (๐‘› = ๐‘ โ†’ ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘›))) + ((9 / 4) ยท (๐บโ€˜(๐‘› / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘›)))) = ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
55 ovex 7336 . . . . . 6 ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) โˆˆ V
5654, 2, 55fvmpt 6903 . . . . 5 (๐‘ โˆˆ โ„• โ†’ (๐นโ€˜๐‘) = ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
578, 56syl 17 . . . 4 (๐œ‘ โ†’ (๐นโ€˜๐‘) = ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
58 sqrt2re 16000 . . . . . . 7 (โˆšโ€˜2) โˆˆ โ„
598nnrpd 12812 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ โ„+)
6059rpsqrtcld 15164 . . . . . . . . 9 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„+)
61 fveq2 6800 . . . . . . . . . . 11 (๐‘ฅ = (โˆšโ€˜๐‘) โ†’ (logโ€˜๐‘ฅ) = (logโ€˜(โˆšโ€˜๐‘)))
62 id 22 . . . . . . . . . . 11 (๐‘ฅ = (โˆšโ€˜๐‘) โ†’ ๐‘ฅ = (โˆšโ€˜๐‘))
6361, 62oveq12d 7321 . . . . . . . . . 10 (๐‘ฅ = (โˆšโ€˜๐‘) โ†’ ((logโ€˜๐‘ฅ) / ๐‘ฅ) = ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)))
64 ovex 7336 . . . . . . . . . 10 ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)) โˆˆ V
6563, 3, 64fvmpt 6903 . . . . . . . . 9 ((โˆšโ€˜๐‘) โˆˆ โ„+ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) = ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)))
6660, 65syl 17 . . . . . . . 8 (๐œ‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) = ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)))
6760relogcld 25819 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„)
6867, 60rerpdivcld 12845 . . . . . . . 8 (๐œ‘ โ†’ ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘)) โˆˆ โ„)
6966, 68eqeltrd 2837 . . . . . . 7 (๐œ‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„)
70 remulcl 10998 . . . . . . 7 (((โˆšโ€˜2) โˆˆ โ„ โˆง (๐บโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„) โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) โˆˆ โ„)
7158, 69, 70sylancr 588 . . . . . 6 (๐œ‘ โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) โˆˆ โ„)
72 9re 12114 . . . . . . . 8 9 โˆˆ โ„
73 4re 12099 . . . . . . . 8 4 โˆˆ โ„
74 4ne0 12123 . . . . . . . 8 4 โ‰  0
7572, 73, 74redivcli 11784 . . . . . . 7 (9 / 4) โˆˆ โ„
7659rphalfcld 12826 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ / 2) โˆˆ โ„+)
77 fveq2 6800 . . . . . . . . . . 11 (๐‘ฅ = (๐‘ / 2) โ†’ (logโ€˜๐‘ฅ) = (logโ€˜(๐‘ / 2)))
78 id 22 . . . . . . . . . . 11 (๐‘ฅ = (๐‘ / 2) โ†’ ๐‘ฅ = (๐‘ / 2))
7977, 78oveq12d 7321 . . . . . . . . . 10 (๐‘ฅ = (๐‘ / 2) โ†’ ((logโ€˜๐‘ฅ) / ๐‘ฅ) = ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))
80 ovex 7336 . . . . . . . . . 10 ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)) โˆˆ V
8179, 3, 80fvmpt 6903 . . . . . . . . 9 ((๐‘ / 2) โˆˆ โ„+ โ†’ (๐บโ€˜(๐‘ / 2)) = ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))
8276, 81syl 17 . . . . . . . 8 (๐œ‘ โ†’ (๐บโ€˜(๐‘ / 2)) = ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))
8376relogcld 25819 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜(๐‘ / 2)) โˆˆ โ„)
8483, 76rerpdivcld 12845 . . . . . . . 8 (๐œ‘ โ†’ ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)) โˆˆ โ„)
8582, 84eqeltrd 2837 . . . . . . 7 (๐œ‘ โ†’ (๐บโ€˜(๐‘ / 2)) โˆˆ โ„)
86 remulcl 10998 . . . . . . 7 (((9 / 4) โˆˆ โ„ โˆง (๐บโ€˜(๐‘ / 2)) โˆˆ โ„) โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))) โˆˆ โ„)
8775, 85, 86sylancr 588 . . . . . 6 (๐œ‘ โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))) โˆˆ โ„)
8871, 87readdcld 11046 . . . . 5 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) โˆˆ โ„)
89 2rp 12777 . . . . . . 7 2 โˆˆ โ„+
90 relogcl 25772 . . . . . . 7 (2 โˆˆ โ„+ โ†’ (logโ€˜2) โˆˆ โ„)
9189, 90ax-mp 5 . . . . . 6 (logโ€˜2) โˆˆ โ„
92 rpmulcl 12795 . . . . . . . 8 ((2 โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„+) โ†’ (2 ยท ๐‘) โˆˆ โ„+)
9389, 59, 92sylancr 588 . . . . . . 7 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„+)
9493rpsqrtcld 15164 . . . . . 6 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„+)
95 rerpdivcl 12802 . . . . . 6 (((logโ€˜2) โˆˆ โ„ โˆง (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„+) โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))) โˆˆ โ„)
9691, 94, 95sylancr 588 . . . . 5 (๐œ‘ โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))) โˆˆ โ„)
9788, 96readdcld 11046 . . . 4 (๐œ‘ โ†’ ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) โˆˆ โ„)
9857, 97eqeltrd 2837 . . 3 (๐œ‘ โ†’ (๐นโ€˜๐‘) โˆˆ โ„)
9991a1i 11 . . . 4 (๐œ‘ โ†’ (logโ€˜2) โˆˆ โ„)
10044simprd 497 . . . 4 (๐œ‘ โ†’ (๐นโ€˜64) < (logโ€˜2))
101 nnrp 12783 . . . . . . . . . . 11 (4 โˆˆ โ„• โ†’ 4 โˆˆ โ„+)
1025, 101ax-mp 5 . . . . . . . . . 10 4 โˆˆ โ„+
103 relogcl 25772 . . . . . . . . . 10 (4 โˆˆ โ„+ โ†’ (logโ€˜4) โˆˆ โ„)
104102, 103ax-mp 5 . . . . . . . . 9 (logโ€˜4) โˆˆ โ„
105 remulcl 10998 . . . . . . . . 9 ((๐‘ โˆˆ โ„ โˆง (logโ€˜4) โˆˆ โ„) โ†’ (๐‘ ยท (logโ€˜4)) โˆˆ โ„)
10636, 104, 105sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ ยท (logโ€˜4)) โˆˆ โ„)
10759relogcld 25819 . . . . . . . 8 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„)
108106, 107resubcld 11445 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆˆ โ„)
109 rpre 12780 . . . . . . . . . . . . 13 ((2 ยท ๐‘) โˆˆ โ„+ โ†’ (2 ยท ๐‘) โˆˆ โ„)
110 rpge0 12785 . . . . . . . . . . . . 13 ((2 ยท ๐‘) โˆˆ โ„+ โ†’ 0 โ‰ค (2 ยท ๐‘))
111109, 110resqrtcld 15170 . . . . . . . . . . . 12 ((2 ยท ๐‘) โˆˆ โ„+ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„)
11293, 111syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„)
113 3nn 12094 . . . . . . . . . . 11 3 โˆˆ โ„•
114 nndivre 12056 . . . . . . . . . . 11 (((โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„ โˆง 3 โˆˆ โ„•) โ†’ ((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„)
115112, 113, 114sylancl 587 . . . . . . . . . 10 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„)
116 2re 12089 . . . . . . . . . 10 2 โˆˆ โ„
117 readdcl 10996 . . . . . . . . . 10 ((((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„ โˆง 2 โˆˆ โ„) โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) โˆˆ โ„)
118115, 116, 117sylancl 587 . . . . . . . . 9 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) โˆˆ โ„)
11993relogcld 25819 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜(2 ยท ๐‘)) โˆˆ โ„)
120118, 119remulcld 11047 . . . . . . . 8 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) โˆˆ โ„)
121 remulcl 10998 . . . . . . . . . . . 12 ((4 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (4 ยท ๐‘) โˆˆ โ„)
12273, 36, 121sylancr 588 . . . . . . . . . . 11 (๐œ‘ โ†’ (4 ยท ๐‘) โˆˆ โ„)
123 nndivre 12056 . . . . . . . . . . 11 (((4 ยท ๐‘) โˆˆ โ„ โˆง 3 โˆˆ โ„•) โ†’ ((4 ยท ๐‘) / 3) โˆˆ โ„)
124122, 113, 123sylancl 587 . . . . . . . . . 10 (๐œ‘ โ†’ ((4 ยท ๐‘) / 3) โˆˆ โ„)
125 5re 12102 . . . . . . . . . 10 5 โˆˆ โ„
126 resubcl 11327 . . . . . . . . . 10 ((((4 ยท ๐‘) / 3) โˆˆ โ„ โˆง 5 โˆˆ โ„) โ†’ (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„)
127124, 125, 126sylancl 587 . . . . . . . . 9 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„)
128 remulcl 10998 . . . . . . . . 9 (((((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„ โˆง (logโ€˜2) โˆˆ โ„) โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆˆ โ„)
129127, 91, 128sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆˆ โ„)
130120, 129readdcld 11046 . . . . . . 7 (๐œ‘ โ†’ (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โˆˆ โ„)
131 remulcl 10998 . . . . . . . . 9 ((((4 ยท ๐‘) / 3) โˆˆ โ„ โˆง (logโ€˜2) โˆˆ โ„) โ†’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆˆ โ„)
132124, 91, 131sylancl 587 . . . . . . . 8 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆˆ โ„)
133132, 107resubcld 11445 . . . . . . 7 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘)) โˆˆ โ„)
1348nnzd 12467 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
135 df-5 12081 . . . . . . . . . . . 12 5 = (4 + 1)
13673a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 4 โˆˆ โ„)
137 6nn 12104 . . . . . . . . . . . . . . . 16 6 โˆˆ โ„•
138 4nn0 12294 . . . . . . . . . . . . . . . 16 4 โˆˆ โ„•0
139 4lt10 12615 . . . . . . . . . . . . . . . 16 4 < 10
140137, 138, 138, 139declti 12517 . . . . . . . . . . . . . . 15 4 < 64
141140a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 4 < 64)
142136, 35, 36, 141, 1lttrd 11178 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 4 < ๐‘)
143 4z 12396 . . . . . . . . . . . . . 14 4 โˆˆ โ„ค
144 zltp1le 12412 . . . . . . . . . . . . . 14 ((4 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (4 < ๐‘ โ†” (4 + 1) โ‰ค ๐‘))
145143, 134, 144sylancr 588 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (4 < ๐‘ โ†” (4 + 1) โ‰ค ๐‘))
146142, 145mpbid 232 . . . . . . . . . . . 12 (๐œ‘ โ†’ (4 + 1) โ‰ค ๐‘)
147135, 146eqbrtrid 5116 . . . . . . . . . . 11 (๐œ‘ โ†’ 5 โ‰ค ๐‘)
148 5nn 12101 . . . . . . . . . . . . 13 5 โˆˆ โ„•
149148nnzi 12386 . . . . . . . . . . . 12 5 โˆˆ โ„ค
150149eluz1i 12632 . . . . . . . . . . 11 (๐‘ โˆˆ (โ„คโ‰ฅโ€˜5) โ†” (๐‘ โˆˆ โ„ค โˆง 5 โ‰ค ๐‘))
151134, 147, 150sylanbrc 584 . . . . . . . . . 10 (๐œ‘ โ†’ ๐‘ โˆˆ (โ„คโ‰ฅโ€˜5))
152 bposlem9.5 . . . . . . . . . . 11 (๐œ‘ โ†’ ยฌ โˆƒ๐‘ โˆˆ โ„™ (๐‘ < ๐‘ โˆง ๐‘ โ‰ค (2 ยท ๐‘)))
153 breq2 5085 . . . . . . . . . . . . 13 (๐‘ = ๐‘ž โ†’ (๐‘ < ๐‘ โ†” ๐‘ < ๐‘ž))
154 breq1 5084 . . . . . . . . . . . . 13 (๐‘ = ๐‘ž โ†’ (๐‘ โ‰ค (2 ยท ๐‘) โ†” ๐‘ž โ‰ค (2 ยท ๐‘)))
155153, 154anbi12d 632 . . . . . . . . . . . 12 (๐‘ = ๐‘ž โ†’ ((๐‘ < ๐‘ โˆง ๐‘ โ‰ค (2 ยท ๐‘)) โ†” (๐‘ < ๐‘ž โˆง ๐‘ž โ‰ค (2 ยท ๐‘))))
156155cbvrexvw 3223 . . . . . . . . . . 11 (โˆƒ๐‘ โˆˆ โ„™ (๐‘ < ๐‘ โˆง ๐‘ โ‰ค (2 ยท ๐‘)) โ†” โˆƒ๐‘ž โˆˆ โ„™ (๐‘ < ๐‘ž โˆง ๐‘ž โ‰ค (2 ยท ๐‘)))
157152, 156sylnib 329 . . . . . . . . . 10 (๐œ‘ โ†’ ยฌ โˆƒ๐‘ž โˆˆ โ„™ (๐‘ < ๐‘ž โˆง ๐‘ž โ‰ค (2 ยท ๐‘)))
158 eqid 2736 . . . . . . . . . 10 (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (๐‘›โ†‘(๐‘› pCnt ((2 ยท ๐‘)C๐‘))), 1)) = (๐‘› โˆˆ โ„• โ†ฆ if(๐‘› โˆˆ โ„™, (๐‘›โ†‘(๐‘› pCnt ((2 ยท ๐‘)C๐‘))), 1))
159 eqid 2736 . . . . . . . . . 10 (โŒŠโ€˜((2 ยท ๐‘) / 3)) = (โŒŠโ€˜((2 ยท ๐‘) / 3))
160 eqid 2736 . . . . . . . . . 10 (โŒŠโ€˜(โˆšโ€˜(2 ยท ๐‘))) = (โŒŠโ€˜(โˆšโ€˜(2 ยท ๐‘)))
161151, 157, 158, 159, 160bposlem6 26478 . . . . . . . . 9 (๐œ‘ โ†’ ((4โ†‘๐‘) / ๐‘) < (((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) ยท (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5))))
162 reexplog 25791 . . . . . . . . . . . 12 ((4 โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„ค) โ†’ (4โ†‘๐‘) = (expโ€˜(๐‘ ยท (logโ€˜4))))
163102, 134, 162sylancr 588 . . . . . . . . . . 11 (๐œ‘ โ†’ (4โ†‘๐‘) = (expโ€˜(๐‘ ยท (logโ€˜4))))
16459reeflogd 25820 . . . . . . . . . . . 12 (๐œ‘ โ†’ (expโ€˜(logโ€˜๐‘)) = ๐‘)
165164eqcomd 2742 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ = (expโ€˜(logโ€˜๐‘)))
166163, 165oveq12d 7321 . . . . . . . . . 10 (๐œ‘ โ†’ ((4โ†‘๐‘) / ๐‘) = ((expโ€˜(๐‘ ยท (logโ€˜4))) / (expโ€˜(logโ€˜๐‘))))
167106recnd 11045 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ ยท (logโ€˜4)) โˆˆ โ„‚)
168107recnd 11045 . . . . . . . . . . 11 (๐œ‘ โ†’ (logโ€˜๐‘) โˆˆ โ„‚)
169 efsub 15850 . . . . . . . . . . 11 (((๐‘ ยท (logโ€˜4)) โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚) โ†’ (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) = ((expโ€˜(๐‘ ยท (logโ€˜4))) / (expโ€˜(logโ€˜๐‘))))
170167, 168, 169syl2anc 585 . . . . . . . . . 10 (๐œ‘ โ†’ (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) = ((expโ€˜(๐‘ ยท (logโ€˜4))) / (expโ€˜(logโ€˜๐‘))))
171166, 170eqtr4d 2779 . . . . . . . . 9 (๐œ‘ โ†’ ((4โ†‘๐‘) / ๐‘) = (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))))
17293rpcnd 12816 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
17393rpne0d 12819 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘) โ‰  0)
174118recnd 11045 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) โˆˆ โ„‚)
175172, 173, 174cxpefd 25908 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) = (expโ€˜((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘)))))
176 2cn 12090 . . . . . . . . . . . 12 2 โˆˆ โ„‚
177 2ne0 12119 . . . . . . . . . . . 12 2 โ‰  0
178127recnd 11045 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„‚)
179 cxpef 25861 . . . . . . . . . . . 12 ((2 โˆˆ โ„‚ โˆง 2 โ‰  0 โˆง (((4 ยท ๐‘) / 3) โˆ’ 5) โˆˆ โ„‚) โ†’ (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5)) = (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))
180176, 177, 178, 179mp3an12i 1465 . . . . . . . . . . 11 (๐œ‘ โ†’ (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5)) = (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))
181175, 180oveq12d 7321 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) ยท (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5))) = ((expโ€˜((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘)))) ยท (expโ€˜((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
182120recnd 11045 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) โˆˆ โ„‚)
183129recnd 11045 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆˆ โ„‚)
184 efadd 15844 . . . . . . . . . . 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 585 . . . . . . . . . 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 2779 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘)โ†‘๐‘(((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2)) ยท (2โ†‘๐‘(((4 ยท ๐‘) / 3) โˆ’ 5))) = (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
187161, 171, 1863brtr3d 5112 . . . . . . . 8 (๐œ‘ โ†’ (expโ€˜((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘))) < (expโ€˜(((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)))))
188 eflt 15867 . . . . . . . . 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 585 . . . . . . . 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 258 . . . . . . 7 (๐œ‘ โ†’ ((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) < (((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))))
191108, 130, 133, 190ltsub1dd 11629 . . . . . 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 11045 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘ โˆˆ โ„‚)
193 mulcom 10999 . . . . . . . . . . 11 ((2 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ (2 ยท ๐‘) = (๐‘ ยท 2))
194176, 192, 193sylancr 588 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท ๐‘) = (๐‘ ยท 2))
195194oveq1d 7318 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘) ยท (logโ€˜2)) = ((๐‘ ยท 2) ยท (logโ€˜2)))
19691recni 11031 . . . . . . . . . . . 12 (logโ€˜2) โˆˆ โ„‚
197 mulass 11001 . . . . . . . . . . . 12 ((๐‘ โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง (logโ€˜2) โˆˆ โ„‚) โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (2 ยท (logโ€˜2))))
198176, 196, 197mp3an23 1453 . . . . . . . . . . 11 (๐‘ โˆˆ โ„‚ โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (2 ยท (logโ€˜2))))
199192, 198syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (2 ยท (logโ€˜2))))
2001962timesi 12153 . . . . . . . . . . . 12 (2 ยท (logโ€˜2)) = ((logโ€˜2) + (logโ€˜2))
201 relogmul 25788 . . . . . . . . . . . . 13 ((2 โˆˆ โ„+ โˆง 2 โˆˆ โ„+) โ†’ (logโ€˜(2 ยท 2)) = ((logโ€˜2) + (logโ€˜2)))
20289, 89, 201mp2an 690 . . . . . . . . . . . 12 (logโ€˜(2 ยท 2)) = ((logโ€˜2) + (logโ€˜2))
203 2t2e4 12179 . . . . . . . . . . . . 13 (2 ยท 2) = 4
204203fveq2i 6803 . . . . . . . . . . . 12 (logโ€˜(2 ยท 2)) = (logโ€˜4)
205200, 202, 2043eqtr2i 2770 . . . . . . . . . . 11 (2 ยท (logโ€˜2)) = (logโ€˜4)
206205oveq2i 7314 . . . . . . . . . 10 (๐‘ ยท (2 ยท (logโ€˜2))) = (๐‘ ยท (logโ€˜4))
207199, 206eqtrdi 2792 . . . . . . . . 9 (๐œ‘ โ†’ ((๐‘ ยท 2) ยท (logโ€˜2)) = (๐‘ ยท (logโ€˜4)))
208195, 207eqtrd 2776 . . . . . . . 8 (๐œ‘ โ†’ ((2 ยท ๐‘) ยท (logโ€˜2)) = (๐‘ ยท (logโ€˜4)))
209208oveq1d 7318 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘) ยท (logโ€˜2)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))) = ((๐‘ ยท (logโ€˜4)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
210124recnd 11045 . . . . . . . . . 10 (๐œ‘ โ†’ ((4 ยท ๐‘) / 3) โˆˆ โ„‚)
211 3rp 12778 . . . . . . . . . . . 12 3 โˆˆ โ„+
212 rpdivcl 12797 . . . . . . . . . . . 12 (((2 ยท ๐‘) โˆˆ โ„+ โˆง 3 โˆˆ โ„+) โ†’ ((2 ยท ๐‘) / 3) โˆˆ โ„+)
21393, 211, 212sylancl 587 . . . . . . . . . . 11 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) โˆˆ โ„+)
214213rpcnd 12816 . . . . . . . . . 10 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) โˆˆ โ„‚)
215 4p2e6 12168 . . . . . . . . . . . . . 14 (4 + 2) = 6
216215oveq1i 7313 . . . . . . . . . . . . 13 ((4 + 2) ยท ๐‘) = (6 ยท ๐‘)
217 4cn 12100 . . . . . . . . . . . . . 14 4 โˆˆ โ„‚
218 adddir 11008 . . . . . . . . . . . . . 14 ((4 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚) โ†’ ((4 + 2) ยท ๐‘) = ((4 ยท ๐‘) + (2 ยท ๐‘)))
219217, 176, 192, 218mp3an12i 1465 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((4 + 2) ยท ๐‘) = ((4 ยท ๐‘) + (2 ยท ๐‘)))
220216, 219eqtr3id 2790 . . . . . . . . . . . 12 (๐œ‘ โ†’ (6 ยท ๐‘) = ((4 ยท ๐‘) + (2 ยท ๐‘)))
221220oveq1d 7318 . . . . . . . . . . 11 (๐œ‘ โ†’ ((6 ยท ๐‘) / 3) = (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3))
222 6cn 12106 . . . . . . . . . . . . . 14 6 โˆˆ โ„‚
223 3cn 12096 . . . . . . . . . . . . . . 15 3 โˆˆ โ„‚
224 3ne0 12121 . . . . . . . . . . . . . . 15 3 โ‰  0
225223, 224pm3.2i 472 . . . . . . . . . . . . . 14 (3 โˆˆ โ„‚ โˆง 3 โ‰  0)
226 div23 11694 . . . . . . . . . . . . . 14 ((6 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ ((6 ยท ๐‘) / 3) = ((6 / 3) ยท ๐‘))
227222, 225, 226mp3an13 1452 . . . . . . . . . . . . 13 (๐‘ โˆˆ โ„‚ โ†’ ((6 ยท ๐‘) / 3) = ((6 / 3) ยท ๐‘))
228192, 227syl 17 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((6 ยท ๐‘) / 3) = ((6 / 3) ยท ๐‘))
229 3t2e6 12181 . . . . . . . . . . . . . . 15 (3 ยท 2) = 6
230229oveq1i 7313 . . . . . . . . . . . . . 14 ((3 ยท 2) / 3) = (6 / 3)
231176, 223, 224divcan3i 11763 . . . . . . . . . . . . . 14 ((3 ยท 2) / 3) = 2
232230, 231eqtr3i 2766 . . . . . . . . . . . . 13 (6 / 3) = 2
233232oveq1i 7313 . . . . . . . . . . . 12 ((6 / 3) ยท ๐‘) = (2 ยท ๐‘)
234228, 233eqtrdi 2792 . . . . . . . . . . 11 (๐œ‘ โ†’ ((6 ยท ๐‘) / 3) = (2 ยท ๐‘))
235122recnd 11045 . . . . . . . . . . . 12 (๐œ‘ โ†’ (4 ยท ๐‘) โˆˆ โ„‚)
236 remulcl 10998 . . . . . . . . . . . . . 14 ((2 โˆˆ โ„ โˆง ๐‘ โˆˆ โ„) โ†’ (2 ยท ๐‘) โˆˆ โ„)
237116, 36, 236sylancr 588 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„)
238237recnd 11045 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท ๐‘) โˆˆ โ„‚)
239 divdir 11700 . . . . . . . . . . . . 13 (((4 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
240225, 239mp3an3 1450 . . . . . . . . . . . 12 (((4 ยท ๐‘) โˆˆ โ„‚ โˆง (2 ยท ๐‘) โˆˆ โ„‚) โ†’ (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
241235, 238, 240syl2anc 585 . . . . . . . . . . 11 (๐œ‘ โ†’ (((4 ยท ๐‘) + (2 ยท ๐‘)) / 3) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
242221, 234, 2413eqtr3d 2784 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท ๐‘) = (((4 ยท ๐‘) / 3) + ((2 ยท ๐‘) / 3)))
243210, 214, 242mvrladdd 11430 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท ๐‘) โˆ’ ((4 ยท ๐‘) / 3)) = ((2 ยท ๐‘) / 3))
244243oveq1d 7318 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘) โˆ’ ((4 ยท ๐‘) / 3)) ยท (logโ€˜2)) = (((2 ยท ๐‘) / 3) ยท (logโ€˜2)))
24599recnd 11045 . . . . . . . . 9 (๐œ‘ โ†’ (logโ€˜2) โˆˆ โ„‚)
246238, 210, 245subdird 11474 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘) โˆ’ ((4 ยท ๐‘) / 3)) ยท (logโ€˜2)) = (((2 ยท ๐‘) ยท (logโ€˜2)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
247244, 246eqtr3d 2778 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) = (((2 ยท ๐‘) ยท (logโ€˜2)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
248132recnd 11045 . . . . . . . 8 (๐œ‘ โ†’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆˆ โ„‚)
249167, 248, 168nnncan2d 11409 . . . . . . 7 (๐œ‘ โ†’ (((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = ((๐‘ ยท (logโ€˜4)) โˆ’ (((4 ยท ๐‘) / 3) ยท (logโ€˜2))))
250209, 247, 2493eqtr4d 2786 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) = (((๐‘ ยท (logโ€˜4)) โˆ’ (logโ€˜๐‘)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))))
251115recnd 11045 . . . . . . . . . 10 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„‚)
252176a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ 2 โˆˆ โ„‚)
253119recnd 11045 . . . . . . . . . 10 (๐œ‘ โ†’ (logโ€˜(2 ยท ๐‘)) โˆˆ โ„‚)
254251, 252, 253adddird 11042 . . . . . . . . 9 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (2 ยท (logโ€˜(2 ยท ๐‘)))))
255 relogmul 25788 . . . . . . . . . . . . 13 ((2 โˆˆ โ„+ โˆง ๐‘ โˆˆ โ„+) โ†’ (logโ€˜(2 ยท ๐‘)) = ((logโ€˜2) + (logโ€˜๐‘)))
25689, 59, 255sylancr 588 . . . . . . . . . . . 12 (๐œ‘ โ†’ (logโ€˜(2 ยท ๐‘)) = ((logโ€˜2) + (logโ€˜๐‘)))
257256oveq2d 7319 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท (logโ€˜(2 ยท ๐‘))) = (2 ยท ((logโ€˜2) + (logโ€˜๐‘))))
258252, 245, 168adddid 11041 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท ((logโ€˜2) + (logโ€˜๐‘))) = ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))))
259257, 258eqtrd 2776 . . . . . . . . . 10 (๐œ‘ โ†’ (2 ยท (logโ€˜(2 ยท ๐‘))) = ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))))
260259oveq2d 7319 . . . . . . . . 9 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (2 ยท (logโ€˜(2 ยท ๐‘)))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))))
261254, 260eqtrd 2776 . . . . . . . 8 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))))
262 5cn 12103 . . . . . . . . . . . 12 5 โˆˆ โ„‚
263262a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ 5 โˆˆ โ„‚)
264210, 263, 245subdird 11474 . . . . . . . . . 10 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) = ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (5 ยท (logโ€˜2))))
265264oveq1d 7318 . . . . . . . . 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 11024 . . . . . . . . . . 11 (5 ยท (logโ€˜2)) โˆˆ โ„‚
267266a1i 11 . . . . . . . . . 10 (๐œ‘ โ†’ (5 ยท (logโ€˜2)) โˆˆ โ„‚)
268248, 267, 168nnncan1d 11408 . . . . . . . . 9 (๐œ‘ โ†’ (((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (5 ยท (logโ€˜2))) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))
269265, 268eqtrd 2776 . . . . . . . 8 (๐œ‘ โ†’ (((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2)) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))) = ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))
270261, 269oveq12d 7321 . . . . . . 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 11045 . . . . . . . 8 (๐œ‘ โ†’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘)) โˆˆ โ„‚)
272182, 183, 271addsubassd 11394 . . . . . . 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 11467 . . . . . . . . . . . . 13 ((5 โˆ’ 3) ยท (logโ€˜2)) = ((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2)))
274 3p2e5 12166 . . . . . . . . . . . . . . . 16 (3 + 2) = 5
275274oveq1i 7313 . . . . . . . . . . . . . . 15 ((3 + 2) โˆ’ 3) = (5 โˆ’ 3)
276 pncan2 11270 . . . . . . . . . . . . . . . 16 ((3 โˆˆ โ„‚ โˆง 2 โˆˆ โ„‚) โ†’ ((3 + 2) โˆ’ 3) = 2)
277223, 176, 276mp2an 690 . . . . . . . . . . . . . . 15 ((3 + 2) โˆ’ 3) = 2
278275, 277eqtr3i 2766 . . . . . . . . . . . . . 14 (5 โˆ’ 3) = 2
279278oveq1i 7313 . . . . . . . . . . . . 13 ((5 โˆ’ 3) ยท (logโ€˜2)) = (2 ยท (logโ€˜2))
280273, 279eqtr3i 2766 . . . . . . . . . . . 12 ((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) = (2 ยท (logโ€˜2))
281280a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ ((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) = (2 ยท (logโ€˜2)))
282 mulcl 10997 . . . . . . . . . . . . 13 ((2 โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚) โ†’ (2 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
283176, 168, 282sylancr 588 . . . . . . . . . . . 12 (๐œ‘ โ†’ (2 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
284 df-3 12079 . . . . . . . . . . . . . . . 16 3 = (2 + 1)
285284oveq1i 7313 . . . . . . . . . . . . . . 15 (3 ยท (logโ€˜๐‘)) = ((2 + 1) ยท (logโ€˜๐‘))
286 1cnd 11012 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 1 โˆˆ โ„‚)
287252, 286, 168adddird 11042 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 + 1) ยท (logโ€˜๐‘)) = ((2 ยท (logโ€˜๐‘)) + (1 ยท (logโ€˜๐‘))))
288285, 287eqtrid 2788 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (3 ยท (logโ€˜๐‘)) = ((2 ยท (logโ€˜๐‘)) + (1 ยท (logโ€˜๐‘))))
289168mulid2d 11035 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (1 ยท (logโ€˜๐‘)) = (logโ€˜๐‘))
290289oveq2d 7319 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((2 ยท (logโ€˜๐‘)) + (1 ยท (logโ€˜๐‘))) = ((2 ยท (logโ€˜๐‘)) + (logโ€˜๐‘)))
291288, 290eqtrd 2776 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (3 ยท (logโ€˜๐‘)) = ((2 ยท (logโ€˜๐‘)) + (logโ€˜๐‘)))
292291oveq1d 7318 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2))) = (((2 ยท (logโ€˜๐‘)) + (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2))))
293283, 168, 267, 292assraddsubd 11431 . . . . . . . . . . 11 (๐œ‘ โ†’ ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2))) = ((2 ยท (logโ€˜๐‘)) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))))
294281, 293oveq12d 7321 . . . . . . . . . 10 (๐œ‘ โ†’ (((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) + ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2)))) = ((2 ยท (logโ€˜2)) + ((2 ยท (logโ€˜๐‘)) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))))
295 relogdiv 25789 . . . . . . . . . . . . . 14 ((๐‘ โˆˆ โ„+ โˆง 2 โˆˆ โ„+) โ†’ (logโ€˜(๐‘ / 2)) = ((logโ€˜๐‘) โˆ’ (logโ€˜2)))
29659, 89, 295sylancl 587 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (logโ€˜(๐‘ / 2)) = ((logโ€˜๐‘) โˆ’ (logโ€˜2)))
297296oveq2d 7319 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท (logโ€˜(๐‘ / 2))) = (3 ยท ((logโ€˜๐‘) โˆ’ (logโ€˜2))))
298 subdi 11450 . . . . . . . . . . . . . 14 ((3 โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚ โˆง (logโ€˜2) โˆˆ โ„‚) โ†’ (3 ยท ((logโ€˜๐‘) โˆ’ (logโ€˜2))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
299223, 196, 298mp3an13 1452 . . . . . . . . . . . . 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 2776 . . . . . . . . . . 11 (๐œ‘ โ†’ (3 ยท (logโ€˜(๐‘ / 2))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
302 div23 11694 . . . . . . . . . . . . . . . . 17 ((2 โˆˆ โ„‚ โˆง ๐‘ โˆˆ โ„‚ โˆง (3 โˆˆ โ„‚ โˆง 3 โ‰  0)) โ†’ ((2 ยท ๐‘) / 3) = ((2 / 3) ยท ๐‘))
303176, 225, 302mp3an13 1452 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ โ„‚ โ†’ ((2 ยท ๐‘) / 3) = ((2 / 3) ยท ๐‘))
304192, 303syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) = ((2 / 3) ยท ๐‘))
305223, 176, 223, 176, 177, 177divmuldivi 11777 . . . . . . . . . . . . . . . . 17 ((3 / 2) ยท (3 / 2)) = ((3 ยท 3) / (2 ยท 2))
306 3t3e9 12182 . . . . . . . . . . . . . . . . . 18 (3 ยท 3) = 9
307306, 203oveq12i 7315 . . . . . . . . . . . . . . . . 17 ((3 ยท 3) / (2 ยท 2)) = (9 / 4)
308305, 307eqtr2i 2765 . . . . . . . . . . . . . . . 16 (9 / 4) = ((3 / 2) ยท (3 / 2))
309308a1i 11 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (9 / 4) = ((3 / 2) ยท (3 / 2)))
310304, 309oveq12d 7321 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (9 / 4)) = (((2 / 3) ยท ๐‘) ยท ((3 / 2) ยท (3 / 2))))
311176, 223, 224divcli 11759 . . . . . . . . . . . . . . 15 (2 / 3) โˆˆ โ„‚
312223, 176, 177divcli 11759 . . . . . . . . . . . . . . . 16 (3 / 2) โˆˆ โ„‚
313 mul4 11185 . . . . . . . . . . . . . . . 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 588 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 / 3) ยท ๐‘) ยท ((3 / 2) ยท (3 / 2))) = (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))))
316 divcan6 11724 . . . . . . . . . . . . . . . . . 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 7313 . . . . . . . . . . . . . . . 16 (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))) = (1 ยท (๐‘ ยท (3 / 2)))
319 mulcl 10997 . . . . . . . . . . . . . . . . . 18 ((๐‘ โˆˆ โ„‚ โˆง (3 / 2) โˆˆ โ„‚) โ†’ (๐‘ ยท (3 / 2)) โˆˆ โ„‚)
320192, 312, 319sylancl 587 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐‘ ยท (3 / 2)) โˆˆ โ„‚)
321320mulid2d 11035 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (1 ยท (๐‘ ยท (3 / 2))) = (๐‘ ยท (3 / 2)))
322318, 321eqtrid 2788 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))) = (๐‘ ยท (3 / 2)))
323 2cnne0 12225 . . . . . . . . . . . . . . . . 17 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
324 div12 11697 . . . . . . . . . . . . . . . . 17 ((๐‘ โˆˆ โ„‚ โˆง 3 โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ (๐‘ ยท (3 / 2)) = (3 ยท (๐‘ / 2)))
325223, 323, 324mp3an23 1453 . . . . . . . . . . . . . . . 16 (๐‘ โˆˆ โ„‚ โ†’ (๐‘ ยท (3 / 2)) = (3 ยท (๐‘ / 2)))
326192, 325syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘ ยท (3 / 2)) = (3 ยท (๐‘ / 2)))
327322, 326eqtrd 2776 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 / 3) ยท (3 / 2)) ยท (๐‘ ยท (3 / 2))) = (3 ยท (๐‘ / 2)))
328310, 315, 3273eqtrd 2780 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (9 / 4)) = (3 ยท (๐‘ / 2)))
329328, 82oveq12d 7321 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((2 ยท ๐‘) / 3) ยท (9 / 4)) ยท (๐บโ€˜(๐‘ / 2))) = ((3 ยท (๐‘ / 2)) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))))
33075recni 11031 . . . . . . . . . . . . . 14 (9 / 4) โˆˆ โ„‚
331330a1i 11 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (9 / 4) โˆˆ โ„‚)
33285recnd 11045 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐บโ€˜(๐‘ / 2)) โˆˆ โ„‚)
333214, 331, 332mulassd 11040 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((2 ยท ๐‘) / 3) ยท (9 / 4)) ยท (๐บโ€˜(๐‘ / 2))) = (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))
334223a1i 11 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ 3 โˆˆ โ„‚)
33576rpcnd 12816 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐‘ / 2) โˆˆ โ„‚)
33683recnd 11045 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (logโ€˜(๐‘ / 2)) โˆˆ โ„‚)
33776rpne0d 12819 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐‘ / 2) โ‰  0)
338336, 335, 337divcld 11793 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)) โˆˆ โ„‚)
339334, 335, 338mulassd 11040 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((3 ยท (๐‘ / 2)) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))) = (3 ยท ((๐‘ / 2) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))))
340336, 335, 337divcan2d 11795 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐‘ / 2) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))) = (logโ€˜(๐‘ / 2)))
341340oveq2d 7319 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (3 ยท ((๐‘ / 2) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2)))) = (3 ยท (logโ€˜(๐‘ / 2))))
342339, 341eqtrd 2776 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((3 ยท (๐‘ / 2)) ยท ((logโ€˜(๐‘ / 2)) / (๐‘ / 2))) = (3 ยท (logโ€˜(๐‘ / 2))))
343329, 333, 3423eqtr3d 2784 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) = (3 ยท (logโ€˜(๐‘ / 2))))
344223, 196mulcli 11024 . . . . . . . . . . . . 13 (3 ยท (logโ€˜2)) โˆˆ โ„‚
345344a1i 11 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท (logโ€˜2)) โˆˆ โ„‚)
346 mulcl 10997 . . . . . . . . . . . . 13 ((3 โˆˆ โ„‚ โˆง (logโ€˜๐‘) โˆˆ โ„‚) โ†’ (3 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
347223, 168, 346sylancr 588 . . . . . . . . . . . 12 (๐œ‘ โ†’ (3 ยท (logโ€˜๐‘)) โˆˆ โ„‚)
348267, 345, 347npncan3d 11410 . . . . . . . . . . 11 (๐œ‘ โ†’ (((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) + ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2)))) = ((3 ยท (logโ€˜๐‘)) โˆ’ (3 ยท (logโ€˜2))))
349301, 343, 3483eqtr4d 2786 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) = (((5 ยท (logโ€˜2)) โˆ’ (3 ยท (logโ€˜2))) + ((3 ยท (logโ€˜๐‘)) โˆ’ (5 ยท (logโ€˜2)))))
350116, 91remulcli 11033 . . . . . . . . . . . . 13 (2 ยท (logโ€˜2)) โˆˆ โ„
351350recni 11031 . . . . . . . . . . . 12 (2 ยท (logโ€˜2)) โˆˆ โ„‚
352351a1i 11 . . . . . . . . . . 11 (๐œ‘ โ†’ (2 ยท (logโ€˜2)) โˆˆ โ„‚)
353 subcl 11262 . . . . . . . . . . . 12 (((logโ€˜๐‘) โˆˆ โ„‚ โˆง (5 ยท (logโ€˜2)) โˆˆ โ„‚) โ†’ ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))) โˆˆ โ„‚)
354168, 266, 353sylancl 587 . . . . . . . . . . 11 (๐œ‘ โ†’ ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))) โˆˆ โ„‚)
355352, 283, 354addassd 11039 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))) = ((2 ยท (logโ€˜2)) + ((2 ยท (logโ€˜๐‘)) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2))))))
356294, 349, 3553eqtr4d 2786 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) = (((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))))
357356oveq2d 7319 . . . . . . . 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 10997 . . . . . . . . . . 11 ((((โˆšโ€˜(2 ยท ๐‘)) / 3) โˆˆ โ„‚ โˆง (logโ€˜2) โˆˆ โ„‚) โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) โˆˆ โ„‚)
359251, 196, 358sylancl 587 . . . . . . . . . 10 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) โˆˆ โ„‚)
360251, 168mulcld 11037 . . . . . . . . . 10 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) โˆˆ โ„‚)
36187recnd 11045 . . . . . . . . . . 11 (๐œ‘ โ†’ ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))) โˆˆ โ„‚)
362214, 361mulcld 11037 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) โˆˆ โ„‚)
363359, 360, 362addassd 11039 . . . . . . . . 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 7319 . . . . . . . . . . 11 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((logโ€˜2) + (logโ€˜๐‘))))
365251, 245, 168adddid 11041 . . . . . . . . . . 11 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((logโ€˜2) + (logโ€˜๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘))))
366364, 365eqtrd 2776 . . . . . . . . . 10 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘))))
367366oveq1d 7318 . . . . . . . . 9 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
36857oveq2d 7319 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = (((2 ยท ๐‘) / 3) ยท ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
36988recnd 11045 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) โˆˆ โ„‚)
37096recnd 11045 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))) โˆˆ โ„‚)
371214, 369, 370adddid 11041 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))) + ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))) = ((((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) + (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
372368, 371eqtrd 2776 . . . . . . . . . 10 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) + (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
37371recnd 11045 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) โˆˆ โ„‚)
374214, 373, 361adddid 11041 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
37593rpge0d 12818 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ 0 โ‰ค (2 ยท ๐‘))
376 remsqsqrt 15009 . . . . . . . . . . . . . . . . . 18 (((2 ยท ๐‘) โˆˆ โ„ โˆง 0 โ‰ค (2 ยท ๐‘)) โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) = (2 ยท ๐‘))
377237, 375, 376syl2anc 585 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) = (2 ยท ๐‘))
378377oveq1d 7318 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) / 3) = ((2 ยท ๐‘) / 3))
379112recnd 11045 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โˆˆ โ„‚)
380224a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 3 โ‰  0)
381379, 379, 334, 380div23d 11830 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) ยท (โˆšโ€˜(2 ยท ๐‘))) / 3) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))))
382378, 381eqtr3d 2778 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((2 ยท ๐‘) / 3) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))))
383382oveq1d 7318 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))))
384251, 379, 373mulassd 11040 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))))))
385 0le2 12117 . . . . . . . . . . . . . . . . . . 19 0 โ‰ค 2
386116, 385pm3.2i 472 . . . . . . . . . . . . . . . . . 18 (2 โˆˆ โ„ โˆง 0 โ‰ค 2)
38759rprege0d 12821 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘))
388 sqrtmul 15012 . . . . . . . . . . . . . . . . . 18 (((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โˆง (๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘)) โ†’ (โˆšโ€˜(2 ยท ๐‘)) = ((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)))
389386, 387, 388sylancr 588 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) = ((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)))
390389oveq1d 7318 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))))
39158recni 11031 . . . . . . . . . . . . . . . . . 18 (โˆšโ€˜2) โˆˆ โ„‚
392391a1i 11 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜2) โˆˆ โ„‚)
39360rpcnd 12816 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โˆˆ โ„‚)
39469recnd 11045 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐บโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„‚)
395392, 393, 392, 394mul4d 11229 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (โˆšโ€˜๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜2) ยท (โˆšโ€˜2)) ยท ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘)))))
396 remsqsqrt 15009 . . . . . . . . . . . . . . . . . . . 20 ((2 โˆˆ โ„ โˆง 0 โ‰ค 2) โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
397116, 385, 396mp2an 690 . . . . . . . . . . . . . . . . . . 19 ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2
398397a1i 11 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((โˆšโ€˜2) ยท (โˆšโ€˜2)) = 2)
39966oveq2d 7319 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘))) = ((โˆšโ€˜๐‘) ยท ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘))))
40067recnd 11045 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (logโ€˜(โˆšโ€˜๐‘)) โˆˆ โ„‚)
40160rpne0d 12819 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (โˆšโ€˜๐‘) โ‰  0)
402400, 393, 401divcan2d 11795 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท ((logโ€˜(โˆšโ€˜๐‘)) / (โˆšโ€˜๐‘))) = (logโ€˜(โˆšโ€˜๐‘)))
403399, 402eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘))) = (logโ€˜(โˆšโ€˜๐‘)))
404398, 403oveq12d 7321 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (โˆšโ€˜2)) ยท ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (2 ยท (logโ€˜(โˆšโ€˜๐‘))))
4054002timesd 12258 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (2 ยท (logโ€˜(โˆšโ€˜๐‘))) = ((logโ€˜(โˆšโ€˜๐‘)) + (logโ€˜(โˆšโ€˜๐‘))))
40660, 60relogmuld 25821 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (logโ€˜((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))) = ((logโ€˜(โˆšโ€˜๐‘)) + (logโ€˜(โˆšโ€˜๐‘))))
407 remsqsqrt 15009 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ โˆˆ โ„ โˆง 0 โ‰ค ๐‘) โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
408387, 407syl 17 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘)) = ๐‘)
409408fveq2d 6804 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (logโ€˜((โˆšโ€˜๐‘) ยท (โˆšโ€˜๐‘))) = (logโ€˜๐‘))
410406, 409eqtr3d 2778 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((logโ€˜(โˆšโ€˜๐‘)) + (logโ€˜(โˆšโ€˜๐‘))) = (logโ€˜๐‘))
411404, 405, 4103eqtrd 2780 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((โˆšโ€˜2) ยท (โˆšโ€˜2)) ยท ((โˆšโ€˜๐‘) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (logโ€˜๐‘))
412390, 395, 4113eqtrd 2780 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (logโ€˜๐‘))
413412oveq2d 7319 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)))
414383, 384, 4133eqtrd 2780 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)))
415414oveq1d 7318 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((2 ยท ๐‘) / 3) ยท ((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘)))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
416374, 415eqtrd 2776 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (((โˆšโ€˜2) ยท (๐บโ€˜(โˆšโ€˜๐‘))) + ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
417382oveq1d 7318 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))))
418251, 379, 370mulassd 11040 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (โˆšโ€˜(2 ยท ๐‘))) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))))
41994rpne0d 12819 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (โˆšโ€˜(2 ยท ๐‘)) โ‰  0)
420245, 379, 419divcan2d 11795 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((โˆšโ€˜(2 ยท ๐‘)) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = (logโ€˜2))
421420oveq2d 7319 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท ((โˆšโ€˜(2 ยท ๐‘)) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘))))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)))
422417, 418, 4213eqtrd 2780 . . . . . . . . . . 11 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท ((logโ€˜2) / (โˆšโ€˜(2 ยท ๐‘)))) = (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)))
423416, 422oveq12d 7321 . . . . . . . . . 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 11036 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))) โˆˆ โ„‚)
425424, 359addcomd 11219 . . . . . . . . . 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 2780 . . . . . . . . 9 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜2)) + ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜๐‘)) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2)))))))
427363, 367, 4263eqtr4rd 2787 . . . . . . . 8 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + (((2 ยท ๐‘) / 3) ยท ((9 / 4) ยท (๐บโ€˜(๐‘ / 2))))))
428251, 253mulcld 11037 . . . . . . . . 9 (๐œ‘ โ†’ (((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) โˆˆ โ„‚)
429 addcl 10995 . . . . . . . . . 10 (((2 ยท (logโ€˜2)) โˆˆ โ„‚ โˆง (2 ยท (logโ€˜๐‘)) โˆˆ โ„‚) โ†’ ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) โˆˆ โ„‚)
430351, 283, 429sylancr 588 . . . . . . . . 9 (๐œ‘ โ†’ ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘))) โˆˆ โ„‚)
431428, 430, 354addassd 11039 . . . . . . . 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 2786 . . . . . . 7 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = (((((โˆšโ€˜(2 ยท ๐‘)) / 3) ยท (logโ€˜(2 ยท ๐‘))) + ((2 ยท (logโ€˜2)) + (2 ยท (logโ€˜๐‘)))) + ((logโ€˜๐‘) โˆ’ (5 ยท (logโ€˜2)))))
433270, 272, 4323eqtr4rd 2787 . . . . . 6 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)) = ((((((โˆšโ€˜(2 ยท ๐‘)) / 3) + 2) ยท (logโ€˜(2 ยท ๐‘))) + ((((4 ยท ๐‘) / 3) โˆ’ 5) ยท (logโ€˜2))) โˆ’ ((((4 ยท ๐‘) / 3) ยท (logโ€˜2)) โˆ’ (logโ€˜๐‘))))
434191, 250, 4333brtr4d 5113 . . . . 5 (๐œ‘ โ†’ (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) < (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘)))
43599, 98, 213ltmul2d 12856 . . . . 5 (๐œ‘ โ†’ ((logโ€˜2) < (๐นโ€˜๐‘) โ†” (((2 ยท ๐‘) / 3) ยท (logโ€˜2)) < (((2 ยท ๐‘) / 3) ยท (๐นโ€˜๐‘))))
436434, 435mpbird 258 . . . 4 (๐œ‘ โ†’ (logโ€˜2) < (๐นโ€˜๐‘))
43745, 99, 98, 100, 436lttrd 11178 . . 3 (๐œ‘ โ†’ (๐นโ€˜64) < (๐นโ€˜๐‘))
43845, 98, 437ltnsymd 11166 . 2 (๐œ‘ โ†’ ยฌ (๐นโ€˜๐‘) < (๐นโ€˜64))
43942, 438pm2.21dd 194 1 (๐œ‘ โ†’ ๐œ“)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2941  โˆƒwrex 3071  ifcif 4465   class class class wbr 5081   โ†ฆ cmpt 5164  โ€˜cfv 6454  (class class class)co 7303  โ„‚cc 10911  โ„cr 10912  0cc0 10913  1c1 10914   + caddc 10916   ยท cmul 10918   < clt 11051   โ‰ค cle 11052   โˆ’ cmin 11247   / cdiv 11674  โ„•cn 12015  2c2 12070  3c3 12071  4c4 12072  5c5 12073  6c6 12074  8c8 12076  9c9 12077  โ„คcz 12361  cdc 12479  โ„คโ‰ฅcuz 12624  โ„+crp 12772  โŒŠcfl 13552  โ†‘cexp 13824  Ccbc 14058  โˆšcsqrt 14985  expce 15812  eceu 15813  โ„™cprime 16417   pCnt cpc 16578  logclog 25751  โ†‘๐‘ccxp 25752
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 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616  ax-inf2 9439  ax-cnex 10969  ax-resscn 10970  ax-1cn 10971  ax-icn 10972  ax-addcl 10973  ax-addrcl 10974  ax-mulcl 10975  ax-mulrcl 10976  ax-mulcom 10977  ax-addass 10978  ax-mulass 10979  ax-distr 10980  ax-i2m1 10981  ax-1ne0 10982  ax-1rid 10983  ax-rnegex 10984  ax-rrecex 10985  ax-cnre 10986  ax-pre-lttri 10987  ax-pre-lttrn 10988  ax-pre-ltadd 10989  ax-pre-mulgt0 10990  ax-pre-sup 10991  ax-addf 10992  ax-mulf 10993
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3285  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-tp 4570  df-op 4572  df-uni 4845  df-int 4887  df-iun 4933  df-iin 4934  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-se 5552  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-pred 6213  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-isom 6463  df-riota 7260  df-ov 7306  df-oprab 7307  df-mpo 7308  df-of 7561  df-om 7741  df-1st 7859  df-2nd 7860  df-supp 8005  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268  df-1o 8324  df-2o 8325  df-oadd 8328  df-er 8525  df-map 8644  df-pm 8645  df-ixp 8713  df-en 8761  df-dom 8762  df-sdom 8763  df-fin 8764  df-fsupp 9169  df-fi 9210  df-sup 9241  df-inf 9242  df-oi 9309  df-dju 9699  df-card 9737  df-pnf 11053  df-mnf 11054  df-xr 11055  df-ltxr 11056  df-le 11057  df-sub 11249  df-neg 11250  df-div 11675  df-nn 12016  df-2 12078  df-3 12079  df-4 12080  df-5 12081  df-6 12082  df-7 12083  df-8 12084  df-9 12085  df-n0 12276  df-xnn0 12348  df-z 12362  df-dec 12480  df-uz 12625  df-q 12731  df-rp 12773  df-xneg 12890  df-xadd 12891  df-xmul 12892  df-ioo 13125  df-ioc 13126  df-ico 13127  df-icc 13128  df-fz 13282  df-fzo 13425  df-fl 13554  df-mod 13632  df-seq 13764  df-exp 13825  df-fac 14030  df-bc 14059  df-hash 14087  df-shft 14819  df-cj 14851  df-re 14852  df-im 14853  df-sqrt 14987  df-abs 14988  df-limsup 15221  df-clim 15238  df-rlim 15239  df-sum 15439  df-ef 15818  df-e 15819  df-sin 15820  df-cos 15821  df-pi 15823  df-dvds 16005  df-gcd 16243  df-prm 16418  df-pc 16579  df-struct 16889  df-sets 16906  df-slot 16924  df-ndx 16936  df-base 16954  df-ress 16983  df-plusg 17016  df-mulr 17017  df-starv 17018  df-sca 17019  df-vsca 17020  df-ip 17021  df-tset 17022  df-ple 17023  df-ds 17025  df-unif 17026  df-hom 17027  df-cco 17028  df-rest 17174  df-topn 17175  df-0g 17193  df-gsum 17194  df-topgen 17195  df-pt 17196  df-prds 17199  df-xrs 17254  df-qtop 17259  df-imas 17260  df-xps 17262  df-mre 17336  df-mrc 17337  df-acs 17339  df-mgm 18367  df-sgrp 18416  df-mnd 18427  df-submnd 18472  df-mulg 18742  df-cntz 18964  df-cmn 19429  df-psmet 20630  df-xmet 20631  df-met 20632  df-bl 20633  df-mopn 20634  df-fbas 20635  df-fg 20636  df-cnfld 20639  df-top 22084  df-topon 22101  df-topsp 22123  df-bases 22137  df-cld 22211  df-ntr 22212  df-cls 22213  df-nei 22290  df-lp 22328  df-perf 22329  df-cn 22419  df-cnp 22420  df-haus 22507  df-tx 22754  df-hmeo 22947  df-fil 23038  df-fm 23130  df-flim 23131  df-flf 23132  df-xms 23514  df-ms 23515  df-tms 23516  df-cncf 24082  df-limc 25071  df-dv 25072  df-log 25753  df-cxp 25754  df-cht 26287  df-ppi 26290
This theorem is referenced by:  bpos  26482
  Copyright terms: Public domain W3C validator