metamath/valid/amc12a-2020-p13.mm

$(
  @{
    amc12a-2020-p13.0 @e |- ( ph -> A e. NN0 ) $@
    amc12a-2020-p13.1 @e |- ( ph -> B e. NN0 ) $@
    amc12a-2020-p13.2 @e |- ( ph -> C e. NN0 ) $@
    amc12a-2020-p13.3 @e |- ( ph -> N e. RR+ ) $@
    amc12a-2020-p13.4 @e |- ( ph -> N =/= 1 ) $@
    amc12a-2020-p13.5 @e |- ( ph -> 1 < A ) $@
    amc12a-2020-p13.6 @e |- ( ph -> 1 < B ) $@
    amc12a-2020-p13.7 @e |- ( ph -> 1 < C ) $@
    amc12a-2020-p13.8 @e |- ( ph -> ( ( N x. ( ( N x. ( N ^c ( 1 / C ) ) ) ^c ( 1 / B ) ) ) ^c ( 1 / A ) ) = ( ( N ^c ; 2 5 ) ^c ( 1 / ; 3 6 ) ) ) $@
    @( (Contributed by Kunhao Zheng, 3-Jun-2021.) @)
    amc12a-2020-p13 @p |- ( ph -> B = 3 ) @=
      ? @.
  @}
$)