![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mulcomnqg | GIF version |
Description: Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.) |
Ref | Expression |
---|---|
mulcomnqg | ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nqqs 7004 | . 2 ⊢ Q = ((N × N) / ~Q ) | |
2 | mulpipqqs 7029 | . 2 ⊢ (((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧ (𝑧 ∈ N ∧ 𝑤 ∈ N)) → ([〈𝑥, 𝑦〉] ~Q ·Q [〈𝑧, 𝑤〉] ~Q ) = [〈(𝑥 ·N 𝑧), (𝑦 ·N 𝑤)〉] ~Q ) | |
3 | mulpipqqs 7029 | . 2 ⊢ (((𝑧 ∈ N ∧ 𝑤 ∈ N) ∧ (𝑥 ∈ N ∧ 𝑦 ∈ N)) → ([〈𝑧, 𝑤〉] ~Q ·Q [〈𝑥, 𝑦〉] ~Q ) = [〈(𝑧 ·N 𝑥), (𝑤 ·N 𝑦)〉] ~Q ) | |
4 | mulcompig 6987 | . . 3 ⊢ ((𝑥 ∈ N ∧ 𝑧 ∈ N) → (𝑥 ·N 𝑧) = (𝑧 ·N 𝑥)) | |
5 | 4 | ad2ant2r 494 | . 2 ⊢ (((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧ (𝑧 ∈ N ∧ 𝑤 ∈ N)) → (𝑥 ·N 𝑧) = (𝑧 ·N 𝑥)) |
6 | mulcompig 6987 | . . 3 ⊢ ((𝑦 ∈ N ∧ 𝑤 ∈ N) → (𝑦 ·N 𝑤) = (𝑤 ·N 𝑦)) | |
7 | 6 | ad2ant2l 493 | . 2 ⊢ (((𝑥 ∈ N ∧ 𝑦 ∈ N) ∧ (𝑧 ∈ N ∧ 𝑤 ∈ N)) → (𝑦 ·N 𝑤) = (𝑤 ·N 𝑦)) |
8 | 1, 2, 3, 5, 7 | ecovicom 6440 | 1 ⊢ ((𝐴 ∈ Q ∧ 𝐵 ∈ Q) → (𝐴 ·Q 𝐵) = (𝐵 ·Q 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1296 ∈ wcel 1445 (class class class)co 5690 Ncnpi 6928 ·N cmi 6930 ~Q ceq 6935 Qcnq 6936 ·Q cmq 6939 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-coll 3975 ax-sep 3978 ax-nul 3986 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-iinf 4431 |
This theorem depends on definitions: df-bi 116 df-dc 784 df-3or 928 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-ral 2375 df-rex 2376 df-reu 2377 df-rab 2379 df-v 2635 df-sbc 2855 df-csb 2948 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-nul 3303 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-iun 3754 df-br 3868 df-opab 3922 df-mpt 3923 df-tr 3959 df-id 4144 df-iord 4217 df-on 4219 df-suc 4222 df-iom 4434 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-rn 4478 df-res 4479 df-ima 4480 df-iota 5014 df-fun 5051 df-fn 5052 df-f 5053 df-f1 5054 df-fo 5055 df-f1o 5056 df-fv 5057 df-ov 5693 df-oprab 5694 df-mpt2 5695 df-1st 5949 df-2nd 5950 df-recs 6108 df-irdg 6173 df-oadd 6223 df-omul 6224 df-er 6332 df-ec 6334 df-qs 6338 df-ni 6960 df-mi 6962 df-mpq 7001 df-enq 7003 df-nqqs 7004 df-mqqs 7006 |
This theorem is referenced by: recmulnqg 7047 recrecnq 7050 rec1nq 7051 lt2mulnq 7061 halfnqq 7066 prarloclemarch 7074 prarloclemarch2 7075 ltrnqg 7076 prarloclemlt 7149 addnqprllem 7183 addnqprulem 7184 addnqprl 7185 addnqpru 7186 appdivnq 7219 prmuloclemcalc 7221 mulnqprl 7224 mulnqpru 7225 mullocprlem 7226 mulclpr 7228 mulcomprg 7236 distrlem4prl 7240 distrlem4pru 7241 1idprl 7246 1idpru 7247 recexprlem1ssl 7289 recexprlem1ssu 7290 recexprlemss1l 7291 recexprlemss1u 7292 |
Copyright terms: Public domain | W3C validator |