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

Theorem 01sqrexlem7 15222
Description: Lemma for 01sqrex 15223. (Contributed by Mario Carneiro, 10-Jul-2013.) (Proof shortened by AV, 9-Jul-2022.)
Hypotheses
Ref Expression
01sqrexlem1.1 ๐‘† = {๐‘ฅ โˆˆ โ„+ โˆฃ (๐‘ฅโ†‘2) โ‰ค ๐ด}
01sqrexlem1.2 ๐ต = sup(๐‘†, โ„, < )
01sqrexlem5.3 ๐‘‡ = {๐‘ฆ โˆฃ โˆƒ๐‘Ž โˆˆ ๐‘† โˆƒ๐‘ โˆˆ ๐‘† ๐‘ฆ = (๐‘Ž ยท ๐‘)}
Assertion
Ref Expression
01sqrexlem7 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ตโ†‘2) = ๐ด)
Distinct variable groups:   ๐‘Ž,๐‘,๐‘ฆ,๐‘†   ๐‘ฅ,๐‘Ž,๐ด,๐‘,๐‘ฆ   ๐‘ฆ,๐ต
Allowed substitution hints:   ๐ต(๐‘ฅ,๐‘Ž,๐‘)   ๐‘†(๐‘ฅ)   ๐‘‡(๐‘ฅ,๐‘ฆ,๐‘Ž,๐‘)

