MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax5seglem7 Structured version   Visualization version   GIF version

Theorem ax5seglem7 28790
Description: Lemma for ax5seg 28793. An algebraic calculation needed further down the line. (Contributed by Scott Fenton, 12-Jun-2013.)
Hypotheses
Ref Expression
ax5seglem7.1 ๐ด โˆˆ โ„‚
ax5seglem7.2 ๐‘‡ โˆˆ โ„‚
ax5seglem7.3 ๐ถ โˆˆ โ„‚
ax5seglem7.4 ๐ท โˆˆ โ„‚
Assertion
Ref Expression
ax5seglem7 (๐‘‡ ยท ((๐ถ โˆ’ ๐ท)โ†‘2)) = ((((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2))))

Proof of Theorem ax5seglem7
StepHypRef Expression
1 ax5seglem7.3 . . . . 5 ๐ถ โˆˆ โ„‚
2 ax5seglem7.4 . . . . 5 ๐ท โˆˆ โ„‚
31, 2binom2subi 14216 . . . 4 ((๐ถ โˆ’ ๐ท)โ†‘2) = (((๐ถโ†‘2) โˆ’ (2 ยท (๐ถ ยท ๐ท))) + (๐ทโ†‘2))
43oveq2i 7427 . . 3 (๐‘‡ ยท ((๐ถ โˆ’ ๐ท)โ†‘2)) = (๐‘‡ ยท (((๐ถโ†‘2) โˆ’ (2 ยท (๐ถ ยท ๐ท))) + (๐ทโ†‘2)))
5 ax5seglem7.2 . . . 4 ๐‘‡ โˆˆ โ„‚
61sqcli 14176 . . . . 5 (๐ถโ†‘2) โˆˆ โ„‚
7 2cn 12317 . . . . . 6 2 โˆˆ โ„‚
81, 2mulcli 11251 . . . . . 6 (๐ถ ยท ๐ท) โˆˆ โ„‚
97, 8mulcli 11251 . . . . 5 (2 ยท (๐ถ ยท ๐ท)) โˆˆ โ„‚
106, 9subcli 11566 . . . 4 ((๐ถโ†‘2) โˆ’ (2 ยท (๐ถ ยท ๐ท))) โˆˆ โ„‚
112sqcli 14176 . . . 4 (๐ทโ†‘2) โˆˆ โ„‚
125, 10, 11adddii 11256 . . 3 (๐‘‡ ยท (((๐ถโ†‘2) โˆ’ (2 ยท (๐ถ ยท ๐ท))) + (๐ทโ†‘2))) = ((๐‘‡ ยท ((๐ถโ†‘2) โˆ’ (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))
135, 6, 9subdii 11693 . . . 4 (๐‘‡ ยท ((๐ถโ†‘2) โˆ’ (2 ยท (๐ถ ยท ๐ท)))) = ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท))))
1413oveq1i 7426 . . 3 ((๐‘‡ ยท ((๐ถโ†‘2) โˆ’ (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2))) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))
154, 12, 143eqtri 2757 . 2 (๐‘‡ ยท ((๐ถ โˆ’ ๐ท)โ†‘2)) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))
16 ax-1cn 11196 . . . . . . . . . . 11 1 โˆˆ โ„‚
1716, 5subcli 11566 . . . . . . . . . 10 (1 โˆ’ ๐‘‡) โˆˆ โ„‚
18 ax5seglem7.1 . . . . . . . . . 10 ๐ด โˆˆ โ„‚
1917, 18mulcli 11251 . . . . . . . . 9 ((1 โˆ’ ๐‘‡) ยท ๐ด) โˆˆ โ„‚
2019sqcli 14176 . . . . . . . 8 (((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) โˆˆ โ„‚
215, 1mulcli 11251 . . . . . . . . . . 11 (๐‘‡ ยท ๐ถ) โˆˆ โ„‚
2221, 2subcli 11566 . . . . . . . . . 10 ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท) โˆˆ โ„‚
2319, 22mulcli 11251 . . . . . . . . 9 (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)) โˆˆ โ„‚
247, 23mulcli 11251 . . . . . . . 8 (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))) โˆˆ โ„‚
2520, 24addcli 11250 . . . . . . 7 ((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) โˆˆ โ„‚
2621sqcli 14176 . . . . . . . 8 ((๐‘‡ ยท ๐ถ)โ†‘2) โˆˆ โ„‚
2726, 11addcli 11250 . . . . . . 7 (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2)) โˆˆ โ„‚
2825, 27addcli 11250 . . . . . 6 (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆˆ โ„‚
2921, 2mulcli 11251 . . . . . . 7 ((๐‘‡ ยท ๐ถ) ยท ๐ท) โˆˆ โ„‚
307, 29mulcli 11251 . . . . . 6 (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)) โˆˆ โ„‚
315, 6mulcli 11251 . . . . . . 7 (๐‘‡ ยท (๐ถโ†‘2)) โˆˆ โ„‚
325, 11mulcli 11251 . . . . . . 7 (๐‘‡ ยท (๐ทโ†‘2)) โˆˆ โ„‚
3331, 32addcli 11250 . . . . . 6 ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆˆ โ„‚
34 subadd23 11502 . . . . . 6 (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆˆ โ„‚ โˆง (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)) โˆˆ โ„‚ โˆง ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆˆ โ„‚) โ†’ (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2)))) = ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)))))
3528, 30, 33, 34mp3an 1457 . . . . 5 (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2)))) = ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))))
3635oveq1i 7426 . . . 4 ((((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2)))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) = (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
3719, 22binom2i 14207 . . . . . . 7 ((((1 โˆ’ ๐‘‡) ยท ๐ด) + ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))โ†‘2) = (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)โ†‘2))
3819, 21, 2addsubassi 11581 . . . . . . . 8 ((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท) = (((1 โˆ’ ๐‘‡) ยท ๐ด) + ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))
3938oveq1i 7426 . . . . . . 7 (((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) = ((((1 โˆ’ ๐‘‡) ยท ๐ด) + ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))โ†‘2)
4025, 27, 30addsubassi 11581 . . . . . . . 8 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) = (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2)) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))))
4121, 2binom2subi 14216 . . . . . . . . . 10 (((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)โ†‘2) = ((((๐‘‡ ยท ๐ถ)โ†‘2) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + (๐ทโ†‘2))
4226, 11, 30addsubi 11582 . . . . . . . . . 10 ((((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2)) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) = ((((๐‘‡ ยท ๐ถ)โ†‘2) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + (๐ทโ†‘2))
4341, 42eqtr4i 2756 . . . . . . . . 9 (((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)โ†‘2) = ((((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2)) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)))
4443oveq2i 7427 . . . . . . . 8 (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)โ†‘2)) = (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2)) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))))
4540, 44eqtr4i 2756 . . . . . . 7 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) = (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)โ†‘2))
4637, 39, 453eqtr4i 2763 . . . . . 6 (((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) = ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)))
4718, 1binom2subi 14216 . . . . . . . . . . . 12 ((๐ด โˆ’ ๐ถ)โ†‘2) = (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))) + (๐ถโ†‘2))
4847oveq2i 7427 . . . . . . . . . . 11 (๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) = (๐‘‡ ยท (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))) + (๐ถโ†‘2)))
4918sqcli 14176 . . . . . . . . . . . . 13 (๐ดโ†‘2) โˆˆ โ„‚
5018, 1mulcli 11251 . . . . . . . . . . . . . 14 (๐ด ยท ๐ถ) โˆˆ โ„‚
517, 50mulcli 11251 . . . . . . . . . . . . 13 (2 ยท (๐ด ยท ๐ถ)) โˆˆ โ„‚
5249, 51subcli 11566 . . . . . . . . . . . 12 ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))) โˆˆ โ„‚
535, 52, 6adddii 11256 . . . . . . . . . . 11 (๐‘‡ ยท (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))) + (๐ถโ†‘2))) = ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) + (๐‘‡ ยท (๐ถโ†‘2)))
5448, 53eqtri 2753 . . . . . . . . . 10 (๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) = ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) + (๐‘‡ ยท (๐ถโ†‘2)))
5518, 2binom2subi 14216 . . . . . . . . . 10 ((๐ด โˆ’ ๐ท)โ†‘2) = (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) + (๐ทโ†‘2))
5654, 55oveq12i 7428 . . . . . . . . 9 ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2)) = (((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) + (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) + (๐ทโ†‘2)))
575, 52mulcli 11251 . . . . . . . . . 10 (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆˆ โ„‚
5818, 2mulcli 11251 . . . . . . . . . . . 12 (๐ด ยท ๐ท) โˆˆ โ„‚
597, 58mulcli 11251 . . . . . . . . . . 11 (2 ยท (๐ด ยท ๐ท)) โˆˆ โ„‚
6049, 59subcli 11566 . . . . . . . . . 10 ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆˆ โ„‚
6157, 31, 60, 11addsub4i 11586 . . . . . . . . 9 (((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) + (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) + (๐ทโ†‘2))) = (((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))) + ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)))
6256, 61eqtri 2753 . . . . . . . 8 ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2)) = (((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))) + ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)))
6362oveq2i 7427 . . . . . . 7 ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2))) = ((1 โˆ’ ๐‘‡) ยท (((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))) + ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))))
6457, 60subcli 11566 . . . . . . . 8 ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))) โˆˆ โ„‚
6531, 11subcli 11566 . . . . . . . 8 ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) โˆˆ โ„‚
6617, 64, 65adddii 11256 . . . . . . 7 ((1 โˆ’ ๐‘‡) ยท (((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))) + ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)))) = (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))))
6716, 5, 65subdiri 11694 . . . . . . . . . 10 ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))) = ((1 ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))) โˆ’ (๐‘‡ ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))))
6865mullidi 11249 . . . . . . . . . . 11 (1 ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))) = ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))
695, 31, 11subdii 11693 . . . . . . . . . . 11 (๐‘‡ ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))) = ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ (๐‘‡ ยท (๐ทโ†‘2)))
7068, 69oveq12i 7428 . . . . . . . . . 10 ((1 ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))) โˆ’ (๐‘‡ ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)))) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) โˆ’ ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ (๐‘‡ ยท (๐ทโ†‘2))))
715, 31mulcli 11251 . . . . . . . . . . . 12 (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆˆ โ„‚
72 subsub3 11522 . . . . . . . . . . . 12 ((((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) โˆˆ โ„‚ โˆง (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆˆ โ„‚ โˆง (๐‘‡ ยท (๐ทโ†‘2)) โˆˆ โ„‚) โ†’ (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) โˆ’ ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ (๐‘‡ ยท (๐ทโ†‘2)))) = ((((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))
7365, 71, 32, 72mp3an 1457 . . . . . . . . . . 11 (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) โˆ’ ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ (๐‘‡ ยท (๐ทโ†‘2)))) = ((((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))
7431, 32, 11addsubi 11582 . . . . . . . . . . . 12 (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐ทโ†‘2)) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2)))
7574oveq1i 7426 . . . . . . . . . . 11 ((((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐ทโ†‘2)) โˆ’ (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) = ((((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))
76 subsub4 11523 . . . . . . . . . . . 12 ((((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆˆ โ„‚ โˆง (๐ทโ†‘2) โˆˆ โ„‚ โˆง (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆˆ โ„‚) โ†’ ((((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐ทโ†‘2)) โˆ’ (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
7733, 11, 71, 76mp3an 1457 . . . . . . . . . . 11 ((((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐ทโ†‘2)) โˆ’ (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))
7873, 75, 773eqtr2i 2759 . . . . . . . . . 10 (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)) โˆ’ ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ (๐‘‡ ยท (๐ทโ†‘2)))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))
7967, 70, 783eqtri 2757 . . . . . . . . 9 ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))
8079oveq2i 7427 . . . . . . . 8 (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)))) = (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
8117, 64mulcli 11251 . . . . . . . . 9 ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆˆ โ„‚
8211, 71addcli 11250 . . . . . . . . 9 ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆˆ โ„‚
83 addsub12 11503 . . . . . . . . 9 ((((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆˆ โ„‚ โˆง ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆˆ โ„‚ โˆง ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆˆ โ„‚) โ†’ (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))))
8481, 33, 82, 83mp3an 1457 . . . . . . . 8 (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
8580, 84eqtri 2753 . . . . . . 7 (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐ทโ†‘2)))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
8663, 66, 853eqtri 2757 . . . . . 6 ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
8746, 86oveq12i 7428 . . . . 5 ((((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2)))) = (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))))
8828, 30subcli 11566 . . . . . 6 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) โˆˆ โ„‚
8981, 82subcli 11566 . . . . . 6 (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))) โˆˆ โ„‚
9088, 33, 89addassi 11254 . . . . 5 ((((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2)))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) = (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))))
9187, 90eqtr4i 2756 . . . 4 ((((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2)))) = ((((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) + ((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2)))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
9233, 30subcli 11566 . . . . 5 (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) โˆˆ โ„‚
9328, 89, 92add32i 11467 . . . 4 (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)))) = (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
9436, 91, 933eqtr4i 2763 . . 3 ((((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2)))) = (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))))
95 subsub2 11518 . . . . . 6 (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆˆ โ„‚ โˆง ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆˆ โ„‚ โˆง ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆˆ โ„‚) โ†’ ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))) = ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))))
9628, 82, 81, 95mp3an 1457 . . . . 5 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))) = ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))))))
9725, 26, 11addassi 11254 . . . . . . 7 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2)) + (๐ทโ†‘2)) = (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2)))
9825, 26addcomi 11435 . . . . . . . . . 10 (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2)) = (((๐‘‡ ยท ๐ถ)โ†‘2) + ((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))))
995, 1sqmuli 14179 . . . . . . . . . . . 12 ((๐‘‡ ยท ๐ถ)โ†‘2) = ((๐‘‡โ†‘2) ยท (๐ถโ†‘2))
1005sqvali 14175 . . . . . . . . . . . . 13 (๐‘‡โ†‘2) = (๐‘‡ ยท ๐‘‡)
101100oveq1i 7426 . . . . . . . . . . . 12 ((๐‘‡โ†‘2) ยท (๐ถโ†‘2)) = ((๐‘‡ ยท ๐‘‡) ยท (๐ถโ†‘2))
1025, 5, 6mulassi 11255 . . . . . . . . . . . 12 ((๐‘‡ ยท ๐‘‡) ยท (๐ถโ†‘2)) = (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))
10399, 101, 1023eqtri 2757 . . . . . . . . . . 11 ((๐‘‡ ยท ๐ถ)โ†‘2) = (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))
10417, 18sqmuli 14179 . . . . . . . . . . . . . . 15 (((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) = (((1 โˆ’ ๐‘‡)โ†‘2) ยท (๐ดโ†‘2))
10517sqvali 14175 . . . . . . . . . . . . . . . 16 ((1 โˆ’ ๐‘‡)โ†‘2) = ((1 โˆ’ ๐‘‡) ยท (1 โˆ’ ๐‘‡))
106105oveq1i 7426 . . . . . . . . . . . . . . 15 (((1 โˆ’ ๐‘‡)โ†‘2) ยท (๐ดโ†‘2)) = (((1 โˆ’ ๐‘‡) ยท (1 โˆ’ ๐‘‡)) ยท (๐ดโ†‘2))
10717, 17, 49mulassi 11255 . . . . . . . . . . . . . . . 16 (((1 โˆ’ ๐‘‡) ยท (1 โˆ’ ๐‘‡)) ยท (๐ดโ†‘2)) = ((1 โˆ’ ๐‘‡) ยท ((1 โˆ’ ๐‘‡) ยท (๐ดโ†‘2)))
10816, 5, 49subdiri 11694 . . . . . . . . . . . . . . . . . 18 ((1 โˆ’ ๐‘‡) ยท (๐ดโ†‘2)) = ((1 ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (๐ดโ†‘2)))
10949mullidi 11249 . . . . . . . . . . . . . . . . . . 19 (1 ยท (๐ดโ†‘2)) = (๐ดโ†‘2)
110109oveq1i 7426 . . . . . . . . . . . . . . . . . 18 ((1 ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) = ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2)))
111108, 110eqtri 2753 . . . . . . . . . . . . . . . . 17 ((1 โˆ’ ๐‘‡) ยท (๐ดโ†‘2)) = ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2)))
112111oveq2i 7427 . . . . . . . . . . . . . . . 16 ((1 โˆ’ ๐‘‡) ยท ((1 โˆ’ ๐‘‡) ยท (๐ดโ†‘2))) = ((1 โˆ’ ๐‘‡) ยท ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))))
113107, 112eqtri 2753 . . . . . . . . . . . . . . 15 (((1 โˆ’ ๐‘‡) ยท (1 โˆ’ ๐‘‡)) ยท (๐ดโ†‘2)) = ((1 โˆ’ ๐‘‡) ยท ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))))
114104, 106, 1133eqtri 2757 . . . . . . . . . . . . . 14 (((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) = ((1 โˆ’ ๐‘‡) ยท ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))))
1157, 19, 22mul12i 11439 . . . . . . . . . . . . . . 15 (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))) = (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))
1167, 22mulcli 11251 . . . . . . . . . . . . . . . 16 (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)) โˆˆ โ„‚
11717, 18, 116mulassi 11255 . . . . . . . . . . . . . . 15 (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))) = ((1 โˆ’ ๐‘‡) ยท (๐ด ยท (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))))
11818, 7mulcomi 11252 . . . . . . . . . . . . . . . . . . 19 (๐ด ยท 2) = (2 ยท ๐ด)
119118oveq1i 7426 . . . . . . . . . . . . . . . . . 18 ((๐ด ยท 2) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)) = ((2 ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))
12018, 7, 22mulassi 11255 . . . . . . . . . . . . . . . . . 18 ((๐ด ยท 2) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)) = (๐ด ยท (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))
121119, 120eqtr3i 2755 . . . . . . . . . . . . . . . . 17 ((2 ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)) = (๐ด ยท (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))
1227, 18mulcli 11251 . . . . . . . . . . . . . . . . . . 19 (2 ยท ๐ด) โˆˆ โ„‚
123122, 21, 2subdii 11693 . . . . . . . . . . . . . . . . . 18 ((2 ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)) = (((2 ยท ๐ด) ยท (๐‘‡ ยท ๐ถ)) โˆ’ ((2 ยท ๐ด) ยท ๐ท))
124122, 5, 1mul12i 11439 . . . . . . . . . . . . . . . . . . . 20 ((2 ยท ๐ด) ยท (๐‘‡ ยท ๐ถ)) = (๐‘‡ ยท ((2 ยท ๐ด) ยท ๐ถ))
1257, 18, 1mulassi 11255 . . . . . . . . . . . . . . . . . . . . 21 ((2 ยท ๐ด) ยท ๐ถ) = (2 ยท (๐ด ยท ๐ถ))
126125oveq2i 7427 . . . . . . . . . . . . . . . . . . . 20 (๐‘‡ ยท ((2 ยท ๐ด) ยท ๐ถ)) = (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))
127124, 126eqtri 2753 . . . . . . . . . . . . . . . . . . 19 ((2 ยท ๐ด) ยท (๐‘‡ ยท ๐ถ)) = (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))
1287, 18, 2mulassi 11255 . . . . . . . . . . . . . . . . . . 19 ((2 ยท ๐ด) ยท ๐ท) = (2 ยท (๐ด ยท ๐ท))
129127, 128oveq12i 7428 . . . . . . . . . . . . . . . . . 18 (((2 ยท ๐ด) ยท (๐‘‡ ยท ๐ถ)) โˆ’ ((2 ยท ๐ด) ยท ๐ท)) = ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท)))
130123, 129eqtri 2753 . . . . . . . . . . . . . . . . 17 ((2 ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)) = ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท)))
131121, 130eqtr3i 2755 . . . . . . . . . . . . . . . 16 (๐ด ยท (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))) = ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท)))
132131oveq2i 7427 . . . . . . . . . . . . . . 15 ((1 โˆ’ ๐‘‡) ยท (๐ด ยท (2 ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) = ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท))))
133115, 117, 1323eqtri 2757 . . . . . . . . . . . . . 14 (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))) = ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท))))
134114, 133oveq12i 7428 . . . . . . . . . . . . 13 ((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) = (((1 โˆ’ ๐‘‡) ยท ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2)))) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท)))))
1355, 49mulcli 11251 . . . . . . . . . . . . . . 15 (๐‘‡ ยท (๐ดโ†‘2)) โˆˆ โ„‚
13649, 135subcli 11566 . . . . . . . . . . . . . 14 ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) โˆˆ โ„‚
1375, 51mulcli 11251 . . . . . . . . . . . . . . 15 (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆˆ โ„‚
138137, 59subcli 11566 . . . . . . . . . . . . . 14 ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆˆ โ„‚
13917, 136, 138adddii 11256 . . . . . . . . . . . . 13 ((1 โˆ’ ๐‘‡) ยท (((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท))))) = (((1 โˆ’ ๐‘‡) ยท ((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2)))) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท)))))
1405, 49, 51subdii 11693 . . . . . . . . . . . . . . . . 17 (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) = ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))
141140oveq2i 7427 . . . . . . . . . . . . . . . 16 (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))))) = (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))))
142140, 57eqeltrri 2822 . . . . . . . . . . . . . . . . 17 ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))) โˆˆ โ„‚
143 sub32 11524 . . . . . . . . . . . . . . . . 17 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))) โˆˆ โ„‚ โˆง (2 ยท (๐ด ยท ๐ท)) โˆˆ โ„‚) โ†’ (((๐ดโ†‘2) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))) โˆ’ (2 ยท (๐ด ยท ๐ท))) = (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))))
14449, 142, 59, 143mp3an 1457 . . . . . . . . . . . . . . . 16 (((๐ดโ†‘2) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))) โˆ’ (2 ยท (๐ด ยท ๐ท))) = (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))))
145141, 144eqtr4i 2756 . . . . . . . . . . . . . . 15 (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))))) = (((๐ดโ†‘2) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))) โˆ’ (2 ยท (๐ด ยท ๐ท)))
146 subsub 11520 . . . . . . . . . . . . . . . . 17 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง (๐‘‡ ยท (๐ดโ†‘2)) โˆˆ โ„‚ โˆง (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆˆ โ„‚) โ†’ ((๐ดโ†‘2) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))) = (((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))))
14749, 135, 137, 146mp3an 1457 . . . . . . . . . . . . . . . 16 ((๐ดโ†‘2) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))) = (((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))
148147oveq1i 7426 . . . . . . . . . . . . . . 15 (((๐ดโ†‘2) โˆ’ ((๐‘‡ ยท (๐ดโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))))) โˆ’ (2 ยท (๐ด ยท ๐ท))) = ((((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))) โˆ’ (2 ยท (๐ด ยท ๐ท)))
149136, 137, 59addsubassi 11581 . . . . . . . . . . . . . . 15 ((((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + (๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ)))) โˆ’ (2 ยท (๐ด ยท ๐ท))) = (((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท))))
150145, 148, 1493eqtrri 2758 . . . . . . . . . . . . . 14 (((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท)))) = (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))))
151150oveq2i 7427 . . . . . . . . . . . . 13 ((1 โˆ’ ๐‘‡) ยท (((๐ดโ†‘2) โˆ’ (๐‘‡ ยท (๐ดโ†‘2))) + ((๐‘‡ ยท (2 ยท (๐ด ยท ๐ถ))) โˆ’ (2 ยท (๐ด ยท ๐ท))))) = ((1 โˆ’ ๐‘‡) ยท (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))))))
152134, 139, 1513eqtr2i 2759 . . . . . . . . . . . 12 ((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) = ((1 โˆ’ ๐‘‡) ยท (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))))))
15357, 60negsubdi2i 11576 . . . . . . . . . . . . 13 -((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))) = (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))))
154153oveq2i 7427 . . . . . . . . . . . 12 ((1 โˆ’ ๐‘‡) ยท -((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) = ((1 โˆ’ ๐‘‡) ยท (((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))) โˆ’ (๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ))))))
15517, 64mulneg2i 11691 . . . . . . . . . . . 12 ((1 โˆ’ ๐‘‡) ยท -((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) = -((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))
156152, 154, 1553eqtr2i 2759 . . . . . . . . . . 11 ((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) = -((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))
157103, 156oveq12i 7428 . . . . . . . . . 10 (((๐‘‡ ยท ๐ถ)โ†‘2) + ((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท))))) = ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) + -((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))
15871, 81negsubi 11568 . . . . . . . . . 10 ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) + -((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))) = ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))
15998, 157, 1583eqtri 2757 . . . . . . . . 9 (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2)) = ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))
160159oveq2i 7427 . . . . . . . 8 ((๐ทโ†‘2) + (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2))) = ((๐ทโ†‘2) + ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))))
16125, 26addcli 11250 . . . . . . . . 9 (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2)) โˆˆ โ„‚
162161, 11addcomi 11435 . . . . . . . 8 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2)) + (๐ทโ†‘2)) = ((๐ทโ†‘2) + (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2)))
16311, 71, 81addsubassi 11581 . . . . . . . 8 (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))) = ((๐ทโ†‘2) + ((๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))))
164160, 162, 1633eqtr4i 2763 . . . . . . 7 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + ((๐‘‡ ยท ๐ถ)โ†‘2)) + (๐ทโ†‘2)) = (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))
16597, 164eqtr3i 2755 . . . . . 6 (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) = (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))
16682, 81subcli 11566 . . . . . . 7 (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))) โˆˆ โ„‚
16728, 166subeq0i 11570 . . . . . 6 (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))) = 0 โ†” (((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) = (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท)))))))
168165, 167mpbir 230 . . . . 5 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) โˆ’ (((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))) โˆ’ ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))))) = 0
16996, 168eqtr3i 2755 . . . 4 ((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) = 0
1705, 1, 2mulassi 11255 . . . . . . . 8 ((๐‘‡ ยท ๐ถ) ยท ๐ท) = (๐‘‡ ยท (๐ถ ยท ๐ท))
171170oveq2i 7427 . . . . . . 7 (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)) = (2 ยท (๐‘‡ ยท (๐ถ ยท ๐ท)))
1727, 5, 8mul12i 11439 . . . . . . 7 (2 ยท (๐‘‡ ยท (๐ถ ยท ๐ท))) = (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))
173171, 172eqtri 2753 . . . . . 6 (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)) = (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))
174173oveq2i 7427 . . . . 5 (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) = (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท))))
1755, 9mulcli 11251 . . . . . 6 (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท))) โˆˆ โ„‚
17631, 32, 175addsubi 11582 . . . . 5 (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))
177174, 176eqtri 2753 . . . 4 (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท))) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))
178169, 177oveq12i 7428 . . 3 (((((((1 โˆ’ ๐‘‡) ยท ๐ด)โ†‘2) + (2 ยท (((1 โˆ’ ๐‘‡) ยท ๐ด) ยท ((๐‘‡ ยท ๐ถ) โˆ’ ๐ท)))) + (((๐‘‡ ยท ๐ถ)โ†‘2) + (๐ทโ†‘2))) + (((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ถ)))) โˆ’ ((๐ดโ†‘2) โˆ’ (2 ยท (๐ด ยท ๐ท))))) โˆ’ ((๐ทโ†‘2) + (๐‘‡ ยท (๐‘‡ ยท (๐ถโ†‘2)))))) + (((๐‘‡ ยท (๐ถโ†‘2)) + (๐‘‡ ยท (๐ทโ†‘2))) โˆ’ (2 ยท ((๐‘‡ ยท ๐ถ) ยท ๐ท)))) = (0 + (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2))))
17931, 175subcli 11566 . . . . 5 ((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) โˆˆ โ„‚
180179, 32addcli 11250 . . . 4 (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2))) โˆˆ โ„‚
181180addlidi 11432 . . 3 (0 + (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))
18294, 178, 1813eqtri 2757 . 2 ((((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2)))) = (((๐‘‡ ยท (๐ถโ†‘2)) โˆ’ (๐‘‡ ยท (2 ยท (๐ถ ยท ๐ท)))) + (๐‘‡ ยท (๐ทโ†‘2)))
18315, 182eqtr4i 2756 1 (๐‘‡ ยท ((๐ถ โˆ’ ๐ท)โ†‘2)) = ((((((1 โˆ’ ๐‘‡) ยท ๐ด) + (๐‘‡ ยท ๐ถ)) โˆ’ ๐ท)โ†‘2) + ((1 โˆ’ ๐‘‡) ยท ((๐‘‡ ยท ((๐ด โˆ’ ๐ถ)โ†‘2)) โˆ’ ((๐ด โˆ’ ๐ท)โ†‘2))))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533   โˆˆ wcel 2098  (class class class)co 7416  โ„‚cc 11136  0cc0 11138  1c1 11139   + caddc 11141   ยท cmul 11143   โˆ’ cmin 11474  -cneg 11475  2c2 12297  โ†‘cexp 14058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-2nd 7992  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-n0 12503  df-z 12589  df-uz 12853  df-seq 13999  df-exp 14059
This theorem is referenced by:  ax5seglem8  28791
  Copyright terms: Public domain W3C validator