sqgcd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > sqgcd		Unicode version

Theorem sqgcd 11984

Description: Square distributes over gcd. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Assertion**
Ref	Expression
sqgcd	$/\$

**Proof of Theorem sqgcd**
Step	Hyp	Ref	Expression
1		gcdnncl 11922	. . . . 5 $/\$
2	1	nnsqcld 10630	. . . 4 $/\$
3	2	nncnd 8892	. . 3 $/\$
4	3	mulid1d 7937	. 2 $/\$
5		nnsqcl 10545	. . . . . . 7
6	5	nnzd 9333	. . . . . 6
7	6	adantr 274	. . . . 5 $/\$
8		nnsqcl 10545	. . . . . . 7
9	8	nnzd 9333	. . . . . 6
10	9	adantl 275	. . . . 5 $/\$
11		nnz 9231	. . . . . . . 8
12		nnz 9231	. . . . . . . 8
13		gcddvds 11918	. . . . . . . 8 $/\$ $/\$
14	11, 12, 13	syl2an 287	. . . . . . 7 $/\$ $/\$
15	14	simpld 111	. . . . . 6 $/\$
16	1	nnzd 9333	. . . . . . 7 $/\$
17	11	adantr 274	. . . . . . 7 $/\$
18		dvdssqim 11979	. . . . . . 7 $/\$
19	16, 17, 18	syl2anc 409	. . . . . 6 $/\$
20	15, 19	mpd 13	. . . . 5 $/\$
21	14	simprd 113	. . . . . 6 $/\$
22	12	adantl 275	. . . . . . 7 $/\$
23		dvdssqim 11979	. . . . . . 7 $/\$
24	16, 22, 23	syl2anc 409	. . . . . 6 $/\$
25	21, 24	mpd 13	. . . . 5 $/\$
26		gcddiv 11974	. . . . 5 $/\$ $/\$ $/\$ $/\$
27	7, 10, 2, 20, 25, 26	syl32anc 1241	. . . 4 $/\$
28		nncn 8886	. . . . . . 7
29	28	adantr 274	. . . . . 6 $/\$
30	1	nncnd 8892	. . . . . 6 $/\$
31	1	nnap0d 8924	. . . . . 6 $/\$ #
32	29, 30, 31	sqdivapd 10622	. . . . 5 $/\$
33		nncn 8886	. . . . . . 7
34	33	adantl 275	. . . . . 6 $/\$
35	34, 30, 31	sqdivapd 10622	. . . . 5 $/\$
36	32, 35	oveq12d 5871	. . . 4 $/\$
37		gcddiv 11974	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
38	17, 22, 1, 14, 37	syl31anc 1236	. . . . . 6 $/\$
39	30, 31	dividapd 8703	. . . . . 6 $/\$
40	38, 39	eqtr3d 2205	. . . . 5 $/\$
41	1	nnne0d 8923	. . . . . . . . 9 $/\$
42		dvdsval2 11752	. . . . . . . . 9 $/\$ $/\$
43	16, 41, 17, 42	syl3anc 1233	. . . . . . . 8 $/\$
44	15, 43	mpbid 146	. . . . . . 7 $/\$
45		nnre 8885	. . . . . . . . 9
46	45	adantr 274	. . . . . . . 8 $/\$
47	1	nnred 8891	. . . . . . . 8 $/\$
48		nngt0 8903	. . . . . . . . 9
49	48	adantr 274	. . . . . . . 8 $/\$
50	1	nngt0d 8922	. . . . . . . 8 $/\$
51	46, 47, 49, 50	divgt0d 8851	. . . . . . 7 $/\$
52		elnnz 9222	. . . . . . 7 $/\$
53	44, 51, 52	sylanbrc 415	. . . . . 6 $/\$
54		dvdsval2 11752	. . . . . . . . 9 $/\$ $/\$
55	16, 41, 22, 54	syl3anc 1233	. . . . . . . 8 $/\$
56	21, 55	mpbid 146	. . . . . . 7 $/\$
57		nnre 8885	. . . . . . . . 9
58	57	adantl 275	. . . . . . . 8 $/\$
59		nngt0 8903	. . . . . . . . 9
60	59	adantl 275	. . . . . . . 8 $/\$
61	58, 47, 60, 50	divgt0d 8851	. . . . . . 7 $/\$
62		elnnz 9222	. . . . . . 7 $/\$
63	56, 61, 62	sylanbrc 415	. . . . . 6 $/\$
64		2nn 9039	. . . . . . 7
65		rppwr 11983	. . . . . . 7 $/\$ $/\$
66	64, 65	mp3an3 1321	. . . . . 6 $/\$
67	53, 63, 66	syl2anc 409	. . . . 5 $/\$
68	40, 67	mpd 13	. . . 4 $/\$
69	27, 36, 68	3eqtr2d 2209	. . 3 $/\$
70	6, 9	anim12i 336	. . . . . 6 $/\$ $/\$
71	5	nnne0d 8923	. . . . . . . . 9
72	71	neneqd 2361	. . . . . . . 8
73	72	intnanrd 927	. . . . . . 7 $/\$
74	73	adantr 274	. . . . . 6 $/\$ $/\$
75		gcdn0cl 11917	. . . . . 6 $/\$ $/\$ $/\$
76	70, 74, 75	syl2anc 409	. . . . 5 $/\$
77	76	nncnd 8892	. . . 4 $/\$
78	2	nnap0d 8924	. . . 4 $/\$ #
79		ax-1cn 7867	. . . . 5
80		divmulap 8592	. . . . 5 $/\$ $/\$ $/\$ #
81	79, 80	mp3an2 1320	. . . 4 $/\$ $/\$ #
82	77, 3, 78, 81	syl12anc 1231	. . 3 $/\$
83	69, 82	mpbid 146	. 2 $/\$
84	4, 83	eqtr3d 2205	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104

wceq 1348

wcel 2141

wne 2340 class class class wbr 3989 (class class class)co 5853

cc 7772

cr 7773

cc0 7774

c1 7775

cmul 7779

clt 7954 # cap 8500

cdiv 8589

cn 8878

c2 8929

cz 9212

cexp 10475

cdvds 11749

cgcd 11897

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-stab 826 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-sup 6961 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-fz 9966 df-fzo 10099 df-fl 10226 df-mod 10279 df-seqfrec 10402 df-exp 10476 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-dvds 11750 df-gcd 11898

This theorem is referenced by: dvdssqlem 11985 nn0gcdsq 12154 pythagtriplem3 12221

W3C validator