Metamath Proof Explorer


Theorem zrtdvds

Description: A positive integer root divides its integer. (Contributed by Steven Nguyen, 6-Apr-2023)

Ref Expression
Assertion zrtdvds ANA1NA1NA

Proof

Step Hyp Ref Expression
1 nnz A1NA1N
2 1 3ad2ant3 ANA1NA1N
3 simp2 ANA1NN
4 iddvdsexp A1NNA1NA1NN
5 2 3 4 syl2anc ANA1NA1NA1NN
6 zcn AA
7 6 3ad2ant1 ANA1NA
8 cxproot ANA1NN=A
9 7 3 8 syl2anc ANA1NA1NN=A
10 5 9 breqtrd ANA1NA1NA