Metamath Proof Explorer


Theorem int-sqdefd

Description: SquareDefinition generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

Ref Expression
Hypotheses int-sqdefd.1 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
int-sqdefd.2 โŠข ( ๐œ‘ โ†’ ๐ด = ๐ต )
Assertion int-sqdefd ( ๐œ‘ โ†’ ( ๐ด ยท ๐ต ) = ( ๐ด โ†‘ 2 ) )

Proof

Step Hyp Ref Expression
1 int-sqdefd.1 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„ )
2 int-sqdefd.2 โŠข ( ๐œ‘ โ†’ ๐ด = ๐ต )
3 2 oveq1d โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘ 2 ) = ( ๐ต โ†‘ 2 ) )
4 1 recnd โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
5 4 sqvald โŠข ( ๐œ‘ โ†’ ( ๐ต โ†‘ 2 ) = ( ๐ต ยท ๐ต ) )
6 eqcom โŠข ( ๐ด = ๐ต โ†” ๐ต = ๐ด )
7 6 imbi2i โŠข ( ( ๐œ‘ โ†’ ๐ด = ๐ต ) โ†” ( ๐œ‘ โ†’ ๐ต = ๐ด ) )
8 2 7 mpbi โŠข ( ๐œ‘ โ†’ ๐ต = ๐ด )
9 8 oveq1d โŠข ( ๐œ‘ โ†’ ( ๐ต ยท ๐ต ) = ( ๐ด ยท ๐ต ) )
10 5 9 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ต โ†‘ 2 ) = ( ๐ด ยท ๐ต ) )
11 3 10 eqtrd โŠข ( ๐œ‘ โ†’ ( ๐ด โ†‘ 2 ) = ( ๐ด ยท ๐ต ) )
12 11 eqcomd โŠข ( ๐œ‘ โ†’ ( ๐ด ยท ๐ต ) = ( ๐ด โ†‘ 2 ) )