Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pellexlem2 Structured version   Visualization version   GIF version

Theorem pellexlem2 41244
Description: Lemma for pellex 41249. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.)
Assertion
Ref Expression
pellexlem2 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) < (1 + (2 ยท (โˆšโ€˜๐ท))))

Proof of Theorem pellexlem2
StepHypRef Expression
1 simpl3 1193 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ต โˆˆ โ„•)
21nnred 12192 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ต โˆˆ โ„)
32resqcld 14055 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘2) โˆˆ โ„)
42sqge0d 14067 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 โ‰ค (๐ตโ†‘2))
53, 4absidd 15334 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(๐ตโ†‘2)) = (๐ตโ†‘2))
65eqcomd 2737 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘2) = (absโ€˜(๐ตโ†‘2)))
76oveq2d 7393 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) / (๐ตโ†‘2)) = ((absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) / (absโ€˜(๐ตโ†‘2))))
8 simpl2 1192 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ด โˆˆ โ„•)
98nncnd 12193 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ด โˆˆ โ„‚)
109sqcld 14074 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ดโ†‘2) โˆˆ โ„‚)
11 simpl1 1191 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ท โˆˆ โ„•)
1211nncnd 12193 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ท โˆˆ โ„‚)
131nncnd 12193 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ต โˆˆ โ„‚)
1413sqcld 14074 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
1512, 14mulcld 11199 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ท ยท (๐ตโ†‘2)) โˆˆ โ„‚)
1610, 15subcld 11536 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) โˆˆ โ„‚)
171nnne0d 12227 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ต โ‰  0)
18 sqne0 14053 . . . . . . . 8 (๐ต โˆˆ โ„‚ โ†’ ((๐ตโ†‘2) โ‰  0 โ†” ๐ต โ‰  0))
1918biimpar 478 . . . . . . 7 ((๐ต โˆˆ โ„‚ โˆง ๐ต โ‰  0) โ†’ (๐ตโ†‘2) โ‰  0)
2013, 17, 19syl2anc 584 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘2) โ‰  0)
2116, 14, 20absdivd 15367 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / (๐ตโ†‘2))) = ((absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) / (absโ€˜(๐ตโ†‘2))))
227, 21eqtr4d 2774 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) / (๐ตโ†‘2)) = (absโ€˜(((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / (๐ตโ†‘2))))
2322oveq2d 7393 . . 3 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) / (๐ตโ†‘2))) = ((๐ตโ†‘2) ยท (absโ€˜(((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / (๐ตโ†‘2)))))
2416abscld 15348 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) โˆˆ โ„)
2524recnd 11207 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) โˆˆ โ„‚)
2625, 14, 20divcan2d 11957 . . 3 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) / (๐ตโ†‘2))) = (absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))))
2710, 15, 14, 20divsubdird 11994 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / (๐ตโ†‘2)) = (((๐ดโ†‘2) / (๐ตโ†‘2)) โˆ’ ((๐ท ยท (๐ตโ†‘2)) / (๐ตโ†‘2))))
289, 13, 17sqdivd 14089 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ด / ๐ต)โ†‘2) = ((๐ดโ†‘2) / (๐ตโ†‘2)))
2928eqcomd 2737 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ดโ†‘2) / (๐ตโ†‘2)) = ((๐ด / ๐ต)โ†‘2))
3011nnred 12192 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ท โˆˆ โ„)
3111nnnn0d 12497 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ท โˆˆ โ„•0)
3231nn0ge0d 12500 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 โ‰ค ๐ท)
33 remsqsqrt 15168 . . . . . . . . 9 ((๐ท โˆˆ โ„ โˆง 0 โ‰ค ๐ท) โ†’ ((โˆšโ€˜๐ท) ยท (โˆšโ€˜๐ท)) = ๐ท)
3430, 32, 33syl2anc 584 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((โˆšโ€˜๐ท) ยท (โˆšโ€˜๐ท)) = ๐ท)
3530, 32resqrtcld 15329 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (โˆšโ€˜๐ท) โˆˆ โ„)
3635recnd 11207 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (โˆšโ€˜๐ท) โˆˆ โ„‚)
3736sqvald 14073 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((โˆšโ€˜๐ท)โ†‘2) = ((โˆšโ€˜๐ท) ยท (โˆšโ€˜๐ท)))
3812, 14, 20divcan4d 11961 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ท ยท (๐ตโ†‘2)) / (๐ตโ†‘2)) = ๐ท)
3934, 37, 383eqtr4rd 2782 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ท ยท (๐ตโ†‘2)) / (๐ตโ†‘2)) = ((โˆšโ€˜๐ท)โ†‘2))
4029, 39oveq12d 7395 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ดโ†‘2) / (๐ตโ†‘2)) โˆ’ ((๐ท ยท (๐ตโ†‘2)) / (๐ตโ†‘2))) = (((๐ด / ๐ต)โ†‘2) โˆ’ ((โˆšโ€˜๐ท)โ†‘2)))
419, 13, 17divcld 11955 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ด / ๐ต) โˆˆ โ„‚)
42 subsq 14139 . . . . . . . 8 (((๐ด / ๐ต) โˆˆ โ„‚ โˆง (โˆšโ€˜๐ท) โˆˆ โ„‚) โ†’ (((๐ด / ๐ต)โ†‘2) โˆ’ ((โˆšโ€˜๐ท)โ†‘2)) = (((๐ด / ๐ต) + (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))))
4341, 36, 42syl2anc 584 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ด / ๐ต)โ†‘2) โˆ’ ((โˆšโ€˜๐ท)โ†‘2)) = (((๐ด / ๐ต) + (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))))
4441, 36addcld 11198 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ด / ๐ต) + (โˆšโ€˜๐ท)) โˆˆ โ„‚)
458nnred 12192 . . . . . . . . . . 11 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ๐ด โˆˆ โ„)
4645, 1nndivred 12231 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ด / ๐ต) โˆˆ โ„)
4746, 35resubcld 11607 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) โˆˆ โ„)
4847recnd 11207 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) โˆˆ โ„‚)
4944, 48mulcomd 11200 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ด / ๐ต) + (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) = (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท))))
5043, 49eqtrd 2771 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ด / ๐ต)โ†‘2) โˆ’ ((โˆšโ€˜๐ท)โ†‘2)) = (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท))))
5127, 40, 503eqtrd 2775 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / (๐ตโ†‘2)) = (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท))))
5251fveq2d 6866 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / (๐ตโ†‘2))) = (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))
5352oveq2d 7393 . . 3 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท (absโ€˜(((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / (๐ตโ†‘2)))) = ((๐ตโ†‘2) ยท (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท))))))
5423, 26, 533eqtr3d 2779 . 2 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) = ((๐ตโ†‘2) ยท (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท))))))
5548, 44absmuld 15366 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) = ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))
5655oveq2d 7393 . . 3 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) = ((๐ตโ†‘2) ยท ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))))
5748abscld 15348 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) โˆˆ โ„)
5844abscld 15348 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))) โˆˆ โ„)
5957, 58remulcld 11209 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) โˆˆ โ„)
603, 59remulcld 11209 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) โˆˆ โ„)
61 2nn0 12454 . . . . . . . . 9 2 โˆˆ โ„•0
6261nn0negzi 12566 . . . . . . . 8 -2 โˆˆ โ„ค
6362a1i 11 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ -2 โˆˆ โ„ค)
642, 17, 63reexpclzd 14177 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘-2) โˆˆ โ„)
6564, 58remulcld 11209 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) โˆˆ โ„)
663, 65remulcld 11209 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) โˆˆ โ„)
67 1red 11180 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 1 โˆˆ โ„)
68 2re 12251 . . . . . . 7 2 โˆˆ โ„
6968a1i 11 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 2 โˆˆ โ„)
7069, 35remulcld 11209 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (2 ยท (โˆšโ€˜๐ท)) โˆˆ โ„)
7167, 70readdcld 11208 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (1 + (2 ยท (โˆšโ€˜๐ท))) โˆˆ โ„)
72 simpr 485 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2))
738nngt0d 12226 . . . . . . . . . . 11 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < ๐ด)
741nngt0d 12226 . . . . . . . . . . 11 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < ๐ต)
7545, 2, 73, 74divgt0d 12114 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < (๐ด / ๐ต))
7611nngt0d 12226 . . . . . . . . . . 11 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < ๐ท)
77 sqrtgt0 15170 . . . . . . . . . . 11 ((๐ท โˆˆ โ„ โˆง 0 < ๐ท) โ†’ 0 < (โˆšโ€˜๐ท))
7830, 76, 77syl2anc 584 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < (โˆšโ€˜๐ท))
7946, 35, 75, 78addgt0d 11754 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < ((๐ด / ๐ต) + (โˆšโ€˜๐ท)))
8079gt0ne0d 11743 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ด / ๐ต) + (โˆšโ€˜๐ท)) โ‰  0)
81 absgt0 15236 . . . . . . . . 9 (((๐ด / ๐ต) + (โˆšโ€˜๐ท)) โˆˆ โ„‚ โ†’ (((๐ด / ๐ต) + (โˆšโ€˜๐ท)) โ‰  0 โ†” 0 < (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))
8281biimpa 477 . . . . . . . 8 ((((๐ด / ๐ต) + (โˆšโ€˜๐ท)) โˆˆ โ„‚ โˆง ((๐ด / ๐ต) + (โˆšโ€˜๐ท)) โ‰  0) โ†’ 0 < (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))
8344, 80, 82syl2anc 584 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))
84 ltmul1 12029 . . . . . . 7 (((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) โˆˆ โ„ โˆง (๐ตโ†‘-2) โˆˆ โ„ โˆง ((absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))) โˆˆ โ„ โˆง 0 < (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2) โ†” ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) < ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))))
8557, 64, 58, 83, 84syl112anc 1374 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2) โ†” ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) < ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))))
8672, 85mpbid 231 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) < ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))
872, 17sqgt0d 14178 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < (๐ตโ†‘2))
88 ltmul2 12030 . . . . . 6 ((((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) โˆˆ โ„ โˆง ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) โˆˆ โ„ โˆง ((๐ตโ†‘2) โˆˆ โ„ โˆง 0 < (๐ตโ†‘2))) โ†’ (((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) < ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) โ†” ((๐ตโ†‘2) ยท ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) < ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))))
8959, 65, 3, 87, 88syl112anc 1374 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) < ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) โ†” ((๐ตโ†‘2) ยท ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) < ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))))
9086, 89mpbid 231 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) < ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))))
9113, 17, 63expclzd 14081 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘-2) โˆˆ โ„‚)
9258recnd 11207 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))) โˆˆ โ„‚)
93 mulass 11163 . . . . . . . 8 (((๐ตโ†‘2) โˆˆ โ„‚ โˆง (๐ตโ†‘-2) โˆˆ โ„‚ โˆง (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))) โˆˆ โ„‚) โ†’ (((๐ตโ†‘2) ยท (๐ตโ†‘-2)) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) = ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))))
9493eqcomd 2737 . . . . . . 7 (((๐ตโ†‘2) โˆˆ โ„‚ โˆง (๐ตโ†‘-2) โˆˆ โ„‚ โˆง (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))) โˆˆ โ„‚) โ†’ ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) = (((๐ตโ†‘2) ยท (๐ตโ†‘-2)) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))
9514, 91, 92, 94syl3anc 1371 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) = (((๐ตโ†‘2) ยท (๐ตโ†‘-2)) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))
96 expneg 14000 . . . . . . . . . 10 ((๐ต โˆˆ โ„‚ โˆง 2 โˆˆ โ„•0) โ†’ (๐ตโ†‘-2) = (1 / (๐ตโ†‘2)))
9713, 61, 96sylancl 586 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘-2) = (1 / (๐ตโ†‘2)))
9897oveq2d 7393 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท (๐ตโ†‘-2)) = ((๐ตโ†‘2) ยท (1 / (๐ตโ†‘2))))
9914, 20recidd 11950 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท (1 / (๐ตโ†‘2))) = 1)
10098, 99eqtrd 2771 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท (๐ตโ†‘-2)) = 1)
101100oveq1d 7392 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ตโ†‘2) ยท (๐ตโ†‘-2)) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) = (1 ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))))
10292mullidd 11197 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (1 ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท)))) = (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))
10395, 101, 1023eqtrd 2775 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) = (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))
10441, 36addcomd 11381 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ด / ๐ต) + (โˆšโ€˜๐ท)) = ((โˆšโ€˜๐ท) + (๐ด / ๐ต)))
105 ppncan 11467 . . . . . . . . . 10 (((โˆšโ€˜๐ท) โˆˆ โ„‚ โˆง (โˆšโ€˜๐ท) โˆˆ โ„‚ โˆง (๐ด / ๐ต) โˆˆ โ„‚) โ†’ (((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) + ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) = ((โˆšโ€˜๐ท) + (๐ด / ๐ต)))
106105eqcomd 2737 . . . . . . . . 9 (((โˆšโ€˜๐ท) โˆˆ โ„‚ โˆง (โˆšโ€˜๐ท) โˆˆ โ„‚ โˆง (๐ด / ๐ต) โˆˆ โ„‚) โ†’ ((โˆšโ€˜๐ท) + (๐ด / ๐ต)) = (((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) + ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))))
10736, 36, 41, 106syl3anc 1371 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((โˆšโ€˜๐ท) + (๐ด / ๐ต)) = (((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) + ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))))
10836, 36addcld 11198 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) โˆˆ โ„‚)
109108, 48addcomd 11381 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) + ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) = (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + ((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท))))
110 2times 12313 . . . . . . . . . . . 12 ((โˆšโ€˜๐ท) โˆˆ โ„‚ โ†’ (2 ยท (โˆšโ€˜๐ท)) = ((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)))
111110eqcomd 2737 . . . . . . . . . . 11 ((โˆšโ€˜๐ท) โˆˆ โ„‚ โ†’ ((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) = (2 ยท (โˆšโ€˜๐ท)))
11236, 111syl 17 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) = (2 ยท (โˆšโ€˜๐ท)))
113112oveq2d 7393 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + ((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท))) = (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท))))
114109, 113eqtrd 2771 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((โˆšโ€˜๐ท) + (โˆšโ€˜๐ท)) + ((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) = (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท))))
115104, 107, 1143eqtrd 2775 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ด / ๐ต) + (โˆšโ€˜๐ท)) = (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท))))
116115fveq2d 6866 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))) = (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท)))))
11747, 70readdcld 11208 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท))) โˆˆ โ„)
118117recnd 11207 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท))) โˆˆ โ„‚)
119118abscld 15348 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท)))) โˆˆ โ„)
12070recnd 11207 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (2 ยท (โˆšโ€˜๐ท)) โˆˆ โ„‚)
121120abscld 15348 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(2 ยท (โˆšโ€˜๐ท))) โˆˆ โ„)
12257, 121readdcld 11208 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) + (absโ€˜(2 ยท (โˆšโ€˜๐ท)))) โˆˆ โ„)
12348, 120abstrid 15368 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท)))) โ‰ค ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) + (absโ€˜(2 ยท (โˆšโ€˜๐ท)))))
124 0le2 12279 . . . . . . . . . . . 12 0 โ‰ค 2
125124a1i 11 . . . . . . . . . . 11 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 โ‰ค 2)
12630, 32sqrtge0d 15332 . . . . . . . . . . 11 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 โ‰ค (โˆšโ€˜๐ท))
12769, 35, 125, 126mulge0d 11756 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 โ‰ค (2 ยท (โˆšโ€˜๐ท)))
12870, 127absidd 15334 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(2 ยท (โˆšโ€˜๐ท))) = (2 ยท (โˆšโ€˜๐ท)))
129128oveq2d 7393 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) + (absโ€˜(2 ยท (โˆšโ€˜๐ท)))) = ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) + (2 ยท (โˆšโ€˜๐ท))))
1301nnsqcld 14172 . . . . . . . . . . . . . . 15 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘2) โˆˆ โ„•)
131130nnge1d 12225 . . . . . . . . . . . . . 14 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 1 โ‰ค (๐ตโ†‘2))
132 0lt1 11701 . . . . . . . . . . . . . . . 16 0 < 1
133132a1i 11 . . . . . . . . . . . . . . 15 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ 0 < 1)
134 lerec 12062 . . . . . . . . . . . . . . 15 (((1 โˆˆ โ„ โˆง 0 < 1) โˆง ((๐ตโ†‘2) โˆˆ โ„ โˆง 0 < (๐ตโ†‘2))) โ†’ (1 โ‰ค (๐ตโ†‘2) โ†” (1 / (๐ตโ†‘2)) โ‰ค (1 / 1)))
13567, 133, 3, 87, 134syl22anc 837 . . . . . . . . . . . . . 14 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (1 โ‰ค (๐ตโ†‘2) โ†” (1 / (๐ตโ†‘2)) โ‰ค (1 / 1)))
136131, 135mpbid 231 . . . . . . . . . . . . 13 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (1 / (๐ตโ†‘2)) โ‰ค (1 / 1))
137 1div1e1 11869 . . . . . . . . . . . . 13 (1 / 1) = 1
138136, 137breqtrdi 5166 . . . . . . . . . . . 12 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (1 / (๐ตโ†‘2)) โ‰ค 1)
13997, 138eqbrtrd 5147 . . . . . . . . . . 11 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (๐ตโ†‘-2) โ‰ค 1)
14057, 64, 67, 72, 139ltletrd 11339 . . . . . . . . . 10 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < 1)
14157, 67, 140ltled 11327 . . . . . . . . 9 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) โ‰ค 1)
14257, 67, 70, 141leadd1dd 11793 . . . . . . . 8 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) + (2 ยท (โˆšโ€˜๐ท))) โ‰ค (1 + (2 ยท (โˆšโ€˜๐ท))))
143129, 142eqbrtrd 5147 . . . . . . 7 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) + (absโ€˜(2 ยท (โˆšโ€˜๐ท)))) โ‰ค (1 + (2 ยท (โˆšโ€˜๐ท))))
144119, 122, 71, 123, 143letrd 11336 . . . . . 6 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) + (2 ยท (โˆšโ€˜๐ท)))) โ‰ค (1 + (2 ยท (โˆšโ€˜๐ท))))
145116, 144eqbrtrd 5147 . . . . 5 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))) โ‰ค (1 + (2 ยท (โˆšโ€˜๐ท))))
146103, 145eqbrtrd 5147 . . . 4 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((๐ตโ†‘-2) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) โ‰ค (1 + (2 ยท (โˆšโ€˜๐ท))))
14760, 66, 71, 90, 146ltletrd 11339 . . 3 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท ((absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) ยท (absโ€˜((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) < (1 + (2 ยท (โˆšโ€˜๐ท))))
14856, 147eqbrtrd 5147 . 2 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ ((๐ตโ†‘2) ยท (absโ€˜(((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท)) ยท ((๐ด / ๐ต) + (โˆšโ€˜๐ท))))) < (1 + (2 ยท (โˆšโ€˜๐ท))))
14954, 148eqbrtrd 5147 1 (((๐ท โˆˆ โ„• โˆง ๐ด โˆˆ โ„• โˆง ๐ต โˆˆ โ„•) โˆง (absโ€˜((๐ด / ๐ต) โˆ’ (โˆšโ€˜๐ท))) < (๐ตโ†‘-2)) โ†’ (absโ€˜((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) < (1 + (2 ยท (โˆšโ€˜๐ท))))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106   โ‰  wne 2939   class class class wbr 5125  โ€˜cfv 6516  (class class class)co 7377  โ„‚cc 11073  โ„cr 11074  0cc0 11075  1c1 11076   + caddc 11078   ยท cmul 11080   < clt 11213   โ‰ค cle 11214   โˆ’ cmin 11409  -cneg 11410   / cdiv 11836  โ„•cn 12177  2c2 12232  โ„•0cn0 12437  โ„คcz 12523  โ†‘cexp 13992  โˆšcsqrt 15145  abscabs 15146
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3364  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-pss 3947  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-iun 4976  df-br 5126  df-opab 5188  df-mpt 5209  df-tr 5243  df-id 5551  df-eprel 5557  df-po 5565  df-so 5566  df-fr 5608  df-we 5610  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-pred 6273  df-ord 6340  df-on 6341  df-lim 6342  df-suc 6343  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-om 7823  df-2nd 7942  df-frecs 8232  df-wrecs 8263  df-recs 8337  df-rdg 8376  df-er 8670  df-en 8906  df-dom 8907  df-sdom 8908  df-sup 9402  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11411  df-neg 11412  df-div 11837  df-nn 12178  df-2 12240  df-3 12241  df-n0 12438  df-z 12524  df-uz 12788  df-rp 12940  df-seq 13932  df-exp 13993  df-cj 15011  df-re 15012  df-im 15013  df-sqrt 15147  df-abs 15148
This theorem is referenced by:  pellexlem3  41245
  Copyright terms: Public domain W3C validator