Proof of Theorem pythagtriplem16
Step | Hyp | Ref
| Expression |
1 | | pythagtriplem15.1 |
. . . . 5
|
2 | | pythagtriplem15.2 |
. . . . 5
|
3 | 1, 2 | oveq12i 6662 |
. . . 4
|
4 | | nncn 11028 |
. . . . . . . . . . . 12
|
5 | | nncn 11028 |
. . . . . . . . . . . 12
|
6 | | addcl 10018 |
. . . . . . . . . . . 12
|
7 | 4, 5, 6 | syl2anr 495 |
. . . . . . . . . . 11
|
8 | 7 | sqrtcld 14176 |
. . . . . . . . . 10
|
9 | | subcl 10280 |
. . . . . . . . . . . 12
|
10 | 4, 5, 9 | syl2anr 495 |
. . . . . . . . . . 11
|
11 | 10 | sqrtcld 14176 |
. . . . . . . . . 10
|
12 | | addcl 10018 |
. . . . . . . . . 10
|
13 | 8, 11, 12 | syl2anc 693 |
. . . . . . . . 9
|
14 | 13 | 3adant1 1079 |
. . . . . . . 8
|
15 | 14 | 3ad2ant1 1082 |
. . . . . . 7
|
16 | | subcl 10280 |
. . . . . . . . . 10
|
17 | 8, 11, 16 | syl2anc 693 |
. . . . . . . . 9
|
18 | 17 | 3adant1 1079 |
. . . . . . . 8
|
19 | 18 | 3ad2ant1 1082 |
. . . . . . 7
|
20 | | 2cnne0 11242 |
. . . . . . . 8
|
21 | | divmuldiv 10725 |
. . . . . . . 8
|
22 | 20, 20, 21 | mpanr12 721 |
. . . . . . 7
|
23 | 15, 19, 22 | syl2anc 693 |
. . . . . 6
|
24 | 13, 17 | mulcld 10060 |
. . . . . . . . 9
|
25 | 24 | 3adant1 1079 |
. . . . . . . 8
|
26 | 25 | 3ad2ant1 1082 |
. . . . . . 7
|
27 | | divdiv1 10736 |
. . . . . . . 8
|
28 | 20, 20, 27 | mp3an23 1416 |
. . . . . . 7
|
29 | 26, 28 | syl 17 |
. . . . . 6
|
30 | 23, 29 | eqtr4d 2659 |
. . . . 5
|
31 | | nnre 11027 |
. . . . . . . . . . . . 13
|
32 | | nnre 11027 |
. . . . . . . . . . . . 13
|
33 | | readdcl 10019 |
. . . . . . . . . . . . 13
|
34 | 31, 32, 33 | syl2anr 495 |
. . . . . . . . . . . 12
|
35 | 34 | 3adant1 1079 |
. . . . . . . . . . 11
|
36 | 35 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
37 | 31 | adantl 482 |
. . . . . . . . . . . . . 14
|
38 | 32 | adantr 481 |
. . . . . . . . . . . . . 14
|
39 | | nngt0 11049 |
. . . . . . . . . . . . . . 15
|
40 | 39 | adantl 482 |
. . . . . . . . . . . . . 14
|
41 | | nngt0 11049 |
. . . . . . . . . . . . . . 15
|
42 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
|
43 | 37, 38, 40, 42 | addgt0d 10602 |
. . . . . . . . . . . . 13
|
44 | | 0re 10040 |
. . . . . . . . . . . . . 14
|
45 | | ltle 10126 |
. . . . . . . . . . . . . 14
|
46 | 44, 45 | mpan 706 |
. . . . . . . . . . . . 13
|
47 | 34, 43, 46 | sylc 65 |
. . . . . . . . . . . 12
|
48 | 47 | 3adant1 1079 |
. . . . . . . . . . 11
|
49 | 48 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
50 | | resqrtth 13996 |
. . . . . . . . . 10
|
51 | 36, 49, 50 | syl2anc 693 |
. . . . . . . . 9
|
52 | | resubcl 10345 |
. . . . . . . . . . . . 13
|
53 | 31, 32, 52 | syl2anr 495 |
. . . . . . . . . . . 12
|
54 | 53 | 3adant1 1079 |
. . . . . . . . . . 11
|
55 | 54 | 3ad2ant1 1082 |
. . . . . . . . . 10
|
56 | | pythagtriplem10 15525 |
. . . . . . . . . . . 12
|
57 | 56 | 3adant3 1081 |
. . . . . . . . . . 11
|
58 | | ltle 10126 |
. . . . . . . . . . . 12
|
59 | 44, 58 | mpan 706 |
. . . . . . . . . . 11
|
60 | 55, 57, 59 | sylc 65 |
. . . . . . . . . 10
|
61 | | resqrtth 13996 |
. . . . . . . . . 10
|
62 | 55, 60, 61 | syl2anc 693 |
. . . . . . . . 9
|
63 | 51, 62 | oveq12d 6668 |
. . . . . . . 8
|
64 | 63 | oveq1d 6665 |
. . . . . . 7
|
65 | | simp12 1092 |
. . . . . . . . . 10
|
66 | | simp13 1093 |
. . . . . . . . . 10
|
67 | 65, 66, 8 | syl2anc 693 |
. . . . . . . . 9
|
68 | 65, 66, 11 | syl2anc 693 |
. . . . . . . . 9
|
69 | | subsq 12972 |
. . . . . . . . 9
|
70 | 67, 68, 69 | syl2anc 693 |
. . . . . . . 8
|
71 | 70 | oveq1d 6665 |
. . . . . . 7
|
72 | | pnncan 10322 |
. . . . . . . . . . . . . 14
|
73 | 72 | 3anidm23 1385 |
. . . . . . . . . . . . 13
|
74 | | 2times 11145 |
. . . . . . . . . . . . . 14
|
75 | 74 | adantl 482 |
. . . . . . . . . . . . 13
|
76 | 73, 75 | eqtr4d 2659 |
. . . . . . . . . . . 12
|
77 | 4, 5, 76 | syl2anr 495 |
. . . . . . . . . . 11
|
78 | 77 | 3adant1 1079 |
. . . . . . . . . 10
|
79 | 78 | 3ad2ant1 1082 |
. . . . . . . . 9
|
80 | 79 | oveq1d 6665 |
. . . . . . . 8
|
81 | | 2cn 11091 |
. . . . . . . . . 10
|
82 | | 2ne0 11113 |
. . . . . . . . . 10
|
83 | | divcan3 10711 |
. . . . . . . . . 10
|
84 | 81, 82, 83 | mp3an23 1416 |
. . . . . . . . 9
|
85 | 65, 5, 84 | 3syl 18 |
. . . . . . . 8
|
86 | 80, 85 | eqtrd 2656 |
. . . . . . 7
|
87 | 64, 71, 86 | 3eqtr3d 2664 |
. . . . . 6
|
88 | 87 | oveq1d 6665 |
. . . . 5
|
89 | 30, 88 | eqtrd 2656 |
. . . 4
|
90 | 3, 89 | syl5eq 2668 |
. . 3
|
91 | 90 | oveq2d 6666 |
. 2
|
92 | | divcan2 10693 |
. . . . . 6
|
93 | 81, 82, 92 | mp3an23 1416 |
. . . . 5
|
94 | 5, 93 | syl 17 |
. . . 4
|
95 | 94 | 3ad2ant2 1083 |
. . 3
|
96 | 95 | 3ad2ant1 1082 |
. 2
|
97 | 91, 96 | eqtr2d 2657 |
1
|