metamath/valid/mathd-algebra-151.mm

${
  $( (Contributed by Kunhao Zheng, 1-Jun-2021.) $)
  mathd-algebra-151 $p |- ( ph -> ( ( |^ ` ( sqrt ` ; 2 7 ) ) - ( |_ ` ( sqrt ` 
; 2 6 ) ) ) = 1 ) $=
( c2 c7 csqrt cfv c6 co c1 wceq c5 wcel cc0 cle wbr 2nn0 nn0ge0i mp2an mpbi cr 
clt cdc cceil cmin cneg 7nn0 deccl nn0rei sqrtcli ax-mp ceilval caddc c3 cfl 
3nn0 6nn nnnn0i c8 c10 7lt8 8lt10 7re 8re 10nn nnrei 2lt3 decltc ltleii lttri 
wb sqrtlei cexp cmul sqvali 6t6e36 eqtri fveq2i sqrtsq eqtr3i breqtri 6cn 
lenegi 5cn 5t5e25 5re 5nn 7nn declt sqrtlt mp4an eqbrtrri ltnegi ax-1cn 5lt7 
5p1e6 addcomli subaddrii eqcomi negeqi negsubdii renegcli nnzi znegcli cz wa 
flbi mpbir2an reflcl recni negcon1i decnncl 5lt6 pm3.2i breq2i nngt0i 6lt10 
df-6 sqrtpclii nn0zi oveq12 syl6eq a1i ) BCUAZDEZUBEZBFUAZDEZUMEZUCGZ 
HIZAYDFIZYGJIZYIYDYCUDZUMEZUDZFYCSKZYDYNILYBMNZYOYBBCOUEUFZPZYBYBYQUGZUHUIZ 
YCUJUIFUDZYMIYNFIYMUUAYMUUAIZUUAYLMNZYLUUAHUKGZTNZYCFMNUUCYCULFUAZDEZFMYBUU 
FMNZYCUUGMNZYBUUFYSUUFULFUNFUOUPZUFZUGZBULCFOUNUEUUJCUQTNUQURTNCURTNUSUTCUQ 
URVAVBURVCVDVHQVEVFVGYPLUUFMNZUUHUUIVIYRUUFUUKPZYBUUFYSUULVJQRFBVKGZDEZUUGF 
UUOUUFDUUOFFVLGUUFFVTVMVNVOVPFSKLFMNUUPFIFUOVDZFUUJPFVQQVRZVSYCFYTUUQWARYLJ 
UDZUUDTJYCTNYLUUSTNBJUAZDEZJYCTJBVKGZDEZUVAJUVBUUTDUVBJJVLGUUTJWBVMWCVOVPJS 
KLJMNUVCJIWDJJWEUPZPJVQQVRZUUTYBTNZUVAYCTNZBJCOUVDWFWMWGUUTSKLUUTMNZYBSKYPU 
VFUVGVIUUTBJOUVDUFZUGZUUTUVIPZYSYRUUTYBWHWIRWJJYCWDYTWKRUUSFHUCGZUDUUDJUVLU 
VLJFHJVTWLWBJHFWBWLWNWOWPWQWRFHVTWLWSVOVSYLSKZUUAXCKUUBUUCUUEXDVIYCYTWTZFFU 
OXAXBYLUUAXEQXFWQFYMVTYMUVMYMSKUVNYLXGUIXHXIRVOYKJYFMNZYFJHUKGZTNZUVAJYFMUV 
EUUTYEMNZUVAYFMNZUUTYEUVJYEBFOUOXJZVDZBJFOUVDUOXKWGVGUVHLYEMNZUVRUVSVIUVKYE 
BFOUUJUFPZUUTYEUVJUWAVJQRWJYFFTNUVQYFUUGFTYEUUFTNZYFUUGTNZBULFFOUNUUJUUJXOV 
EVFYESKZUWBXDUUFSKZUUMXDUWDUWEVIUWFUWBUWAUWCXLUWGUUMUULUUNXLYEUUFWHQRUURVSF 
UVPYFTXPXMRYFSKJXCKYKUVOUVQXDVIYEUWAYEUVTXNXQJUVDXRYFJXEQXFYJYKXDYHFJUCGHYD 
FYGJUCXSFJHVTWBWLWNWPXTQYA $.
$}