Proof of Theorem 01sqrexlem7
Dummy variable ๐‘ง is distinct from all other variables.
StepHypRef Expression
1 01sqrexlem1.1 . . 3 ๐‘† = {๐‘ฅ โˆˆ โ„+ โˆฃ (๐‘ฅโ†‘2) โ‰ค ๐ด}
2 01sqrexlem1.2 . . 3 ๐ต = sup(๐‘†, โ„, < )
3 01sqrexlem5.3 . . 3 ๐‘‡ = {๐‘ฆ โˆฃ โˆƒ๐‘Ž โˆˆ ๐‘† โˆƒ๐‘ โˆˆ ๐‘† ๐‘ฆ = (๐‘Ž ยท ๐‘)}
41, 2, 301sqrexlem6 15221 . 2 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ตโ†‘2) โ‰ค ๐ด)
51, 201sqrexlem3 15218 . . . . 5 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐‘† โІ โ„ โˆง ๐‘† โ‰  โˆ… โˆง โˆƒ๐‘ฆ โˆˆ โ„ โˆ€๐‘ง โˆˆ ๐‘† ๐‘ง โ‰ค ๐‘ฆ))
65adantr 479 . . . 4 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐‘† โІ โ„ โˆง ๐‘† โ‰  โˆ… โˆง โˆƒ๐‘ฆ โˆˆ โ„ โˆ€๐‘ง โˆˆ ๐‘† ๐‘ง โ‰ค ๐‘ฆ))
71, 201sqrexlem4 15219 . . . . . . . 8 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ต โˆˆ โ„+ โˆง ๐ต โ‰ค 1))
87adantr 479 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ต โˆˆ โ„+ โˆง ๐ต โ‰ค 1))
98simpld 493 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ๐ต โˆˆ โ„+)
10 rpre 13009 . . . . . . . . . . 11 (๐ด โˆˆ โ„+ โ†’ ๐ด โˆˆ โ„)
1110adantr 479 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ ๐ด โˆˆ โ„)
12 rpre 13009 . . . . . . . . . . . . 13 (๐ต โˆˆ โ„+ โ†’ ๐ต โˆˆ โ„)
1312adantr 479 . . . . . . . . . . . 12 ((๐ต โˆˆ โ„+ โˆง ๐ต โ‰ค 1) โ†’ ๐ต โˆˆ โ„)
147, 13syl 17 . . . . . . . . . . 11 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ ๐ต โˆˆ โ„)
1514resqcld 14116 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ตโ†‘2) โˆˆ โ„)
1611, 15resubcld 11667 . . . . . . . . 9 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„)
1716adantr 479 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„)
1815, 11posdifd 11826 . . . . . . . . 9 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ ((๐ตโ†‘2) < ๐ด โ†” 0 < (๐ด โˆ’ (๐ตโ†‘2))))
1918biimpa 475 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ 0 < (๐ด โˆ’ (๐ตโ†‘2)))
2017, 19elrpd 13040 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„+)
21 3rp 13007 . . . . . . 7 3 โˆˆ โ„+
22 rpdivcl 13026 . . . . . . 7 (((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„+ โˆง 3 โˆˆ โ„+) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„+)
2320, 21, 22sylancl 584 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„+)
249, 23rpaddcld 13058 . . . . 5 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ โ„+)
2514adantr 479 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ๐ต โˆˆ โ„)
2625recnd 11267 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ๐ต โˆˆ โ„‚)
27 3nn 12316 . . . . . . . . . . 11 3 โˆˆ โ„•
28 nndivre 12278 . . . . . . . . . . 11 (((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„ โˆง 3 โˆˆ โ„•) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„)
2916, 27, 28sylancl 584 . . . . . . . . . 10 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„)
3029adantr 479 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„)
3130recnd 11267 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„‚)
32 binom2 14207 . . . . . . . 8 ((๐ต โˆˆ โ„‚ โˆง ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„‚) โ†’ ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))โ†‘2) = (((๐ตโ†‘2) + (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)))
3326, 31, 32syl2anc 582 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))โ†‘2) = (((๐ตโ†‘2) + (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)))
3415adantr 479 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ตโ†‘2) โˆˆ โ„)
3534recnd 11267 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
36 2re 12311 . . . . . . . . . 10 2 โˆˆ โ„
3725, 30remulcld 11269 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ โ„)
38 remulcl 11218 . . . . . . . . . 10 ((2 โˆˆ โ„ โˆง (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ โ„) โ†’ (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) โˆˆ โ„)
3936, 37, 38sylancr 585 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) โˆˆ โ„)
4039recnd 11267 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) โˆˆ โ„‚)
4130resqcld 14116 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2) โˆˆ โ„)
4241recnd 11267 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2) โˆˆ โ„‚)
4335, 40, 42addassd 11261 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((๐ตโ†‘2) + (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)) = ((๐ตโ†‘2) + ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2))))
4433, 43eqtrd 2765 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))โ†‘2) = ((๐ตโ†‘2) + ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2))))
45 2cn 12312 . . . . . . . . . . . 12 2 โˆˆ โ„‚
46 mulass 11221 . . . . . . . . . . . 12 ((2 โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ โˆง ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„‚) โ†’ ((2 ยท ๐ต) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) = (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))))
4745, 26, 31, 46mp3an2i 1462 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท ๐ต) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) = (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))))
4847eqcomd 2731 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) = ((2 ยท ๐ต) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)))
4931sqvald 14134 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2) = (((๐ด โˆ’ (๐ตโ†‘2)) / 3) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)))
5048, 49oveq12d 7431 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)) = (((2 ยท ๐ต) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))))
51 remulcl 11218 . . . . . . . . . . . 12 ((2 โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โ†’ (2 ยท ๐ต) โˆˆ โ„)
5236, 25, 51sylancr 585 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (2 ยท ๐ต) โˆˆ โ„)
5352recnd 11267 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (2 ยท ๐ต) โˆˆ โ„‚)
5453, 31, 31adddird 11264 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) = (((2 ยท ๐ต) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))))
5550, 54eqtr4d 2768 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)) = (((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)))
567simprd 494 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ ๐ต โ‰ค 1)
57 1red 11240 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ 1 โˆˆ โ„)
58 2rp 13006 . . . . . . . . . . . . . . . . 17 2 โˆˆ โ„+
5958a1i 11 . . . . . . . . . . . . . . . 16 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ 2 โˆˆ โ„+)
6014, 57, 59lemul2d 13087 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ต โ‰ค 1 โ†” (2 ยท ๐ต) โ‰ค (2 ยท 1)))
6156, 60mpbid 231 . . . . . . . . . . . . . 14 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (2 ยท ๐ต) โ‰ค (2 ยท 1))
6261adantr 479 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (2 ยท ๐ต) โ‰ค (2 ยท 1))
63 2t1e2 12400 . . . . . . . . . . . . 13 (2 ยท 1) = 2
6462, 63breqtrdi 5185 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (2 ยท ๐ต) โ‰ค 2)
6511adantr 479 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ๐ด โˆˆ โ„)
66 1red 11240 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ 1 โˆˆ โ„)
6725sqge0d 14128 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ 0 โ‰ค (๐ตโ†‘2))
6865, 34addge01d 11827 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (0 โ‰ค (๐ตโ†‘2) โ†” ๐ด โ‰ค (๐ด + (๐ตโ†‘2))))
6967, 68mpbid 231 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ๐ด โ‰ค (๐ด + (๐ตโ†‘2)))
7065, 34, 65lesubaddd 11836 . . . . . . . . . . . . . . . . 17 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) โ‰ค ๐ด โ†” ๐ด โ‰ค (๐ด + (๐ตโ†‘2))))
7169, 70mpbird 256 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค ๐ด)
72 simplr 767 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ๐ด โ‰ค 1)
7317, 65, 66, 71, 72letrd 11396 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 1)
74 1le3 12449 . . . . . . . . . . . . . . . 16 1 โ‰ค 3
75 1re 11239 . . . . . . . . . . . . . . . . . 18 1 โˆˆ โ„
76 3re 12317 . . . . . . . . . . . . . . . . . 18 3 โˆˆ โ„
77 letr 11333 . . . . . . . . . . . . . . . . . 18 (((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง 3 โˆˆ โ„) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 1 โˆง 1 โ‰ค 3) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 3))
7875, 76, 77mp3an23 1449 . . . . . . . . . . . . . . . . 17 ((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„ โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 1 โˆง 1 โ‰ค 3) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 3))
7917, 78syl 17 . . . . . . . . . . . . . . . 16 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 1 โˆง 1 โ‰ค 3) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 3))
8074, 79mpan2i 695 . . . . . . . . . . . . . . 15 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 1 โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 3))
8173, 80mpd 15 . . . . . . . . . . . . . 14 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค 3)
82 3t1e3 12402 . . . . . . . . . . . . . 14 (3 ยท 1) = 3
8381, 82breqtrrdi 5186 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค (3 ยท 1))
84 3pos 12342 . . . . . . . . . . . . . . 15 0 < 3
85 ledivmul 12115 . . . . . . . . . . . . . . . 16 (((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„ โˆง 1 โˆˆ โ„ โˆง (3 โˆˆ โ„ โˆง 0 < 3)) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1 โ†” (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค (3 ยท 1)))
8675, 85mp3an2 1445 . . . . . . . . . . . . . . 15 (((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„ โˆง (3 โˆˆ โ„ โˆง 0 < 3)) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1 โ†” (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค (3 ยท 1)))
8776, 84, 86mpanr12 703 . . . . . . . . . . . . . 14 ((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„ โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1 โ†” (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค (3 ยท 1)))
8817, 87syl 17 . . . . . . . . . . . . 13 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1 โ†” (๐ด โˆ’ (๐ตโ†‘2)) โ‰ค (3 ยท 1)))
8983, 88mpbird 256 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1)
90 le2add 11721 . . . . . . . . . . . . . 14 ((((2 ยท ๐ต) โˆˆ โ„ โˆง ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„) โˆง (2 โˆˆ โ„ โˆง 1 โˆˆ โ„)) โ†’ (((2 ยท ๐ต) โ‰ค 2 โˆง ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1) โ†’ ((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค (2 + 1)))
9136, 75, 90mpanr12 703 . . . . . . . . . . . . 13 (((2 ยท ๐ต) โˆˆ โ„ โˆง ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โˆˆ โ„) โ†’ (((2 ยท ๐ต) โ‰ค 2 โˆง ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1) โ†’ ((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค (2 + 1)))
9252, 30, 91syl2anc 582 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((2 ยท ๐ต) โ‰ค 2 โˆง ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ‰ค 1) โ†’ ((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค (2 + 1)))
9364, 89, 92mp2and 697 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค (2 + 1))
94 df-3 12301 . . . . . . . . . . 11 3 = (2 + 1)
9593, 94breqtrrdi 5186 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค 3)
9652, 30readdcld 11268 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ โ„)
9776a1i 11 . . . . . . . . . . 11 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ 3 โˆˆ โ„)
9896, 97, 23lemul1d 13086 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค 3 โ†” (((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค (3 ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))))
9995, 98mpbid 231 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค (3 ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)))
10017recnd 11267 . . . . . . . . . 10 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„‚)
101 3cn 12318 . . . . . . . . . . 11 3 โˆˆ โ„‚
102 3ne0 12343 . . . . . . . . . . 11 3 โ‰  0
103 divcan2 11905 . . . . . . . . . . 11 (((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„‚ โˆง 3 โˆˆ โ„‚ โˆง 3 โ‰  0) โ†’ (3 ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) = (๐ด โˆ’ (๐ตโ†‘2)))
104101, 102, 103mp3an23 1449 . . . . . . . . . 10 ((๐ด โˆ’ (๐ตโ†‘2)) โˆˆ โ„‚ โ†’ (3 ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) = (๐ด โˆ’ (๐ตโ†‘2)))
105100, 104syl 17 . . . . . . . . 9 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (3 ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) = (๐ด โˆ’ (๐ตโ†‘2)))
10699, 105breqtrd 5170 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((2 ยท ๐ต) + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค (๐ด โˆ’ (๐ตโ†‘2)))
10755, 106eqbrtrd 5166 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)) โ‰ค (๐ด โˆ’ (๐ตโ†‘2)))
10839, 41readdcld 11268 . . . . . . . 8 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)) โˆˆ โ„)
10934, 108, 65leaddsub2d 11841 . . . . . . 7 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (((๐ตโ†‘2) + ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2))) โ‰ค ๐ด โ†” ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2)) โ‰ค (๐ด โˆ’ (๐ตโ†‘2))))
110107, 109mpbird 256 . . . . . 6 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ตโ†‘2) + ((2 ยท (๐ต ยท ((๐ด โˆ’ (๐ตโ†‘2)) / 3))) + (((๐ด โˆ’ (๐ตโ†‘2)) / 3)โ†‘2))) โ‰ค ๐ด)
11144, 110eqbrtrd 5166 . . . . 5 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))โ†‘2) โ‰ค ๐ด)
112 oveq1 7420 . . . . . . 7 (๐‘ฆ = (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ†’ (๐‘ฆโ†‘2) = ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))โ†‘2))
113112breq1d 5154 . . . . . 6 (๐‘ฆ = (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ†’ ((๐‘ฆโ†‘2) โ‰ค ๐ด โ†” ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))โ†‘2) โ‰ค ๐ด))
114 oveq1 7420 . . . . . . . . 9 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘ฅโ†‘2) = (๐‘ฆโ†‘2))
115114breq1d 5154 . . . . . . . 8 (๐‘ฅ = ๐‘ฆ โ†’ ((๐‘ฅโ†‘2) โ‰ค ๐ด โ†” (๐‘ฆโ†‘2) โ‰ค ๐ด))
116115cbvrabv 3430 . . . . . . 7 {๐‘ฅ โˆˆ โ„+ โˆฃ (๐‘ฅโ†‘2) โ‰ค ๐ด} = {๐‘ฆ โˆˆ โ„+ โˆฃ (๐‘ฆโ†‘2) โ‰ค ๐ด}
1171, 116eqtri 2753 . . . . . 6 ๐‘† = {๐‘ฆ โˆˆ โ„+ โˆฃ (๐‘ฆโ†‘2) โ‰ค ๐ด}
118113, 117elrab2 3679 . . . . 5 ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ ๐‘† โ†” ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ โ„+ โˆง ((๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))โ†‘2) โ‰ค ๐ด))
11924, 111, 118sylanbrc 581 . . . 4 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ ๐‘†)
120 suprub 12200 . . . . 5 (((๐‘† โІ โ„ โˆง ๐‘† โ‰  โˆ… โˆง โˆƒ๐‘ฆ โˆˆ โ„ โˆ€๐‘ง โˆˆ ๐‘† ๐‘ง โ‰ค ๐‘ฆ) โˆง (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ ๐‘†) โ†’ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค sup(๐‘†, โ„, < ))
121120, 2breqtrrdi 5186 . . . 4 (((๐‘† โІ โ„ โˆง ๐‘† โ‰  โˆ… โˆง โˆƒ๐‘ฆ โˆˆ โ„ โˆ€๐‘ง โˆˆ ๐‘† ๐‘ง โ‰ค ๐‘ฆ) โˆง (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ ๐‘†) โ†’ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค ๐ต)
1226, 119, 121syl2anc 582 . . 3 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค ๐ต)
12323rpgt0d 13046 . . . 4 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ 0 < ((๐ด โˆ’ (๐ตโ†‘2)) / 3))
12429, 14ltaddposd 11823 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (0 < ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ†” ๐ต < (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3))))
12514, 29readdcld 11268 . . . . . . 7 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โˆˆ โ„)
12614, 125ltnled 11386 . . . . . 6 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ต < (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ†” ยฌ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค ๐ต))
127124, 126bitrd 278 . . . . 5 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (0 < ((๐ด โˆ’ (๐ตโ†‘2)) / 3) โ†” ยฌ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค ๐ต))
128127biimpa 475 . . . 4 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง 0 < ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ†’ ยฌ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค ๐ต)
129123, 128syldan 589 . . 3 (((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โˆง (๐ตโ†‘2) < ๐ด) โ†’ ยฌ (๐ต + ((๐ด โˆ’ (๐ตโ†‘2)) / 3)) โ‰ค ๐ต)
130122, 129pm2.65da 815 . 2 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ ยฌ (๐ตโ†‘2) < ๐ด)
13115, 11eqleltd 11383 . 2 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ ((๐ตโ†‘2) = ๐ด โ†” ((๐ตโ†‘2) โ‰ค ๐ด โˆง ยฌ (๐ตโ†‘2) < ๐ด)))
1324, 130, 131mpbir2and 711 1 ((๐ด โˆˆ โ„+ โˆง ๐ด โ‰ค 1) โ†’ (๐ตโ†‘2) = ๐ด)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098  {cab 2702   โ‰  wne 2930  โˆ€wral 3051  โˆƒwrex 3060  {crab 3419   โІ wss 3941  โˆ…c0 4319   class class class wbr 5144  (class class class)co 7413  supcsup 9458  โ„‚cc 11131  โ„cr 11132  0cc0 11133  1c1 11134   + caddc 11136   ยท cmul 11138   < clt 11273   โ‰ค cle 11274   โˆ’ cmin 11469   / cdiv 11896  โ„•cn 12237  2c2 12292  3c3 12293  โ„+crp 13001  โ†‘cexp 14053
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 2696  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210  ax-pre-sup 11211
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 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8958  df-dom 8959  df-sdom 8960  df-sup 9460  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-div 11897  df-nn 12238  df-2 12300  df-3 12301  df-n0 12498  df-z 12584  df-uz 12848  df-rp 13002  df-seq 13994  df-exp 14054
This theorem is referenced by:  01sqrex  15223
  Copyright terms: Public domain W3C validator